refactor: rename Fg to FG (#3948)

Please refer to this Zulip thread:
https://leanprover.zulipchat.com/#narrow/stream/287929-mathlib4/topic/Naming.20convention/near/357712556

Mathlib.lean

@@ -1762,7 +1762,7 @@ import Mathlib.Probability.ProbabilityMassFunction.Basic
 import Mathlib.Probability.ProbabilityMassFunction.Monad
 import Mathlib.RepresentationTheory.Maschke
 import Mathlib.RingTheory.Adjoin.Basic
-import Mathlib.RingTheory.Adjoin.Fg
+import Mathlib.RingTheory.Adjoin.FG
 import Mathlib.RingTheory.Adjoin.Tower
 import Mathlib.RingTheory.AlgebraTower
 import Mathlib.RingTheory.ChainOfDivisors
@@ -1779,7 +1779,7 @@ import Mathlib.RingTheory.Flat
 import Mathlib.RingTheory.FreeRing
 import Mathlib.RingTheory.Ideal.AssociatedPrime
 import Mathlib.RingTheory.Ideal.Basic
-import Mathlib.RingTheory.Ideal.IdempotentFg
+import Mathlib.RingTheory.Ideal.IdempotentFG
 import Mathlib.RingTheory.Ideal.Operations
 import Mathlib.RingTheory.Ideal.Prod
 import Mathlib.RingTheory.Ideal.Quotient

Mathlib/GroupTheory/Abelianization.lean

@@ -59,7 +59,7 @@ instance commutator_characteristic : (commutator G).Characteristic :=
   Subgroup.commutator_characteristic ⊤ ⊤
 #align commutator_characteristic commutator_characteristic
 
-instance [Finite (commutatorSet G)] : Group.Fg (commutator G) := by
+instance [Finite (commutatorSet G)] : Group.FG (commutator G) := by
   rw [commutator_eq_closure]
   apply Group.closure_finite_fg
 
@@ -276,7 +276,7 @@ def closureCommutatorRepresentatives : Subgroup G :=
 #align closure_commutator_representatives closureCommutatorRepresentatives
 
 instance closureCommutatorRepresentatives_fg [Finite (commutatorSet G)] :
-    Group.Fg (closureCommutatorRepresentatives G) :=
+    Group.FG (closureCommutatorRepresentatives G) :=
   Group.closure_finite_fg _
 #align closure_commutator_representatives_fg closureCommutatorRepresentatives_fg
 

Mathlib/GroupTheory/Index.lean

@@ -602,12 +602,12 @@ instance finiteIndex_normalCore [H.FiniteIndex] : H.normalCore.FiniteIndex := by
 
 variable (G)
 
-instance finiteIndex_center [Finite (commutatorSet G)] [Group.Fg G] : FiniteIndex (center G) := by
+instance finiteIndex_center [Finite (commutatorSet G)] [Group.FG G] : FiniteIndex (center G) := by
   obtain ⟨S, -, hS⟩ := Group.rank_spec G
   exact ⟨mt (Finite.card_eq_zero_of_embedding (quotientCenterEmbedding hS)) Finite.card_pos.ne'⟩
 #align subgroup.finite_index_center Subgroup.finiteIndex_center
 
-theorem index_center_le_pow [Finite (commutatorSet G)] [Group.Fg G] :
+theorem index_center_le_pow [Finite (commutatorSet G)] [Group.FG G] :
     (center G).index ≤ Nat.card (commutatorSet G) ^ Group.rank G := by
   obtain ⟨S, hS1, hS2⟩ := Group.rank_spec G
   rw [← hS1, ← Fintype.card_coe, ← Nat.card_eq_fintype_card, ← Finset.coe_sort_coe, ← Nat.card_fun]

Mathlib/LinearAlgebra/FiniteDimensional.lean

@@ -705,7 +705,7 @@ section DivisionRing
 variable [DivisionRing K] [AddCommGroup V] [Module K V]
 
 /-- A submodule is finitely generated if and only if it is finite-dimensional -/
-theorem fg_iff_finiteDimensional (s : Submodule K V) : s.Fg ↔ FiniteDimensional K s :=
+theorem fg_iff_finiteDimensional (s : Submodule K V) : s.FG ↔ FiniteDimensional K s :=
   ⟨fun h => Module.finite_def.2 <| (fg_top s).2 h, fun h => (fg_top s).1 <| Module.finite_def.1 h⟩
 #align submodule.fg_iff_finite_dimensional Submodule.fg_iff_finiteDimensional
 

Mathlib/RingTheory/Adjoin/Fg.lean → Mathlib/RingTheory/Adjoin/FG.lean

@@ -19,7 +19,7 @@ This file develops the basic theory of finitely-generated subalgebras.
 
 ## Definitions
 
-* `Fg (S : Subalgebra R A)` : A predicate saying that the subalgebra is finitely-generated
+* `FG (S : Subalgebra R A)` : A predicate saying that the subalgebra is finitely-generated
 as an A-algebra
 
 ## Tags
@@ -40,8 +40,8 @@ namespace Algebra
 variable {R : Type u} {A : Type v} {B : Type w} [CommSemiring R] [CommSemiring A] [Algebra R A]
   {s t : Set A}
 
-theorem fg_trans (h1 : (adjoin R s).toSubmodule.Fg) (h2 : (adjoin (adjoin R s) t).toSubmodule.Fg) :
-    (adjoin R (s ∪ t)).toSubmodule.Fg := by
+theorem fg_trans (h1 : (adjoin R s).toSubmodule.FG) (h2 : (adjoin (adjoin R s) t).toSubmodule.FG) :
+    (adjoin R (s ∪ t)).toSubmodule.FG := by
   rcases fg_def.1 h1 with ⟨p, hp, hp'⟩
   rcases fg_def.1 h2 with ⟨q, hq, hq'⟩
   refine' fg_def.2 ⟨p * q, hp.mul hq, le_antisymm _ _⟩
@@ -93,23 +93,23 @@ variable [CommSemiring R] [Semiring A] [Algebra R A] [Semiring B] [Algebra R B]
 
 /-- A subalgebra `S` is finitely generated if there exists `t : finset A` such that
 `algebra.adjoin R t = S`. -/
-def Fg (S : Subalgebra R A) : Prop :=
+def FG (S : Subalgebra R A) : Prop :=
   ∃ t : Finset A, Algebra.adjoin R ↑t = S
-#align subalgebra.fg Subalgebra.Fg
+#align subalgebra.fg Subalgebra.FG
 
-theorem fg_adjoin_finset (s : Finset A) : (Algebra.adjoin R (↑s : Set A)).Fg :=
+theorem fg_adjoin_finset (s : Finset A) : (Algebra.adjoin R (↑s : Set A)).FG :=
   ⟨s, rfl⟩
 #align subalgebra.fg_adjoin_finset Subalgebra.fg_adjoin_finset
 
-theorem fg_def {S : Subalgebra R A} : S.Fg ↔ ∃ t : Set A, Set.Finite t ∧ Algebra.adjoin R t = S :=
+theorem fg_def {S : Subalgebra R A} : S.FG ↔ ∃ t : Set A, Set.Finite t ∧ Algebra.adjoin R t = S :=
   Iff.symm Set.exists_finite_iff_finset
 #align subalgebra.fg_def Subalgebra.fg_def
 
-theorem fg_bot : (⊥ : Subalgebra R A).Fg :=
+theorem fg_bot : (⊥ : Subalgebra R A).FG :=
   ⟨∅, Finset.coe_empty ▸ Algebra.adjoin_empty R A⟩
 #align subalgebra.fg_bot Subalgebra.fg_bot
 
-theorem fg_of_fg_toSubmodule {S : Subalgebra R A} : S.toSubmodule.Fg → S.Fg :=
+theorem fg_of_fg_toSubmodule {S : Subalgebra R A} : S.toSubmodule.FG → S.FG :=
   fun ⟨t, ht⟩ ↦ ⟨t, le_antisymm
     (Algebra.adjoin_le fun x hx ↦ show x ∈ Subalgebra.toSubmodule S from ht ▸ subset_span hx) <|
     show Subalgebra.toSubmodule S ≤ Subalgebra.toSubmodule (Algebra.adjoin R ↑t) from fun x hx ↦
@@ -119,41 +119,41 @@ theorem fg_of_fg_toSubmodule {S : Subalgebra R A} : S.toSubmodule.Fg → S.Fg :=
           exact hx)⟩
 #align subalgebra.fg_of_fg_to_submodule Subalgebra.fg_of_fg_toSubmodule
 
