chore(ring_theory/*): dot notation for submodule.fg and `subalgebra…

….fg` (#13737)

src/linear_algebra/finite_dimensional.lean

@@ -731,7 +731,7 @@ instance finite_dimensional_sup (S₁ S₂ : submodule K V) [h₁ : finite_dimen
 begin
   unfold finite_dimensional at *,
   rw [finite_def] at *,
-  exact (fg_top _).2 (submodule.fg_sup ((fg_top S₁).1 h₁) ((fg_top S₂).1 h₂)),
+  exact (fg_top _).2 (((fg_top S₁).1 h₁).sup ((fg_top S₂).1 h₂)),
 end
 
 /-- The submodule generated by a finite supremum of finite dimensional submodules is

src/ring_theory/adjoin/fg.lean

@@ -108,7 +108,7 @@ lemma fg_of_submodule_fg (h : (⊤ : submodule R A).fg) : (⊤ : subalgebra R A)
 let ⟨s, hs⟩ := h in ⟨s, to_submodule_injective $
 by { rw [algebra.top_to_submodule, eq_top_iff, ← hs, span_le], exact algebra.subset_adjoin }⟩
 
-lemma fg_prod {S : subalgebra R A} {T : subalgebra R B} (hS : S.fg) (hT : T.fg) : (S.prod T).fg :=
+lemma fg.prod {S : subalgebra R A} {T : subalgebra R B} (hS : S.fg) (hT : T.fg) : (S.prod T).fg :=
 begin
   obtain ⟨s, hs⟩ := fg_def.1 hS,
   obtain ⟨t, ht⟩ := fg_def.1 hT,
@@ -121,7 +121,7 @@ end
 
 section
 open_locale classical
-lemma fg_map (S : subalgebra R A) (f : A →ₐ[R] B) (hs : S.fg) : (S.map f).fg :=
+lemma fg.map {S : subalgebra R A} (f : A →ₐ[R] B) (hs : S.fg) : (S.map f).fg :=
 let ⟨s, hs⟩ := hs in ⟨s.image f, by rw [finset.coe_image, algebra.adjoin_image, hs]⟩
 end
 
@@ -132,7 +132,7 @@ by { rw [← algebra.adjoin_image, finset.coe_preimage, set.image_preimage_eq_of
   rw [← alg_hom.coe_range, ← algebra.adjoin_le_iff, hs, ← algebra.map_top], exact map_mono le_top }⟩
 
 lemma fg_top (S : subalgebra R A) : (⊤ : subalgebra R S).fg ↔ S.fg :=
-⟨λ h, by { rw [← S.range_val, ← algebra.map_top], exact fg_map _ _ h },
+⟨λ h, by { rw [← S.range_val, ← algebra.map_top], exact fg.map _ h },
 λ h, fg_of_fg_map _ S.val subtype.val_injective $ by { rw [algebra.map_top, range_val], exact h }⟩
 
 lemma induction_on_adjoin [is_noetherian R A] (P : subalgebra R A → Prop)

src/ring_theory/finiteness.lean

@@ -109,7 +109,7 @@ variables {R M}
 instance prod [hM : finite R M] [hN : finite R N] : finite R (M × N) :=
 ⟨begin
   rw ← submodule.prod_top,
-  exact submodule.fg_prod hM.1 hN.1
+  exact hM.1.prod hN.1
 end⟩
 
 instance pi {ι : Type*} {M : ι → Type*} [fintype ι] [Π i, add_comm_monoid (M i)]
@@ -186,7 +186,7 @@ variables {R A B}
 lemma of_surjective (hRA : finite_type R A) (f : A →ₐ[R] B) (hf : surjective f) :
   finite_type R B :=
 ⟨begin
-  convert subalgebra.fg_map _ f hRA.1,
+  convert hRA.1.map f,
   simpa only [map_top f, @eq_comm _ ⊤, eq_top_iff, alg_hom.mem_range] using hf
 end⟩
 
@@ -255,7 +255,7 @@ end
 instance prod [hA : finite_type R A] [hB : finite_type R B] : finite_type R (A × B) :=
 ⟨begin
   rw ← subalgebra.prod_top,
-  exact subalgebra.fg_prod hA.1 hB.1
+  exact hA.1.prod hB.1
 end⟩
 
 end finite_type

src/ring_theory/integral_closure.lean

@@ -194,7 +194,7 @@ set.finite.induction_on hfs (λ _, ⟨{1}, submodule.ext $ λ x,
   by { erw [algebra.adjoin_empty, finset.coe_singleton, ← one_eq_span, one_eq_range,
             linear_map.mem_range, algebra.mem_bot], refl }⟩)
 (λ a s has hs ih his, by rw [← set.union_singleton, algebra.adjoin_union_coe_submodule]; exact
-  fg_mul _ _ (ih $ λ i hi, his i $ set.mem_insert_of_mem a hi)
+  fg.mul (ih $ λ i hi, his i $ set.mem_insert_of_mem a hi)
     (fg_adjoin_singleton_of_integral _ $ his a $ set.mem_insert a s)) his
 
 lemma is_noetherian_adjoin_finset [is_noetherian_ring R] (s : finset A)
@@ -291,7 +291,7 @@ lemma ring_hom.is_integral_of_mem_closure {x y z : S}
   f.is_integral_elem z :=
 begin
   letI : algebra R S := f.to_algebra,
-  have := fg_mul _ _ (fg_adjoin_singleton_of_integral x hx) (fg_adjoin_singleton_of_integral y hy),
+  have := (fg_adjoin_singleton_of_integral x hx).mul (fg_adjoin_singleton_of_integral y hy),
   rw [← algebra.adjoin_union_coe_submodule, set.singleton_union] at this,
   exact is_integral_of_mem_of_fg (algebra.adjoin R {x, y}) this z
     (algebra.mem_adjoin_iff.2 $ subring.closure_mono (set.subset_union_right _ _) hz),

src/ring_theory/noetherian.lean

@@ -149,7 +149,7 @@ theorem fg_span {s : set M} (hs : finite s) : fg (span R s) :=
 theorem fg_span_singleton (x : M) : fg (R ∙ x) :=
 fg_span (finite_singleton x)
 
-theorem fg_sup {N₁ N₂ : submodule R M}
+theorem fg.sup {N₁ N₂ : submodule R M}
   (hN₁ : N₁.fg) (hN₂ : N₂.fg) : (N₁ ⊔ N₂).fg :=
 let ⟨t₁, ht₁⟩ := fg_def.1 hN₁, ⟨t₂, ht₂⟩ := fg_def.1 hN₂ in
 fg_def.2 ⟨t₁ ∪ t₂, ht₁.1.union ht₂.1, by rw [span_union, ht₁.2, ht₂.2]⟩
@@ -182,7 +182,7 @@ lemma fg_of_linear_equiv (e : M ≃ₗ[R] P) (h : (⊤ : submodule R P).fg) :
   (⊤ : submodule R M).fg :=
 e.symm.range ▸ map_top (e.symm : P →ₗ[R] M) ▸ h.map _
 
-theorem fg_prod {sb : submodule R M} {sc : submodule R P}
+theorem fg.prod {sb : submodule R M} {sc : submodule R P}
   (hsb : sb.fg) (hsc : sc.fg) : (sb.prod sc).fg :=
 let ⟨tb, htb⟩ := fg_def.1 hsb, ⟨tc, htc⟩ := fg_def.1 hsc in
 fg_def.2 ⟨linear_map.inl R M P '' tb ∪ linear_map.inr R M P '' tc,
@@ -775,15 +775,15 @@ is_noetherian_ring_of_surjective R S f.to_ring_hom f.to_equiv.surjective
 
 namespace submodule
 variables {R : Type*} {A : Type*} [comm_semiring R] [semiring A] [algebra R A]
-variables (M N : submodule R A)
+variables {M N : submodule R A}
 
-theorem fg_mul (hm : M.fg) (hn : N.fg) : (M * N).fg :=
+theorem fg.mul (hm : M.fg) (hn : N.fg) : (M * N).fg :=
 let ⟨m, hfm, hm⟩ := fg_def.1 hm, ⟨n, hfn, hn⟩ := fg_def.1 hn in
 fg_def.2 ⟨m * n, hfm.mul hfn, span_mul_span R m n ▸ hm ▸ hn ▸ rfl⟩
 
-lemma fg_pow (h : M.fg) (n : ℕ) : (M ^ n).fg :=
+lemma fg.pow (h : M.fg) (n : ℕ) : (M ^ n).fg :=
 nat.rec_on n
-(⟨{1}, by simp [one_eq_span]⟩)
-(λ n ih, by simpa [pow_succ] using fg_mul _ _ h ih)
+  (⟨{1}, by simp [one_eq_span]⟩)
+  (λ n ih, by simpa [pow_succ] using h.mul ih)
 
 end submodule