[Merged by Bors] - feat(CategoryTheory/Limits): sigmaConst preserves colimits

Mathlib.lean

@@ -2814,6 +2814,7 @@ public import Mathlib.CategoryTheory.Limits.Preserves.Shapes.Pullbacks
 public import Mathlib.CategoryTheory.Limits.Preserves.Shapes.Square
 public import Mathlib.CategoryTheory.Limits.Preserves.Shapes.Terminal
 public import Mathlib.CategoryTheory.Limits.Preserves.Shapes.Zero
+public import Mathlib.CategoryTheory.Limits.Preserves.SigmaConst
 public import Mathlib.CategoryTheory.Limits.Preserves.Ulift
 public import Mathlib.CategoryTheory.Limits.Preserves.Yoneda
 public import Mathlib.CategoryTheory.Limits.Presheaf

Mathlib/Algebra/Category/ModuleCat/Sheaf/Free.lean

@@ -7,6 +7,7 @@ module
 
 public import Mathlib.Algebra.Category.ModuleCat.Presheaf.Colimits
 public import Mathlib.Algebra.Category.ModuleCat.Sheaf.Colimits
+public import Mathlib.CategoryTheory.Limits.Preserves.SigmaConst
 
 /-!
 # Free sheaves of modules
@@ -42,7 +43,6 @@ noncomputable def free (I : Type u) : SheafOfModules.{u} R := ∐ (fun (_ : I) 
 noncomputable def ιFree {I : Type u} (i : I) : unit R ⟶ free I :=
   Sigma.ι (fun (_ : I) ↦ unit R) i
 
-
 /-- The tautological cofan with point `free I : SheafOfModules R`. -/
 noncomputable def freeCofan (I : Type u) : Cofan (fun (_ : I) ↦ unit R) :=
   Cofan.mk (P := free I) ιFree
@@ -127,52 +127,21 @@ end
 /-- The functor `Type u ⥤ SheafOfModules.{u} R` which sends a type `I` to
 `free I` which is a coproduct indexed by `I` of copies of `R` (thought of as a
 presheaf of modules over itself). -/
-@[simps]
-noncomputable def freeFunctor : Type u ⥤ SheafOfModules.{u} R where
-  obj X := free X
-  map f := freeMap f
-  map_id X := (freeHomEquiv _).injective (by ext1 i; simp)
-  map_comp {I J K} f g := (freeHomEquiv _).injective (by ext1; simp [freeHomEquiv_comp_apply])
+noncomputable def freeFunctor : Type u ⥤ SheafOfModules.{u} R :=
+  sigmaConst.obj (unit R)
 
-set_option backward.isDefEq.respectTransparency false in
-/- If `C` was in `Type u`, we could show that `freeFunctor` is a left adjoint, and
-deduce that `freeFunctor` preserves all colimits. Instead, we use
-the natural bijection `freeHomEquiv`, which is as close as an adjunction we can get. -/
-instance : PreservesColimitsOfSize.{v₂, u₂} (freeFunctor (R := R)) where
-  preservesColimitsOfShape {J} _ := ⟨fun {K} ↦ ⟨fun {c} hc ↦ ⟨by
-    replace hc := (Types.isColimit_iff_coconeTypesIsColimit c).1 ⟨hc⟩
-    let coconeTypes (s : Cocone (K ⋙ freeFunctor (R := R))) :
-        K.CoconeTypes :=
-      { pt := s.pt.sections
-        ι j := freeHomEquiv _ (s.ι.app j)
-        ι_naturality {j j'} f := by
-          funext x
-          dsimp
-          rw [← s.w f]
-          dsimp
-          rw [freeHomEquiv_comp_apply, freeHomEquiv_freeMap,
-            Function.comp_apply, freeHomEquiv_apply] }
-    exact {
-      desc s := (freeHomEquiv _).symm (hc.desc (coconeTypes s))
-      fac s j := (freeHomEquiv _).injective (by
-        funext x
-        dsimp
-        rw [freeHomEquiv_comp_apply, freeHomEquiv_freeMap, Function.comp_apply,
-          sectionsMap_freeHomEquiv_symm_freeSection, dsimp% hc.fac_apply (coconeTypes s) j x])
-      uniq s m hm := (freeHomEquiv _).injective (by
-        funext x
-        obtain ⟨j, x, rfl⟩ := Functor.CoconeTypes.IsColimit.ι_jointly_surjective hc x
-        replace hm := congr_fun ((freeHomEquiv _).congr_arg (hm j)) x
-        dsimp at hm
-        rw [freeHomEquiv_comp_apply, freeHomEquiv_freeMap,
-          Function.comp_apply] at hm
-        rw [freeHomEquiv_apply, freeHomEquiv_apply,
-          sectionsMap_freeHomEquiv_symm_freeSection,
-          Functor.coconeTypesEquiv_symm_apply_ι,
-          dsimp% [-Functor.const_obj_obj] hc.fac_apply (coconeTypes s) j x]
-        dsimp
-        rw [hm]) }⟩⟩⟩
+@[simp]
+lemma freeFunctor_obj (X : Type u) :
+    (freeFunctor (R := R)).obj X = free X := rfl
+
+@[simp]
+lemma freeFunctor_map {X Y : Type u} (f : X ⟶ Y) :
+    dsimp% (freeFunctor (R := R)).map f = freeMap f :=
+  Cofan.IsColimit.hom_ext (isColimitFreeCofan _) _ _
+    (fun i ↦ (Sigma.ι_desc _ _).trans (ιFree_freeMap f i).symm)
 
+instance : PreservesColimitsOfSize.{v₂, u₂} (freeFunctor (R := R)) :=
+  inferInstanceAs (PreservesColimitsOfSize.{v₂, u₂} (sigmaConst.obj _))
 
 section
 
@@ -188,14 +157,16 @@ noncomputable def freeSumIso : free I ⨿ free J ≅ free (R := R) (I ⊕ J) :=
 
 @[reassoc (attr := simp)]
 lemma inl_freeSumIso_hom :
-    coprod.inl ≫ (freeSumIso (R := R) I J).hom = freeMap Sum.inl :=
-  IsColimit.comp_coconePointUniqueUpToIso_hom
+    coprod.inl ≫ (freeSumIso (R := R) I J).hom = freeMap Sum.inl := by
+  rw [← dsimp% freeFunctor_map (TypeCat.ofHom (Sum.inl : I → I ⊕ J))]
+  exact IsColimit.comp_coconePointUniqueUpToIso_hom
     (coprodIsCoprod (free (R := R) I) (free J)) _ (.mk .left)
 
 @[reassoc (attr := simp)]
 lemma inr_freeSumIso_hom :
-    coprod.inr ≫ (freeSumIso (R := R) I J).hom = freeMap Sum.inr :=
-  IsColimit.comp_coconePointUniqueUpToIso_hom
+    coprod.inr ≫ (freeSumIso (R := R) I J).hom = freeMap Sum.inr := by
+  rw [← dsimp% freeFunctor_map (TypeCat.ofHom (Sum.inr : J → I ⊕ J))]
+  exact IsColimit.comp_coconePointUniqueUpToIso_hom
     (coprodIsCoprod (free (R := R) I) (free J)) _ (.mk .right)
 
 end

Mathlib/CategoryTheory/Limits/Preserves/SigmaConst.lean

@@ -0,0 +1,122 @@
+/-
+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.Preserves.Basic
+public import Mathlib.CategoryTheory.Limits.Shapes.ZeroMorphisms
+public import Mathlib.CategoryTheory.Limits.Shapes.Kernels
+public import Mathlib.CategoryTheory.Limits.Types.Coproducts
+
+/-!
+# `sigmaConst.obj` preserves colimits
+
+Given an object `R` in a category `C` with coproducts of size `w`,
+the functor `sigmaConst.obj R : Type w ⥤ C` which sends
+a type `T` to the coproduct of copies of `R` indexed by `T`
+preserves all colimits.
+
+-/
+
+@[expose] public section
+
+universe w v' v u' u
+
+namespace CategoryTheory.Limits
+
+variable {C : Type u} [Category.{v} C]
+
+set_option backward.isDefEq.respectTransparency false in
+/- If the morphisms in `C` were in `Type w`, the functor
+`sigmaConst.{w}`
+would be a left adjoint (see `sigmaConstAdj`). In general, we cannot
+expect this functor to be a left adjoint, but the commutation
+with colimits always holds. -/
+instance [HasCoproducts.{w} C] (R : C) :
+    PreservesColimitsOfSize.{v', u'} (sigmaConst.{w}.obj R) where
+  preservesColimitsOfShape {J _} := ⟨fun {K} ↦ ⟨fun {c} hc ↦ ⟨by
+    replace hc := (Types.isColimit_iff_coconeTypesIsColimit ..).1 ⟨hc⟩
+    let coconeTypes (s : Cocone (K ⋙ sigmaConst.obj R)) : K.CoconeTypes :=
+      { pt := R ⟶ s.pt
+        ι j k := Sigma.ι (fun _ ↦ R) k ≫ s.ι.app j
+        ι_naturality g := by ext; simp [← s.w g] }
+    exact {
+      desc s := Sigma.desc (hc.desc (coconeTypes s))
+      fac s j := by
+        dsimp
+        ext k
+        simp [dsimp% hc.fac_apply, dsimp% Sigma.ι_desc (hc.desc (coconeTypes s)), coconeTypes]
+      uniq s m hm := by
+        dsimp
+        ext x
+        obtain ⟨j, k, rfl⟩ := Functor.CoconeTypes.IsColimit.ι_jointly_surjective hc x
+        simp [coconeTypes, ← hm, dsimp% hc.fac_apply,
+          dsimp% Sigma.ι_desc (hc.desc (coconeTypes s))] }⟩⟩⟩
+
+variable [HasZeroMorphisms C] (R : C)
+
+section
+
+variable {α β : Type*} (f : α → β)
+  [HasCoproduct (fun (_ : α) ↦ R)] [HasCoproduct (fun (_ : β) ↦ R)]
+  [HasCoproduct (fun (_ : ((Set.range f)ᶜ : Set _)) ↦ R)]
+
+open Classical in
+/-- A colimit cokernel cofork for the map
+`∐ fun (_ : α) ↦ R ⟶ ∐ fun (_ : β) ↦ R` induced by a map `f : α → β`. -/
+@[simps! pt]
+noncomputable def sigmaConstCokernelCofork :
+    CokernelCofork
+      (Sigma.map' (f := fun (_ : α) ↦ R) (g := fun (_ : β) ↦ R) f (fun _ ↦ 𝟙 R)) :=
+  CokernelCofork.ofπ (Z := ∐ fun (_ : ((Set.range f)ᶜ : Set _)) ↦ R)
+    (Sigma.desc (fun b ↦
+      if hb : b ∈ (Set.range f)ᶜ then Sigma.ι (fun _ ↦ R) ⟨b, hb⟩ else 0))
+    (by ext; simp [Sigma.ι_desc])
+
+@[reassoc]
+lemma ι_sigmaConstCokernelCofork_π (b : β) (hb : b ∉ Set.range f) :
+    dsimp% Sigma.ι (fun _ ↦ R) b ≫ (sigmaConstCokernelCofork R f).π =
+      Sigma.ι (fun _ ↦ R) ⟨b, hb⟩ := by
+  dsimp [sigmaConstCokernelCofork]
+  rw [Sigma.ι_desc]
+  apply dif_pos
+
+@[reassoc (attr := simp)]
+lemma ι_sigmaConstCokernelCofork_π_eq_zero (a : α) :
+    dsimp% Sigma.ι (fun _ ↦ R) (f a) ≫ (sigmaConstCokernelCofork R f).π = 0 := by
+  dsimp [sigmaConstCokernelCofork]
+  rw [Sigma.ι_desc]
+  exact dif_neg (by simp)
+
+set_option backward.isDefEq.respectTransparency false in
+/-- The cokernel of the map `∐ fun (_ : α) ↦ R ⟶ ∐ fun (_ : β) ↦ R` induced
+by a map `f : α → β` identifies to the coproduct of copies of `R`
+indexed by the complement of the range of `f`. -/
+noncomputable def isColimitSigmaConstCokernelCofork :
+    IsColimit (sigmaConstCokernelCofork R f) :=
+  Cofork.IsColimit.mk _
+    (fun s ↦ Sigma.desc (fun ⟨b, _⟩ ↦ Sigma.ι (fun _ ↦ R) b ≫ s.π))
+    (fun s ↦ by
+      ext b
+      by_cases hb : b ∈ Set.range f
+      · obtain ⟨a, rfl⟩ := hb
+        simpa [-CokernelCofork.condition] using Sigma.ι (fun _ ↦ R) a ≫= s.condition.symm
+      · simp [ι_sigmaConstCokernelCofork_π_assoc _ _ _ hb])
+    (fun s m hm ↦ by
+      dsimp
+      ext ⟨b, hb⟩
+      rw [Sigma.ι_desc, ← hm, ι_sigmaConstCokernelCofork_π_assoc])
+
+instance :
+    HasCokernel (Sigma.map' (f := fun (_ : α) ↦ R) (g := fun (_ : β) ↦ R) f (fun _ ↦ 𝟙 R)) :=
+  ⟨_, isColimitSigmaConstCokernelCofork R f⟩
+
+end
+
+instance [HasCoproducts.{w} C] {α β : Type w} (f : α ⟶ β) :
+    HasCokernel ((sigmaConst.obj R).map f) := by
+  dsimp; infer_instance
+
+end CategoryTheory.Limits