-theorem fg_of_noetherian [IsNoetherian R A] (S : Subalgebra R A) : S.Fg :=
+theorem fg_of_noetherian [IsNoetherian R A] (S : Subalgebra R A) : S.FG :=
   fg_of_fg_toSubmodule (IsNoetherian.noetherian (Subalgebra.toSubmodule S))
 #align subalgebra.fg_of_noetherian Subalgebra.fg_of_noetherian
 
-theorem fg_of_submodule_fg (h : (⊤ : Submodule R A).Fg) : (⊤ : Subalgebra R A).Fg :=
+theorem fg_of_submodule_fg (h : (⊤ : Submodule R A).FG) : (⊤ : Subalgebra R A).FG :=
   let ⟨s, hs⟩ := h
   ⟨s, toSubmodule.injective <| by
     rw [Algebra.top_toSubmodule, eq_top_iff, ← hs, span_le]
     exact Algebra.subset_adjoin⟩
 #align subalgebra.fg_of_submodule_fg Subalgebra.fg_of_submodule_fg
 
-theorem Fg.prod {S : Subalgebra R A} {T : Subalgebra R B} (hS : S.Fg) (hT : T.Fg) :
-    (S.prod T).Fg := by
+theorem FG.prod {S : Subalgebra R A} {T : Subalgebra R B} (hS : S.FG) (hT : T.FG) :
+    (S.prod T).FG := by
   obtain ⟨s, hs⟩ := fg_def.1 hS
   obtain ⟨t, ht⟩ := fg_def.1 hT
   rw [← hs.2, ← ht.2]
   exact fg_def.2 ⟨LinearMap.inl R A B '' (s ∪ {1}) ∪ LinearMap.inr R A B '' (t ∪ {1}),
     Set.Finite.union (Set.Finite.image _ (Set.Finite.union hs.1 (Set.finite_singleton _)))
       (Set.Finite.image _ (Set.Finite.union ht.1 (Set.finite_singleton _))),
     Algebra.adjoin_inl_union_inr_eq_prod R s t⟩
