feat(CategoryTheory): Guitart exact squares (#10270)

This PR defines the categorical notion of `2`-exact square in the sense of Guitart. It is introduced in order to prepare for future applications to derived functors.



Co-authored-by: Joël Riou <37772949+joelriou@users.noreply.github.com>

Mathlib.lean

@@ -1084,6 +1084,7 @@ import Mathlib.CategoryTheory.Groupoid.Basic
 import Mathlib.CategoryTheory.Groupoid.FreeGroupoid
 import Mathlib.CategoryTheory.Groupoid.Subgroupoid
 import Mathlib.CategoryTheory.Groupoid.VertexGroup
+import Mathlib.CategoryTheory.GuitartExact
 import Mathlib.CategoryTheory.Idempotents.Basic
 import Mathlib.CategoryTheory.Idempotents.Biproducts
 import Mathlib.CategoryTheory.Idempotents.FunctorCategories

Mathlib/CategoryTheory/GuitartExact.lean

@@ -0,0 +1,228 @@
+/-
+Copyright (c) 2024 Joël Riou. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Joël Riou
+-/
+import Mathlib.CategoryTheory.Limits.Final
+
+/-!
+# Guitart exact squares
+
+Given four functors `T`, `L`, `R` and `B`, a 2-square `TwoSquare T L R B` consists of
+a natural transformation `w : T ⋙ R ⟶ L ⋙ B`:
+```
+     T
+  C₁ ⥤ C₂
+L |     | R
+  v     v
+  C₃ ⥤ C₄
+     B
+```
+
+In this file, we define a typeclass `w.GuitartExact` which expresses
+that this square is exact in the sense of Guitart. This means that
+for any `X₃ : C₃`, the induced functor
+`CostructuredArrow L X₃ ⥤ CostructuredArrow R (B.obj X₃)` is final.
+It is also equivalent to the fact that for any `X₂ : C₂`, the
+induced functor `StructuredArrow X₂ T ⥤ StructuredArrow (R.obj X₂) B`
+is initial.
+
+Various categorical notions (fully faithful functors, adjunctions, etc.) can
+be characterized in terms of Guitart exact squares. Their particular role
+in pointwise Kan extensions shall also be used in the construction of
+derived functors.
+
+## TODO
+
+* Define the notion of derivability structure from
+[the paper by Kahn and Maltsiniotis][KahnMaltsiniotis2008] using Guitart exact squares
+and construct (pointwise) derived functors using this notion
+
+## References
+* https://ncatlab.org/nlab/show/exact+square
+* [René Guitart, *Relations et carrés exacts*][Guitart1980]
+* [Bruno Kahn and Georges Maltsiniotis, *Structures de dérivabilité*][KahnMaltsiniotis2008]
+
+-/
+
+universe v₁ v₂ v₃ v₄ u₁ u₂ u₃ u₄
+
+namespace CategoryTheory
+
+variable {C₁ : Type u₁} {C₂ : Type u₂} {C₃ : Type u₃} {C₄ : Type u₄}
+  [Category.{v₁} C₁] [Category.{v₂} C₂] [Category.{v₃} C₃] [Category.{v₄} C₄]
+  (T : C₁ ⥤ C₂) (L : C₁ ⥤ C₃) (R : C₂ ⥤ C₄) (B : C₃ ⥤ C₄)
+
+/-- A `2`-square consists of a natural transformation `T ⋙ R ⟶ L ⋙ B`
+involving fours functors `T`, `L`, `R`, `B` that are on the
+top/left/right/bottom sides of a square of categories. -/
+def TwoSquare := T ⋙ R ⟶ L ⋙ B
+
+namespace TwoSquare
+
+variable {T L R B}
+
+@[ext]
+lemma ext (w w' : TwoSquare T L R B) (h : ∀ (X : C₁), w.app X = w'.app X) :
+    w = w' :=
+  NatTrans.ext _ _ (funext h)
+
+variable (w : TwoSquare T L R B)
+
+/-- Given `w : TwoSquare T L R B` and `X₃ : C₃`, this is the obvious functor
+`CostructuredArrow L X₃ ⥤ CostructuredArrow R (B.obj X₃)`. -/
+@[simps! obj map]
+def costructuredArrowRightwards (X₃ : C₃) :
+    CostructuredArrow L X₃ ⥤ CostructuredArrow R (B.obj X₃) :=
+  CostructuredArrow.post L B X₃ ⋙ Comma.mapLeft _ w ⋙
+    CostructuredArrow.pre T R (B.obj X₃)
+
+/-- Given `w : TwoSquare T L R B` and `X₂ : C₂`, this is the obvious functor
+`StructuredArrow X₂ T ⥤ StructuredArrow (R.obj X₂) B`. -/
+@[simps! obj map]
+def structuredArrowDownwards (X₂ : C₂) :
+    StructuredArrow X₂ T ⥤ StructuredArrow (R.obj X₂) B :=
+  StructuredArrow.post X₂ T R ⋙ Comma.mapRight _ w ⋙
+    StructuredArrow.pre (R.obj X₂) L B
+
+section
+
+variable {X₂ : C₂} {X₃ : C₃} (g : R.obj X₂ ⟶ B.obj X₃)
+
+/- In [the paper by Kahn and Maltsiniotis, §4.3][KahnMaltsiniotis2008], given
+`w : TwoSquare T L R B` and `g : R.obj X₂ ⟶ B.obj X₃`, a category `J` is introduced
+and it is observed that it is equivalent to the two categories
+`w.StructuredArrowRightwards g` and `w.CostructuredArrowDownwards g`. We shall show below
+that there is an equivalence
+`w.equivalenceJ g : w.StructuredArrowRightwards g ≌ w.CostructuredArrowDownwards g`. -/
+
+/-- Given `w : TwoSquare T L R B` and a morphism `g : R.obj X₂ ⟶ B.obj X₃`, this is the
+category `StructuredArrow (CostructuredArrow.mk g) (w.costructuredArrowRightwards X₃)`,
+see the constructor `StructuredArrowRightwards.mk` for the data that is involved.-/
+abbrev StructuredArrowRightwards :=
+  StructuredArrow (CostructuredArrow.mk g) (w.costructuredArrowRightwards X₃)
+
+/-- Given `w : TwoSquare T L R B` and a morphism `g : R.obj X₂ ⟶ B.obj X₃`, this is the
+category `CostructuredArrow (w.structuredArrowDownwards X₂) (StructuredArrow.mk g)`,
+see the constructor `CostructuredArrowDownwards.mk` for the data that is involved. -/
+abbrev CostructuredArrowDownwards :=
+  CostructuredArrow (w.structuredArrowDownwards X₂) (StructuredArrow.mk g)
+
+section
+
+variable (X₁ : C₁) (a : X₂ ⟶ T.obj X₁) (b : L.obj X₁ ⟶ X₃)
+  (comm : R.map a ≫ w.app X₁ ≫ B.map b = g)
+
+/-- Constructor for objects in `w.StructuredArrowRightwards g`. -/
+abbrev StructuredArrowRightwards.mk : w.StructuredArrowRightwards g :=
+  StructuredArrow.mk (Y := CostructuredArrow.mk b) (CostructuredArrow.homMk a comm)
+
+/-- Constructor for objects in `w.CostructuredArrowDownwards g`. -/
+abbrev CoStructuredArrowDownwards.mk : w.CostructuredArrowDownwards g :=
+  CostructuredArrow.mk (Y := StructuredArrow.mk a)
+    (StructuredArrow.homMk b (by simpa using comm))
+
+end
+
+namespace EquivalenceJ
+
+/-- Given `w : TwoSquare T L R B` and a morphism `g : R.obj X₂ ⟶ B.obj X₃`, this is
+the obvious functor `w.StructuredArrowRightwards g ⥤ w.CostructuredArrowDownwards g`. -/
+@[simps]
+def functor : w.StructuredArrowRightwards g ⥤ w.CostructuredArrowDownwards g where
+  obj f := CostructuredArrow.mk (Y := StructuredArrow.mk f.hom.left)
+      (StructuredArrow.homMk f.right.hom (by simpa using CostructuredArrow.w f.hom))
+  map {f₁ f₂} φ :=
+    CostructuredArrow.homMk (StructuredArrow.homMk φ.right.left
+      (by dsimp; rw [← StructuredArrow.w φ]; rfl))
+      (by ext; exact CostructuredArrow.w φ.right)
+  map_id _ := rfl
+  map_comp _ _ := rfl
+
+/-- Given `w : TwoSquare T L R B` and a morphism `g : R.obj X₂ ⟶ B.obj X₃`, this is
+the obvious functor `w.CostructuredArrowDownwards g ⥤ w.StructuredArrowRightwards g`. -/
+@[simps]
+def inverse : w.CostructuredArrowDownwards g ⥤ w.StructuredArrowRightwards g where
+  obj f := StructuredArrow.mk (Y := CostructuredArrow.mk f.hom.right)
+      (CostructuredArrow.homMk f.left.hom (by simpa using StructuredArrow.w f.hom))
+  map {f₁ f₂} φ :=
+    StructuredArrow.homMk (CostructuredArrow.homMk φ.left.right
+      (by dsimp; rw [← CostructuredArrow.w φ]; rfl))
+      (by ext; exact StructuredArrow.w φ.left)
+  map_id _ := rfl
+  map_comp _ _ := rfl
+
+end EquivalenceJ
+
+/-- Given `w : TwoSquare T L R B` and a morphism `g : R.obj X₂ ⟶ B.obj X₃`, this is
+the obvious equivalence of categories
+`w.StructuredArrowRightwards g ≌ w.CostructuredArrowDownwards g`. -/
+@[simps functor inverse unitIso counitIso]
+def equivalenceJ : w.StructuredArrowRightwards g ≌ w.CostructuredArrowDownwards g where
+  functor := EquivalenceJ.functor w g
+  inverse := EquivalenceJ.inverse w g
+  unitIso := Iso.refl _
+  counitIso := Iso.refl _
+
+lemma isConnected_rightwards_iff_downwards :
+    IsConnected (w.StructuredArrowRightwards g) ↔ IsConnected (w.CostructuredArrowDownwards g) :=
+  isConnected_iff_of_equivalence (w.equivalenceJ g)
+
+end
+
+/-- Condition on `w : TwoSquare T L R B` expressing that it is a Guitart exact square.
+It is equivalent to saying that for any `X₃ : C₃`, the induced functor
+`CostructuredArrow L X₃ ⥤ CostructuredArrow R (B.obj X₃)` is final (see `guitartExact_iff_final`)
+or equivalently that for any `X₂ : C₂`, the induced functor
+`StructuredArrow X₂ T ⥤ StructuredArrow (R.obj X₂) B` is initial (see `guitartExact_iff_initial`).
+See also  `guitartExact_iff_isConnected_rightwards`, `guitartExact_iff_isConnected_downwards`
+for characterizations in terms of the connectedness of auxiliary categories. -/
+class GuitartExact : Prop where
+  isConnected_rightwards {X₂ : C₂} {X₃ : C₃} (g : R.obj X₂ ⟶ B.obj X₃) :
+    IsConnected (w.StructuredArrowRightwards g)
+
+lemma guitartExact_iff_isConnected_rightwards :
+    w.GuitartExact ↔ ∀ {X₂ : C₂} {X₃ : C₃} (g : R.obj X₂ ⟶ B.obj X₃),
+      IsConnected (w.StructuredArrowRightwards g) :=
+  ⟨fun h => h.isConnected_rightwards, fun h => ⟨h⟩⟩
+
+lemma guitartExact_iff_isConnected_downwards :
+    w.GuitartExact ↔ ∀ {X₂ : C₂} {X₃ : C₃} (g : R.obj X₂ ⟶ B.obj X₃),
+      IsConnected (w.CostructuredArrowDownwards g) := by
+  simp only [guitartExact_iff_isConnected_rightwards,
+    isConnected_rightwards_iff_downwards]
+
+instance [hw : w.GuitartExact] {X₃ : C₃} (g : CostructuredArrow R (B.obj X₃)) :
+    IsConnected (StructuredArrow g (w.costructuredArrowRightwards X₃)) := by
+  rw [guitartExact_iff_isConnected_rightwards] at hw
+  apply hw
+
+instance [hw : w.GuitartExact] {X₂ : C₂} (g : StructuredArrow (R.obj X₂) B) :
+    IsConnected (CostructuredArrow (w.structuredArrowDownwards X₂) g) := by
+  rw [guitartExact_iff_isConnected_downwards] at hw
+  apply hw
+
+lemma guitartExact_iff_final :
+    w.GuitartExact ↔ ∀ (X₃ : C₃), (w.costructuredArrowRightwards X₃).Final :=
+  ⟨fun _ _ => ⟨fun _ => inferInstance⟩, fun _ => ⟨fun _ => inferInstance⟩⟩
+
+instance [hw : w.GuitartExact] (X₃ : C₃) :
+    (w.costructuredArrowRightwards X₃).Final := by
+  rw [guitartExact_iff_final] at hw
+  apply hw
+
+lemma guitartExact_iff_initial :
+    w.GuitartExact ↔ ∀ (X₂ : C₂), (w.structuredArrowDownwards X₂).Initial :=
+  ⟨fun _ _ => ⟨fun _ => inferInstance⟩, by
+    rw [guitartExact_iff_isConnected_downwards]
+    intros
+    infer_instance⟩
+
+instance [hw : w.GuitartExact] (X₂ : C₂) :
+    (w.structuredArrowDownwards X₂).Initial := by
+  rw [guitartExact_iff_initial] at hw
+  apply hw
+
+end TwoSquare
+
+end CategoryTheory

Mathlib/CategoryTheory/IsConnected.lean

@@ -232,13 +232,21 @@ theorem isPreconnected_of_equivalent {K : Type u₂} [Category.{v₂} K] [IsPrec
         _ ≅ (Functor.const K).obj (F.obj k) := NatIso.ofComponents fun X => Iso.refl _⟩
 #align category_theory.is_preconnected_of_equivalent CategoryTheory.isPreconnected_of_equivalent
 
+lemma isPreconnected_iff_of_equivalence {K : Type u₂} [Category.{v₂} K] (e : J ≌ K) :
+    IsPreconnected J ↔ IsPreconnected K :=
+  ⟨fun _ => isPreconnected_of_equivalent e, fun _ => isPreconnected_of_equivalent e.symm⟩
+
 /-- If `J` and `K` are equivalent, then if `J` is connected then `K` is as well. -/
 theorem isConnected_of_equivalent {K : Type u₂} [Category.{v₂} K] (e : J ≌ K) [IsConnected J] :
     IsConnected K :=
   { is_nonempty := Nonempty.map e.functor.obj (by infer_instance)
     toIsPreconnected := isPreconnected_of_equivalent e }
 #align category_theory.is_connected_of_equivalent CategoryTheory.isConnected_of_equivalent
 
+lemma isConnected_iff_of_equivalence {K : Type u₂} [Category.{v₂} K] (e : J ≌ K) :
+    IsConnected J ↔ IsConnected K :=
+  ⟨fun _ => isConnected_of_equivalent e, fun _ => isConnected_of_equivalent e.symm⟩
+
 /-- If `J` is preconnected, then `Jᵒᵖ` is preconnected as well. -/
 instance isPreconnected_op [IsPreconnected J] : IsPreconnected Jᵒᵖ where
   iso_constant := fun {α} F X =>

docs/references.bib

@@ -1368,6 +1368,21 @@ @Unpublished{     grinberg_clifford_2016
   year          = {2016}
 }
 
+@Article{         Guitart1980,
+  author        = {Guitart, Ren\'{e}},
+  tilte         = {Relations et carr\'{e}s exacts},
+  journal       = {Ann. Sci. Math. Qu\'{e}bec},
+  fjournal      = {Annales des Sciences Math\'{e}matiques du Qu\'{e}bec},
+  volume        = {4},
+  year          = {1980},
+  number        = {2},
+  pages         = {103--125},
+  issn          = {0707-9109},
+  mrclass       = {18A99 (18D99 18E99)},
+  mrnumber      = {599050},
+  mrreviewer    = {Marta\ C.\ Bunge}
+}
+
 @Book{            gunter1992,
   title         = {Semantics of Programming Languages: Structures and
                   Techniques},