feat(CategoryTheory): results abouts kernels and pullback squares (leanprover-community#34495)

In a pullback square, the kernel of the top map identifies to the kernel of the bottom map. If the category is abelian and a square is pushout, the morphism from the kernel of the top map to the kernel of the bottom map is an epimorphism.
Dual results are also obtained.

Author: joelriou

Mathlib.lean

@@ -2731,6 +2731,7 @@ public import Mathlib.CategoryTheory.Limits.Shapes.Pullback.HasPullback
 public import Mathlib.CategoryTheory.Limits.Shapes.Pullback.IsPullback.Basic
 public import Mathlib.CategoryTheory.Limits.Shapes.Pullback.IsPullback.BicartesianSq
 public import Mathlib.CategoryTheory.Limits.Shapes.Pullback.IsPullback.Defs
+public import Mathlib.CategoryTheory.Limits.Shapes.Pullback.IsPullback.Kernels
 public import Mathlib.CategoryTheory.Limits.Shapes.Pullback.Iso
 public import Mathlib.CategoryTheory.Limits.Shapes.Pullback.Mono
 public import Mathlib.CategoryTheory.Limits.Shapes.Pullback.Pasting

Mathlib/CategoryTheory/Abelian/CommSq.lean

@@ -6,6 +6,7 @@ Authors: Joël Riou
 module
 
 public import Mathlib.CategoryTheory.Abelian.Refinements
+public import Mathlib.CategoryTheory.MorphismProperty.Limits
 public import Mathlib.Algebra.Homology.CommSq
 
 /-!
@@ -14,13 +15,16 @@ public import Mathlib.Algebra.Homology.CommSq
 Consider a pushout square in an abelian category:
 
 ```
-X₁ ⟶ X₂
-|    |
-v    v
-X₃ ⟶ X₄
+    t
+ X₁ ⟶ X₂
+l|    |r
+ v    v
+ X₃ ⟶ X₄
+    b
 ```
 
 We study the associated exact sequence `X₁ ⟶ X₂ ⊞ X₃ ⟶ X₄ ⟶ 0`.
+We also show that the induced morphism `kernel t ⟶ kernel b` is an epimorphism.
 
 -/
 
@@ -32,8 +36,19 @@ namespace CategoryTheory
 
 open Category Limits
 
-variable {C : Type u} [Category.{v} C] [Abelian C] {X₁ X₂ X₃ X₄ : C}
-  {t : X₁ ⟶ X₂} {l : X₁ ⟶ X₃} {r : X₂ ⟶ X₄} {b : X₃ ⟶ X₄}
+variable {C : Type u} [Category.{v} C] [Abelian C]
+
+namespace Abelian
+
+instance : (MorphismProperty.monomorphisms C).IsStableUnderCobaseChange :=
+  .mk' (fun _ _ _ _ _ _ (_ : Mono _) ↦ inferInstanceAs (Mono _))
+
+instance : (MorphismProperty.epimorphisms C).IsStableUnderBaseChange :=
+  .mk' (fun _ _ _ _ _ _ (_ : Epi _) ↦ inferInstanceAs (Epi _))
+
+end Abelian
+
+variable {X₁ X₂ X₃ X₄ : C} {t : X₁ ⟶ X₂} {l : X₁ ⟶ X₃} {r : X₂ ⟶ X₄} {b : X₃ ⟶ X₄}
 
 namespace IsPushout
 
@@ -113,5 +128,36 @@ statement to `IsPushout.hom_eq_add_up_to_refinements`.
 
 end IsPullback
 
+namespace Abelian
+
+variable {X₁ X₂ X₃ X₄ : C} {t : X₁ ⟶ X₂} {l : X₁ ⟶ X₃} {r : X₂ ⟶ X₄} {b : X₃ ⟶ X₄}
+
+lemma mono_cokernel_map_of_isPullback (sq : IsPullback t l r b) :
+    Mono (cokernel.map _ _ _ _ sq.w) := by
+  rw [Preadditive.mono_iff_cancel_zero]
+  intro A₀ z hz
+  obtain ⟨A₁, π₁, _, x₂, hx₂⟩ :=
+    surjective_up_to_refinements_of_epi (cokernel.π t) z
+  have : (ShortComplex.mk _ _ (cokernel.condition b)).Exact :=
+    ShortComplex.exact_of_g_is_cokernel _ (cokernelIsCokernel b)
+  obtain ⟨A₂, π₂, _, x₃, hx₃⟩ := this.exact_up_to_refinements (x₂ ≫ r) (by
+    simpa [hz] using hx₂.symm =≫ cokernel.map _ _ _ _ sq.w)
+  obtain ⟨x₁, hx₁, rfl⟩ := sq.exists_lift (π₂ ≫ x₂) x₃ (by simpa)
+  simp [← cancel_epi π₁, ← cancel_epi π₂, hx₂, ← reassoc_of% hx₁]
+
+lemma epi_kernel_map_of_isPushout (sq : IsPushout t l r b) :
+    Epi (kernel.map _ _ _ _ sq.w) := by
+  rw [epi_iff_surjective_up_to_refinements]
+  intro A₀ z
+  obtain ⟨A₁, π₁, _, x₁, hx₁⟩ := ((ShortComplex.mk _ _
+    sq.cokernelCofork.condition).exact_of_g_is_cokernel
+      sq.isColimitCokernelCofork).exact_up_to_refinements
+        (z ≫ kernel.ι _ ≫ biprod.inr) (by simp)
+  refine ⟨A₁, π₁, inferInstance, -kernel.lift _ x₁ ?_, ?_⟩
+  · simpa using hx₁.symm =≫ biprod.fst
+  · ext
+    simpa using hx₁ =≫ biprod.snd
+
+end Abelian
 
 end CategoryTheory

Mathlib/CategoryTheory/Galois/Examples.lean

@@ -107,7 +107,7 @@ instance : GaloisCategory (Action FintypeCat G) where
 
 /-- The `G`-action on a connected finite `G`-set is transitive. -/
 theorem Action.pretransitive_of_isConnected (X : Action FintypeCat G)
-    [IsConnected X] : MulAction.IsPretransitive G X.V where
+    [PreGaloisCategory.IsConnected X] : MulAction.IsPretransitive G X.V where
   exists_smul_eq x y := by
     /- We show that the `G`-orbit of `x` is a non-initial subobject of `X` and hence by
     connectedness, the orbit equals `X.V`. -/
@@ -131,7 +131,7 @@ theorem Action.pretransitive_of_isConnected (X : Action FintypeCat G)
 /-- A nonempty `G`-set with transitive `G`-action is connected. -/
 theorem Action.isConnected_of_transitive (X : FintypeCat) [MulAction G X]
     [MulAction.IsPretransitive G X] [h : Nonempty X] :
-    IsConnected (Action.FintypeCat.ofMulAction G X) where
+    PreGaloisCategory.IsConnected (Action.FintypeCat.ofMulAction G X) where
   notInitial := not_initial_of_inhabited (Action.forget _ _) h.some
   noTrivialComponent Y i hm hni := by
     /- We show that the induced inclusion `i.hom` of finite sets is surjective, using the
@@ -151,15 +151,15 @@ theorem Action.isConnected_of_transitive (X : FintypeCat) [MulAction G X]
 
 /-- A nonempty finite `G`-set is connected if and only if the `G`-action is transitive. -/
 theorem Action.isConnected_iff_transitive (X : Action FintypeCat G) [Nonempty X.V] :
-    IsConnected X ↔ MulAction.IsPretransitive G X.V :=
+    PreGaloisCategory.IsConnected X ↔ MulAction.IsPretransitive G X.V :=
   ⟨fun _ ↦ pretransitive_of_isConnected G X, fun _ ↦ isConnected_of_transitive G X.V⟩
 
 variable {G}
 
 /-- If `X` is a connected `G`-set and `x` is an element of `X`, `X` is isomorphic
 to the quotient of `G` by the stabilizer of `x` as `G`-sets. -/
 noncomputable def isoQuotientStabilizerOfIsConnected (X : Action FintypeCat G)
-    [IsConnected X] (x : X.V) [Fintype (G ⧸ (MulAction.stabilizer G x))] :
+    [PreGaloisCategory.IsConnected X] (x : X.V) [Fintype (G ⧸ (MulAction.stabilizer G x))] :
     X ≅ G ⧸ₐ MulAction.stabilizer G x :=
   haveI : MulAction.IsPretransitive G X.V := Action.pretransitive_of_isConnected G X
   let e : X.V ≃ G ⧸ MulAction.stabilizer G x :=

Mathlib/CategoryTheory/Limits/Shapes/Kernels.lean

@@ -314,6 +314,12 @@ lemma kernel.map_id {X Y : C} (f : X ⟶ Y) [HasKernel f] (q : Y ⟶ Y)
     (w : f ≫ q = 𝟙 _ ≫ f) : kernel.map f f (𝟙 _) q w = 𝟙 _ := by
   cat_disch
 
+instance {X' Y' : C} (f' : X' ⟶ Y') [HasKernel f'] (p : X ⟶ X') (q : Y ⟶ Y')
+    (w : f ≫ q = p ≫ f') [IsIso p] [Mono q] :
+    IsIso (kernel.map _ _ _ _ w) :=
+  ⟨kernel.lift _ (kernel.ι f' ≫ inv p) (by simp [← cancel_mono q, w]),
+    by cat_disch, by cat_disch⟩
+
 /-- Given a commutative diagram
 ```
     X --f--> Y --g--> Z
@@ -802,6 +808,12 @@ abbrev cokernel.map {X' Y' : C} (f' : X' ⟶ Y') [HasCokernel f'] (p : X ⟶ X')
       apply congrArg (· ≫ π f') w
     simp [this])
 
+instance {X' Y' : C} (f' : X' ⟶ Y') [HasCokernel f'] (p : X ⟶ X') (q : Y ⟶ Y')
+    (w : f ≫ q = p ≫ f') [Epi p] [IsIso q] :
+    IsIso (cokernel.map _ _ _ _ w) :=
+  ⟨cokernel.desc _ (inv q ≫ cokernel.π f) (by simp [← cancel_epi p, ← reassoc_of% w]),
+    by cat_disch, by cat_disch⟩
+
 @[simp]
 lemma cokernel.map_id {X Y : C} (f : X ⟶ Y) [HasCokernel f] (q : X ⟶ X)
     (w : f ≫ 𝟙 _ = q ≫ f) : cokernel.map f f q (𝟙 _) w = 𝟙 _ := by

Mathlib/CategoryTheory/Limits/Shapes/Pullback/IsPullback/Kernels.lean

@@ -0,0 +1,54 @@
+/-
+Copyright (c) 2026 Joël Riou. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Joël Riou
+-/
+module
+
+public import Mathlib.CategoryTheory.Limits.Shapes.Kernels
+public import Mathlib.CategoryTheory.Limits.Shapes.Pullback.IsPullback.Basic
+
+/-!
+# Horizontal maps in a pullback square have the same kernel
+
+Consider a commutative square:
+```
+    t
+ X₁ --> X₂
+l|      |r
+ v      v
+ X₃ --> X₄
+    b
+```
+* If this is a pullback square, then the induced map `kernel t ⟶ kernel b`
+is an isomorphism.
+* If this is a pushout square, then the induced map `cokernel t ⟶ cokernel b`
+is an isomorphism.
+
+(Similar results for the (co)kernels of the vertical maps can be obtained
+by applying these results to the flipped square.)
+
+-/
+
+@[expose] public section
+
+universe v v' u u'
+
+namespace CategoryTheory.Limits
+
+variable {C : Type*} [Category* C] [HasZeroMorphisms C]
+  {X₁ X₂ X₃ X₄ : C} {t : X₁ ⟶ X₂} {l : X₁ ⟶ X₃} {r : X₂ ⟶ X₄} {b : X₃ ⟶ X₄}
+
+lemma isIso_kernel_map_of_isPullback [HasKernel t] [HasKernel b]
+    (sq : IsPullback t l r b) :
+    IsIso (kernel.map _ _ _ _ sq.w) :=
+  ⟨kernel.lift _ (sq.lift 0 (kernel.ι b) (by simp)) (by simp),
+    by ext; exact sq.hom_ext (by cat_disch) (by cat_disch), by cat_disch⟩
+
+lemma isIso_cokernel_map_of_isPushout [HasCokernel t] [HasCokernel b]
+    (sq : IsPushout t l r b) :
+    IsIso (cokernel.map _ _ _ _ sq.w) :=
+  ⟨cokernel.desc _ (sq.desc (cokernel.π t) 0 (by simp)) (by simp),
+    by cat_disch, by ext; exact sq.hom_ext (by cat_disch) (by cat_disch)⟩
+
+end CategoryTheory.Limits