-#align subalgebra.fg.prod Subalgebra.Fg.prod
+#align subalgebra.fg.prod Subalgebra.FG.prod
 
 section
 
 open Classical
 
-theorem Fg.map {S : Subalgebra R A} (f : A →ₐ[R] B) (hs : S.Fg) : (S.map f).Fg :=
+theorem FG.map {S : Subalgebra R A} (f : A →ₐ[R] B) (hs : S.FG) : (S.map f).FG :=
   let ⟨s, hs⟩ := hs
   ⟨s.image f, by rw [Finset.coe_image, Algebra.adjoin_image, hs]⟩
-#align subalgebra.fg.map Subalgebra.Fg.map
+#align subalgebra.fg.map Subalgebra.FG.map
 
 end
 
 theorem fg_of_fg_map (S : Subalgebra R A) (f : A →ₐ[R] B) (hf : Function.Injective f)
-    (hs : (S.map f).Fg) : S.Fg :=
+    (hs : (S.map f).FG) : S.FG :=
   let ⟨s, hs⟩ := hs
   ⟨s.preimage f fun _ _ _ _ h ↦ hf h,
     map_injective hf <| by
@@ -162,10 +162,10 @@ theorem fg_of_fg_map (S : Subalgebra R A) (f : A →ₐ[R] B) (hf : Function.Inj
       exact map_mono le_top⟩
 #align subalgebra.fg_of_fg_map Subalgebra.fg_of_fg_map
 
-theorem fg_top (S : Subalgebra R A) : (⊤ : Subalgebra R S).Fg ↔ S.Fg :=
+theorem fg_top (S : Subalgebra R A) : (⊤ : Subalgebra R S).FG ↔ S.FG :=
   ⟨fun h ↦ by
     rw [← S.range_val, ← Algebra.map_top]
-    exact Fg.map _ h, fun h ↦
+    exact FG.map _ h, fun h ↦
     fg_of_fg_map _ S.val Subtype.val_injective <| by
       rw [Algebra.map_top, range_val]
       exact h⟩
@@ -205,7 +205,7 @@ variable {R : Type u} {A : Type v} {B : Type w}
 
 variable [CommRing R] [CommRing A] [CommRing B] [Algebra R A] [Algebra R B]
 
-theorem isNoetherianRing_of_fg {S : Subalgebra R A} (HS : S.Fg) [IsNoetherianRing R] :
+theorem isNoetherianRing_of_fg {S : Subalgebra R A} (HS : S.FG) [IsNoetherianRing R] :
     IsNoetherianRing S :=
   let ⟨t, ht⟩ := HS
   ht ▸ (Algebra.adjoin_eq_range R (↑t : Set A)).symm ▸ AlgHom.isNoetherianRing_range _

Mathlib/RingTheory/Adjoin/Tower.lean

@@ -8,7 +8,7 @@ Authors: Kenny Lau
 ! Please do not edit these lines, except to modify the commit id
 ! if you have ported upstream changes.
 -/
-import Mathlib.RingTheory.Adjoin.Fg
+import Mathlib.RingTheory.Adjoin.FG
 
 /-!
 # Adjoining elements and being finitely generated in an algebra tower
@@ -75,8 +75,8 @@ section
 open Classical
 
 theorem Algebra.fg_trans' {R S A : Type _} [CommSemiring R] [CommSemiring S] [CommSemiring A]
-    [Algebra R S] [Algebra S A] [Algebra R A] [IsScalarTower R S A] (hRS : (⊤ : Subalgebra R S).Fg)
-    (hSA : (⊤ : Subalgebra S A).Fg) : (⊤ : Subalgebra R A).Fg :=
+    [Algebra R S] [Algebra S A] [Algebra R A] [IsScalarTower R S A] (hRS : (⊤ : Subalgebra R S).FG)
+    (hSA : (⊤ : Subalgebra S A).FG) : (⊤ : Subalgebra R A).FG :=
   let ⟨s, hs⟩ := hRS
   let ⟨t, ht⟩ := hSA
   ⟨s.image (algebraMap S A) ∪ t, by
@@ -101,8 +101,8 @@ open Finset Submodule
 
 open Classical
 
-theorem exists_subalgebra_of_fg (hAC : (⊤ : Subalgebra A C).Fg) (hBC : (⊤ : Submodule B C).Fg) :
-    ∃ B₀ : Subalgebra A B, B₀.Fg ∧ (⊤ : Submodule B₀ C).Fg := by
+theorem exists_subalgebra_of_fg (hAC : (⊤ : Subalgebra A C).FG) (hBC : (⊤ : Submodule B C).FG) :
+    ∃ B₀ : Subalgebra A B, B₀.FG ∧ (⊤ : Submodule B₀ C).FG := by
   cases' hAC with x hx
   cases' hBC with y hy
   have := hy
@@ -162,9 +162,9 @@ A is noetherian, and C is algebra-finite over A, and C is module-finite over B,
 then B is algebra-finite over A.
 
 References: Atiyah--Macdonald Proposition 7.8; Stacks 00IS; Altman--Kleiman 16.17. -/
-theorem fg_of_fg_of_fg [IsNoetherianRing A] (hAC : (⊤ : Subalgebra A C).Fg)
-    (hBC : (⊤ : Submodule B C).Fg) (hBCi : Function.Injective (algebraMap B C)) :
-    (⊤ : Subalgebra A B).Fg :=
+theorem fg_of_fg_of_fg [IsNoetherianRing A] (hAC : (⊤ : Subalgebra A C).FG)
+    (hBC : (⊤ : Submodule B C).FG) (hBCi : Function.Injective (algebraMap B C)) :
+    (⊤ : Subalgebra A B).FG :=
   let ⟨B₀, hAB₀, hB₀C⟩ := exists_subalgebra_of_fg A B C hAC hBC
   Algebra.fg_trans' (B₀.fg_top.2 hAB₀) <|
     Subalgebra.fg_of_submodule_fg <|
@@ -176,4 +176,3 @@ theorem fg_of_fg_of_fg [IsNoetherianRing A] (hAC : (⊤ : Subalgebra A C).Fg)
 end Ring
 
 end ArtinTate
-

Mathlib/RingTheory/FiniteType.lean

@@ -37,7 +37,7 @@ variable (R) (A : Type u) (B M N : Type _)
 /-- An algebra over a commutative semiring is of `FiniteType` if it is finitely generated
 over the base ring as algebra. -/
 class Algebra.FiniteType [CommSemiring R] [Semiring A] [Algebra R A] : Prop where
-  out : (⊤ : Subalgebra R A).Fg
+  out : (⊤ : Subalgebra R A).FG
 #align algebra.finite_type Algebra.FiniteType
 
 namespace Module
@@ -180,7 +180,7 @@ theorem isNoetherianRing (R S : Type _) [CommRing R] [CommRing S] [Algebra R S]
 #align algebra.finite_type.is_noetherian_ring Algebra.FiniteType.isNoetherianRing
 
 theorem _root_.Subalgebra.fg_iff_finiteType {R A : Type _} [CommSemiring R]
-    [Semiring A] [Algebra R A] (S : Subalgebra R A) : S.Fg ↔ Algebra.FiniteType R S :=
+    [Semiring A] [Algebra R A] (S : Subalgebra R A) : S.FG ↔ Algebra.FiniteType R S :=
   S.fg_top.symm.trans ⟨fun h => ⟨h⟩, fun h => h.out⟩
 #align subalgebra.fg_iff_finite_type Subalgebra.fg_iff_finiteType
 
@@ -449,7 +449,7 @@ variable (R M)
 
 /-- If an additive monoid `M` is finitely generated then `AddMonoidAlgebra R M` is of finite
 type. -/
-instance finiteType_of_fg [CommRing R] [h : AddMonoid.Fg M] :
+instance finiteType_of_fg [CommRing R] [h : AddMonoid.FG M] :
     FiniteType R (AddMonoidAlgebra R M) := by
   obtain ⟨S, hS⟩ := h.out
   exact (FiniteType.mvPolynomial R (S : Set M)).of_surjective
@@ -462,7 +462,7 @@ variable {R M}
 /-- An additive monoid `M` is finitely generated if and only if `AddMonoidAlgebra R M` is of
 finite type. -/
 theorem finiteType_iff_fg [CommRing R] [Nontrivial R] :
-    FiniteType R (AddMonoidAlgebra R M) ↔ AddMonoid.Fg M := by
+    FiniteType R (AddMonoidAlgebra R M) ↔ AddMonoid.FG M := by
   refine' ⟨fun h => _, fun h => @AddMonoidAlgebra.finiteType_of_fg _ _ _ _ h⟩
   obtain ⟨S, hS⟩ := @exists_finset_adjoin_eq_top R M _ _ h
   refine' AddMonoid.fg_def.2 ⟨S, (eq_top_iff' _).2 fun m => _⟩
