feat(CategoryTheory): covariant functoriality of graded objects on th…

…e index set (#7425)

Mathlib/CategoryTheory/GradedObject.lean

@@ -1,7 +1,7 @@
 /-
 Copyright (c) 2020 Scott Morrison. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
-Authors: Scott Morrison
+Authors: Scott Morrison, Joël Riou
 -/
 import Mathlib.Algebra.GroupPower.Lemmas
 import Mathlib.CategoryTheory.Pi.Basic
@@ -25,6 +25,11 @@ functor on `β`-graded objects
 
 When `C` has coproducts we construct the `total` functor `GradedObject β C ⥤ C`,
 show that it is faithful, and deduce that when `C` is concrete so is `GradedObject β C`.
+
+A covariant functoriality of `GradedObject β C` with respect to the index set `β` is also
+introduced: if `p : I → J` is a map such that `C` has coproducts indexed by `p ⁻¹' {j}`, we
+have a functor `map : GradedObject I C ⥤ GradedObject J C`.
+
 -/
 
 set_option autoImplicit true
@@ -80,6 +85,40 @@ def eval {β : Type w} (b : β) : GradedObject β C ⥤ C where
 
 section
 
+variable {β : Type*} (X Y : GradedObject β C)
+
+/-- Constructor for isomorphisms in `GradedObject` -/
+@[simps]
+def isoMk (e : ∀ i, X i ≅ Y i) : X ≅ Y where
+  hom i := (e i).hom
+  inv i := (e i).inv
+
+variable {X Y}
+
+-- this lemma is not an instance as it may create a loop with `isIso_apply_of_isIso`
+lemma isIso_of_isIso_apply (f : X ⟶ Y) [hf : ∀ i, IsIso (f i)] :
+    IsIso f := by
+  change IsIso (isoMk X Y (fun i => asIso (f i))).hom
+  infer_instance
+
+@[reassoc (attr := simp)]
+lemma iso_hom_inv_id_apply (e : X ≅ Y) (i : β) :
+    e.hom i ≫ e.inv i = 𝟙 _ :=
+  congr_fun e.hom_inv_id i
+
+@[reassoc (attr := simp)]
+lemma iso_inv_hom_id_apply (e : X ≅ Y) (i : β) :
+    e.inv i ≫ e.hom i = 𝟙 _ :=
+  congr_fun e.inv_hom_id i
+
+instance isIso_apply_of_isIso (f : X ⟶ Y) [IsIso f] (i : β) : IsIso (f i) := by
+  change IsIso ((eval i).map f)
+  infer_instance
+
+end
+
+section
+
 variable (C)
 
 -- porting note: added to ease the port
@@ -238,4 +277,142 @@ end
 
 end GradedObject
 
+namespace GradedObject
+
+variable {I J : Type*} {C : Type*} [Category C]
+  (X Y Z : GradedObject I C) (φ : X ⟶ Y) (e : X ≅ Y) (ψ : Y ⟶ Z) (p : I → J)
+
+/-- If `X : GradedObject I C` and `p : I → J`, `X.mapObjFun p j` is the family of objects `X i`
+for `i : I` such that `p i = j`. -/
+abbrev mapObjFun (j : J) (i : p ⁻¹' {j}) : C := X i
+
+variable (j : J)
+
+/-- Given `X : GradedObject I C` and `p : I → J`, `X.HasMap p` is the condition that
+for all `j : J`, the coproduct of all `X i` such `p i = j` exists. -/
+abbrev HasMap : Prop := ∀ (j : J), HasCoproduct (X.mapObjFun p j)
+
+variable [X.HasMap p] [Y.HasMap p] [Z.HasMap p]
+
+/-- Given `X : GradedObject I C` and `p : I → J`, `X.mapObj p` is the graded object by `J`
+which in degree `j` consists of the coproduct of the `X i` such that `p i = j`. -/
+noncomputable def mapObj : GradedObject J C := fun j => ∐ (X.mapObjFun p j)
+
+/-- The canonical inclusion `X i ⟶ X.mapObj p j` when `i : I` and `j : J` are such
+that `p i = j`. -/
+noncomputable def ιMapObj (i : I) (j : J) (hij : p i = j) : X i ⟶ X.mapObj p j :=
+  Sigma.ι (X.mapObjFun p j) ⟨i, hij⟩
+
+/-- Given `X : GradedObject I C`, `p : I → J` and `j : J`,
+`CofanMapObjFun X p j` is the type `Cofan (X.mapObjFun p j)`. The point object of
+such colimits cofans are isomorphic to `X.mapObj p j`, see `CofanMapObjFun.iso`. -/
+abbrev CofanMapObjFun (j : J) : Type _ := Cofan (X.mapObjFun p j)
+
+-- in order to use the cofan API, some definitions below
+-- have a `simp` attribute rather than `simps`
+/-- Constructor for `CofanMapObjFun X p j`. -/
+@[simp]
+def CofanMapObjFun.mk (j : J) (pt : C) (ι' : ∀ (i : I) (_ : p i = j), X i ⟶ pt) :
+    CofanMapObjFun X p j :=
+  Cofan.mk pt (fun ⟨i, hi⟩ => ι' i hi)
+
+/-- The tautological cofan corresponding to the coproduct decomposition of `X.mapObj p j`. -/
+@[simp]
+noncomputable def cofanMapObj (j : J) : CofanMapObjFun X p j :=
+  CofanMapObjFun.mk X p j (X.mapObj p j) (fun i hi => X.ιMapObj p i j hi)
+
+/-- Given `X : GradedObject I C`, `p : I → J` and `j : J`, `X.mapObj p j` satisfies
+the universal property of the coproduct of those `X i` such that `p i = j`. -/
+noncomputable def isColimitCofanMapObj (j : J) : IsColimit (X.cofanMapObj p j) :=
+  colimit.isColimit _
+
+@[ext]
+lemma mapObj_ext {A : C} {j : J} (f g : X.mapObj p j ⟶ A)
+    (hfg : ∀ (i : I) (hij : p i = j), X.ιMapObj p i j hij ≫ f = X.ιMapObj p i j hij ≫ g) :
+    f = g :=
+  Cofan.IsColimit.hom_ext (X.isColimitCofanMapObj p j) _ _ (fun ⟨i, hij⟩ => hfg i hij)
+
+/-- This is the morphism `X.mapObj p j ⟶ A` constructed from a family of
+morphisms `X i ⟶ A` for all `i : I` such that `p i = j`. -/
+noncomputable def descMapObj {A : C} {j : J} (φ : ∀ (i : I) (_ : p i = j), X i ⟶ A) :
+    X.mapObj p j ⟶ A :=
+  Cofan.IsColimit.desc (X.isColimitCofanMapObj p j) (fun ⟨i, hi⟩ => φ i hi)
+
+@[reassoc (attr := simp)]
+lemma ι_descMapObj {A : C} {j : J}
+    (φ : ∀ (i : I) (_ : p i = j), X i ⟶ A) (i : I) (hi : p i = j) :
+    X.ιMapObj p i j hi ≫ X.descMapObj p φ = φ i hi := by
+  apply Cofan.IsColimit.fac
+
+namespace CofanMapObjFun
+
+lemma hasMap (c : ∀ j, CofanMapObjFun X p j) (hc : ∀ j, IsColimit (c j)) :
+    X.HasMap p := fun j => ⟨_, hc j⟩
+
+variable {j X p}
+  {c : CofanMapObjFun X p j} (hc : IsColimit c) [X.HasMap p]
+
+/-- If `c : CofanMapObjFun X p j` is a colimit cofan, this is the induced
+isomorphism `c.pt ≅ X.mapObj p j`. -/
+noncomputable def iso : c.pt ≅ X.mapObj p j :=
+  IsColimit.coconePointUniqueUpToIso hc (X.isColimitCofanMapObj p j)
+
+@[reassoc (attr := simp)]
+lemma inj_iso_hom (i : I) (hi : p i = j) :
+    c.inj ⟨i, hi⟩ ≫ (c.iso hc).hom = X.ιMapObj p i j hi := by
+  apply IsColimit.comp_coconePointUniqueUpToIso_hom
+
+@[reassoc (attr := simp)]
+lemma ιMapObj_iso_inv (i : I) (hi : p i = j) :
+    X.ιMapObj p i j hi ≫ (c.iso hc).inv = c.inj ⟨i, hi⟩ := by
+  apply IsColimit.comp_coconePointUniqueUpToIso_inv
+
+end CofanMapObjFun
+
+variable {X Y}
+
+/-- The canonical morphism of `J`-graded objects `X.mapObj p ⟶ Y.mapObj p` induced by
+a morphism `X ⟶ Y` of `I`-graded objects and a map `p : I → J`. -/
+noncomputable def mapMap : X.mapObj p ⟶ Y.mapObj p := fun j =>
+  X.descMapObj p (fun i hi => φ i ≫ Y.ιMapObj p i j hi)
+
+@[reassoc (attr := simp)]
+lemma ι_mapMap (i : I) (j : J) (hij : p i = j) :
+    X.ιMapObj p i j hij ≫ mapMap φ p j = φ i ≫ Y.ιMapObj p i j hij := by
+  simp only [mapMap, ι_descMapObj]
+
+lemma congr_mapMap (φ₁ φ₂ : X ⟶ Y) (h : φ₁ = φ₂) : mapMap φ₁ p = mapMap φ₂ p := by
+  subst h
+  rfl
+
+variable (X)
+
+@[simp]
+lemma mapMap_id : mapMap (𝟙 X) p = 𝟙 _ := by aesop_cat
+
+variable {X Z}
+
+@[simp, reassoc]
+lemma mapMap_comp : mapMap (φ ≫ ψ) p = mapMap φ p ≫ mapMap ψ p := by aesop_cat
+
+/-- The isomorphism of `J`-graded objects `X.mapObj p ≅ Y.mapObj p` induced by an
+isomorphism `X ≅ Y` of graded objects and a map `p : I → J`. -/
+@[simps]
+noncomputable def mapIso : X.mapObj p ≅ Y.mapObj p where
+  hom := mapMap e.hom p
+  inv := mapMap e.inv p
+
+variable (C)
+
+/-- Given a map `p : I → J`, this is the functor `GradedObject I C ⥤ GradedObject J C` which
+sends an `I`-object `X` to the graded object `X.mapObj p` which in degree `j : J` is given
+by the coproduct of those `X i` such that `p i = j`. -/
+@[simps]
+noncomputable def map [∀ (j : J), HasColimitsOfShape (Discrete (p ⁻¹' {j})) C] :
+    GradedObject I C ⥤ GradedObject J C where
+  obj X := X.mapObj p
+  map φ := mapMap φ p
+
+end GradedObject
+
 end CategoryTheory

Mathlib/CategoryTheory/Limits/Shapes/Products.lean

@@ -117,6 +117,21 @@ def mkFanLimit {f : β → C} (t : Fan f) (lift : ∀ s : Fan f, s.pt ⟶ t.pt)
   { lift }
 #align category_theory.limits.mk_fan_limit CategoryTheory.Limits.mkFanLimit
 
+/-- Constructor for morphisms to the point of a limit fan. -/
+def Fan.IsLimit.desc {F : β → C} {c : Fan F} (hc : IsLimit c) {A : C}
+    (f : ∀ i, A ⟶ F i) : A ⟶ c.pt :=
+  hc.lift (Fan.mk A f)
+
+@[reassoc (attr := simp)]
+lemma Fan.IsLimit.fac {F : β → C} {c : Fan F} (hc : IsLimit c) {A : C}
+    (f : ∀ i, A ⟶ F i) (i : β) :
+    Fan.IsLimit.desc hc f ≫ c.proj i = f i :=
+  hc.fac (Fan.mk A f) ⟨i⟩
+
+lemma Fan.IsLimit.hom_ext {F : I → C} {c : Fan F} (hc : IsLimit c) {A : C}
+    (f g : A ⟶ c.pt) (h : ∀ i, f ≫ c.proj i = g ≫ c.proj i) : f = g :=
+  hc.hom_ext (fun ⟨i⟩ => h i)
+
 /-- Make a cofan `f` into a colimit cofan by providing `desc`, `fac`, and `uniq` --
   just a convenience lemma to avoid having to go through `Discrete` -/
 @[simps]
@@ -127,6 +142,21 @@ def mkCofanColimit {f : β → C} (s : Cofan f) (desc : ∀ t : Cofan f, s.pt 
     IsColimit s :=
   { desc }
 
+/-- Constructor for morphisms from the point of a colimit cofan. -/
+def Cofan.IsColimit.desc {F : β → C} {c : Cofan F} (hc : IsColimit c) {A : C}
+    (f : ∀ i, F i ⟶ A) : c.pt ⟶ A :=
+  hc.desc (Cofan.mk A f)
+
+@[reassoc (attr := simp)]
+lemma Cofan.IsColimit.fac {F : β → C} {c : Cofan F} (hc : IsColimit c) {A : C}
+    (f : ∀ i, F i ⟶ A) (i : β) :
+    c.inj i ≫ Cofan.IsColimit.desc hc f = f i :=
+  hc.fac (Cofan.mk A f) ⟨i⟩
+
+lemma Cofan.IsColimit.hom_ext {F : I → C} {c : Cofan F} (hc : IsColimit c) {A : C}
+    (f g : c.pt ⟶ A) (h : ∀ i, c.inj i ≫ f = c.inj i ≫ g) : f = g :=
+  hc.hom_ext (fun ⟨i⟩ => h i)
+
 section
 
 variable (C)