feat(Algebra/Homology): sandwich a comm group between two finite comm groups (#31227)

From ClassFieldTheory

Author: YaelDillies

Mathlib/Algebra/Homology/ShortComplex/Ab.lean

@@ -3,10 +3,11 @@ Copyright (c) 2023 Joël Riou. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Joël Riou
 -/
-import Mathlib.Algebra.Homology.ShortComplex.ShortExact
 import Mathlib.Algebra.Category.Grp.Abelian
 import Mathlib.Algebra.Category.Grp.Kernels
 import Mathlib.Algebra.Exact
+import Mathlib.Algebra.Homology.ShortComplex.ShortExact
+import Mathlib.GroupTheory.QuotientGroup.Finite
 
 /-!
 # Homology and exactness of short complexes of abelian groups
@@ -121,6 +122,8 @@ lemma ab_exact_iff_function_exact :
     simp only [ab_zero_apply]
   · tauto
 
+variable {S}
+
 lemma ab_exact_iff_ker_le_range : S.Exact ↔ S.g.hom.ker ≤ S.f.hom.range := S.ab_exact_iff
 
 lemma ab_exact_iff_range_eq_ker : S.Exact ↔ S.f.hom.range = S.g.hom.ker := by
@@ -134,7 +137,17 @@ lemma ab_exact_iff_range_eq_ker : S.Exact ↔ S.f.hom.range = S.g.hom.ker := by
   · intro h
     rw [h]
 
-variable {S}
+alias ⟨Exact.ab_range_eq_ker, _⟩ := ab_exact_iff_range_eq_ker
+
+/-- In an exact sequence of abelian groups, if the first and last groups are finite, then so is the
+middle one. -/
+lemma Exact.ab_finite {S : ShortComplex Ab.{u}} (hS : S.Exact) [Finite S.X₁] [Finite S.X₃] :
+    Finite S.X₂ := by
+  have : Finite S.f.hom.range := Set.finite_range _
+  have : Finite (S.X₂ ⧸ S.f.hom.range) := by
+    rw [hS.ab_range_eq_ker]
+    exact .of_equiv _ (QuotientAddGroup.quotientKerEquivRange _).toEquiv.symm
+  exact .of_addSubgroup_quotient (H := S.f.hom.range)
 
 lemma ShortExact.ab_injective_f (hS : S.ShortExact) :
     Function.Injective S.f :=
@@ -144,12 +157,15 @@ lemma ShortExact.ab_surjective_g (hS : S.ShortExact) :
     Function.Surjective S.g :=
   (AddCommGrpCat.epi_iff_surjective _).1 hS.epi_g
 
-variable (S)
+/-- In a short exact sequence of abelian groups, the middle group is finite iff the first and last
+are. -/
+lemma ShortExact.ab_finite_iff {S : ShortComplex Ab.{u}} (hS : S.ShortExact) :
+    Finite S.X₂ ↔ Finite S.X₁ ∧ Finite S.X₃ where
+  mp _ := ⟨.of_injective _ hS.ab_injective_f, .of_surjective _ hS.ab_surjective_g⟩
+  mpr | ⟨_, _⟩ => hS.exact.ab_finite
 
-lemma ShortExact.ab_exact_iff_function_exact :
-    S.Exact ↔ Function.Exact S.f S.g := by
-  rw [ab_exact_iff_range_eq_ker, AddMonoidHom.exact_iff]
-  tauto
+@[deprecated (since := "2025-11-03")]
+protected alias ShortExact.ab_exact_iff_function_exact := ab_exact_iff_function_exact
 
 end ShortComplex
 

Mathlib/Data/Finite/Prod.lean

@@ -38,6 +38,10 @@ theorem prod_right (α) [Finite (α × β)] [Nonempty α] : Finite β :=
 
 end Finite
 
+lemma Prod.finite_iff [Nonempty α] [Nonempty β] : Finite (α × β) ↔ Finite α ∧ Finite β where
+  mp _ := ⟨.prod_left β, .prod_right α⟩
+  mpr | ⟨_, _⟩ => inferInstance
+
 instance Pi.finite {α : Sort*} {β : α → Sort*} [Finite α] [∀ a, Finite (β a)] :
     Finite (∀ a, β a) := by
   classical

Mathlib/Data/Set/Finite/Basic.lean

@@ -664,6 +664,9 @@ theorem finite_union {s t : Set α} : (s ∪ t).Finite ↔ s.Finite ∧ t.Finite
 theorem finite_image_iff {s : Set α} {f : α → β} (hi : InjOn f s) : (f '' s).Finite ↔ s.Finite :=
   ⟨fun h => h.of_finite_image hi, Finite.image _⟩
 
+lemma finite_range_iff {f : α → β} (hf : f.Injective) : (range f).Finite ↔ Finite α := by
+  simpa [finite_univ_iff] using finite_image_iff (s := univ) hf.injOn
+
 theorem univ_finite_iff_nonempty_fintype : (univ : Set α).Finite ↔ Nonempty (Fintype α) :=
   ⟨fun h => ⟨fintypeOfFiniteUniv h⟩, fun ⟨_i⟩ => finite_univ⟩
 
@@ -865,9 +868,8 @@ theorem infinite_image_iff {s : Set α} {f : α → β} (hi : InjOn f s) :
     (f '' s).Infinite ↔ s.Infinite :=
   not_congr <| finite_image_iff hi
 
-theorem infinite_range_iff {f : α → β} (hi : Injective f) :
-    (range f).Infinite ↔ Infinite α := by
-  rw [← image_univ, infinite_image_iff hi.injOn, infinite_univ_iff]
+theorem infinite_range_iff {f : α → β} (hf : Injective f) : (range f).Infinite ↔ Infinite α := by
+  simpa using (finite_range_iff hf).not
 
 protected alias ⟨_, Infinite.image⟩ := infinite_image_iff
 

Mathlib/GroupTheory/QuotientGroup/Finite.lean

@@ -13,18 +13,15 @@ import Mathlib.GroupTheory.QuotientGroup.Basic
 # Deducing finiteness of a group.
 -/
 
-open Function
+open Function QuotientGroup Subgroup
 open scoped Pointwise
 
-universe u v w x
 
-namespace Group
-
-open QuotientGroup Subgroup
-
-variable {F G H : Type u} [Group F] [Group G] [Group H] [Fintype F] [Fintype H]
+variable {F G H : Type*} [Group F] [Group G] [Group H] [Fintype F] [Fintype H]
 variable (f : F →* G) (g : G →* H)
 
+namespace Group
+
 open scoped Classical in
 /-- If `F` and `H` are finite such that `ker(G →* H) ≤ im(F →* G)`, then `G` is finite. -/
 @[to_additive
@@ -52,9 +49,18 @@ noncomputable def fintypeOfKerOfCodom [Fintype g.ker] : Fintype G :=
 noncomputable def fintypeOfDomOfCoker [Normal f.range] [Fintype <| G ⧸ f.range] : Fintype G :=
   fintypeOfKerLeRange _ (mk' f.range) fun x => (eq_one_iff x).mp
 
+end Group
+
 @[to_additive]
-lemma _root_.Finite.of_finite_quot_finite_subgroup {H : Subgroup G} [Finite H] [Finite (G ⧸ H)] :
-    Finite G :=
-  Finite.of_equiv _ (groupEquivQuotientProdSubgroup (s := H)).symm
+lemma finite_iff_subgroup_quotient (H : Subgroup G) : Finite G ↔ Finite H ∧ Finite (G ⧸ H) := by
+  rw [(groupEquivQuotientProdSubgroup (s := H)).finite_iff, Prod.finite_iff, and_comm]
 
-end Group
+@[to_additive]
+lemma Finite.of_subgroup_quotient (H : Subgroup G) [Finite H] [Finite (G ⧸ H)] : Finite G := by
+  rw [finite_iff_subgroup_quotient]; constructor <;> assumption
+
+@[deprecated (since := "2025-11-11")]
+alias Finite.of_finite_quot_finite_subgroup := Finite.of_subgroup_quotient
+
+@[deprecated (since := "2025-11-11")]
+alias Finite.of_finite_quot_finite_addSubgroup := Finite.of_addSubgroup_quotient

Mathlib/RingTheory/Ideal/Quotient/Basic.lean

@@ -24,20 +24,14 @@ See `Algebra.RingQuot` for quotients of semirings.
 
 -/
 
-
-universe u v w
-
-namespace Ideal
-
 open Set
 
-variable {R : Type u} [Ring R] (I J : Ideal R) {a b : R}
-variable {S : Type v}
+variable {ι ι' R S : Type*} [Ring R] (I J : Ideal R) {a b : R}
 
-namespace Quotient
+namespace Ideal.Quotient
 
 @[simp]
-lemma mk_span_range {ι : Type*} (f : ι → R) [(span (range f)).IsTwoSided] (i : ι) :
+lemma mk_span_range (f : ι → R) [(span (range f)).IsTwoSided] (i : ι) :
     mk (span (.range f)) (f i) = 0 := by
   rw [Ideal.Quotient.eq_zero_iff_mem]
   exact Ideal.subset_span ⟨i, rfl⟩
@@ -174,8 +168,6 @@ end Quotient
 
 section Pi
 
-variable (ι : Type v)
-
 /-- `R^n/I^n` is a `R/I`-module. -/
 instance modulePi [I.IsTwoSided] : Module (R ⧸ I) ((ι → R) ⧸ pi fun _ ↦ I) where
   smul c m :=
@@ -192,6 +184,7 @@ instance modulePi [I.IsTwoSided] : Module (R ⧸ I) ((ι → R) ⧸ pi fun _ ↦
   add_smul := by rintro ⟨a⟩ ⟨b⟩ ⟨c⟩; exact congr_arg _ (add_smul _ _ _)
   zero_smul := by rintro ⟨a⟩; exact congr_arg _ (zero_smul _ _)
 
+variable (ι) in
 /-- `R^n/I^n` is isomorphic to `(R/I)^n` as an `R/I`-module. -/
 noncomputable def piQuotEquiv [I.IsTwoSided] : ((ι → R) ⧸ pi fun _ ↦ I) ≃ₗ[R ⧸ I] ι → (R ⧸ I) where
   toFun x := Quotient.liftOn' x (fun f i ↦ Ideal.Quotient.mk I (f i)) fun _ _ hab ↦
@@ -206,7 +199,7 @@ noncomputable def piQuotEquiv [I.IsTwoSided] : ((ι → R) ⧸ pi fun _ ↦ I) 
 
 /-- If `f : R^n → R^m` is an `R`-linear map and `I ⊆ R` is an ideal, then the image of `I^n` is
     contained in `I^m`. -/
-theorem map_pi [I.IsTwoSided] {ι : Type*} [Finite ι] {ι' : Type w} (x : ι → R) (hi : ∀ i, x i ∈ I)
+theorem map_pi [I.IsTwoSided] [Finite ι] (x : ι → R) (hi : ∀ i, x i ∈ I)
     (f : (ι → R) →ₗ[R] ι' → R) (i : ι') : f x i ∈ I := by
   classical
     cases nonempty_fintype ι
@@ -221,8 +214,13 @@ open scoped Pointwise in
 lemma univ_eq_iUnion_image_add : (Set.univ (α := R)) = ⋃ x : R ⧸ I, x.out +ᵥ (I : Set R) :=
   QuotientAddGroup.univ_eq_iUnion_vadd I.toAddSubgroup
 
-variable {I} in
-lemma _root_.Finite.of_finite_quot_finite_ideal [hI : Finite I] [h : Finite (R ⧸ I)] : Finite R :=
-  @Finite.of_finite_quot_finite_addSubgroup _ _ _ hI h
-
 end Ideal
+
+lemma finite_iff_ideal_quotient (I : Ideal R) : Finite R ↔ Finite I ∧ Finite (R ⧸ I) :=
+  finite_iff_addSubgroup_quotient I.toAddSubgroup
+
+lemma Finite.of_ideal_quotient (I : Ideal R) [Finite I] [Finite (R ⧸ I)] : Finite R := by
+  rw [finite_iff_ideal_quotient]; constructor <;> assumption
+
+@[deprecated (since := "2025-11-11")]
+alias Finite.of_finite_quot_finite_ideal := Finite.of_ideal_quotient

Mathlib/Topology/Algebra/Valued/LocallyCompact.lean

@@ -114,8 +114,7 @@ lemma finite_quotient_maximalIdeal_pow_of_finite_residueField [IsDiscreteValuati
     have : 𝓂[K] ^ (n + 1) ≤ 𝓂[K] ^ n := Ideal.pow_le_pow_right (by simp)
     replace ih := Finite.of_equiv _ (DoubleQuot.quotQuotEquivQuotOfLE this).symm.toEquiv
     suffices Finite (Ideal.map (Ideal.Quotient.mk (𝓂[K] ^ (n + 1))) (𝓂[K] ^ n)) from
-      Finite.of_finite_quot_finite_ideal
-        (I := Ideal.map (Ideal.Quotient.mk _) (𝓂[K] ^ n))
+      .of_ideal_quotient (.map (Ideal.Quotient.mk _) (𝓂[K] ^ n))
     exact @Finite.of_equiv _ _ h
       ((Ideal.quotEquivPowQuotPowSuccEquiv (IsPrincipalIdealRing.principal 𝓂[K])
         (IsDiscreteValuationRing.not_a_field _) n).trans