@@ -474,14 +474,14 @@ theorem finiteType_iff_fg [CommRing R] [Nontrivial R] :
 
 /-- If `AddMonoidAlgebra R M` is of finite type then `M` is finitely generated. -/
 theorem fg_of_finiteType [CommRing R] [Nontrivial R] [h : FiniteType R (AddMonoidAlgebra R M)] :
-    AddMonoid.Fg M :=
+    AddMonoid.FG M :=
   finiteType_iff_fg.1 h
 #align add_monoid_algebra.fg_of_finite_type AddMonoidAlgebra.fg_of_finiteType
 
 /-- An additive group `G` is finitely generated if and only if `AddMonoidAlgebra R G` is of
 finite type. -/
 theorem finiteType_iff_group_fg {G : Type _} [AddCommGroup G] [CommRing R] [Nontrivial R] :
-    FiniteType R (AddMonoidAlgebra R G) ↔ AddGroup.Fg G := by
+    FiniteType R (AddMonoidAlgebra R G) ↔ AddGroup.FG G := by
   simpa [AddGroup.fg_iff_addMonoid_fg] using finiteType_iff_fg
 #align add_monoid_algebra.finite_type_iff_group_fg AddMonoidAlgebra.finiteType_iff_group_fg
 
@@ -601,13 +601,13 @@ theorem mvPolynomial_aeval_of_surjective_of_closure [CommSemiring R] {S : Set M}
 #align monoid_algebra.mv_polynomial_aeval_of_surjective_of_closure MonoidAlgebra.mvPolynomial_aeval_of_surjective_of_closure
 
 /-- If a monoid `M` is finitely generated then `MonoidAlgebra R M` is of finite type. -/
