From d63c52e5c0b3375b087ed4979563cd4a17ad94d5 Mon Sep 17 00:00:00 2001 From: David Kurniadi Angdinata Date: Mon, 31 Jul 2023 08:59:25 +0000 Subject: [PATCH] feat(Algebra/Category/GroupCat/Abelian): prove AddCommGroupCat is AB5 (#5597) This work was done during the 2023 Copenhagen masterclass on formalisation of condensed mathematics. Numerous participants contributed. Co-authored-by: Moritz Firsching Co-authored-by: Nikolas Kuhn Co-authored-by: Amelia Livingston <101damnations@github.com> Co-authored-by: Markus Himmel Co-authored-by: Moritz Firsching Co-authored-by: adamtopaz Co-authored-by: nick-kuhn --- Mathlib.lean | 1 + .../Algebra/Category/GroupCat/Abelian.lean | 56 ++++++++++++------- Mathlib/Algebra/Category/GroupCat/Basic.lean | 6 ++ .../Algebra/Category/GroupCat/Kernels.lean | 47 ++++++++++++++++ Mathlib/GroupTheory/QuotientGroup.lean | 8 ++- Mathlib/GroupTheory/Subgroup/Basic.lean | 6 +- 6 files changed, 103 insertions(+), 21 deletions(-) create mode 100644 Mathlib/Algebra/Category/GroupCat/Kernels.lean diff --git a/Mathlib.lean b/Mathlib.lean index b08812ae5e939..802d5bbdcc373 100644 --- a/Mathlib.lean +++ b/Mathlib.lean @@ -47,6 +47,7 @@ import Mathlib.Algebra.Category.GroupCat.EquivalenceGroupAddGroup import Mathlib.Algebra.Category.GroupCat.FilteredColimits import Mathlib.Algebra.Category.GroupCat.Images import Mathlib.Algebra.Category.GroupCat.Injective +import Mathlib.Algebra.Category.GroupCat.Kernels import Mathlib.Algebra.Category.GroupCat.Limits import Mathlib.Algebra.Category.GroupCat.Preadditive import Mathlib.Algebra.Category.GroupCat.Subobject diff --git a/Mathlib/Algebra/Category/GroupCat/Abelian.lean b/Mathlib/Algebra/Category/GroupCat/Abelian.lean index 668c9cb80afe4..132e9ea6932c5 100644 --- a/Mathlib/Algebra/Category/GroupCat/Abelian.lean +++ b/Mathlib/Algebra/Category/GroupCat/Abelian.lean @@ -3,11 +3,14 @@ Copyright (c) 2020 Markus Himmel. All rights reserved. Released under Apache 2.0 license as described in the file LICENSE. Authors: Markus Himmel -/ -import Mathlib.Algebra.Category.GroupCat.ZModuleEquivalence -import Mathlib.Algebra.Category.GroupCat.Limits import Mathlib.Algebra.Category.GroupCat.Colimits +import Mathlib.Algebra.Category.GroupCat.FilteredColimits +import Mathlib.Algebra.Category.GroupCat.Kernels +import Mathlib.Algebra.Category.GroupCat.Limits +import Mathlib.Algebra.Category.GroupCat.ZModuleEquivalence import Mathlib.Algebra.Category.ModuleCat.Abelian -import Mathlib.CategoryTheory.Abelian.Basic +import Mathlib.CategoryTheory.Abelian.FunctorCategory +import Mathlib.CategoryTheory.Limits.ConcreteCategory #align_import algebra.category.Group.abelian from "leanprover-community/mathlib"@"f7baecbb54bd0f24f228576f97b1752fc3c9b318" @@ -15,10 +18,7 @@ import Mathlib.CategoryTheory.Abelian.Basic # The category of abelian groups is abelian -/ - -open CategoryTheory - -open CategoryTheory.Limits +open CategoryTheory Limits universe u @@ -26,9 +26,7 @@ noncomputable section namespace AddCommGroupCat -section - -variable {X Y : AddCommGroupCat.{u}} (f : X ⟶ Y) +variable {X Y Z : AddCommGroupCat.{u}} (f : X ⟶ Y) (g : Y ⟶ Z) /-- In the category of abelian groups, every monomorphism is normal. -/ def normalMono (_ : Mono f) : NormalMono f := @@ -44,18 +42,38 @@ def normalEpi (_ : Epi f) : NormalEpi f := set_option linter.uppercaseLean3 false in #align AddCommGroup.normal_epi AddCommGroupCat.normalEpi -end - /-- The category of abelian groups is abelian. -/ instance : Abelian AddCommGroupCat.{u} where - has_finite_products := ⟨by infer_instance⟩ + has_finite_products := ⟨HasFiniteProducts.out⟩ normalMonoOfMono := normalMono normalEpiOfEpi := normalEpi - add_comp := by - intros - simp only [Preadditive.add_comp] - comp_add := by - intros - simp only [Preadditive.comp_add] + +theorem exact_iff : Exact f g ↔ f.range = g.ker := by + rw [Abelian.exact_iff' f g (kernelIsLimit _) (cokernelIsColimit _)] + exact + ⟨fun h => ((AddMonoidHom.range_le_ker_iff _ _).mpr h.left).antisymm + ((QuotientAddGroup.ker_le_range_iff _ _).mpr h.right), + fun h => ⟨(AddMonoidHom.range_le_ker_iff _ _).mp h.le, + (QuotientAddGroup.ker_le_range_iff _ _).mp h.symm.le⟩⟩ + +/-- The category of abelian groups satisfies Grothedieck's Axiom AB5. -/ +instance {J : Type u} [SmallCategory J] [IsFiltered J] : + PreservesFiniteLimits <| colim (J := J) (C := AddCommGroupCat.{u}) := by + refine Functor.preservesFiniteLimitsOfMapExact _ + fun F G H η γ h => (exact_iff _ _).mpr (le_antisymm ?_ ?_) + all_goals replace h : ∀ j : J, Exact (η.app j) (γ.app j) := + fun j => Functor.map_exact ((evaluation _ _).obj j) η γ h + · rw [AddMonoidHom.range_le_ker_iff, ← comp_def] + exact colimit.hom_ext fun j => by simp [reassoc_of% (h j).w] + · intro x (hx : _ = _) + rcases Concrete.colimit_exists_rep G x with ⟨j, y, rfl⟩ + erw [← comp_apply, colimit.ι_map, comp_apply, + ← map_zero (by exact colimit.ι H j : H.obj j →+ ↑(colimit H))] at hx + rcases Concrete.colimit_exists_of_rep_eq H _ _ hx with ⟨k, e₁, e₂, hk : _ = H.map e₂ 0⟩ + rw [map_zero, ← comp_apply, ← NatTrans.naturality, comp_apply] at hk + rcases ((exact_iff _ _).mp <| h k).ge hk with ⟨t, ht⟩ + use colimit.ι F k t + erw [← comp_apply, colimit.ι_map, comp_apply, ht] + exact colimit.w_apply G e₁ y end AddCommGroupCat diff --git a/Mathlib/Algebra/Category/GroupCat/Basic.lean b/Mathlib/Algebra/Category/GroupCat/Basic.lean index 312095608f17a..501b876afec33 100644 --- a/Mathlib/Algebra/Category/GroupCat/Basic.lean +++ b/Mathlib/Algebra/Category/GroupCat/Basic.lean @@ -74,6 +74,9 @@ lemma coe_id {X : GroupCat} : (𝟙 X : X → X) = id := rfl @[to_additive (attr := simp)] lemma coe_comp {X Y Z : GroupCat} {f : X ⟶ Y} {g : Y ⟶ Z} : (f ≫ g : X → Z) = g ∘ f := rfl +@[to_additive] +lemma comp_def {X Y Z : GroupCat} {f : X ⟶ Y} {g : Y ⟶ Z} : f ≫ g = g.comp f := rfl + -- porting note: added @[simp] lemma forget_map (f : X ⟶ Y) : (forget GroupCat).map f = (f : X → Y) := rfl @@ -220,6 +223,9 @@ lemma coe_id {X : CommGroupCat} : (𝟙 X : X → X) = id := rfl @[to_additive (attr := simp)] lemma coe_comp {X Y Z : CommGroupCat} {f : X ⟶ Y} {g : Y ⟶ Z} : (f ≫ g : X → Z) = g ∘ f := rfl +@[to_additive] +lemma comp_def {X Y Z : CommGroupCat} {f : X ⟶ Y} {g : Y ⟶ Z} : f ≫ g = g.comp f := rfl + -- porting note: added @[to_additive (attr := simp)] lemma forget_map {X Y : CommGroupCat} (f : X ⟶ Y) : diff --git a/Mathlib/Algebra/Category/GroupCat/Kernels.lean b/Mathlib/Algebra/Category/GroupCat/Kernels.lean new file mode 100644 index 0000000000000..48087ae001490 --- /dev/null +++ b/Mathlib/Algebra/Category/GroupCat/Kernels.lean @@ -0,0 +1,47 @@ +/- +Copyright (c) 2023 Moritz Firsching. All rights reserved. +Released under Apache 2.0 license as described in the file LICENSE. +Authors: David Kurniadi Angdinata, Moritz Firsching, Nikolas Kuhn +-/ +import Mathlib.Algebra.Category.GroupCat.EpiMono +import Mathlib.Algebra.Category.GroupCat.Preadditive +import Mathlib.CategoryTheory.Limits.Shapes.Kernels + +/-! +# The concrete (co)kernels in the category of abelian groups are categorical (co)kernels. +-/ + +namespace AddCommGroupCat + +open AddMonoidHom CategoryTheory Limits QuotientAddGroup + +universe u + +variable {G H : AddCommGroupCat.{u}} (f : G ⟶ H) + +/-- The kernel cone induced by the concrete kernel. -/ +def kernelCone : KernelFork f := + KernelFork.ofι (Z := of f.ker) f.ker.subtype <| ext fun x => x.casesOn fun _ hx => hx + +/-- The kernel of a group homomorphism is a kernel in the categorical sense. -/ +def kernelIsLimit : IsLimit <| kernelCone f := + Fork.IsLimit.mk _ + (fun s => (by exact Fork.ι s : _ →+ G).codRestrict _ <| fun c => f.mem_ker.mpr <| + by exact FunLike.congr_fun s.condition c) + (fun _ => by rfl) + (fun _ _ h => ext fun x => Subtype.ext_iff_val.mpr <| by exact FunLike.congr_fun h x) + +/-- The cokernel cocone induced by the projection onto the quotient. -/ +def cokernelCocone : CokernelCofork f := + CokernelCofork.ofπ (Z := of <| H ⧸ f.range) (mk' f.range) <| ext fun x => + (eq_zero_iff _).mpr ⟨x, rfl⟩ + +/-- The projection onto the quotient is a cokernel in the categorical sense. -/ +def cokernelIsColimit : IsColimit <| cokernelCocone f := + Cofork.IsColimit.mk _ + (fun s => lift _ _ <| (range_le_ker_iff _ _).mpr <| CokernelCofork.condition s) + (fun _ => rfl) + (fun _ _ h => have : Epi (cokernelCocone f).π := (epi_iff_surjective _).mpr <| mk'_surjective _ + (cancel_epi _).mp <| by simpa only [parallelPair_obj_one] using h) + +end AddCommGroupCat diff --git a/Mathlib/GroupTheory/QuotientGroup.lean b/Mathlib/GroupTheory/QuotientGroup.lean index 693a5133db1fc..ba2dde4cc5f24 100644 --- a/Mathlib/GroupTheory/QuotientGroup.lean +++ b/Mathlib/GroupTheory/QuotientGroup.lean @@ -44,7 +44,7 @@ isomorphism theorems, quotient groups open Function -universe u v +universe u v w namespace QuotientGroup @@ -122,6 +122,12 @@ theorem eq_one_iff {N : Subgroup G} [nN : N.Normal] (x : G) : (x : G ⧸ N) = 1 #align quotient_group.eq_one_iff QuotientGroup.eq_one_iff #align quotient_add_group.eq_zero_iff QuotientAddGroup.eq_zero_iff +@[to_additive] +theorem ker_le_range_iff {I : Type w} [Group I] (f : G →* H) [f.range.Normal] (g : H →* I) : + g.ker ≤ f.range ↔ (mk' f.range).comp g.ker.subtype = 1 := + ⟨fun h => MonoidHom.ext fun ⟨_, hx⟩ => (eq_one_iff _).mpr <| h hx, + fun h x hx => (eq_one_iff _).mp <| by exact FunLike.congr_fun h ⟨x, hx⟩⟩ + @[to_additive (attr := simp)] theorem ker_mk' : MonoidHom.ker (QuotientGroup.mk' N : G →* G ⧸ N) = N := Subgroup.ext eq_one_iff diff --git a/Mathlib/GroupTheory/Subgroup/Basic.lean b/Mathlib/GroupTheory/Subgroup/Basic.lean index 626fba0fe1d81..18bd0a0d66964 100644 --- a/Mathlib/GroupTheory/Subgroup/Basic.lean +++ b/Mathlib/GroupTheory/Subgroup/Basic.lean @@ -89,7 +89,7 @@ subgroup, subgroups open Function open Int -variable {G G' : Type _} [Group G] [Group G'] +variable {G G' G'' : Type _} [Group G] [Group G'] [Group G''] variable {A : Type _} [AddGroup A] @@ -2869,6 +2869,10 @@ theorem ker_prodMap {G' : Type _} {N' : Type _} [Group G'] [Group N'] (f : G → #align monoid_hom.ker_prod_map MonoidHom.ker_prodMap #align add_monoid_hom.ker_sum_map AddMonoidHom.ker_sumMap +@[to_additive] +theorem range_le_ker_iff (f : G →* G') (g : G' →* G'') : f.range ≤ g.ker ↔ g.comp f = 1 := + ⟨fun h => ext fun x => h ⟨x, rfl⟩, by rintro h _ ⟨y, rfl⟩; exact FunLike.congr_fun h y⟩ + @[to_additive] instance (priority := 100) normal_ker (f : G →* M) : f.ker.Normal := ⟨fun x hx y => by