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]
def
CategoryTheory.TwoSquare.costructuredArrowRightwards
{C₁ : Type u₁}
{C₂ : Type u₂}
{C₃ : Type u₃}
{C₄ : Type u₄}
[Category.{v₁, u₁} C₁]
[Category.{v₂, u₂} C₂]
[Category.{v₃, u₃} C₃]
[Category.{v₄, u₄} C₄]
{T : Functor C₁ C₂}
{L : Functor C₁ C₃}
{R : Functor C₂ C₄}
{B : Functor C₃ C₄}
(w : TwoSquare T L R B)
(X₃ : C₃)
:
Functor (CostructuredArrow L X₃) (CostructuredArrow R (B.obj X₃))
Given w : TwoSquare T L R B and X₃ : C₃, this is the obvious functor
CostructuredArrow L X₃ ⥤ CostructuredArrow R (B.obj X₃).
Equations
Instances For
@[simp]
theorem
CategoryTheory.TwoSquare.costructuredArrowRightwards_obj
{C₁ : Type u₁}
{C₂ : Type u₂}
{C₃ : Type u₃}
{C₄ : Type u₄}
[Category.{v₁, u₁} C₁]
[Category.{v₂, u₂} C₂]
[Category.{v₃, u₃} C₃]
[Category.{v₄, u₄} C₄]
{T : Functor C₁ C₂}
{L : Functor C₁ C₃}
{R : Functor C₂ C₄}
{B : Functor C₃ C₄}
(w : TwoSquare T L R B)
(X₃ : C₃)
(X : CostructuredArrow L X₃)
:
(w.costructuredArrowRightwards X₃).obj X = (CostructuredArrow.pre T R (B.obj X₃)).obj
((Comma.mapLeft (Functor.fromPUnit (B.obj X₃)) w).obj (CostructuredArrow.mk (B.map X.hom)))
@[simp]
theorem
CategoryTheory.TwoSquare.costructuredArrowRightwards_map
{C₁ : Type u₁}
{C₂ : Type u₂}
{C₃ : Type u₃}
{C₄ : Type u₄}
[Category.{v₁, u₁} C₁]
[Category.{v₂, u₂} C₂]
[Category.{v₃, u₃} C₃]
[Category.{v₄, u₄} C₄]
{T : Functor C₁ C₂}
{L : Functor C₁ C₃}
{R : Functor C₂ C₄}
{B : Functor C₃ C₄}
(w : TwoSquare T L R B)
(X₃ : C₃)
{X✝ Y✝ : CostructuredArrow L X₃}
(f : X✝ ⟶ Y✝)
:
(w.costructuredArrowRightwards X₃).map f = (CostructuredArrow.pre T R (B.obj X₃)).map
((Comma.mapLeft (Functor.fromPUnit (B.obj X₃)) w).map (CostructuredArrow.homMk f.left ⋯))
def
CategoryTheory.TwoSquare.structuredArrowDownwards
{C₁ : Type u₁}
{C₂ : Type u₂}
{C₃ : Type u₃}
{C₄ : Type u₄}
[Category.{v₁, u₁} C₁]
[Category.{v₂, u₂} C₂]
[Category.{v₃, u₃} C₃]
[Category.{v₄, u₄} C₄]
{T : Functor C₁ C₂}
{L : Functor C₁ C₃}
{R : Functor C₂ C₄}
{B : Functor C₃ C₄}
(w : TwoSquare T L R B)
(X₂ : C₂)
:
Functor (StructuredArrow X₂ T) (StructuredArrow (R.obj X₂) B)
Given w : TwoSquare T L R B and X₂ : C₂, this is the obvious functor
StructuredArrow X₂ T ⥤ StructuredArrow (R.obj X₂) B.
Equations
Instances For
@[simp]
theorem
CategoryTheory.TwoSquare.structuredArrowDownwards_obj
{C₁ : Type u₁}
{C₂ : Type u₂}
{C₃ : Type u₃}
{C₄ : Type u₄}
[Category.{v₁, u₁} C₁]
[Category.{v₂, u₂} C₂]
[Category.{v₃, u₃} C₃]
[Category.{v₄, u₄} C₄]
{T : Functor C₁ C₂}
{L : Functor C₁ C₃}
{R : Functor C₂ C₄}
{B : Functor C₃ C₄}
(w : TwoSquare T L R B)
(X₂ : C₂)
(X : StructuredArrow X₂ T)
:
(w.structuredArrowDownwards X₂).obj X = (StructuredArrow.pre (R.obj X₂) L B).obj
((Comma.mapRight (Functor.fromPUnit (R.obj X₂)) w).obj (StructuredArrow.mk (R.map X.hom)))
@[simp]
theorem
CategoryTheory.TwoSquare.structuredArrowDownwards_map
{C₁ : Type u₁}
{C₂ : Type u₂}
{C₃ : Type u₃}
{C₄ : Type u₄}
[Category.{v₁, u₁} C₁]
[Category.{v₂, u₂} C₂]
[Category.{v₃, u₃} C₃]
[Category.{v₄, u₄} C₄]
{T : Functor C₁ C₂}
{L : Functor C₁ C₃}
{R : Functor C₂ C₄}
{B : Functor C₃ C₄}
(w : TwoSquare T L R B)
(X₂ : C₂)
{X✝ Y✝ : StructuredArrow X₂ T}
(f : X✝ ⟶ Y✝)
:
(w.structuredArrowDownwards X₂).map f = (StructuredArrow.pre (R.obj X₂) L B).map
((Comma.mapRight (Functor.fromPUnit (R.obj X₂)) w).map (StructuredArrow.homMk f.right ⋯))
@[reducible, inline]
abbrev
CategoryTheory.TwoSquare.StructuredArrowRightwards
{C₁ : Type u₁}
{C₂ : Type u₂}
{C₃ : Type u₃}
{C₄ : Type u₄}
[Category.{v₁, u₁} C₁]
[Category.{v₂, u₂} C₂]
[Category.{v₃, u₃} C₃]
[Category.{v₄, u₄} C₄]
{T : Functor C₁ C₂}
{L : Functor C₁ C₃}
{R : Functor C₂ C₄}
{B : Functor C₃ C₄}
(w : TwoSquare T L R B)
{X₂ : C₂}
{X₃ : C₃}
(g : R.obj X₂ ⟶ B.obj X₃)
:
Type (max (max u₁ v₃) v₂)
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.
Equations
Instances For
@[reducible, inline]
abbrev
CategoryTheory.TwoSquare.CostructuredArrowDownwards
{C₁ : Type u₁}
{C₂ : Type u₂}
{C₃ : Type u₃}
{C₄ : Type u₄}
[Category.{v₁, u₁} C₁]
[Category.{v₂, u₂} C₂]
[Category.{v₃, u₃} C₃]
[Category.{v₄, u₄} C₄]
{T : Functor C₁ C₂}
{L : Functor C₁ C₃}
{R : Functor C₂ C₄}
{B : Functor C₃ C₄}
(w : TwoSquare T L R B)
{X₂ : C₂}
{X₃ : C₃}
(g : R.obj X₂ ⟶ B.obj X₃)
:
Type (max (max u₁ v₂) v₃)
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.
Equations
Instances For
@[reducible, inline]
abbrev
CategoryTheory.TwoSquare.StructuredArrowRightwards.mk
{C₁ : Type u₁}
{C₂ : Type u₂}
{C₃ : Type u₃}
{C₄ : Type u₄}
[Category.{v₁, u₁} C₁]
[Category.{v₂, u₂} C₂]
[Category.{v₃, u₃} C₃]
[Category.{v₄, u₄} C₄]
{T : Functor C₁ C₂}
{L : Functor C₁ C₃}
{R : Functor C₂ C₄}
{B : Functor C₃ C₄}
(w : TwoSquare T L R B)
{X₂ : C₂}
{X₃ : C₃}
(g : R.obj X₂ ⟶ B.obj X₃)
(X₁ : C₁)
(a : X₂ ⟶ T.obj X₁)
(b : L.obj X₁ ⟶ X₃)
(comm : CategoryStruct.comp (R.map a) (CategoryStruct.comp (w.app X₁) (B.map b)) = g)
:
Constructor for objects in w.StructuredArrowRightwards g.
Equations
Instances For
@[reducible, inline]
abbrev
CategoryTheory.TwoSquare.CostructuredArrowDownwards.mk
{C₁ : Type u₁}
{C₂ : Type u₂}
{C₃ : Type u₃}
{C₄ : Type u₄}
[Category.{v₁, u₁} C₁]
[Category.{v₂, u₂} C₂]
[Category.{v₃, u₃} C₃]
[Category.{v₄, u₄} C₄]
{T : Functor C₁ C₂}
{L : Functor C₁ C₃}
{R : Functor C₂ C₄}
{B : Functor C₃ C₄}
(w : TwoSquare T L R B)
{X₂ : C₂}
{X₃ : C₃}
(g : R.obj X₂ ⟶ B.obj X₃)
(X₁ : C₁)
(a : X₂ ⟶ T.obj X₁)
(b : L.obj X₁ ⟶ X₃)
(comm : CategoryStruct.comp (R.map a) (CategoryStruct.comp (w.app X₁) (B.map b)) = g)
:
Constructor for objects in w.CostructuredArrowDownwards g.
Equations
Instances For
theorem
CategoryTheory.TwoSquare.StructuredArrowRightwards.mk_surjective
{C₁ : Type u₁}
{C₂ : Type u₂}
{C₃ : Type u₃}
{C₄ : Type u₄}
[Category.{v₁, u₁} C₁]
[Category.{v₂, u₂} C₂]
[Category.{v₃, u₃} C₃]
[Category.{v₄, u₄} C₄]
{T : Functor C₁ C₂}
{L : Functor C₁ C₃}
{R : Functor C₂ C₄}
{B : Functor C₃ C₄}
{w : TwoSquare T L R B}
{X₂ : C₂}
{X₃ : C₃}
{g : R.obj X₂ ⟶ B.obj X₃}
(f : w.StructuredArrowRightwards g)
:
theorem
CategoryTheory.TwoSquare.CostructuredArrowDownwards.mk_surjective
{C₁ : Type u₁}
{C₂ : Type u₂}
{C₃ : Type u₃}
{C₄ : Type u₄}
[Category.{v₁, u₁} C₁]
[Category.{v₂, u₂} C₂]
[Category.{v₃, u₃} C₃]
[Category.{v₄, u₄} C₄]
{T : Functor C₁ C₂}
{L : Functor C₁ C₃}
{R : Functor C₂ C₄}
{B : Functor C₃ C₄}
{w : TwoSquare T L R B}
{X₂ : C₂}
{X₃ : C₃}
{g : R.obj X₂ ⟶ B.obj X₃}
(f : w.CostructuredArrowDownwards g)
:
def
CategoryTheory.TwoSquare.EquivalenceJ.functor
{C₁ : Type u₁}
{C₂ : Type u₂}
{C₃ : Type u₃}
{C₄ : Type u₄}
[Category.{v₁, u₁} C₁]
[Category.{v₂, u₂} C₂]
[Category.{v₃, u₃} C₃]
[Category.{v₄, u₄} C₄]
{T : Functor C₁ C₂}
{L : Functor C₁ C₃}
{R : Functor C₂ C₄}
{B : Functor C₃ C₄}
(w : TwoSquare T L R B)
{X₂ : C₂}
{X₃ : C₃}
(g : R.obj X₂ ⟶ B.obj X₃)
:
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.
Equations
Instances For
@[simp]
theorem
CategoryTheory.TwoSquare.EquivalenceJ.functor_obj
{C₁ : Type u₁}
{C₂ : Type u₂}
{C₃ : Type u₃}
{C₄ : Type u₄}
[Category.{v₁, u₁} C₁]
[Category.{v₂, u₂} C₂]
[Category.{v₃, u₃} C₃]
[Category.{v₄, u₄} C₄]
{T : Functor C₁ C₂}
{L : Functor C₁ C₃}
{R : Functor C₂ C₄}
{B : Functor C₃ C₄}
(w : TwoSquare T L R B)
{X₂ : C₂}
{X₃ : C₃}
(g : R.obj X₂ ⟶ B.obj X₃)
(f : w.StructuredArrowRightwards g)
:
@[simp]
theorem
CategoryTheory.TwoSquare.EquivalenceJ.functor_map
{C₁ : Type u₁}
{C₂ : Type u₂}
{C₃ : Type u₃}
{C₄ : Type u₄}
[Category.{v₁, u₁} C₁]
[Category.{v₂, u₂} C₂]
[Category.{v₃, u₃} C₃]
[Category.{v₄, u₄} C₄]
{T : Functor C₁ C₂}
{L : Functor C₁ C₃}
{R : Functor C₂ C₄}
{B : Functor C₃ C₄}
(w : TwoSquare T L R B)
{X₂ : C₂}
{X₃ : C₃}
(g : R.obj X₂ ⟶ B.obj X₃)
{f₁ f₂ : w.StructuredArrowRightwards g}
(φ : f₁ ⟶ f₂)
:
def
CategoryTheory.TwoSquare.EquivalenceJ.inverse
{C₁ : Type u₁}
{C₂ : Type u₂}
{C₃ : Type u₃}
{C₄ : Type u₄}
[Category.{v₁, u₁} C₁]
[Category.{v₂, u₂} C₂]
[Category.{v₃, u₃} C₃]
[Category.{v₄, u₄} C₄]
{T : Functor C₁ C₂}
{L : Functor C₁ C₃}
{R : Functor C₂ C₄}
{B : Functor C₃ C₄}
(w : TwoSquare T L R B)
{X₂ : C₂}
{X₃ : C₃}
(g : R.obj X₂ ⟶ B.obj X₃)
:
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.
Equations
Instances For
@[simp]
theorem
CategoryTheory.TwoSquare.EquivalenceJ.inverse_obj
{C₁ : Type u₁}
{C₂ : Type u₂}
{C₃ : Type u₃}
{C₄ : Type u₄}
[Category.{v₁, u₁} C₁]
[Category.{v₂, u₂} C₂]
[Category.{v₃, u₃} C₃]
[Category.{v₄, u₄} C₄]
{T : Functor C₁ C₂}
{L : Functor C₁ C₃}
{R : Functor C₂ C₄}
{B : Functor C₃ C₄}
(w : TwoSquare T L R B)
{X₂ : C₂}
{X₃ : C₃}
(g : R.obj X₂ ⟶ B.obj X₃)
(f : w.CostructuredArrowDownwards g)
:
@[simp]
theorem
CategoryTheory.TwoSquare.EquivalenceJ.inverse_map
{C₁ : Type u₁}
{C₂ : Type u₂}
{C₃ : Type u₃}
{C₄ : Type u₄}
[Category.{v₁, u₁} C₁]
[Category.{v₂, u₂} C₂]
[Category.{v₃, u₃} C₃]
[Category.{v₄, u₄} C₄]
{T : Functor C₁ C₂}
{L : Functor C₁ C₃}
{R : Functor C₂ C₄}
{B : Functor C₃ C₄}
(w : TwoSquare T L R B)
{X₂ : C₂}
{X₃ : C₃}
(g : R.obj X₂ ⟶ B.obj X₃)
{f₁ f₂ : w.CostructuredArrowDownwards g}
(φ : f₁ ⟶ f₂)
:
def
CategoryTheory.TwoSquare.equivalenceJ
{C₁ : Type u₁}
{C₂ : Type u₂}
{C₃ : Type u₃}
{C₄ : Type u₄}
[Category.{v₁, u₁} C₁]
[Category.{v₂, u₂} C₂]
[Category.{v₃, u₃} C₃]
[Category.{v₄, u₄} C₄]
{T : Functor C₁ C₂}
{L : Functor C₁ C₃}
{R : Functor C₂ C₄}
{B : Functor C₃ C₄}
(w : TwoSquare T L R B)
{X₂ : C₂}
{X₃ : C₃}
(g : R.obj X₂ ⟶ B.obj X₃)
:
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.
Equations
Instances For
@[simp]
theorem
CategoryTheory.TwoSquare.equivalenceJ_unitIso
{C₁ : Type u₁}
{C₂ : Type u₂}
{C₃ : Type u₃}
{C₄ : Type u₄}
[Category.{v₁, u₁} C₁]
[Category.{v₂, u₂} C₂]
[Category.{v₃, u₃} C₃]
[Category.{v₄, u₄} C₄]
{T : Functor C₁ C₂}
{L : Functor C₁ C₃}
{R : Functor C₂ C₄}
{B : Functor C₃ C₄}
(w : TwoSquare T L R B)
{X₂ : C₂}
{X₃ : C₃}
(g : R.obj X₂ ⟶ B.obj X₃)
:
@[simp]
theorem
CategoryTheory.TwoSquare.equivalenceJ_counitIso
{C₁ : Type u₁}
{C₂ : Type u₂}
{C₃ : Type u₃}
{C₄ : Type u₄}
[Category.{v₁, u₁} C₁]
[Category.{v₂, u₂} C₂]
[Category.{v₃, u₃} C₃]
[Category.{v₄, u₄} C₄]
{T : Functor C₁ C₂}
{L : Functor C₁ C₃}
{R : Functor C₂ C₄}
{B : Functor C₃ C₄}
(w : TwoSquare T L R B)
{X₂ : C₂}
{X₃ : C₃}
(g : R.obj X₂ ⟶ B.obj X₃)
:
(w.equivalenceJ g).counitIso = Iso.refl ((EquivalenceJ.inverse w g).comp (EquivalenceJ.functor w g))
@[simp]
theorem
CategoryTheory.TwoSquare.equivalenceJ_inverse
{C₁ : Type u₁}
{C₂ : Type u₂}
{C₃ : Type u₃}
{C₄ : Type u₄}
[Category.{v₁, u₁} C₁]
[Category.{v₂, u₂} C₂]
[Category.{v₃, u₃} C₃]
[Category.{v₄, u₄} C₄]
{T : Functor C₁ C₂}
{L : Functor C₁ C₃}
{R : Functor C₂ C₄}
{B : Functor C₃ C₄}
(w : TwoSquare T L R B)
{X₂ : C₂}
{X₃ : C₃}
(g : R.obj X₂ ⟶ B.obj X₃)
:
@[simp]
theorem
CategoryTheory.TwoSquare.equivalenceJ_functor
{C₁ : Type u₁}
{C₂ : Type u₂}
{C₃ : Type u₃}
{C₄ : Type u₄}
[Category.{v₁, u₁} C₁]
[Category.{v₂, u₂} C₂]
[Category.{v₃, u₃} C₃]
[Category.{v₄, u₄} C₄]
{T : Functor C₁ C₂}
{L : Functor C₁ C₃}
{R : Functor C₂ C₄}
{B : Functor C₃ C₄}
(w : TwoSquare T L R B)
{X₂ : C₂}
{X₃ : C₃}
(g : R.obj X₂ ⟶ B.obj X₃)
:
theorem
CategoryTheory.TwoSquare.isConnected_rightwards_iff_downwards
{C₁ : Type u₁}
{C₂ : Type u₂}
{C₃ : Type u₃}
{C₄ : Type u₄}
[Category.{v₁, u₁} C₁]
[Category.{v₂, u₂} C₂]
[Category.{v₃, u₃} C₃]
[Category.{v₄, u₄} C₄]
{T : Functor C₁ C₂}
{L : Functor C₁ C₃}
{R : Functor C₂ C₄}
{B : Functor C₃ C₄}
(w : TwoSquare T L R B)
{X₂ : C₂}
{X₃ : C₃}
(g : R.obj X₂ ⟶ B.obj X₃)
:
def
CategoryTheory.TwoSquare.costructuredArrowDownwardsPrecomp
{C₁ : Type u₁}
{C₂ : Type u₂}
{C₃ : Type u₃}
{C₄ : Type u₄}
[Category.{v₁, u₁} C₁]
[Category.{v₂, u₂} C₂]
[Category.{v₃, u₃} C₃]
[Category.{v₄, u₄} C₄]
{T : Functor C₁ C₂}
{L : Functor C₁ C₃}
{R : Functor C₂ C₄}
{B : Functor C₃ C₄}
(w : TwoSquare T L R B)
{X₂ X₂' : C₂}
{X₃ : C₃}
(g : R.obj X₂ ⟶ B.obj X₃)
(g' : R.obj X₂' ⟶ B.obj X₃)
(γ : X₂' ⟶ X₂)
(hγ : CategoryStruct.comp (R.map γ) g = g')
:
Functor (w.CostructuredArrowDownwards g) (w.CostructuredArrowDownwards g')
The functor w.CostructuredArrowDownwards g ⥤ w.CostructuredArrowDownwards g' induced
by a morphism γ such that R.map γ ≫ g = g'.
Equations
Instances For
@[simp]
theorem
CategoryTheory.TwoSquare.costructuredArrowDownwardsPrecomp_map
{C₁ : Type u₁}
{C₂ : Type u₂}
{C₃ : Type u₃}
{C₄ : Type u₄}
[Category.{v₁, u₁} C₁]
[Category.{v₂, u₂} C₂]
[Category.{v₃, u₃} C₃]
[Category.{v₄, u₄} C₄]
{T : Functor C₁ C₂}
{L : Functor C₁ C₃}
{R : Functor C₂ C₄}
{B : Functor C₃ C₄}
(w : TwoSquare T L R B)
{X₂ X₂' : C₂}
{X₃ : C₃}
(g : R.obj X₂ ⟶ B.obj X₃)
(g' : R.obj X₂' ⟶ B.obj X₃)
(γ : X₂' ⟶ X₂)
(hγ : CategoryStruct.comp (R.map γ) g = g')
{A A' : w.CostructuredArrowDownwards g}
(φ : A ⟶ A')
:
(w.costructuredArrowDownwardsPrecomp g g' γ hγ).map φ = CostructuredArrow.homMk (StructuredArrow.homMk φ.left.right ⋯) ⋯
@[simp]
theorem
CategoryTheory.TwoSquare.costructuredArrowDownwardsPrecomp_obj
{C₁ : Type u₁}
{C₂ : Type u₂}
{C₃ : Type u₃}
{C₄ : Type u₄}
[Category.{v₁, u₁} C₁]
[Category.{v₂, u₂} C₂]
[Category.{v₃, u₃} C₃]
[Category.{v₄, u₄} C₄]
{T : Functor C₁ C₂}
{L : Functor C₁ C₃}
{R : Functor C₂ C₄}
{B : Functor C₃ C₄}
(w : TwoSquare T L R B)
{X₂ X₂' : C₂}
{X₃ : C₃}
(g : R.obj X₂ ⟶ B.obj X₃)
(g' : R.obj X₂' ⟶ B.obj X₃)
(γ : X₂' ⟶ X₂)
(hγ : CategoryStruct.comp (R.map γ) g = g')
(A : w.CostructuredArrowDownwards g)
:
(w.costructuredArrowDownwardsPrecomp g g' γ hγ).obj A = CostructuredArrowDownwards.mk w g' A.left.right (CategoryStruct.comp γ A.left.hom) A.hom.right ⋯
class
CategoryTheory.TwoSquare.GuitartExact
{C₁ : Type u₁}
{C₂ : Type u₂}
{C₃ : Type u₃}
{C₄ : Type u₄}
[Category.{v₁, u₁} C₁]
[Category.{v₂, u₂} C₂]
[Category.{v₃, u₃} C₃]
[Category.{v₄, u₄} C₄]
{T : Functor C₁ C₂}
{L : Functor C₁ C₃}
{R : Functor C₂ C₄}
{B : Functor C₃ C₄}
(w : TwoSquare T L R B)
:
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.
- isConnected_rightwards {X₂ : C₂} {X₃ : C₃} (g : R.obj X₂ ⟶ B.obj X₃) : IsConnected (w.StructuredArrowRightwards g)
Instances
theorem
CategoryTheory.TwoSquare.guitartExact_iff_isConnected_rightwards
{C₁ : Type u₁}
{C₂ : Type u₂}
{C₃ : Type u₃}
{C₄ : Type u₄}
[Category.{v₁, u₁} C₁]
[Category.{v₂, u₂} C₂]
[Category.{v₃, u₃} C₃]
[Category.{v₄, u₄} C₄]
{T : Functor C₁ C₂}
{L : Functor C₁ C₃}
{R : Functor C₂ C₄}
{B : Functor C₃ C₄}
(w : TwoSquare T L R B)
:
w.GuitartExact ↔ ∀ {X₂ : C₂} {X₃ : C₃} (g : R.obj X₂ ⟶ B.obj X₃), IsConnected (w.StructuredArrowRightwards g)
theorem
CategoryTheory.TwoSquare.guitartExact_iff_isConnected_downwards
{C₁ : Type u₁}
{C₂ : Type u₂}
{C₃ : Type u₃}
{C₄ : Type u₄}
[Category.{v₁, u₁} C₁]
[Category.{v₂, u₂} C₂]
[Category.{v₃, u₃} C₃]
[Category.{v₄, u₄} C₄]
{T : Functor C₁ C₂}
{L : Functor C₁ C₃}
{R : Functor C₂ C₄}
{B : Functor C₃ C₄}
(w : TwoSquare T L R B)
:
w.GuitartExact ↔ ∀ {X₂ : C₂} {X₃ : C₃} (g : R.obj X₂ ⟶ B.obj X₃), IsConnected (w.CostructuredArrowDownwards g)
instance
CategoryTheory.TwoSquare.instIsConnectedStructuredArrowCostructuredArrowObjCostructuredArrowRightwardsOfGuitartExact
{C₁ : Type u₁}
{C₂ : Type u₂}
{C₃ : Type u₃}
{C₄ : Type u₄}
[Category.{v₁, u₁} C₁]
[Category.{v₂, u₂} C₂]
[Category.{v₃, u₃} C₃]
[Category.{v₄, u₄} C₄]
{T : Functor C₁ C₂}
{L : Functor C₁ C₃}
{R : Functor C₂ C₄}
{B : Functor C₃ C₄}
(w : TwoSquare T L R B)
[hw : w.GuitartExact]
{X₃ : C₃}
(g : CostructuredArrow R (B.obj X₃))
:
instance
CategoryTheory.TwoSquare.instIsConnectedCostructuredArrowStructuredArrowObjStructuredArrowDownwardsOfGuitartExact
{C₁ : Type u₁}
{C₂ : Type u₂}
{C₃ : Type u₃}
{C₄ : Type u₄}
[Category.{v₁, u₁} C₁]
[Category.{v₂, u₂} C₂]
[Category.{v₃, u₃} C₃]
[Category.{v₄, u₄} C₄]
{T : Functor C₁ C₂}
{L : Functor C₁ C₃}
{R : Functor C₂ C₄}
{B : Functor C₃ C₄}
(w : TwoSquare T L R B)
[hw : w.GuitartExact]
{X₂ : C₂}
(g : StructuredArrow (R.obj X₂) B)
:
IsConnected (CostructuredArrow (w.structuredArrowDownwards X₂) g)
theorem
CategoryTheory.TwoSquare.guitartExact_iff_final
{C₁ : Type u₁}
{C₂ : Type u₂}
{C₃ : Type u₃}
{C₄ : Type u₄}
[Category.{v₁, u₁} C₁]
[Category.{v₂, u₂} C₂]
[Category.{v₃, u₃} C₃]
[Category.{v₄, u₄} C₄]
{T : Functor C₁ C₂}
{L : Functor C₁ C₃}
{R : Functor C₂ C₄}
{B : Functor C₃ C₄}
(w : TwoSquare T L R B)
:
instance
CategoryTheory.TwoSquare.instFinalCostructuredArrowObjCostructuredArrowRightwardsOfGuitartExact
{C₁ : Type u₁}
{C₂ : Type u₂}
{C₃ : Type u₃}
{C₄ : Type u₄}
[Category.{v₁, u₁} C₁]
[Category.{v₂, u₂} C₂]
[Category.{v₃, u₃} C₃]
[Category.{v₄, u₄} C₄]
{T : Functor C₁ C₂}
{L : Functor C₁ C₃}
{R : Functor C₂ C₄}
{B : Functor C₃ C₄}
(w : TwoSquare T L R B)
[hw : w.GuitartExact]
(X₃ : C₃)
:
(w.costructuredArrowRightwards X₃).Final
theorem
CategoryTheory.TwoSquare.guitartExact_iff_initial
{C₁ : Type u₁}
{C₂ : Type u₂}
{C₃ : Type u₃}
{C₄ : Type u₄}
[Category.{v₁, u₁} C₁]
[Category.{v₂, u₂} C₂]
[Category.{v₃, u₃} C₃]
[Category.{v₄, u₄} C₄]
{T : Functor C₁ C₂}
{L : Functor C₁ C₃}
{R : Functor C₂ C₄}
{B : Functor C₃ C₄}
(w : TwoSquare T L R B)
:
instance
CategoryTheory.TwoSquare.instInitialStructuredArrowObjStructuredArrowDownwardsOfGuitartExact
{C₁ : Type u₁}
{C₂ : Type u₂}
{C₃ : Type u₃}
{C₄ : Type u₄}
[Category.{v₁, u₁} C₁]
[Category.{v₂, u₂} C₂]
[Category.{v₃, u₃} C₃]
[Category.{v₄, u₄} C₄]
{T : Functor C₁ C₂}
{L : Functor C₁ C₃}
{R : Functor C₂ C₄}
{B : Functor C₃ C₄}
(w : TwoSquare T L R B)
[hw : w.GuitartExact]
(X₂ : C₂)
:
(w.structuredArrowDownwards X₂).Initial
@[instance 100]
instance
CategoryTheory.TwoSquare.guitartExact_of_isEquivalence_of_isIso
{C₁ : Type u₁}
{C₂ : Type u₂}
{C₃ : Type u₃}
{C₄ : Type u₄}
[Category.{v₁, u₁} C₁]
[Category.{v₂, u₂} C₂]
[Category.{v₃, u₃} C₃]
[Category.{v₄, u₄} C₄]
{T : Functor C₁ C₂}
{L : Functor C₁ C₃}
{R : Functor C₂ C₄}
{B : Functor C₃ C₄}
(w : TwoSquare T L R B)
[L.IsEquivalence]
[R.IsEquivalence]
[IsIso w]
:
When the left and right functors of a 2-square are equivalences, and the natural transformation of the 2-square is an isomorphism, then the 2-square is Guitart exact.
instance
CategoryTheory.TwoSquare.guitartExact_id
{C₁ : Type u₁}
{C₂ : Type u₂}
[Category.{v₁, u₁} C₁]
[Category.{v₂, u₂} C₂]
(F : Functor C₁ C₂)
:
(mk (Functor.id C₁) F F (Functor.id C₂) (CategoryStruct.id F)).GuitartExact