-instance finiteType_of_fg [CommRing R] [Monoid.Fg M] : FiniteType R (MonoidAlgebra R M) :=
+instance finiteType_of_fg [CommRing R] [Monoid.FG M] : FiniteType R (MonoidAlgebra R M) :=
   (AddMonoidAlgebra.finiteType_of_fg R (Additive M)).equiv (toAdditiveAlgEquiv R M).symm
 #align monoid_algebra.finite_type_of_fg MonoidAlgebra.finiteType_of_fg
 
 /-- A monoid `M` is finitely generated if and only if `MonoidAlgebra R M` is of finite type. -/
 theorem finiteType_iff_fg [CommRing R] [Nontrivial R] :
-    FiniteType R (MonoidAlgebra R M) ↔ Monoid.Fg M :=
+    FiniteType R (MonoidAlgebra R M) ↔ Monoid.FG M :=
   ⟨fun h =>
     Monoid.fg_iff_add_fg.2 <|
       AddMonoidAlgebra.finiteType_iff_fg.1 <| h.equiv <| toAdditiveAlgEquiv R M,
@@ -616,13 +616,13 @@ theorem finiteType_iff_fg [CommRing R] [Nontrivial R] :
 
 /-- If `MonoidAlgebra R M` is of finite type then `M` is finitely generated. -/
 theorem fg_of_finiteType [CommRing R] [Nontrivial R] [h : FiniteType R (MonoidAlgebra R M)] :
-    Monoid.Fg M :=
+    Monoid.FG M :=
   finiteType_iff_fg.1 h
 #align monoid_algebra.fg_of_finite_type MonoidAlgebra.fg_of_finiteType
 
 /-- A group `G` is finitely generated if and only if `AddMonoidAlgebra R G` is of finite type. -/
 theorem finiteType_iff_group_fg {G : Type _} [CommGroup G] [CommRing R] [Nontrivial R] :
-    FiniteType R (MonoidAlgebra R G) ↔ Group.Fg G := by
+    FiniteType R (MonoidAlgebra R G) ↔ Group.FG G := by
   simpa [Group.fg_iff_monoid_fg] using finiteType_iff_fg
 #align monoid_algebra.finite_type_iff_group_fg MonoidAlgebra.finiteType_iff_group_fg