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
{C₁ : Type u₁}
{C₂ : Type u₂}
{C₃ : Type u₃}
{C₄ : Type u₄}
[CategoryTheory.Category.{v₁, u₁} C₁]
[CategoryTheory.Category.{v₂, u₂} C₂]
[CategoryTheory.Category.{v₃, u₃} C₃]
[CategoryTheory.Category.{v₄, u₄} C₄]
(T : CategoryTheory.Functor C₁ C₂)
(L : CategoryTheory.Functor C₁ C₃)
(R : CategoryTheory.Functor C₂ C₄)
(B : CategoryTheory.Functor C₃ C₄)
:
Type (max u₁ v₄)
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.
Equations
- CategoryTheory.TwoSquare T L R B = (T.comp R ⟶ L.comp B)
Instances For
@[reducible, inline]
abbrev
CategoryTheory.TwoSquare.mk
{C₁ : Type u₁}
{C₂ : Type u₂}
{C₃ : Type u₃}
{C₄ : Type u₄}
[CategoryTheory.Category.{v₁, u₁} C₁]
[CategoryTheory.Category.{v₂, u₂} C₂]
[CategoryTheory.Category.{v₃, u₃} C₃]
[CategoryTheory.Category.{v₄, u₄} C₄]
(T : CategoryTheory.Functor C₁ C₂)
(L : CategoryTheory.Functor C₁ C₃)
(R : CategoryTheory.Functor C₂ C₄)
(B : CategoryTheory.Functor C₃ C₄)
(α : T.comp R ⟶ L.comp B)
:
CategoryTheory.TwoSquare T L R B
Constructor for TwoSquare.
Equations
- CategoryTheory.TwoSquare.mk T L R B α = α
Instances For
theorem
CategoryTheory.TwoSquare.ext
{C₁ : Type u₁}
{C₂ : Type u₂}
{C₃ : Type u₃}
{C₄ : Type u₄}
[CategoryTheory.Category.{v₁, u₁} C₁]
[CategoryTheory.Category.{v₂, u₂} C₂]
[CategoryTheory.Category.{v₃, u₃} C₃]
[CategoryTheory.Category.{v₄, u₄} C₄]
{T : CategoryTheory.Functor C₁ C₂}
{L : CategoryTheory.Functor C₁ C₃}
{R : CategoryTheory.Functor C₂ C₄}
{B : CategoryTheory.Functor C₃ C₄}
(w : CategoryTheory.TwoSquare T L R B)
(w' : CategoryTheory.TwoSquare T L R B)
(h : ∀ (X : C₁), w.app X = w'.app X)
:
w = w'
@[simp]
theorem
CategoryTheory.TwoSquare.costructuredArrowRightwards_obj
{C₁ : Type u₁}
{C₂ : Type u₂}
{C₃ : Type u₃}
{C₄ : Type u₄}
[CategoryTheory.Category.{v₁, u₁} C₁]
[CategoryTheory.Category.{v₂, u₂} C₂]
[CategoryTheory.Category.{v₃, u₃} C₃]
[CategoryTheory.Category.{v₄, u₄} C₄]
{T : CategoryTheory.Functor C₁ C₂}
{L : CategoryTheory.Functor C₁ C₃}
{R : CategoryTheory.Functor C₂ C₄}
{B : CategoryTheory.Functor C₃ C₄}
(w : CategoryTheory.TwoSquare T L R B)
(X₃ : C₃)
(X : CategoryTheory.CostructuredArrow L X₃)
:
(w.costructuredArrowRightwards X₃).obj X = (CategoryTheory.CostructuredArrow.pre T R (B.obj X₃)).obj
((CategoryTheory.Comma.mapLeft (CategoryTheory.Functor.fromPUnit (B.obj X₃)) w).obj
(CategoryTheory.CostructuredArrow.mk (B.map X.hom)))
@[simp]
theorem
CategoryTheory.TwoSquare.costructuredArrowRightwards_map
{C₁ : Type u₁}
{C₂ : Type u₂}
{C₃ : Type u₃}
{C₄ : Type u₄}
[CategoryTheory.Category.{v₁, u₁} C₁]
[CategoryTheory.Category.{v₂, u₂} C₂]
[CategoryTheory.Category.{v₃, u₃} C₃]
[CategoryTheory.Category.{v₄, u₄} C₄]
{T : CategoryTheory.Functor C₁ C₂}
{L : CategoryTheory.Functor C₁ C₃}
{R : CategoryTheory.Functor C₂ C₄}
{B : CategoryTheory.Functor C₃ C₄}
(w : CategoryTheory.TwoSquare T L R B)
(X₃ : C₃)
:
∀ {X Y : CategoryTheory.CostructuredArrow L X₃} (f : X ⟶ Y),
(w.costructuredArrowRightwards X₃).map f = (CategoryTheory.CostructuredArrow.pre T R (B.obj X₃)).map
((CategoryTheory.Comma.mapLeft (CategoryTheory.Functor.fromPUnit (B.obj X₃)) w).map
(CategoryTheory.CostructuredArrow.homMk f.left ⋯))
def
CategoryTheory.TwoSquare.costructuredArrowRightwards
{C₁ : Type u₁}
{C₂ : Type u₂}
{C₃ : Type u₃}
{C₄ : Type u₄}
[CategoryTheory.Category.{v₁, u₁} C₁]
[CategoryTheory.Category.{v₂, u₂} C₂]
[CategoryTheory.Category.{v₃, u₃} C₃]
[CategoryTheory.Category.{v₄, u₄} C₄]
{T : CategoryTheory.Functor C₁ C₂}
{L : CategoryTheory.Functor C₁ C₃}
{R : CategoryTheory.Functor C₂ C₄}
{B : CategoryTheory.Functor C₃ C₄}
(w : CategoryTheory.TwoSquare T L R B)
(X₃ : C₃)
:
CategoryTheory.Functor (CategoryTheory.CostructuredArrow L X₃) (CategoryTheory.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
- One or more equations did not get rendered due to their size.
Instances For
@[simp]
theorem
CategoryTheory.TwoSquare.structuredArrowDownwards_map
{C₁ : Type u₁}
{C₂ : Type u₂}
{C₃ : Type u₃}
{C₄ : Type u₄}
[CategoryTheory.Category.{v₁, u₁} C₁]
[CategoryTheory.Category.{v₂, u₂} C₂]
[CategoryTheory.Category.{v₃, u₃} C₃]
[CategoryTheory.Category.{v₄, u₄} C₄]
{T : CategoryTheory.Functor C₁ C₂}
{L : CategoryTheory.Functor C₁ C₃}
{R : CategoryTheory.Functor C₂ C₄}
{B : CategoryTheory.Functor C₃ C₄}
(w : CategoryTheory.TwoSquare T L R B)
(X₂ : C₂)
:
∀ {X Y : CategoryTheory.StructuredArrow X₂ T} (f : X ⟶ Y),
(w.structuredArrowDownwards X₂).map f = (CategoryTheory.StructuredArrow.pre (R.obj X₂) L B).map
((CategoryTheory.Comma.mapRight (CategoryTheory.Functor.fromPUnit (R.obj X₂)) w).map
(CategoryTheory.StructuredArrow.homMk f.right ⋯))
@[simp]
theorem
CategoryTheory.TwoSquare.structuredArrowDownwards_obj
{C₁ : Type u₁}
{C₂ : Type u₂}
{C₃ : Type u₃}
{C₄ : Type u₄}
[CategoryTheory.Category.{v₁, u₁} C₁]
[CategoryTheory.Category.{v₂, u₂} C₂]
[CategoryTheory.Category.{v₃, u₃} C₃]
[CategoryTheory.Category.{v₄, u₄} C₄]
{T : CategoryTheory.Functor C₁ C₂}
{L : CategoryTheory.Functor C₁ C₃}
{R : CategoryTheory.Functor C₂ C₄}
{B : CategoryTheory.Functor C₃ C₄}
(w : CategoryTheory.TwoSquare T L R B)
(X₂ : C₂)
(X : CategoryTheory.StructuredArrow X₂ T)
:
(w.structuredArrowDownwards X₂).obj X = (CategoryTheory.StructuredArrow.pre (R.obj X₂) L B).obj
((CategoryTheory.Comma.mapRight (CategoryTheory.Functor.fromPUnit (R.obj X₂)) w).obj
(CategoryTheory.StructuredArrow.mk (R.map X.hom)))
def
CategoryTheory.TwoSquare.structuredArrowDownwards
{C₁ : Type u₁}
{C₂ : Type u₂}
{C₃ : Type u₃}
{C₄ : Type u₄}
[CategoryTheory.Category.{v₁, u₁} C₁]
[CategoryTheory.Category.{v₂, u₂} C₂]
[CategoryTheory.Category.{v₃, u₃} C₃]
[CategoryTheory.Category.{v₄, u₄} C₄]
{T : CategoryTheory.Functor C₁ C₂}
{L : CategoryTheory.Functor C₁ C₃}
{R : CategoryTheory.Functor C₂ C₄}
{B : CategoryTheory.Functor C₃ C₄}
(w : CategoryTheory.TwoSquare T L R B)
(X₂ : C₂)
:
CategoryTheory.Functor (CategoryTheory.StructuredArrow X₂ T) (CategoryTheory.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
- One or more equations did not get rendered due to their size.
Instances For
@[reducible, inline]
abbrev
CategoryTheory.TwoSquare.StructuredArrowRightwards
{C₁ : Type u₁}
{C₂ : Type u₂}
{C₃ : Type u₃}
{C₄ : Type u₄}
[CategoryTheory.Category.{v₁, u₁} C₁]
[CategoryTheory.Category.{v₂, u₂} C₂]
[CategoryTheory.Category.{v₃, u₃} C₃]
[CategoryTheory.Category.{v₄, u₄} C₄]
{T : CategoryTheory.Functor C₁ C₂}
{L : CategoryTheory.Functor C₁ C₃}
{R : CategoryTheory.Functor C₂ C₄}
{B : CategoryTheory.Functor C₃ C₄}
(w : CategoryTheory.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
- w.StructuredArrowRightwards g = CategoryTheory.StructuredArrow (CategoryTheory.CostructuredArrow.mk g) (w.costructuredArrowRightwards X₃)
Instances For
@[reducible, inline]
abbrev
CategoryTheory.TwoSquare.CostructuredArrowDownwards
{C₁ : Type u₁}
{C₂ : Type u₂}
{C₃ : Type u₃}
{C₄ : Type u₄}
[CategoryTheory.Category.{v₁, u₁} C₁]
[CategoryTheory.Category.{v₂, u₂} C₂]
[CategoryTheory.Category.{v₃, u₃} C₃]
[CategoryTheory.Category.{v₄, u₄} C₄]
{T : CategoryTheory.Functor C₁ C₂}
{L : CategoryTheory.Functor C₁ C₃}
{R : CategoryTheory.Functor C₂ C₄}
{B : CategoryTheory.Functor C₃ C₄}
(w : CategoryTheory.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
- w.CostructuredArrowDownwards g = CategoryTheory.CostructuredArrow (w.structuredArrowDownwards X₂) (CategoryTheory.StructuredArrow.mk g)
Instances For
@[reducible, inline]
abbrev
CategoryTheory.TwoSquare.StructuredArrowRightwards.mk
{C₁ : Type u₁}
{C₂ : Type u₂}
{C₃ : Type u₃}
{C₄ : Type u₄}
[CategoryTheory.Category.{v₁, u₁} C₁]
[CategoryTheory.Category.{v₂, u₂} C₂]
[CategoryTheory.Category.{v₃, u₃} C₃]
[CategoryTheory.Category.{v₄, u₄} C₄]
{T : CategoryTheory.Functor C₁ C₂}
{L : CategoryTheory.Functor C₁ C₃}
{R : CategoryTheory.Functor C₂ C₄}
{B : CategoryTheory.Functor C₃ C₄}
(w : CategoryTheory.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 : CategoryTheory.CategoryStruct.comp (R.map a) (CategoryTheory.CategoryStruct.comp (w.app X₁) (B.map b)) = g)
:
w.StructuredArrowRightwards 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₄}
[CategoryTheory.Category.{v₁, u₁} C₁]
[CategoryTheory.Category.{v₂, u₂} C₂]
[CategoryTheory.Category.{v₃, u₃} C₃]
[CategoryTheory.Category.{v₄, u₄} C₄]
{T : CategoryTheory.Functor C₁ C₂}
{L : CategoryTheory.Functor C₁ C₃}
{R : CategoryTheory.Functor C₂ C₄}
{B : CategoryTheory.Functor C₃ C₄}
(w : CategoryTheory.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 : CategoryTheory.CategoryStruct.comp (R.map a) (CategoryTheory.CategoryStruct.comp (w.app X₁) (B.map b)) = g)
:
w.CostructuredArrowDownwards 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₄}
[CategoryTheory.Category.{v₁, u₁} C₁]
[CategoryTheory.Category.{v₂, u₂} C₂]
[CategoryTheory.Category.{v₃, u₃} C₃]
[CategoryTheory.Category.{v₄, u₄} C₄]
{T : CategoryTheory.Functor C₁ C₂}
{L : CategoryTheory.Functor C₁ C₃}
{R : CategoryTheory.Functor C₂ C₄}
{B : CategoryTheory.Functor C₃ C₄}
{w : CategoryTheory.TwoSquare T L R B}
{X₂ : C₂}
{X₃ : C₃}
{g : R.obj X₂ ⟶ B.obj X₃}
(f : w.StructuredArrowRightwards g)
:
∃ (X₁ : C₁) (a : X₂ ⟶ T.obj X₁) (b : L.obj X₁ ⟶ X₃) (comm :
CategoryTheory.CategoryStruct.comp (R.map a) (CategoryTheory.CategoryStruct.comp (w.app X₁) (B.map b)) = g),
f = CategoryTheory.TwoSquare.StructuredArrowRightwards.mk w g X₁ a b comm
theorem
CategoryTheory.TwoSquare.CostructuredArrowDownwards.mk_surjective
{C₁ : Type u₁}
{C₂ : Type u₂}
{C₃ : Type u₃}
{C₄ : Type u₄}
[CategoryTheory.Category.{v₁, u₁} C₁]
[CategoryTheory.Category.{v₂, u₂} C₂]
[CategoryTheory.Category.{v₃, u₃} C₃]
[CategoryTheory.Category.{v₄, u₄} C₄]
{T : CategoryTheory.Functor C₁ C₂}
{L : CategoryTheory.Functor C₁ C₃}
{R : CategoryTheory.Functor C₂ C₄}
{B : CategoryTheory.Functor C₃ C₄}
{w : CategoryTheory.TwoSquare T L R B}
{X₂ : C₂}
{X₃ : C₃}
{g : R.obj X₂ ⟶ B.obj X₃}
(f : w.CostructuredArrowDownwards g)
:
∃ (X₁ : C₁) (a : X₂ ⟶ T.obj X₁) (b : L.obj X₁ ⟶ X₃) (comm :
CategoryTheory.CategoryStruct.comp (R.map a) (CategoryTheory.CategoryStruct.comp (w.app X₁) (B.map b)) = g),
f = CategoryTheory.TwoSquare.CostructuredArrowDownwards.mk w g X₁ a b comm
@[simp]
theorem
CategoryTheory.TwoSquare.EquivalenceJ.functor_obj
{C₁ : Type u₁}
{C₂ : Type u₂}
{C₃ : Type u₃}
{C₄ : Type u₄}
[CategoryTheory.Category.{v₁, u₁} C₁]
[CategoryTheory.Category.{v₂, u₂} C₂]
[CategoryTheory.Category.{v₃, u₃} C₃]
[CategoryTheory.Category.{v₄, u₄} C₄]
{T : CategoryTheory.Functor C₁ C₂}
{L : CategoryTheory.Functor C₁ C₃}
{R : CategoryTheory.Functor C₂ C₄}
{B : CategoryTheory.Functor C₃ C₄}
(w : CategoryTheory.TwoSquare T L R B)
{X₂ : C₂}
{X₃ : C₃}
(g : R.obj X₂ ⟶ B.obj X₃)
(f : w.StructuredArrowRightwards g)
:
(CategoryTheory.TwoSquare.EquivalenceJ.functor w g).obj f = CategoryTheory.CostructuredArrow.mk (CategoryTheory.StructuredArrow.homMk f.right.hom ⋯)
@[simp]
theorem
CategoryTheory.TwoSquare.EquivalenceJ.functor_map
{C₁ : Type u₁}
{C₂ : Type u₂}
{C₃ : Type u₃}
{C₄ : Type u₄}
[CategoryTheory.Category.{v₁, u₁} C₁]
[CategoryTheory.Category.{v₂, u₂} C₂]
[CategoryTheory.Category.{v₃, u₃} C₃]
[CategoryTheory.Category.{v₄, u₄} C₄]
{T : CategoryTheory.Functor C₁ C₂}
{L : CategoryTheory.Functor C₁ C₃}
{R : CategoryTheory.Functor C₂ C₄}
{B : CategoryTheory.Functor C₃ C₄}
(w : CategoryTheory.TwoSquare T L R B)
{X₂ : C₂}
{X₃ : C₃}
(g : R.obj X₂ ⟶ B.obj X₃)
{f₁ : w.StructuredArrowRightwards g}
{f₂ : w.StructuredArrowRightwards g}
(φ : f₁ ⟶ f₂)
:
(CategoryTheory.TwoSquare.EquivalenceJ.functor w g).map φ = CategoryTheory.CostructuredArrow.homMk (CategoryTheory.StructuredArrow.homMk φ.right.left ⋯) ⋯
def
CategoryTheory.TwoSquare.EquivalenceJ.functor
{C₁ : Type u₁}
{C₂ : Type u₂}
{C₃ : Type u₃}
{C₄ : Type u₄}
[CategoryTheory.Category.{v₁, u₁} C₁]
[CategoryTheory.Category.{v₂, u₂} C₂]
[CategoryTheory.Category.{v₃, u₃} C₃]
[CategoryTheory.Category.{v₄, u₄} C₄]
{T : CategoryTheory.Functor C₁ C₂}
{L : CategoryTheory.Functor C₁ C₃}
{R : CategoryTheory.Functor C₂ C₄}
{B : CategoryTheory.Functor C₃ C₄}
(w : CategoryTheory.TwoSquare T L R B)
{X₂ : C₂}
{X₃ : C₃}
(g : R.obj X₂ ⟶ B.obj X₃)
:
CategoryTheory.Functor (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 obvious functor w.StructuredArrowRightwards g ⥤ w.CostructuredArrowDownwards g.
Equations
- One or more equations did not get rendered due to their size.
Instances For
@[simp]
theorem
CategoryTheory.TwoSquare.EquivalenceJ.inverse_map
{C₁ : Type u₁}
{C₂ : Type u₂}
{C₃ : Type u₃}
{C₄ : Type u₄}
[CategoryTheory.Category.{v₁, u₁} C₁]
[CategoryTheory.Category.{v₂, u₂} C₂]
[CategoryTheory.Category.{v₃, u₃} C₃]
[CategoryTheory.Category.{v₄, u₄} C₄]
{T : CategoryTheory.Functor C₁ C₂}
{L : CategoryTheory.Functor C₁ C₃}
{R : CategoryTheory.Functor C₂ C₄}
{B : CategoryTheory.Functor C₃ C₄}
(w : CategoryTheory.TwoSquare T L R B)
{X₂ : C₂}
{X₃ : C₃}
(g : R.obj X₂ ⟶ B.obj X₃)
{f₁ : w.CostructuredArrowDownwards g}
{f₂ : w.CostructuredArrowDownwards g}
(φ : f₁ ⟶ f₂)
:
(CategoryTheory.TwoSquare.EquivalenceJ.inverse w g).map φ = CategoryTheory.StructuredArrow.homMk (CategoryTheory.CostructuredArrow.homMk φ.left.right ⋯) ⋯
@[simp]
theorem
CategoryTheory.TwoSquare.EquivalenceJ.inverse_obj
{C₁ : Type u₁}
{C₂ : Type u₂}
{C₃ : Type u₃}
{C₄ : Type u₄}
[CategoryTheory.Category.{v₁, u₁} C₁]
[CategoryTheory.Category.{v₂, u₂} C₂]
[CategoryTheory.Category.{v₃, u₃} C₃]
[CategoryTheory.Category.{v₄, u₄} C₄]
{T : CategoryTheory.Functor C₁ C₂}
{L : CategoryTheory.Functor C₁ C₃}
{R : CategoryTheory.Functor C₂ C₄}
{B : CategoryTheory.Functor C₃ C₄}
(w : CategoryTheory.TwoSquare T L R B)
{X₂ : C₂}
{X₃ : C₃}
(g : R.obj X₂ ⟶ B.obj X₃)
(f : w.CostructuredArrowDownwards g)
:
(CategoryTheory.TwoSquare.EquivalenceJ.inverse w g).obj f = CategoryTheory.StructuredArrow.mk (CategoryTheory.CostructuredArrow.homMk f.left.hom ⋯)
def
CategoryTheory.TwoSquare.EquivalenceJ.inverse
{C₁ : Type u₁}
{C₂ : Type u₂}
{C₃ : Type u₃}
{C₄ : Type u₄}
[CategoryTheory.Category.{v₁, u₁} C₁]
[CategoryTheory.Category.{v₂, u₂} C₂]
[CategoryTheory.Category.{v₃, u₃} C₃]
[CategoryTheory.Category.{v₄, u₄} C₄]
{T : CategoryTheory.Functor C₁ C₂}
{L : CategoryTheory.Functor C₁ C₃}
{R : CategoryTheory.Functor C₂ C₄}
{B : CategoryTheory.Functor C₃ C₄}
(w : CategoryTheory.TwoSquare T L R B)
{X₂ : C₂}
{X₃ : C₃}
(g : R.obj X₂ ⟶ B.obj X₃)
:
CategoryTheory.Functor (w.CostructuredArrowDownwards g) (w.StructuredArrowRightwards g)
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
- One or more equations did not get rendered due to their size.
Instances For
@[simp]
theorem
CategoryTheory.TwoSquare.equivalenceJ_functor
{C₁ : Type u₁}
{C₂ : Type u₂}
{C₃ : Type u₃}
{C₄ : Type u₄}
[CategoryTheory.Category.{v₁, u₁} C₁]
[CategoryTheory.Category.{v₂, u₂} C₂]
[CategoryTheory.Category.{v₃, u₃} C₃]
[CategoryTheory.Category.{v₄, u₄} C₄]
{T : CategoryTheory.Functor C₁ C₂}
{L : CategoryTheory.Functor C₁ C₃}
{R : CategoryTheory.Functor C₂ C₄}
{B : CategoryTheory.Functor C₃ C₄}
(w : CategoryTheory.TwoSquare T L R B)
{X₂ : C₂}
{X₃ : C₃}
(g : R.obj X₂ ⟶ B.obj X₃)
:
(w.equivalenceJ g).functor = CategoryTheory.TwoSquare.EquivalenceJ.functor w g
@[simp]
theorem
CategoryTheory.TwoSquare.equivalenceJ_inverse
{C₁ : Type u₁}
{C₂ : Type u₂}
{C₃ : Type u₃}
{C₄ : Type u₄}
[CategoryTheory.Category.{v₁, u₁} C₁]
[CategoryTheory.Category.{v₂, u₂} C₂]
[CategoryTheory.Category.{v₃, u₃} C₃]
[CategoryTheory.Category.{v₄, u₄} C₄]
{T : CategoryTheory.Functor C₁ C₂}
{L : CategoryTheory.Functor C₁ C₃}
{R : CategoryTheory.Functor C₂ C₄}
{B : CategoryTheory.Functor C₃ C₄}
(w : CategoryTheory.TwoSquare T L R B)
{X₂ : C₂}
{X₃ : C₃}
(g : R.obj X₂ ⟶ B.obj X₃)
:
(w.equivalenceJ g).inverse = CategoryTheory.TwoSquare.EquivalenceJ.inverse w g
@[simp]
theorem
CategoryTheory.TwoSquare.equivalenceJ_counitIso
{C₁ : Type u₁}
{C₂ : Type u₂}
{C₃ : Type u₃}
{C₄ : Type u₄}
[CategoryTheory.Category.{v₁, u₁} C₁]
[CategoryTheory.Category.{v₂, u₂} C₂]
[CategoryTheory.Category.{v₃, u₃} C₃]
[CategoryTheory.Category.{v₄, u₄} C₄]
{T : CategoryTheory.Functor C₁ C₂}
{L : CategoryTheory.Functor C₁ C₃}
{R : CategoryTheory.Functor C₂ C₄}
{B : CategoryTheory.Functor C₃ C₄}
(w : CategoryTheory.TwoSquare T L R B)
{X₂ : C₂}
{X₃ : C₃}
(g : R.obj X₂ ⟶ B.obj X₃)
:
(w.equivalenceJ g).counitIso = CategoryTheory.Iso.refl
((CategoryTheory.TwoSquare.EquivalenceJ.inverse w g).comp (CategoryTheory.TwoSquare.EquivalenceJ.functor w g))
@[simp]
theorem
CategoryTheory.TwoSquare.equivalenceJ_unitIso
{C₁ : Type u₁}
{C₂ : Type u₂}
{C₃ : Type u₃}
{C₄ : Type u₄}
[CategoryTheory.Category.{v₁, u₁} C₁]
[CategoryTheory.Category.{v₂, u₂} C₂]
[CategoryTheory.Category.{v₃, u₃} C₃]
[CategoryTheory.Category.{v₄, u₄} C₄]
{T : CategoryTheory.Functor C₁ C₂}
{L : CategoryTheory.Functor C₁ C₃}
{R : CategoryTheory.Functor C₂ C₄}
{B : CategoryTheory.Functor C₃ C₄}
(w : CategoryTheory.TwoSquare T L R B)
{X₂ : C₂}
{X₃ : C₃}
(g : R.obj X₂ ⟶ B.obj X₃)
:
(w.equivalenceJ g).unitIso = CategoryTheory.Iso.refl (CategoryTheory.Functor.id (w.StructuredArrowRightwards g))
def
CategoryTheory.TwoSquare.equivalenceJ
{C₁ : Type u₁}
{C₂ : Type u₂}
{C₃ : Type u₃}
{C₄ : Type u₄}
[CategoryTheory.Category.{v₁, u₁} C₁]
[CategoryTheory.Category.{v₂, u₂} C₂]
[CategoryTheory.Category.{v₃, u₃} C₃]
[CategoryTheory.Category.{v₄, u₄} C₄]
{T : CategoryTheory.Functor C₁ C₂}
{L : CategoryTheory.Functor C₁ C₃}
{R : CategoryTheory.Functor C₂ C₄}
{B : CategoryTheory.Functor C₃ C₄}
(w : CategoryTheory.TwoSquare T L R B)
{X₂ : C₂}
{X₃ : C₃}
(g : R.obj X₂ ⟶ B.obj X₃)
:
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 obvious equivalence of categories
w.StructuredArrowRightwards g ≌ w.CostructuredArrowDownwards g.
Equations
- One or more equations did not get rendered due to their size.
Instances For
theorem
CategoryTheory.TwoSquare.isConnected_rightwards_iff_downwards
{C₁ : Type u₁}
{C₂ : Type u₂}
{C₃ : Type u₃}
{C₄ : Type u₄}
[CategoryTheory.Category.{v₁, u₁} C₁]
[CategoryTheory.Category.{v₂, u₂} C₂]
[CategoryTheory.Category.{v₃, u₃} C₃]
[CategoryTheory.Category.{v₄, u₄} C₄]
{T : CategoryTheory.Functor C₁ C₂}
{L : CategoryTheory.Functor C₁ C₃}
{R : CategoryTheory.Functor C₂ C₄}
{B : CategoryTheory.Functor C₃ C₄}
(w : CategoryTheory.TwoSquare T L R B)
{X₂ : C₂}
{X₃ : C₃}
(g : R.obj X₂ ⟶ B.obj X₃)
:
CategoryTheory.IsConnected (w.StructuredArrowRightwards g) ↔ CategoryTheory.IsConnected (w.CostructuredArrowDownwards g)
@[simp]
theorem
CategoryTheory.TwoSquare.costructuredArrowDownwardsPrecomp_obj
{C₁ : Type u₁}
{C₂ : Type u₂}
{C₃ : Type u₃}
{C₄ : Type u₄}
[CategoryTheory.Category.{v₁, u₁} C₁]
[CategoryTheory.Category.{v₂, u₂} C₂]
[CategoryTheory.Category.{v₃, u₃} C₃]
[CategoryTheory.Category.{v₄, u₄} C₄]
{T : CategoryTheory.Functor C₁ C₂}
{L : CategoryTheory.Functor C₁ C₃}
{R : CategoryTheory.Functor C₂ C₄}
{B : CategoryTheory.Functor C₃ C₄}
(w : CategoryTheory.TwoSquare T L R B)
{X₂ : C₂}
{X₂' : C₂}
{X₃ : C₃}
(g : R.obj X₂ ⟶ B.obj X₃)
(g' : R.obj X₂' ⟶ B.obj X₃)
(γ : X₂' ⟶ X₂)
(hγ : CategoryTheory.CategoryStruct.comp (R.map γ) g = g')
(A : w.CostructuredArrowDownwards g)
:
(w.costructuredArrowDownwardsPrecomp g g' γ hγ).obj A = CategoryTheory.TwoSquare.CostructuredArrowDownwards.mk w g' A.left.right
(CategoryTheory.CategoryStruct.comp γ A.left.hom) A.hom.right ⋯
@[simp]
theorem
CategoryTheory.TwoSquare.costructuredArrowDownwardsPrecomp_map
{C₁ : Type u₁}
{C₂ : Type u₂}
{C₃ : Type u₃}
{C₄ : Type u₄}
[CategoryTheory.Category.{v₁, u₁} C₁]
[CategoryTheory.Category.{v₂, u₂} C₂]
[CategoryTheory.Category.{v₃, u₃} C₃]
[CategoryTheory.Category.{v₄, u₄} C₄]
{T : CategoryTheory.Functor C₁ C₂}
{L : CategoryTheory.Functor C₁ C₃}
{R : CategoryTheory.Functor C₂ C₄}
{B : CategoryTheory.Functor C₃ C₄}
(w : CategoryTheory.TwoSquare T L R B)
{X₂ : C₂}
{X₂' : C₂}
{X₃ : C₃}
(g : R.obj X₂ ⟶ B.obj X₃)
(g' : R.obj X₂' ⟶ B.obj X₃)
(γ : X₂' ⟶ X₂)
(hγ : CategoryTheory.CategoryStruct.comp (R.map γ) g = g')
{A : w.CostructuredArrowDownwards g}
{A' : w.CostructuredArrowDownwards g}
(φ : A ⟶ A')
:
(w.costructuredArrowDownwardsPrecomp g g' γ hγ).map φ = CategoryTheory.CostructuredArrow.homMk (CategoryTheory.StructuredArrow.homMk φ.left.right ⋯) ⋯
def
CategoryTheory.TwoSquare.costructuredArrowDownwardsPrecomp
{C₁ : Type u₁}
{C₂ : Type u₂}
{C₃ : Type u₃}
{C₄ : Type u₄}
[CategoryTheory.Category.{v₁, u₁} C₁]
[CategoryTheory.Category.{v₂, u₂} C₂]
[CategoryTheory.Category.{v₃, u₃} C₃]
[CategoryTheory.Category.{v₄, u₄} C₄]
{T : CategoryTheory.Functor C₁ C₂}
{L : CategoryTheory.Functor C₁ C₃}
{R : CategoryTheory.Functor C₂ C₄}
{B : CategoryTheory.Functor C₃ C₄}
(w : CategoryTheory.TwoSquare T L R B)
{X₂ : C₂}
{X₂' : C₂}
{X₃ : C₃}
(g : R.obj X₂ ⟶ B.obj X₃)
(g' : R.obj X₂' ⟶ B.obj X₃)
(γ : X₂' ⟶ X₂)
(hγ : CategoryTheory.CategoryStruct.comp (R.map γ) g = g')
:
CategoryTheory.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
- One or more equations did not get rendered due to their size.
Instances For
class
CategoryTheory.TwoSquare.GuitartExact
{C₁ : Type u₁}
{C₂ : Type u₂}
{C₃ : Type u₃}
{C₄ : Type u₄}
[CategoryTheory.Category.{v₁, u₁} C₁]
[CategoryTheory.Category.{v₂, u₂} C₂]
[CategoryTheory.Category.{v₃, u₃} C₃]
[CategoryTheory.Category.{v₄, u₄} C₄]
{T : CategoryTheory.Functor C₁ C₂}
{L : CategoryTheory.Functor C₁ C₃}
{R : CategoryTheory.Functor C₂ C₄}
{B : CategoryTheory.Functor C₃ C₄}
(w : CategoryTheory.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₃), CategoryTheory.IsConnected (w.StructuredArrowRightwards g)
Instances
theorem
CategoryTheory.TwoSquare.GuitartExact.isConnected_rightwards
{C₁ : Type u₁}
{C₂ : Type u₂}
{C₃ : Type u₃}
{C₄ : Type u₄}
[CategoryTheory.Category.{v₁, u₁} C₁]
[CategoryTheory.Category.{v₂, u₂} C₂]
[CategoryTheory.Category.{v₃, u₃} C₃]
[CategoryTheory.Category.{v₄, u₄} C₄]
{T : CategoryTheory.Functor C₁ C₂}
{L : CategoryTheory.Functor C₁ C₃}
{R : CategoryTheory.Functor C₂ C₄}
{B : CategoryTheory.Functor C₃ C₄}
{w : CategoryTheory.TwoSquare T L R B}
[self : w.GuitartExact]
{X₂ : C₂}
{X₃ : C₃}
(g : R.obj X₂ ⟶ B.obj X₃)
:
CategoryTheory.IsConnected (w.StructuredArrowRightwards g)
theorem
CategoryTheory.TwoSquare.guitartExact_iff_isConnected_rightwards
{C₁ : Type u₁}
{C₂ : Type u₂}
{C₃ : Type u₃}
{C₄ : Type u₄}
[CategoryTheory.Category.{v₁, u₁} C₁]
[CategoryTheory.Category.{v₂, u₂} C₂]
[CategoryTheory.Category.{v₃, u₃} C₃]
[CategoryTheory.Category.{v₄, u₄} C₄]
{T : CategoryTheory.Functor C₁ C₂}
{L : CategoryTheory.Functor C₁ C₃}
{R : CategoryTheory.Functor C₂ C₄}
{B : CategoryTheory.Functor C₃ C₄}
(w : CategoryTheory.TwoSquare T L R B)
:
w.GuitartExact ↔ ∀ {X₂ : C₂} {X₃ : C₃} (g : R.obj X₂ ⟶ B.obj X₃), CategoryTheory.IsConnected (w.StructuredArrowRightwards g)
theorem
CategoryTheory.TwoSquare.guitartExact_iff_isConnected_downwards
{C₁ : Type u₁}
{C₂ : Type u₂}
{C₃ : Type u₃}
{C₄ : Type u₄}
[CategoryTheory.Category.{v₁, u₁} C₁]
[CategoryTheory.Category.{v₂, u₂} C₂]
[CategoryTheory.Category.{v₃, u₃} C₃]
[CategoryTheory.Category.{v₄, u₄} C₄]
{T : CategoryTheory.Functor C₁ C₂}
{L : CategoryTheory.Functor C₁ C₃}
{R : CategoryTheory.Functor C₂ C₄}
{B : CategoryTheory.Functor C₃ C₄}
(w : CategoryTheory.TwoSquare T L R B)
:
w.GuitartExact ↔ ∀ {X₂ : C₂} {X₃ : C₃} (g : R.obj X₂ ⟶ B.obj X₃), CategoryTheory.IsConnected (w.CostructuredArrowDownwards g)
instance
CategoryTheory.TwoSquare.instIsConnectedStructuredArrowCostructuredArrowObjCostructuredArrowRightwardsOfGuitartExact
{C₁ : Type u₁}
{C₂ : Type u₂}
{C₃ : Type u₃}
{C₄ : Type u₄}
[CategoryTheory.Category.{v₁, u₁} C₁]
[CategoryTheory.Category.{v₂, u₂} C₂]
[CategoryTheory.Category.{v₃, u₃} C₃]
[CategoryTheory.Category.{v₄, u₄} C₄]
{T : CategoryTheory.Functor C₁ C₂}
{L : CategoryTheory.Functor C₁ C₃}
{R : CategoryTheory.Functor C₂ C₄}
{B : CategoryTheory.Functor C₃ C₄}
(w : CategoryTheory.TwoSquare T L R B)
[hw : w.GuitartExact]
{X₃ : C₃}
(g : CategoryTheory.CostructuredArrow R (B.obj X₃))
:
CategoryTheory.IsConnected (CategoryTheory.StructuredArrow g (w.costructuredArrowRightwards X₃))
Equations
- ⋯ = ⋯
instance
CategoryTheory.TwoSquare.instIsConnectedCostructuredArrowStructuredArrowObjStructuredArrowDownwardsOfGuitartExact
{C₁ : Type u₁}
{C₂ : Type u₂}
{C₃ : Type u₃}
{C₄ : Type u₄}
[CategoryTheory.Category.{v₁, u₁} C₁]
[CategoryTheory.Category.{v₂, u₂} C₂]
[CategoryTheory.Category.{v₃, u₃} C₃]
[CategoryTheory.Category.{v₄, u₄} C₄]
{T : CategoryTheory.Functor C₁ C₂}
{L : CategoryTheory.Functor C₁ C₃}
{R : CategoryTheory.Functor C₂ C₄}
{B : CategoryTheory.Functor C₃ C₄}
(w : CategoryTheory.TwoSquare T L R B)
[hw : w.GuitartExact]
{X₂ : C₂}
(g : CategoryTheory.StructuredArrow (R.obj X₂) B)
:
CategoryTheory.IsConnected (CategoryTheory.CostructuredArrow (w.structuredArrowDownwards X₂) g)
Equations
- ⋯ = ⋯
theorem
CategoryTheory.TwoSquare.guitartExact_iff_final
{C₁ : Type u₁}
{C₂ : Type u₂}
{C₃ : Type u₃}
{C₄ : Type u₄}
[CategoryTheory.Category.{v₁, u₁} C₁]
[CategoryTheory.Category.{v₂, u₂} C₂]
[CategoryTheory.Category.{v₃, u₃} C₃]
[CategoryTheory.Category.{v₄, u₄} C₄]
{T : CategoryTheory.Functor C₁ C₂}
{L : CategoryTheory.Functor C₁ C₃}
{R : CategoryTheory.Functor C₂ C₄}
{B : CategoryTheory.Functor C₃ C₄}
(w : CategoryTheory.TwoSquare T L R B)
:
w.GuitartExact ↔ ∀ (X₃ : C₃), (w.costructuredArrowRightwards X₃).Final
instance
CategoryTheory.TwoSquare.instFinalCostructuredArrowObjCostructuredArrowRightwardsOfGuitartExact
{C₁ : Type u₁}
{C₂ : Type u₂}
{C₃ : Type u₃}
{C₄ : Type u₄}
[CategoryTheory.Category.{v₁, u₁} C₁]
[CategoryTheory.Category.{v₂, u₂} C₂]
[CategoryTheory.Category.{v₃, u₃} C₃]
[CategoryTheory.Category.{v₄, u₄} C₄]
{T : CategoryTheory.Functor C₁ C₂}
{L : CategoryTheory.Functor C₁ C₃}
{R : CategoryTheory.Functor C₂ C₄}
{B : CategoryTheory.Functor C₃ C₄}
(w : CategoryTheory.TwoSquare T L R B)
[hw : w.GuitartExact]
(X₃ : C₃)
:
(w.costructuredArrowRightwards X₃).Final
Equations
- ⋯ = ⋯
theorem
CategoryTheory.TwoSquare.guitartExact_iff_initial
{C₁ : Type u₁}
{C₂ : Type u₂}
{C₃ : Type u₃}
{C₄ : Type u₄}
[CategoryTheory.Category.{v₁, u₁} C₁]
[CategoryTheory.Category.{v₂, u₂} C₂]
[CategoryTheory.Category.{v₃, u₃} C₃]
[CategoryTheory.Category.{v₄, u₄} C₄]
{T : CategoryTheory.Functor C₁ C₂}
{L : CategoryTheory.Functor C₁ C₃}
{R : CategoryTheory.Functor C₂ C₄}
{B : CategoryTheory.Functor C₃ C₄}
(w : CategoryTheory.TwoSquare T L R B)
:
w.GuitartExact ↔ ∀ (X₂ : C₂), (w.structuredArrowDownwards X₂).Initial
instance
CategoryTheory.TwoSquare.instInitialStructuredArrowObjStructuredArrowDownwardsOfGuitartExact
{C₁ : Type u₁}
{C₂ : Type u₂}
{C₃ : Type u₃}
{C₄ : Type u₄}
[CategoryTheory.Category.{v₁, u₁} C₁]
[CategoryTheory.Category.{v₂, u₂} C₂]
[CategoryTheory.Category.{v₃, u₃} C₃]
[CategoryTheory.Category.{v₄, u₄} C₄]
{T : CategoryTheory.Functor C₁ C₂}
{L : CategoryTheory.Functor C₁ C₃}
{R : CategoryTheory.Functor C₂ C₄}
{B : CategoryTheory.Functor C₃ C₄}
(w : CategoryTheory.TwoSquare T L R B)
[hw : w.GuitartExact]
(X₂ : C₂)
:
(w.structuredArrowDownwards X₂).Initial
Equations
- ⋯ = ⋯
@[instance 100]
instance
CategoryTheory.TwoSquare.guitartExact_of_isEquivalence_of_isIso
{C₁ : Type u₁}
{C₂ : Type u₂}
{C₃ : Type u₃}
{C₄ : Type u₄}
[CategoryTheory.Category.{v₁, u₁} C₁]
[CategoryTheory.Category.{v₂, u₂} C₂]
[CategoryTheory.Category.{v₃, u₃} C₃]
[CategoryTheory.Category.{v₄, u₄} C₄]
{T : CategoryTheory.Functor C₁ C₂}
{L : CategoryTheory.Functor C₁ C₃}
{R : CategoryTheory.Functor C₂ C₄}
{B : CategoryTheory.Functor C₃ C₄}
(w : CategoryTheory.TwoSquare T L R B)
[L.IsEquivalence]
[R.IsEquivalence]
[CategoryTheory.IsIso w]
:
w.GuitartExact
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.
Equations
- ⋯ = ⋯
instance
CategoryTheory.TwoSquare.guitartExact_id
{C₁ : Type u₁}
{C₂ : Type u₂}
[CategoryTheory.Category.{v₁, u₁} C₁]
[CategoryTheory.Category.{v₂, u₂} C₂]
(F : CategoryTheory.Functor C₁ C₂)
:
(CategoryTheory.TwoSquare.mk (CategoryTheory.Functor.id C₁) F F (CategoryTheory.Functor.id C₂)
(CategoryTheory.CategoryStruct.id F)).GuitartExact
Equations
- ⋯ = ⋯