Pullbacks #
We define a category WalkingCospan (resp. WalkingSpan), which is the index category
for the given data for a pullback (resp. pushout) diagram. Convenience methods cospan f g
and span f g construct functors from the walking (co)span, hitting the given morphisms.
We define pullback f g and pushout f g as limits and colimits of such functors.
References #
@[inline, reducible]
The type of objects for the diagram indexing a pullback, defined as a special case of
WidePullbackShape.
Instances For
@[match_pattern, inline, reducible]
The left point of the walking cospan.
Instances For
@[match_pattern, inline, reducible]
The right point of the walking cospan.
Instances For
@[match_pattern, inline, reducible]
The central point of the walking cospan.
Instances For
@[inline, reducible]
The type of objects for the diagram indexing a pushout, defined as a special case of
WidePushoutShape.
Instances For
@[match_pattern, inline, reducible]
The left point of the walking span.
Instances For
@[match_pattern, inline, reducible]
The right point of the walking span.
Instances For
@[match_pattern, inline, reducible]
The central point of the walking span.
Instances For
@[inline, reducible]
The type of arrows for the diagram indexing a pullback.
Instances For
@[match_pattern, inline, reducible]
The left arrow of the walking cospan.
Instances For
@[match_pattern, inline, reducible]
The right arrow of the walking cospan.
Instances For
@[match_pattern, inline, reducible]
The identity arrows of the walking cospan.
Instances For
@[inline, reducible]
The type of arrows for the diagram indexing a pushout.
Instances For
@[match_pattern, inline, reducible]
The left arrow of the walking span.
Instances For
@[match_pattern, inline, reducible]
The right arrow of the walking span.
Instances For
@[match_pattern, inline, reducible]
The identity arrows of the walking span.
Instances For
def
CategoryTheory.Limits.WalkingCospan.ext
{C : Type u}
[CategoryTheory.Category.{v, u} C]
{F : CategoryTheory.Functor CategoryTheory.Limits.WalkingCospan C}
{s : CategoryTheory.Limits.Cone F}
{t : CategoryTheory.Limits.Cone F}
(i : s.pt ≅ t.pt)
(w₁ : s.π.app CategoryTheory.Limits.WalkingCospan.left = CategoryTheory.CategoryStruct.comp i.hom (t.π.app CategoryTheory.Limits.WalkingCospan.left))
(w₂ : s.π.app CategoryTheory.Limits.WalkingCospan.right = CategoryTheory.CategoryStruct.comp i.hom (t.π.app CategoryTheory.Limits.WalkingCospan.right))
:
s ≅ t
To construct an isomorphism of cones over the walking cospan,
it suffices to construct an isomorphism
of the cone points and check it commutes with the legs to left and right.
Instances For
def
CategoryTheory.Limits.WalkingSpan.ext
{C : Type u}
[CategoryTheory.Category.{v, u} C]
{F : CategoryTheory.Functor CategoryTheory.Limits.WalkingSpan C}
{s : CategoryTheory.Limits.Cocone F}
{t : CategoryTheory.Limits.Cocone F}
(i : s.pt ≅ t.pt)
(w₁ : CategoryTheory.CategoryStruct.comp (s.ι.app CategoryTheory.Limits.WalkingCospan.left) i.hom = t.ι.app CategoryTheory.Limits.WalkingCospan.left)
(w₂ : CategoryTheory.CategoryStruct.comp (s.ι.app CategoryTheory.Limits.WalkingCospan.right) i.hom = t.ι.app CategoryTheory.Limits.WalkingCospan.right)
:
s ≅ t
To construct an isomorphism of cocones over the walking span,
it suffices to construct an isomorphism
of the cocone points and check it commutes with the legs from left and right.
Instances For
def
CategoryTheory.Limits.cospan
{C : Type u}
[CategoryTheory.Category.{v, u} C]
{X : C}
{Y : C}
{Z : C}
(f : X ⟶ Z)
(g : Y ⟶ Z)
:
cospan f g is the functor from the walking cospan hitting f and g.
Instances For
def
CategoryTheory.Limits.span
{C : Type u}
[CategoryTheory.Category.{v, u} C]
{X : C}
{Y : C}
{Z : C}
(f : X ⟶ Y)
(g : X ⟶ Z)
:
span f g is the functor from the walking span hitting f and g.
Instances For
@[simp]
theorem
CategoryTheory.Limits.cospan_left
{C : Type u}
[CategoryTheory.Category.{v, u} C]
{X : C}
{Y : C}
{Z : C}
(f : X ⟶ Z)
(g : Y ⟶ Z)
:
@[simp]
theorem
CategoryTheory.Limits.span_left
{C : Type u}
[CategoryTheory.Category.{v, u} C]
{X : C}
{Y : C}
{Z : C}
(f : X ⟶ Y)
(g : X ⟶ Z)
:
@[simp]
theorem
CategoryTheory.Limits.cospan_right
{C : Type u}
[CategoryTheory.Category.{v, u} C]
{X : C}
{Y : C}
{Z : C}
(f : X ⟶ Z)
(g : Y ⟶ Z)
:
@[simp]
theorem
CategoryTheory.Limits.span_right
{C : Type u}
[CategoryTheory.Category.{v, u} C]
{X : C}
{Y : C}
{Z : C}
(f : X ⟶ Y)
(g : X ⟶ Z)
:
@[simp]
theorem
CategoryTheory.Limits.cospan_one
{C : Type u}
[CategoryTheory.Category.{v, u} C]
{X : C}
{Y : C}
{Z : C}
(f : X ⟶ Z)
(g : Y ⟶ Z)
:
@[simp]
theorem
CategoryTheory.Limits.span_zero
{C : Type u}
[CategoryTheory.Category.{v, u} C]
{X : C}
{Y : C}
{Z : C}
(f : X ⟶ Y)
(g : X ⟶ Z)
:
@[simp]
theorem
CategoryTheory.Limits.cospan_map_inl
{C : Type u}
[CategoryTheory.Category.{v, u} C]
{X : C}
{Y : C}
{Z : C}
(f : X ⟶ Z)
(g : Y ⟶ Z)
:
@[simp]
theorem
CategoryTheory.Limits.span_map_fst
{C : Type u}
[CategoryTheory.Category.{v, u} C]
{X : C}
{Y : C}
{Z : C}
(f : X ⟶ Y)
(g : X ⟶ Z)
:
@[simp]
theorem
CategoryTheory.Limits.cospan_map_inr
{C : Type u}
[CategoryTheory.Category.{v, u} C]
{X : C}
{Y : C}
{Z : C}
(f : X ⟶ Z)
(g : Y ⟶ Z)
:
@[simp]
theorem
CategoryTheory.Limits.span_map_snd
{C : Type u}
[CategoryTheory.Category.{v, u} C]
{X : C}
{Y : C}
{Z : C}
(f : X ⟶ Y)
(g : X ⟶ Z)
:
theorem
CategoryTheory.Limits.cospan_map_id
{C : Type u}
[CategoryTheory.Category.{v, u} C]
{X : C}
{Y : C}
{Z : C}
(f : X ⟶ Z)
(g : Y ⟶ Z)
(w : CategoryTheory.Limits.WalkingCospan)
:
theorem
CategoryTheory.Limits.span_map_id
{C : Type u}
[CategoryTheory.Category.{v, u} C]
{X : C}
{Y : C}
{Z : C}
(f : X ⟶ Y)
(g : X ⟶ Z)
(w : CategoryTheory.Limits.WalkingSpan)
:
(CategoryTheory.Limits.span f g).map (CategoryTheory.Limits.WalkingSpan.Hom.id w) = CategoryTheory.CategoryStruct.id ((CategoryTheory.Limits.span f g).obj w)
@[simp]
theorem
CategoryTheory.Limits.diagramIsoCospan_inv_app
{C : Type u}
[CategoryTheory.Category.{v, u} C]
(F : CategoryTheory.Functor CategoryTheory.Limits.WalkingCospan C)
(X : CategoryTheory.Limits.WalkingCospan)
:
(CategoryTheory.Limits.diagramIsoCospan F).inv.app X = CategoryTheory.eqToHom
(_ :
(CategoryTheory.Limits.cospan (F.map CategoryTheory.Limits.WalkingCospan.Hom.inl)
(F.map CategoryTheory.Limits.WalkingCospan.Hom.inr)).obj
X = F.obj X)
@[simp]
theorem
CategoryTheory.Limits.diagramIsoCospan_hom_app
{C : Type u}
[CategoryTheory.Category.{v, u} C]
(F : CategoryTheory.Functor CategoryTheory.Limits.WalkingCospan C)
(X : CategoryTheory.Limits.WalkingCospan)
:
(CategoryTheory.Limits.diagramIsoCospan F).hom.app X = CategoryTheory.eqToHom
(_ :
F.obj X = (CategoryTheory.Limits.cospan (F.map CategoryTheory.Limits.WalkingCospan.Hom.inl)
(F.map CategoryTheory.Limits.WalkingCospan.Hom.inr)).obj
X)
def
CategoryTheory.Limits.diagramIsoCospan
{C : Type u}
[CategoryTheory.Category.{v, u} C]
(F : CategoryTheory.Functor CategoryTheory.Limits.WalkingCospan C)
:
Every diagram indexing a pullback is naturally isomorphic (actually, equal) to a cospan
Instances For
@[simp]
theorem
CategoryTheory.Limits.diagramIsoSpan_inv_app
{C : Type u}
[CategoryTheory.Category.{v, u} C]
(F : CategoryTheory.Functor CategoryTheory.Limits.WalkingSpan C)
(X : CategoryTheory.Limits.WalkingSpan)
:
(CategoryTheory.Limits.diagramIsoSpan F).inv.app X = CategoryTheory.eqToHom
(_ :
(CategoryTheory.Limits.span (F.map CategoryTheory.Limits.WalkingSpan.Hom.fst)
(F.map CategoryTheory.Limits.WalkingSpan.Hom.snd)).obj
X = F.obj X)
@[simp]
theorem
CategoryTheory.Limits.diagramIsoSpan_hom_app
{C : Type u}
[CategoryTheory.Category.{v, u} C]
(F : CategoryTheory.Functor CategoryTheory.Limits.WalkingSpan C)
(X : CategoryTheory.Limits.WalkingSpan)
:
(CategoryTheory.Limits.diagramIsoSpan F).hom.app X = CategoryTheory.eqToHom
(_ :
F.obj X = (CategoryTheory.Limits.span (F.map CategoryTheory.Limits.WalkingSpan.Hom.fst)
(F.map CategoryTheory.Limits.WalkingSpan.Hom.snd)).obj
X)
def
CategoryTheory.Limits.diagramIsoSpan
{C : Type u}
[CategoryTheory.Category.{v, u} C]
(F : CategoryTheory.Functor CategoryTheory.Limits.WalkingSpan C)
:
Every diagram indexing a pushout is naturally isomorphic (actually, equal) to a span
Instances For
def
CategoryTheory.Limits.cospanCompIso
{C : Type u}
[CategoryTheory.Category.{v, u} C]
{D : Type u₂}
[CategoryTheory.Category.{v₂, u₂} D]
(F : CategoryTheory.Functor C D)
{X : C}
{Y : C}
{Z : C}
(f : X ⟶ Z)
(g : Y ⟶ Z)
:
CategoryTheory.Functor.comp (CategoryTheory.Limits.cospan f g) F ≅ CategoryTheory.Limits.cospan (F.map f) (F.map g)
A functor applied to a cospan is a cospan.
Instances For
@[simp]
theorem
CategoryTheory.Limits.cospanCompIso_app_left
{C : Type u}
[CategoryTheory.Category.{v, u} C]
{D : Type u₂}
[CategoryTheory.Category.{v₂, u₂} D]
(F : CategoryTheory.Functor C D)
{X : C}
{Y : C}
{Z : C}
(f : X ⟶ Z)
(g : Y ⟶ Z)
:
@[simp]
theorem
CategoryTheory.Limits.cospanCompIso_app_right
{C : Type u}
[CategoryTheory.Category.{v, u} C]
{D : Type u₂}
[CategoryTheory.Category.{v₂, u₂} D]
(F : CategoryTheory.Functor C D)
{X : C}
{Y : C}
{Z : C}
(f : X ⟶ Z)
(g : Y ⟶ Z)
:
@[simp]
theorem
CategoryTheory.Limits.cospanCompIso_app_one
{C : Type u}
[CategoryTheory.Category.{v, u} C]
{D : Type u₂}
[CategoryTheory.Category.{v₂, u₂} D]
(F : CategoryTheory.Functor C D)
{X : C}
{Y : C}
{Z : C}
(f : X ⟶ Z)
(g : Y ⟶ Z)
:
@[simp]
theorem
CategoryTheory.Limits.cospanCompIso_hom_app_left
{C : Type u}
[CategoryTheory.Category.{v, u} C]
{D : Type u₂}
[CategoryTheory.Category.{v₂, u₂} D]
(F : CategoryTheory.Functor C D)
{X : C}
{Y : C}
{Z : C}
(f : X ⟶ Z)
(g : Y ⟶ Z)
:
@[simp]
theorem
CategoryTheory.Limits.cospanCompIso_hom_app_right
{C : Type u}
[CategoryTheory.Category.{v, u} C]
{D : Type u₂}
[CategoryTheory.Category.{v₂, u₂} D]
(F : CategoryTheory.Functor C D)
{X : C}
{Y : C}
{Z : C}
(f : X ⟶ Z)
(g : Y ⟶ Z)
:
@[simp]
theorem
CategoryTheory.Limits.cospanCompIso_hom_app_one
{C : Type u}
[CategoryTheory.Category.{v, u} C]
{D : Type u₂}
[CategoryTheory.Category.{v₂, u₂} D]
(F : CategoryTheory.Functor C D)
{X : C}
{Y : C}
{Z : C}
(f : X ⟶ Z)
(g : Y ⟶ Z)
:
@[simp]
theorem
CategoryTheory.Limits.cospanCompIso_inv_app_left
{C : Type u}
[CategoryTheory.Category.{v, u} C]
{D : Type u₂}
[CategoryTheory.Category.{v₂, u₂} D]
(F : CategoryTheory.Functor C D)
{X : C}
{Y : C}
{Z : C}
(f : X ⟶ Z)
(g : Y ⟶ Z)
:
(CategoryTheory.Limits.cospanCompIso F f g).inv.app CategoryTheory.Limits.WalkingCospan.left = CategoryTheory.CategoryStruct.id
((CategoryTheory.Limits.cospan (F.map f) (F.map g)).obj CategoryTheory.Limits.WalkingCospan.left)
@[simp]
theorem
CategoryTheory.Limits.cospanCompIso_inv_app_right
{C : Type u}
[CategoryTheory.Category.{v, u} C]
{D : Type u₂}
[CategoryTheory.Category.{v₂, u₂} D]
(F : CategoryTheory.Functor C D)
{X : C}
{Y : C}
{Z : C}
(f : X ⟶ Z)
(g : Y ⟶ Z)
:
(CategoryTheory.Limits.cospanCompIso F f g).inv.app CategoryTheory.Limits.WalkingCospan.right = CategoryTheory.CategoryStruct.id
((CategoryTheory.Limits.cospan (F.map f) (F.map g)).obj CategoryTheory.Limits.WalkingCospan.right)
@[simp]
theorem
CategoryTheory.Limits.cospanCompIso_inv_app_one
{C : Type u}
[CategoryTheory.Category.{v, u} C]
{D : Type u₂}
[CategoryTheory.Category.{v₂, u₂} D]
(F : CategoryTheory.Functor C D)
{X : C}
{Y : C}
{Z : C}
(f : X ⟶ Z)
(g : Y ⟶ Z)
:
(CategoryTheory.Limits.cospanCompIso F f g).inv.app CategoryTheory.Limits.WalkingCospan.one = CategoryTheory.CategoryStruct.id
((CategoryTheory.Limits.cospan (F.map f) (F.map g)).obj CategoryTheory.Limits.WalkingCospan.one)
def
CategoryTheory.Limits.spanCompIso
{C : Type u}
[CategoryTheory.Category.{v, u} C]
{D : Type u₂}
[CategoryTheory.Category.{v₂, u₂} D]
(F : CategoryTheory.Functor C D)
{X : C}
{Y : C}
{Z : C}
(f : X ⟶ Y)
(g : X ⟶ Z)
:
CategoryTheory.Functor.comp (CategoryTheory.Limits.span f g) F ≅ CategoryTheory.Limits.span (F.map f) (F.map g)
A functor applied to a span is a span.
Instances For
@[simp]
theorem
CategoryTheory.Limits.spanCompIso_app_left
{C : Type u}
[CategoryTheory.Category.{v, u} C]
{D : Type u₂}
[CategoryTheory.Category.{v₂, u₂} D]
(F : CategoryTheory.Functor C D)
{X : C}
{Y : C}
{Z : C}
(f : X ⟶ Y)
(g : X ⟶ Z)
:
@[simp]
theorem
CategoryTheory.Limits.spanCompIso_app_right
{C : Type u}
[CategoryTheory.Category.{v, u} C]
{D : Type u₂}
[CategoryTheory.Category.{v₂, u₂} D]
(F : CategoryTheory.Functor C D)
{X : C}
{Y : C}
{Z : C}
(f : X ⟶ Y)
(g : X ⟶ Z)
:
@[simp]
theorem
CategoryTheory.Limits.spanCompIso_app_zero
{C : Type u}
[CategoryTheory.Category.{v, u} C]
{D : Type u₂}
[CategoryTheory.Category.{v₂, u₂} D]
(F : CategoryTheory.Functor C D)
{X : C}
{Y : C}
{Z : C}
(f : X ⟶ Y)
(g : X ⟶ Z)
:
@[simp]
theorem
CategoryTheory.Limits.spanCompIso_hom_app_left
{C : Type u}
[CategoryTheory.Category.{v, u} C]
{D : Type u₂}
[CategoryTheory.Category.{v₂, u₂} D]
(F : CategoryTheory.Functor C D)
{X : C}
{Y : C}
{Z : C}
(f : X ⟶ Y)
(g : X ⟶ Z)
:
@[simp]
theorem
CategoryTheory.Limits.spanCompIso_hom_app_right
{C : Type u}
[CategoryTheory.Category.{v, u} C]
{D : Type u₂}
[CategoryTheory.Category.{v₂, u₂} D]
(F : CategoryTheory.Functor C D)
{X : C}
{Y : C}
{Z : C}
(f : X ⟶ Y)
(g : X ⟶ Z)
:
@[simp]
theorem
CategoryTheory.Limits.spanCompIso_hom_app_zero
{C : Type u}
[CategoryTheory.Category.{v, u} C]
{D : Type u₂}
[CategoryTheory.Category.{v₂, u₂} D]
(F : CategoryTheory.Functor C D)
{X : C}
{Y : C}
{Z : C}
(f : X ⟶ Y)
(g : X ⟶ Z)
:
@[simp]
theorem
CategoryTheory.Limits.spanCompIso_inv_app_left
{C : Type u}
[CategoryTheory.Category.{v, u} C]
{D : Type u₂}
[CategoryTheory.Category.{v₂, u₂} D]
(F : CategoryTheory.Functor C D)
{X : C}
{Y : C}
{Z : C}
(f : X ⟶ Y)
(g : X ⟶ Z)
:
(CategoryTheory.Limits.spanCompIso F f g).inv.app CategoryTheory.Limits.WalkingSpan.left = CategoryTheory.CategoryStruct.id
((CategoryTheory.Limits.span (F.map f) (F.map g)).obj CategoryTheory.Limits.WalkingSpan.left)
@[simp]
theorem
CategoryTheory.Limits.spanCompIso_inv_app_right
{C : Type u}
[CategoryTheory.Category.{v, u} C]
{D : Type u₂}
[CategoryTheory.Category.{v₂, u₂} D]
(F : CategoryTheory.Functor C D)
{X : C}
{Y : C}
{Z : C}
(f : X ⟶ Y)
(g : X ⟶ Z)
:
(CategoryTheory.Limits.spanCompIso F f g).inv.app CategoryTheory.Limits.WalkingSpan.right = CategoryTheory.CategoryStruct.id
((CategoryTheory.Limits.span (F.map f) (F.map g)).obj CategoryTheory.Limits.WalkingSpan.right)
@[simp]
theorem
CategoryTheory.Limits.spanCompIso_inv_app_zero
{C : Type u}
[CategoryTheory.Category.{v, u} C]
{D : Type u₂}
[CategoryTheory.Category.{v₂, u₂} D]
(F : CategoryTheory.Functor C D)
{X : C}
{Y : C}
{Z : C}
(f : X ⟶ Y)
(g : X ⟶ Z)
:
(CategoryTheory.Limits.spanCompIso F f g).inv.app CategoryTheory.Limits.WalkingSpan.zero = CategoryTheory.CategoryStruct.id
((CategoryTheory.Limits.span (F.map f) (F.map g)).obj CategoryTheory.Limits.WalkingSpan.zero)
def
CategoryTheory.Limits.cospanExt
{C : Type u}
[CategoryTheory.Category.{v, u} C]
{X : C}
{Y : C}
{Z : C}
{X' : C}
{Y' : C}
{Z' : C}
(iX : X ≅ X')
(iY : Y ≅ Y')
(iZ : Z ≅ Z')
{f : X ⟶ Z}
{g : Y ⟶ Z}
{f' : X' ⟶ Z'}
{g' : Y' ⟶ Z'}
(wf : CategoryTheory.CategoryStruct.comp iX.hom f' = CategoryTheory.CategoryStruct.comp f iZ.hom)
(wg : CategoryTheory.CategoryStruct.comp iY.hom g' = CategoryTheory.CategoryStruct.comp g iZ.hom)
:
Construct an isomorphism of cospans from components.
Instances For
@[simp]
theorem
CategoryTheory.Limits.cospanExt_app_left
{C : Type u}
[CategoryTheory.Category.{v, u} C]
{X : C}
{Y : C}
{Z : C}
{X' : C}
{Y' : C}
{Z' : C}
(iX : X ≅ X')
(iY : Y ≅ Y')
(iZ : Z ≅ Z')
{f : X ⟶ Z}
{g : Y ⟶ Z}
{f' : X' ⟶ Z'}
{g' : Y' ⟶ Z'}
(wf : CategoryTheory.CategoryStruct.comp iX.hom f' = CategoryTheory.CategoryStruct.comp f iZ.hom)
(wg : CategoryTheory.CategoryStruct.comp iY.hom g' = CategoryTheory.CategoryStruct.comp g iZ.hom)
:
(CategoryTheory.Limits.cospanExt iX iY iZ wf wg).app CategoryTheory.Limits.WalkingCospan.left = iX
@[simp]
theorem
CategoryTheory.Limits.cospanExt_app_right
{C : Type u}
[CategoryTheory.Category.{v, u} C]
{X : C}
{Y : C}
{Z : C}
{X' : C}
{Y' : C}
{Z' : C}
(iX : X ≅ X')
(iY : Y ≅ Y')
(iZ : Z ≅ Z')
{f : X ⟶ Z}
{g : Y ⟶ Z}
{f' : X' ⟶ Z'}
{g' : Y' ⟶ Z'}
(wf : CategoryTheory.CategoryStruct.comp iX.hom f' = CategoryTheory.CategoryStruct.comp f iZ.hom)
(wg : CategoryTheory.CategoryStruct.comp iY.hom g' = CategoryTheory.CategoryStruct.comp g iZ.hom)
:
(CategoryTheory.Limits.cospanExt iX iY iZ wf wg).app CategoryTheory.Limits.WalkingCospan.right = iY
@[simp]
theorem
CategoryTheory.Limits.cospanExt_app_one
{C : Type u}
[CategoryTheory.Category.{v, u} C]
{X : C}
{Y : C}
{Z : C}
{X' : C}
{Y' : C}
{Z' : C}
(iX : X ≅ X')
(iY : Y ≅ Y')
(iZ : Z ≅ Z')
{f : X ⟶ Z}
{g : Y ⟶ Z}
{f' : X' ⟶ Z'}
{g' : Y' ⟶ Z'}
(wf : CategoryTheory.CategoryStruct.comp iX.hom f' = CategoryTheory.CategoryStruct.comp f iZ.hom)
(wg : CategoryTheory.CategoryStruct.comp iY.hom g' = CategoryTheory.CategoryStruct.comp g iZ.hom)
:
(CategoryTheory.Limits.cospanExt iX iY iZ wf wg).app CategoryTheory.Limits.WalkingCospan.one = iZ
@[simp]
theorem
CategoryTheory.Limits.cospanExt_hom_app_left
{C : Type u}
[CategoryTheory.Category.{v, u} C]
{X : C}
{Y : C}
{Z : C}
{X' : C}
{Y' : C}
{Z' : C}
(iX : X ≅ X')
(iY : Y ≅ Y')
(iZ : Z ≅ Z')
{f : X ⟶ Z}
{g : Y ⟶ Z}
{f' : X' ⟶ Z'}
{g' : Y' ⟶ Z'}
(wf : CategoryTheory.CategoryStruct.comp iX.hom f' = CategoryTheory.CategoryStruct.comp f iZ.hom)
(wg : CategoryTheory.CategoryStruct.comp iY.hom g' = CategoryTheory.CategoryStruct.comp g iZ.hom)
:
(CategoryTheory.Limits.cospanExt iX iY iZ wf wg).hom.app CategoryTheory.Limits.WalkingCospan.left = iX.hom
@[simp]
theorem
CategoryTheory.Limits.cospanExt_hom_app_right
{C : Type u}
[CategoryTheory.Category.{v, u} C]
{X : C}
{Y : C}
{Z : C}
{X' : C}
{Y' : C}
{Z' : C}
(iX : X ≅ X')
(iY : Y ≅ Y')
(iZ : Z ≅ Z')
{f : X ⟶ Z}
{g : Y ⟶ Z}
{f' : X' ⟶ Z'}
{g' : Y' ⟶ Z'}
(wf : CategoryTheory.CategoryStruct.comp iX.hom f' = CategoryTheory.CategoryStruct.comp f iZ.hom)
(wg : CategoryTheory.CategoryStruct.comp iY.hom g' = CategoryTheory.CategoryStruct.comp g iZ.hom)
:
(CategoryTheory.Limits.cospanExt iX iY iZ wf wg).hom.app CategoryTheory.Limits.WalkingCospan.right = iY.hom
@[simp]
theorem
CategoryTheory.Limits.cospanExt_hom_app_one
{C : Type u}
[CategoryTheory.Category.{v, u} C]
{X : C}
{Y : C}
{Z : C}
{X' : C}
{Y' : C}
{Z' : C}
(iX : X ≅ X')
(iY : Y ≅ Y')
(iZ : Z ≅ Z')
{f : X ⟶ Z}
{g : Y ⟶ Z}
{f' : X' ⟶ Z'}
{g' : Y' ⟶ Z'}
(wf : CategoryTheory.CategoryStruct.comp iX.hom f' = CategoryTheory.CategoryStruct.comp f iZ.hom)
(wg : CategoryTheory.CategoryStruct.comp iY.hom g' = CategoryTheory.CategoryStruct.comp g iZ.hom)
:
(CategoryTheory.Limits.cospanExt iX iY iZ wf wg).hom.app CategoryTheory.Limits.WalkingCospan.one = iZ.hom
@[simp]
theorem
CategoryTheory.Limits.cospanExt_inv_app_left
{C : Type u}
[CategoryTheory.Category.{v, u} C]
{X : C}
{Y : C}
{Z : C}
{X' : C}
{Y' : C}
{Z' : C}
(iX : X ≅ X')
(iY : Y ≅ Y')
(iZ : Z ≅ Z')
{f : X ⟶ Z}
{g : Y ⟶ Z}
{f' : X' ⟶ Z'}
{g' : Y' ⟶ Z'}
(wf : CategoryTheory.CategoryStruct.comp iX.hom f' = CategoryTheory.CategoryStruct.comp f iZ.hom)
(wg : CategoryTheory.CategoryStruct.comp iY.hom g' = CategoryTheory.CategoryStruct.comp g iZ.hom)
:
(CategoryTheory.Limits.cospanExt iX iY iZ wf wg).inv.app CategoryTheory.Limits.WalkingCospan.left = iX.inv
@[simp]
theorem
CategoryTheory.Limits.cospanExt_inv_app_right
{C : Type u}
[CategoryTheory.Category.{v, u} C]
{X : C}
{Y : C}
{Z : C}
{X' : C}
{Y' : C}
{Z' : C}
(iX : X ≅ X')
(iY : Y ≅ Y')
(iZ : Z ≅ Z')
{f : X ⟶ Z}
{g : Y ⟶ Z}
{f' : X' ⟶ Z'}
{g' : Y' ⟶ Z'}
(wf : CategoryTheory.CategoryStruct.comp iX.hom f' = CategoryTheory.CategoryStruct.comp f iZ.hom)
(wg : CategoryTheory.CategoryStruct.comp iY.hom g' = CategoryTheory.CategoryStruct.comp g iZ.hom)
:
(CategoryTheory.Limits.cospanExt iX iY iZ wf wg).inv.app CategoryTheory.Limits.WalkingCospan.right = iY.inv
@[simp]
theorem
CategoryTheory.Limits.cospanExt_inv_app_one
{C : Type u}
[CategoryTheory.Category.{v, u} C]
{X : C}
{Y : C}
{Z : C}
{X' : C}
{Y' : C}
{Z' : C}
(iX : X ≅ X')
(iY : Y ≅ Y')
(iZ : Z ≅ Z')
{f : X ⟶ Z}
{g : Y ⟶ Z}
{f' : X' ⟶ Z'}
{g' : Y' ⟶ Z'}
(wf : CategoryTheory.CategoryStruct.comp iX.hom f' = CategoryTheory.CategoryStruct.comp f iZ.hom)
(wg : CategoryTheory.CategoryStruct.comp iY.hom g' = CategoryTheory.CategoryStruct.comp g iZ.hom)
:
(CategoryTheory.Limits.cospanExt iX iY iZ wf wg).inv.app CategoryTheory.Limits.WalkingCospan.one = iZ.inv
def
CategoryTheory.Limits.spanExt
{C : Type u}
[CategoryTheory.Category.{v, u} C]
{X : C}
{Y : C}
{Z : C}
{X' : C}
{Y' : C}
{Z' : C}
(iX : X ≅ X')
(iY : Y ≅ Y')
(iZ : Z ≅ Z')
{f : X ⟶ Y}
{g : X ⟶ Z}
{f' : X' ⟶ Y'}
{g' : X' ⟶ Z'}
(wf : CategoryTheory.CategoryStruct.comp iX.hom f' = CategoryTheory.CategoryStruct.comp f iY.hom)
(wg : CategoryTheory.CategoryStruct.comp iX.hom g' = CategoryTheory.CategoryStruct.comp g iZ.hom)
:
Construct an isomorphism of spans from components.
Instances For
@[simp]
theorem
CategoryTheory.Limits.spanExt_app_left
{C : Type u}
[CategoryTheory.Category.{v, u} C]
{X : C}
{Y : C}
{Z : C}
{X' : C}
{Y' : C}
{Z' : C}
(iX : X ≅ X')
(iY : Y ≅ Y')
(iZ : Z ≅ Z')
{f : X ⟶ Y}
{g : X ⟶ Z}
{f' : X' ⟶ Y'}
{g' : X' ⟶ Z'}
(wf : CategoryTheory.CategoryStruct.comp iX.hom f' = CategoryTheory.CategoryStruct.comp f iY.hom)
(wg : CategoryTheory.CategoryStruct.comp iX.hom g' = CategoryTheory.CategoryStruct.comp g iZ.hom)
:
(CategoryTheory.Limits.spanExt iX iY iZ wf wg).app CategoryTheory.Limits.WalkingSpan.left = iY
@[simp]
theorem
CategoryTheory.Limits.spanExt_app_right
{C : Type u}
[CategoryTheory.Category.{v, u} C]
{X : C}
{Y : C}
{Z : C}
{X' : C}
{Y' : C}
{Z' : C}
(iX : X ≅ X')
(iY : Y ≅ Y')
(iZ : Z ≅ Z')
{f : X ⟶ Y}
{g : X ⟶ Z}
{f' : X' ⟶ Y'}
{g' : X' ⟶ Z'}
(wf : CategoryTheory.CategoryStruct.comp iX.hom f' = CategoryTheory.CategoryStruct.comp f iY.hom)
(wg : CategoryTheory.CategoryStruct.comp iX.hom g' = CategoryTheory.CategoryStruct.comp g iZ.hom)
:
(CategoryTheory.Limits.spanExt iX iY iZ wf wg).app CategoryTheory.Limits.WalkingSpan.right = iZ
@[simp]
theorem
CategoryTheory.Limits.spanExt_app_one
{C : Type u}
[CategoryTheory.Category.{v, u} C]
{X : C}
{Y : C}
{Z : C}
{X' : C}
{Y' : C}
{Z' : C}
(iX : X ≅ X')
(iY : Y ≅ Y')
(iZ : Z ≅ Z')
{f : X ⟶ Y}
{g : X ⟶ Z}
{f' : X' ⟶ Y'}
{g' : X' ⟶ Z'}
(wf : CategoryTheory.CategoryStruct.comp iX.hom f' = CategoryTheory.CategoryStruct.comp f iY.hom)
(wg : CategoryTheory.CategoryStruct.comp iX.hom g' = CategoryTheory.CategoryStruct.comp g iZ.hom)
:
(CategoryTheory.Limits.spanExt iX iY iZ wf wg).app CategoryTheory.Limits.WalkingSpan.zero = iX
@[simp]
theorem
CategoryTheory.Limits.spanExt_hom_app_left
{C : Type u}
[CategoryTheory.Category.{v, u} C]
{X : C}
{Y : C}
{Z : C}
{X' : C}
{Y' : C}
{Z' : C}
(iX : X ≅ X')
(iY : Y ≅ Y')
(iZ : Z ≅ Z')
{f : X ⟶ Y}
{g : X ⟶ Z}
{f' : X' ⟶ Y'}
{g' : X' ⟶ Z'}
(wf : CategoryTheory.CategoryStruct.comp iX.hom f' = CategoryTheory.CategoryStruct.comp f iY.hom)
(wg : CategoryTheory.CategoryStruct.comp iX.hom g' = CategoryTheory.CategoryStruct.comp g iZ.hom)
:
(CategoryTheory.Limits.spanExt iX iY iZ wf wg).hom.app CategoryTheory.Limits.WalkingSpan.left = iY.hom
@[simp]
theorem
CategoryTheory.Limits.spanExt_hom_app_right
{C : Type u}
[CategoryTheory.Category.{v, u} C]
{X : C}
{Y : C}
{Z : C}
{X' : C}
{Y' : C}
{Z' : C}
(iX : X ≅ X')
(iY : Y ≅ Y')
(iZ : Z ≅ Z')
{f : X ⟶ Y}
{g : X ⟶ Z}
{f' : X' ⟶ Y'}
{g' : X' ⟶ Z'}
(wf : CategoryTheory.CategoryStruct.comp iX.hom f' = CategoryTheory.CategoryStruct.comp f iY.hom)
(wg : CategoryTheory.CategoryStruct.comp iX.hom g' = CategoryTheory.CategoryStruct.comp g iZ.hom)
:
(CategoryTheory.Limits.spanExt iX iY iZ wf wg).hom.app CategoryTheory.Limits.WalkingSpan.right = iZ.hom
@[simp]
theorem
CategoryTheory.Limits.spanExt_hom_app_zero
{C : Type u}
[CategoryTheory.Category.{v, u} C]
{X : C}
{Y : C}
{Z : C}
{X' : C}
{Y' : C}
{Z' : C}
(iX : X ≅ X')
(iY : Y ≅ Y')
(iZ : Z ≅ Z')
{f : X ⟶ Y}
{g : X ⟶ Z}
{f' : X' ⟶ Y'}
{g' : X' ⟶ Z'}
(wf : CategoryTheory.CategoryStruct.comp iX.hom f' = CategoryTheory.CategoryStruct.comp f iY.hom)
(wg : CategoryTheory.CategoryStruct.comp iX.hom g' = CategoryTheory.CategoryStruct.comp g iZ.hom)
:
(CategoryTheory.Limits.spanExt iX iY iZ wf wg).hom.app CategoryTheory.Limits.WalkingSpan.zero = iX.hom
@[simp]
theorem
CategoryTheory.Limits.spanExt_inv_app_left
{C : Type u}
[CategoryTheory.Category.{v, u} C]
{X : C}
{Y : C}
{Z : C}
{X' : C}
{Y' : C}
{Z' : C}
(iX : X ≅ X')
(iY : Y ≅ Y')
(iZ : Z ≅ Z')
{f : X ⟶ Y}
{g : X ⟶ Z}
{f' : X' ⟶ Y'}
{g' : X' ⟶ Z'}
(wf : CategoryTheory.CategoryStruct.comp iX.hom f' = CategoryTheory.CategoryStruct.comp f iY.hom)
(wg : CategoryTheory.CategoryStruct.comp iX.hom g' = CategoryTheory.CategoryStruct.comp g iZ.hom)
:
(CategoryTheory.Limits.spanExt iX iY iZ wf wg).inv.app CategoryTheory.Limits.WalkingSpan.left = iY.inv
@[simp]
theorem
CategoryTheory.Limits.spanExt_inv_app_right
{C : Type u}
[CategoryTheory.Category.{v, u} C]
{X : C}
{Y : C}
{Z : C}
{X' : C}
{Y' : C}
{Z' : C}
(iX : X ≅ X')
(iY : Y ≅ Y')
(iZ : Z ≅ Z')
{f : X ⟶ Y}
{g : X ⟶ Z}
{f' : X' ⟶ Y'}
{g' : X' ⟶ Z'}
(wf : CategoryTheory.CategoryStruct.comp iX.hom f' = CategoryTheory.CategoryStruct.comp f iY.hom)
(wg : CategoryTheory.CategoryStruct.comp iX.hom g' = CategoryTheory.CategoryStruct.comp g iZ.hom)
:
(CategoryTheory.Limits.spanExt iX iY iZ wf wg).inv.app CategoryTheory.Limits.WalkingSpan.right = iZ.inv
@[simp]
theorem
CategoryTheory.Limits.spanExt_inv_app_zero
{C : Type u}
[CategoryTheory.Category.{v, u} C]
{X : C}
{Y : C}
{Z : C}
{X' : C}
{Y' : C}
{Z' : C}
(iX : X ≅ X')
(iY : Y ≅ Y')
(iZ : Z ≅ Z')
{f : X ⟶ Y}
{g : X ⟶ Z}
{f' : X' ⟶ Y'}
{g' : X' ⟶ Z'}
(wf : CategoryTheory.CategoryStruct.comp iX.hom f' = CategoryTheory.CategoryStruct.comp f iY.hom)
(wg : CategoryTheory.CategoryStruct.comp iX.hom g' = CategoryTheory.CategoryStruct.comp g iZ.hom)
:
(CategoryTheory.Limits.spanExt iX iY iZ wf wg).inv.app CategoryTheory.Limits.WalkingSpan.zero = iX.inv
@[inline, reducible]
abbrev
CategoryTheory.Limits.PullbackCone
{C : Type u}
[CategoryTheory.Category.{v, u} C]
{X : C}
{Y : C}
{Z : C}
(f : X ⟶ Z)
(g : Y ⟶ Z)
:
Type (max u v)
A pullback cone is just a cone on the cospan formed by two morphisms f : X ⟶ Z and
g : Y ⟶ Z.
Instances For
@[inline, reducible]
abbrev
CategoryTheory.Limits.PullbackCone.fst
{C : Type u}
[CategoryTheory.Category.{v, u} C]
{X : C}
{Y : C}
{Z : C}
{f : X ⟶ Z}
{g : Y ⟶ Z}
(t : CategoryTheory.Limits.PullbackCone f g)
:
t.pt ⟶ X
The first projection of a pullback cone.
Instances For
@[inline, reducible]
abbrev
CategoryTheory.Limits.PullbackCone.snd
{C : Type u}
[CategoryTheory.Category.{v, u} C]
{X : C}
{Y : C}
{Z : C}
{f : X ⟶ Z}
{g : Y ⟶ Z}
(t : CategoryTheory.Limits.PullbackCone f g)
:
t.pt ⟶ Y
The second projection of a pullback cone.
Instances For
@[simp]
theorem
CategoryTheory.Limits.PullbackCone.π_app_left
{C : Type u}
[CategoryTheory.Category.{v, u} C]
{X : C}
{Y : C}
{Z : C}
{f : X ⟶ Z}
{g : Y ⟶ Z}
(c : CategoryTheory.Limits.PullbackCone f g)
:
@[simp]
theorem
CategoryTheory.Limits.PullbackCone.π_app_right
{C : Type u}
[CategoryTheory.Category.{v, u} C]
{X : C}
{Y : C}
{Z : C}
{f : X ⟶ Z}
{g : Y ⟶ Z}
(c : CategoryTheory.Limits.PullbackCone f g)
:
@[simp]
theorem
CategoryTheory.Limits.PullbackCone.condition_one
{C : Type u}
[CategoryTheory.Category.{v, u} C]
{X : C}
{Y : C}
{Z : C}
{f : X ⟶ Z}
{g : Y ⟶ Z}
(t : CategoryTheory.Limits.PullbackCone f g)
:
def
CategoryTheory.Limits.PullbackCone.isLimitAux
{C : Type u}
[CategoryTheory.Category.{v, u} C]
{X : C}
{Y : C}
{Z : C}
{f : X ⟶ Z}
{g : Y ⟶ Z}
(t : CategoryTheory.Limits.PullbackCone f g)
(lift : (s : CategoryTheory.Limits.PullbackCone f g) → s.pt ⟶ t.pt)
(fac_left : ∀ (s : CategoryTheory.Limits.PullbackCone f g),
CategoryTheory.CategoryStruct.comp (lift s) (CategoryTheory.Limits.PullbackCone.fst t) = CategoryTheory.Limits.PullbackCone.fst s)
(fac_right : ∀ (s : CategoryTheory.Limits.PullbackCone f g),
CategoryTheory.CategoryStruct.comp (lift s) (CategoryTheory.Limits.PullbackCone.snd t) = CategoryTheory.Limits.PullbackCone.snd s)
(uniq : ∀ (s : CategoryTheory.Limits.PullbackCone f g) (m : s.pt ⟶ t.pt),
(∀ (j : CategoryTheory.Limits.WalkingCospan), CategoryTheory.CategoryStruct.comp m (t.π.app j) = s.π.app j) →
m = lift s)
:
This is a slightly more convenient method to verify that a pullback cone is a limit cone. It only asks for a proof of facts that carry any mathematical content
Instances For
def
CategoryTheory.Limits.PullbackCone.isLimitAux'
{C : Type u}
[CategoryTheory.Category.{v, u} C]
{X : C}
{Y : C}
{Z : C}
{f : X ⟶ Z}
{g : Y ⟶ Z}
(t : CategoryTheory.Limits.PullbackCone f g)
(create : (s : CategoryTheory.Limits.PullbackCone f g) →
{ l //
CategoryTheory.CategoryStruct.comp l (CategoryTheory.Limits.PullbackCone.fst t) = CategoryTheory.Limits.PullbackCone.fst s ∧ CategoryTheory.CategoryStruct.comp l (CategoryTheory.Limits.PullbackCone.snd t) = CategoryTheory.Limits.PullbackCone.snd s ∧ ∀ {m : s.pt ⟶ t.pt},
CategoryTheory.CategoryStruct.comp m (CategoryTheory.Limits.PullbackCone.fst t) = CategoryTheory.Limits.PullbackCone.fst s →
CategoryTheory.CategoryStruct.comp m (CategoryTheory.Limits.PullbackCone.snd t) = CategoryTheory.Limits.PullbackCone.snd s →
m = l })
:
This is another convenient method to verify that a pullback cone is a limit cone. It
only asks for a proof of facts that carry any mathematical content, and allows access to the
same s for all parts.
Instances For
@[simp]
theorem
CategoryTheory.Limits.PullbackCone.mk_π_app
{C : Type u}
[CategoryTheory.Category.{v, u} C]
{X : C}
{Y : C}
{Z : C}
{f : X ⟶ Z}
{g : Y ⟶ Z}
{W : C}
(fst : W ⟶ X)
(snd : W ⟶ Y)
(eq : CategoryTheory.CategoryStruct.comp fst f = CategoryTheory.CategoryStruct.comp snd g)
(j : CategoryTheory.Limits.WalkingCospan)
:
(CategoryTheory.Limits.PullbackCone.mk fst snd eq).π.app j = Option.casesOn j (CategoryTheory.CategoryStruct.comp fst f) fun j' =>
CategoryTheory.Limits.WalkingPair.casesOn j' fst snd
@[simp]
theorem
CategoryTheory.Limits.PullbackCone.mk_pt
{C : Type u}
[CategoryTheory.Category.{v, u} C]
{X : C}
{Y : C}
{Z : C}
{f : X ⟶ Z}
{g : Y ⟶ Z}
{W : C}
(fst : W ⟶ X)
(snd : W ⟶ Y)
(eq : CategoryTheory.CategoryStruct.comp fst f = CategoryTheory.CategoryStruct.comp snd g)
:
(CategoryTheory.Limits.PullbackCone.mk fst snd eq).pt = W
def
CategoryTheory.Limits.PullbackCone.mk
{C : Type u}
[CategoryTheory.Category.{v, u} C]
{X : C}
{Y : C}
{Z : C}
{f : X ⟶ Z}
{g : Y ⟶ Z}
{W : C}
(fst : W ⟶ X)
(snd : W ⟶ Y)
(eq : CategoryTheory.CategoryStruct.comp fst f = CategoryTheory.CategoryStruct.comp snd g)
:
A pullback cone on f and g is determined by morphisms fst : W ⟶ X and snd : W ⟶ Y
such that fst ≫ f = snd ≫ g.
Instances For
@[simp]
theorem
CategoryTheory.Limits.PullbackCone.mk_π_app_left
{C : Type u}
[CategoryTheory.Category.{v, u} C]
{X : C}
{Y : C}
{Z : C}
{f : X ⟶ Z}
{g : Y ⟶ Z}
{W : C}
(fst : W ⟶ X)
(snd : W ⟶ Y)
(eq : CategoryTheory.CategoryStruct.comp fst f = CategoryTheory.CategoryStruct.comp snd g)
:
(CategoryTheory.Limits.PullbackCone.mk fst snd eq).π.app CategoryTheory.Limits.WalkingCospan.left = fst
@[simp]
theorem
CategoryTheory.Limits.PullbackCone.mk_π_app_right
{C : Type u}
[CategoryTheory.Category.{v, u} C]
{X : C}
{Y : C}
{Z : C}
{f : X ⟶ Z}
{g : Y ⟶ Z}
{W : C}
(fst : W ⟶ X)
(snd : W ⟶ Y)
(eq : CategoryTheory.CategoryStruct.comp fst f = CategoryTheory.CategoryStruct.comp snd g)
:
(CategoryTheory.Limits.PullbackCone.mk fst snd eq).π.app CategoryTheory.Limits.WalkingCospan.right = snd
@[simp]
theorem
CategoryTheory.Limits.PullbackCone.mk_π_app_one
{C : Type u}
[CategoryTheory.Category.{v, u} C]
{X : C}
{Y : C}
{Z : C}
{f : X ⟶ Z}
{g : Y ⟶ Z}
{W : C}
(fst : W ⟶ X)
(snd : W ⟶ Y)
(eq : CategoryTheory.CategoryStruct.comp fst f = CategoryTheory.CategoryStruct.comp snd g)
:
(CategoryTheory.Limits.PullbackCone.mk fst snd eq).π.app CategoryTheory.Limits.WalkingCospan.one = CategoryTheory.CategoryStruct.comp fst f
@[simp]
theorem
CategoryTheory.Limits.PullbackCone.mk_fst
{C : Type u}
[CategoryTheory.Category.{v, u} C]
{X : C}
{Y : C}
{Z : C}
{f : X ⟶ Z}
{g : Y ⟶ Z}
{W : C}
(fst : W ⟶ X)
(snd : W ⟶ Y)
(eq : CategoryTheory.CategoryStruct.comp fst f = CategoryTheory.CategoryStruct.comp snd g)
:
CategoryTheory.Limits.PullbackCone.fst (CategoryTheory.Limits.PullbackCone.mk fst snd eq) = fst
@[simp]
theorem
CategoryTheory.Limits.PullbackCone.mk_snd
{C : Type u}
[CategoryTheory.Category.{v, u} C]
{X : C}
{Y : C}
{Z : C}
{f : X ⟶ Z}
{g : Y ⟶ Z}
{W : C}
(fst : W ⟶ X)
(snd : W ⟶ Y)
(eq : CategoryTheory.CategoryStruct.comp fst f = CategoryTheory.CategoryStruct.comp snd g)
:
CategoryTheory.Limits.PullbackCone.snd (CategoryTheory.Limits.PullbackCone.mk fst snd eq) = snd
theorem
CategoryTheory.Limits.PullbackCone.condition_assoc
{C : Type u}
[CategoryTheory.Category.{v, u} C]
{X : C}
{Y : C}
{Z : C}
{f : X ⟶ Z}
{g : Y ⟶ Z}
(t : CategoryTheory.Limits.PullbackCone f g)
{Z : C}
(h : Z ⟶ Z)
:
theorem
CategoryTheory.Limits.PullbackCone.condition
{C : Type u}
[CategoryTheory.Category.{v, u} C]
{X : C}
{Y : C}
{Z : C}
{f : X ⟶ Z}
{g : Y ⟶ Z}
(t : CategoryTheory.Limits.PullbackCone f g)
:
theorem
CategoryTheory.Limits.PullbackCone.equalizer_ext
{C : Type u}
[CategoryTheory.Category.{v, u} C]
{X : C}
{Y : C}
{Z : C}
{f : X ⟶ Z}
{g : Y ⟶ Z}
(t : CategoryTheory.Limits.PullbackCone f g)
{W : C}
{k : W ⟶ t.pt}
{l : W ⟶ t.pt}
(h₀ : CategoryTheory.CategoryStruct.comp k (CategoryTheory.Limits.PullbackCone.fst t) = CategoryTheory.CategoryStruct.comp l (CategoryTheory.Limits.PullbackCone.fst t))
(h₁ : CategoryTheory.CategoryStruct.comp k (CategoryTheory.Limits.PullbackCone.snd t) = CategoryTheory.CategoryStruct.comp l (CategoryTheory.Limits.PullbackCone.snd t))
(j : CategoryTheory.Limits.WalkingCospan)
:
CategoryTheory.CategoryStruct.comp k (t.π.app j) = CategoryTheory.CategoryStruct.comp l (t.π.app j)
To check whether a morphism is equalized by the maps of a pullback cone, it suffices to check
it for fst t and snd t
theorem
CategoryTheory.Limits.PullbackCone.IsLimit.hom_ext
{C : Type u}
[CategoryTheory.Category.{v, u} C]
{X : C}
{Y : C}
{Z : C}
{f : X ⟶ Z}
{g : Y ⟶ Z}
{t : CategoryTheory.Limits.PullbackCone f g}
(ht : CategoryTheory.Limits.IsLimit t)
{W : C}
{k : W ⟶ t.pt}
{l : W ⟶ t.pt}
(h₀ : CategoryTheory.CategoryStruct.comp k (CategoryTheory.Limits.PullbackCone.fst t) = CategoryTheory.CategoryStruct.comp l (CategoryTheory.Limits.PullbackCone.fst t))
(h₁ : CategoryTheory.CategoryStruct.comp k (CategoryTheory.Limits.PullbackCone.snd t) = CategoryTheory.CategoryStruct.comp l (CategoryTheory.Limits.PullbackCone.snd t))
:
k = l
theorem
CategoryTheory.Limits.PullbackCone.mono_snd_of_is_pullback_of_mono
{C : Type u}
[CategoryTheory.Category.{v, u} C]
{X : C}
{Y : C}
{Z : C}
{f : X ⟶ Z}
{g : Y ⟶ Z}
{t : CategoryTheory.Limits.PullbackCone f g}
(ht : CategoryTheory.Limits.IsLimit t)
[CategoryTheory.Mono f]
:
theorem
CategoryTheory.Limits.PullbackCone.mono_fst_of_is_pullback_of_mono
{C : Type u}
[CategoryTheory.Category.{v, u} C]
{X : C}
{Y : C}
{Z : C}
{f : X ⟶ Z}
{g : Y ⟶ Z}
{t : CategoryTheory.Limits.PullbackCone f g}
(ht : CategoryTheory.Limits.IsLimit t)
[CategoryTheory.Mono g]
:
def
CategoryTheory.Limits.PullbackCone.ext
{C : Type u}
[CategoryTheory.Category.{v, u} C]
{X : C}
{Y : C}
{Z : C}
{f : X ⟶ Z}
{g : Y ⟶ Z}
{s : CategoryTheory.Limits.PullbackCone f g}
{t : CategoryTheory.Limits.PullbackCone f g}
(i : s.pt ≅ t.pt)
(w₁ : CategoryTheory.Limits.PullbackCone.fst s = CategoryTheory.CategoryStruct.comp i.hom (CategoryTheory.Limits.PullbackCone.fst t))
(w₂ : CategoryTheory.Limits.PullbackCone.snd s = CategoryTheory.CategoryStruct.comp i.hom (CategoryTheory.Limits.PullbackCone.snd t))
:
s ≅ t
To construct an isomorphism of pullback cones, it suffices to construct an isomorphism
of the cone points and check it commutes with fst and snd.
Instances For
def
CategoryTheory.Limits.PullbackCone.IsLimit.lift
{C : Type u}
[CategoryTheory.Category.{v, u} C]
{X : C}
{Y : C}
{Z : C}
{f : X ⟶ Z}
{g : Y ⟶ Z}
{t : CategoryTheory.Limits.PullbackCone f g}
(ht : CategoryTheory.Limits.IsLimit t)
{W : C}
(h : W ⟶ X)
(k : W ⟶ Y)
(w : CategoryTheory.CategoryStruct.comp h f = CategoryTheory.CategoryStruct.comp k g)
:
W ⟶ t.pt
If t is a limit pullback cone over f and g and h : W ⟶ X and k : W ⟶ Y are such that
h ≫ f = k ≫ g, then we get l : W ⟶ t.pt, which satisfies l ≫ fst t = h
and l ≫ snd t = k, see IsLimit.lift_fst and IsLimit.lift_snd.
Instances For
@[simp]
theorem
CategoryTheory.Limits.PullbackCone.IsLimit.lift_fst_assoc
{C : Type u}
[CategoryTheory.Category.{v, u} C]
{X : C}
{Y : C}
{Z : C}
{f : X ⟶ Z}
{g : Y ⟶ Z}
{t : CategoryTheory.Limits.PullbackCone f g}
(ht : CategoryTheory.Limits.IsLimit t)
{W : C}
(h : W ⟶ X)
(k : W ⟶ Y)
(w : CategoryTheory.CategoryStruct.comp h f = CategoryTheory.CategoryStruct.comp k g)
{Z : C}
(h : X ⟶ Z)
:
@[simp]
theorem
CategoryTheory.Limits.PullbackCone.IsLimit.lift_fst
{C : Type u}
[CategoryTheory.Category.{v, u} C]
{X : C}
{Y : C}
{Z : C}
{f : X ⟶ Z}
{g : Y ⟶ Z}
{t : CategoryTheory.Limits.PullbackCone f g}
(ht : CategoryTheory.Limits.IsLimit t)
{W : C}
(h : W ⟶ X)
(k : W ⟶ Y)
(w : CategoryTheory.CategoryStruct.comp h f = CategoryTheory.CategoryStruct.comp k g)
:
@[simp]
theorem
CategoryTheory.Limits.PullbackCone.IsLimit.lift_snd_assoc
{C : Type u}
[CategoryTheory.Category.{v, u} C]
{X : C}
{Y : C}
{Z : C}
{f : X ⟶ Z}
{g : Y ⟶ Z}
{t : CategoryTheory.Limits.PullbackCone f g}
(ht : CategoryTheory.Limits.IsLimit t)
{W : C}
(h : W ⟶ X)
(k : W ⟶ Y)
(w : CategoryTheory.CategoryStruct.comp h f = CategoryTheory.CategoryStruct.comp k g)
{Z : C}
(h : Y ⟶ Z)
:
@[simp]
theorem
CategoryTheory.Limits.PullbackCone.IsLimit.lift_snd
{C : Type u}
[CategoryTheory.Category.{v, u} C]
{X : C}
{Y : C}
{Z : C}
{f : X ⟶ Z}
{g : Y ⟶ Z}
{t : CategoryTheory.Limits.PullbackCone f g}
(ht : CategoryTheory.Limits.IsLimit t)
{W : C}
(h : W ⟶ X)
(k : W ⟶ Y)
(w : CategoryTheory.CategoryStruct.comp h f = CategoryTheory.CategoryStruct.comp k g)
:
def
CategoryTheory.Limits.PullbackCone.IsLimit.lift'
{C : Type u}
[CategoryTheory.Category.{v, u} C]
{X : C}
{Y : C}
{Z : C}
{f : X ⟶ Z}
{g : Y ⟶ Z}
{t : CategoryTheory.Limits.PullbackCone f g}
(ht : CategoryTheory.Limits.IsLimit t)
{W : C}
(h : W ⟶ X)
(k : W ⟶ Y)
(w : CategoryTheory.CategoryStruct.comp h f = CategoryTheory.CategoryStruct.comp k g)
:
If t is a limit pullback cone over f and g and h : W ⟶ X and k : W ⟶ Y are such that
h ≫ f = k ≫ g, then we have l : W ⟶ t.pt satisfying l ≫ fst t = h and l ≫ snd t = k.
Instances For
def
CategoryTheory.Limits.PullbackCone.IsLimit.mk
{C : Type u}
[CategoryTheory.Category.{v, u} C]
{X : C}
{Y : C}
{Z : C}
{f : X ⟶ Z}
{g : Y ⟶ Z}
{W : C}
{fst : W ⟶ X}
{snd : W ⟶ Y}
(eq : CategoryTheory.CategoryStruct.comp fst f = CategoryTheory.CategoryStruct.comp snd g)
(lift : (s : CategoryTheory.Limits.PullbackCone f g) → s.pt ⟶ W)
(fac_left : ∀ (s : CategoryTheory.Limits.PullbackCone f g),
CategoryTheory.CategoryStruct.comp (lift s) fst = CategoryTheory.Limits.PullbackCone.fst s)
(fac_right : ∀ (s : CategoryTheory.Limits.PullbackCone f g),
CategoryTheory.CategoryStruct.comp (lift s) snd = CategoryTheory.Limits.PullbackCone.snd s)
(uniq : ∀ (s : CategoryTheory.Limits.PullbackCone f g) (m : s.pt ⟶ W),
CategoryTheory.CategoryStruct.comp m fst = CategoryTheory.Limits.PullbackCone.fst s →
CategoryTheory.CategoryStruct.comp m snd = CategoryTheory.Limits.PullbackCone.snd s → m = lift s)
:
This is a more convenient formulation to show that a PullbackCone constructed using
PullbackCone.mk is a limit cone.
Instances For
def
CategoryTheory.Limits.PullbackCone.flipIsLimit
{C : Type u}
[CategoryTheory.Category.{v, u} C]
{X : C}
{Y : C}
{Z : C}
{f : X ⟶ Z}
{g : Y ⟶ Z}
{W : C}
{h : W ⟶ X}
{k : W ⟶ Y}
{comm : CategoryTheory.CategoryStruct.comp h f = CategoryTheory.CategoryStruct.comp k g}
(t : CategoryTheory.Limits.IsLimit
(CategoryTheory.Limits.PullbackCone.mk k h
(_ : CategoryTheory.CategoryStruct.comp k g = CategoryTheory.CategoryStruct.comp h f)))
:
The flip of a pullback square is a pullback square.
Instances For
def
CategoryTheory.Limits.PullbackCone.isLimitMkIdId
{C : Type u}
[CategoryTheory.Category.{v, u} C]
{X : C}
{Y : C}
(f : X ⟶ Y)
[CategoryTheory.Mono f]
:
The pullback cone (𝟙 X, 𝟙 X) for the pair (f, f) is a limit if f is a mono. The converse is
shown in mono_of_pullback_is_id.
Instances For
theorem
CategoryTheory.Limits.PullbackCone.mono_of_isLimitMkIdId
{C : Type u}
[CategoryTheory.Category.{v, u} C]
{X : C}
{Y : C}
(f : X ⟶ Y)
(t : CategoryTheory.Limits.IsLimit
(CategoryTheory.Limits.PullbackCone.mk (CategoryTheory.CategoryStruct.id X) (CategoryTheory.CategoryStruct.id X)
(_ :
CategoryTheory.CategoryStruct.comp (CategoryTheory.CategoryStruct.id X) f = CategoryTheory.CategoryStruct.comp (CategoryTheory.CategoryStruct.id X) f)))
:
f is a mono if the pullback cone (𝟙 X, 𝟙 X) is a limit for the pair (f, f). The converse is
given in PullbackCone.is_id_of_mono.
def
CategoryTheory.Limits.PullbackCone.isLimitOfFactors
{C : Type u}
[CategoryTheory.Category.{v, u} C]
{W : C}
{X : C}
{Y : C}
{Z : C}
(f : X ⟶ Z)
(g : Y ⟶ Z)
(h : W ⟶ Z)
[CategoryTheory.Mono h]
(x : X ⟶ W)
(y : Y ⟶ W)
(hxh : CategoryTheory.CategoryStruct.comp x h = f)
(hyh : CategoryTheory.CategoryStruct.comp y h = g)
(s : CategoryTheory.Limits.PullbackCone f g)
(hs : CategoryTheory.Limits.IsLimit s)
:
CategoryTheory.Limits.IsLimit
(CategoryTheory.Limits.PullbackCone.mk (CategoryTheory.Limits.PullbackCone.fst s)
(CategoryTheory.Limits.PullbackCone.snd s)
(_ :
CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.PullbackCone.fst s) x = CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.PullbackCone.snd s) y))
Suppose f and g are two morphisms with a common codomain and s is a limit cone over the
diagram formed by f and g. Suppose f and g both factor through a monomorphism h via
x and y, respectively. Then s is also a limit cone over the diagram formed by x and
y.
Instances For
def
CategoryTheory.Limits.PullbackCone.isLimitOfCompMono
{C : Type u}
[CategoryTheory.Category.{v, u} C]
{W : C}
{X : C}
{Y : C}
{Z : C}
(f : X ⟶ W)
(g : Y ⟶ W)
(i : W ⟶ Z)
[CategoryTheory.Mono i]
(s : CategoryTheory.Limits.PullbackCone f g)
(H : CategoryTheory.Limits.IsLimit s)
:
CategoryTheory.Limits.IsLimit
(CategoryTheory.Limits.PullbackCone.mk (CategoryTheory.Limits.PullbackCone.fst s)
(CategoryTheory.Limits.PullbackCone.snd s)
(_ :
CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.PullbackCone.fst s)
(CategoryTheory.CategoryStruct.comp f i) = CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.PullbackCone.snd s)
(CategoryTheory.CategoryStruct.comp g i)))
If W is the pullback of f, g,
it is also the pullback of f ≫ i, g ≫ i for any mono i.
Instances For
@[inline, reducible]
abbrev
CategoryTheory.Limits.PushoutCocone
{C : Type u}
[CategoryTheory.Category.{v, u} C]
{X : C}
{Y : C}
{Z : C}
(f : X ⟶ Y)
(g : X ⟶ Z)
:
Type (max u v)
A pushout cocone is just a cocone on the span formed by two morphisms f : X ⟶ Y and
g : X ⟶ Z.
Instances For
@[inline, reducible]
abbrev
CategoryTheory.Limits.PushoutCocone.inl
{C : Type u}
[CategoryTheory.Category.{v, u} C]
{X : C}
{Y : C}
{Z : C}
{f : X ⟶ Y}
{g : X ⟶ Z}
(t : CategoryTheory.Limits.PushoutCocone f g)
:
Y ⟶ t.pt
The first inclusion of a pushout cocone.
Instances For
@[inline, reducible]
abbrev
CategoryTheory.Limits.PushoutCocone.inr
{C : Type u}
[CategoryTheory.Category.{v, u} C]
{X : C}
{Y : C}
{Z : C}
{f : X ⟶ Y}
{g : X ⟶ Z}
(t : CategoryTheory.Limits.PushoutCocone f g)
:
Z ⟶ t.pt
The second inclusion of a pushout cocone.
Instances For
@[simp]
theorem
CategoryTheory.Limits.PushoutCocone.ι_app_left
{C : Type u}
[CategoryTheory.Category.{v, u} C]
{X : C}
{Y : C}
{Z : C}
{f : X ⟶ Y}
{g : X ⟶ Z}
(c : CategoryTheory.Limits.PushoutCocone f g)
:
@[simp]
theorem
CategoryTheory.Limits.PushoutCocone.ι_app_right
{C : Type u}
[CategoryTheory.Category.{v, u} C]
{X : C}
{Y : C}
{Z : C}
{f : X ⟶ Y}
{g : X ⟶ Z}
(c : CategoryTheory.Limits.PushoutCocone f g)
:
@[simp]
theorem
CategoryTheory.Limits.PushoutCocone.condition_zero
{C : Type u}
[CategoryTheory.Category.{v, u} C]
{X : C}
{Y : C}
{Z : C}
{f : X ⟶ Y}
{g : X ⟶ Z}
(t : CategoryTheory.Limits.PushoutCocone f g)
:
def
CategoryTheory.Limits.PushoutCocone.isColimitAux
{C : Type u}
[CategoryTheory.Category.{v, u} C]
{X : C}
{Y : C}
{Z : C}
{f : X ⟶ Y}
{g : X ⟶ Z}
(t : CategoryTheory.Limits.PushoutCocone f g)
(desc : (s : CategoryTheory.Limits.PushoutCocone f g) → t.pt ⟶ s.pt)
(fac_left : ∀ (s : CategoryTheory.Limits.PushoutCocone f g),
CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.PushoutCocone.inl t) (desc s) = CategoryTheory.Limits.PushoutCocone.inl s)
(fac_right : ∀ (s : CategoryTheory.Limits.PushoutCocone f g),
CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.PushoutCocone.inr t) (desc s) = CategoryTheory.Limits.PushoutCocone.inr s)
(uniq : ∀ (s : CategoryTheory.Limits.PushoutCocone f g) (m : t.pt ⟶ s.pt),
(∀ (j : CategoryTheory.Limits.WalkingSpan), CategoryTheory.CategoryStruct.comp (t.ι.app j) m = s.ι.app j) → m = desc s)
:
This is a slightly more convenient method to verify that a pushout cocone is a colimit cocone. It only asks for a proof of facts that carry any mathematical content
Instances For
def
CategoryTheory.Limits.PushoutCocone.isColimitAux'
{C : Type u}
[CategoryTheory.Category.{v, u} C]
{X : C}
{Y : C}
{Z : C}
{f : X ⟶ Y}
{g : X ⟶ Z}
(t : CategoryTheory.Limits.PushoutCocone f g)
(create : (s : CategoryTheory.Limits.PushoutCocone f g) →
{ l //
CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.PushoutCocone.inl t) l = CategoryTheory.Limits.PushoutCocone.inl s ∧ CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.PushoutCocone.inr t) l = CategoryTheory.Limits.PushoutCocone.inr s ∧ ∀ {m : t.pt ⟶ s.pt},
CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.PushoutCocone.inl t) m = CategoryTheory.Limits.PushoutCocone.inl s →
CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.PushoutCocone.inr t) m = CategoryTheory.Limits.PushoutCocone.inr s →
m = l })
:
This is another convenient method to verify that a pushout cocone is a colimit cocone. It
only asks for a proof of facts that carry any mathematical content, and allows access to the
same s for all parts.
Instances For
@[simp]
theorem
CategoryTheory.Limits.PushoutCocone.mk_ι_app
{C : Type u}
[CategoryTheory.Category.{v, u} C]
{X : C}
{Y : C}
{Z : C}
{f : X ⟶ Y}
{g : X ⟶ Z}
{W : C}
(inl : Y ⟶ W)
(inr : Z ⟶ W)
(eq : CategoryTheory.CategoryStruct.comp f inl = CategoryTheory.CategoryStruct.comp g inr)
(j : CategoryTheory.Limits.WalkingSpan)
:
(CategoryTheory.Limits.PushoutCocone.mk inl inr eq).ι.app j = Option.casesOn j (CategoryTheory.CategoryStruct.comp f inl) fun j' =>
CategoryTheory.Limits.WalkingPair.casesOn j' inl inr
@[simp]
theorem
CategoryTheory.Limits.PushoutCocone.mk_pt
{C : Type u}
[CategoryTheory.Category.{v, u} C]
{X : C}
{Y : C}
{Z : C}
{f : X ⟶ Y}
{g : X ⟶ Z}
{W : C}
(inl : Y ⟶ W)
(inr : Z ⟶ W)
(eq : CategoryTheory.CategoryStruct.comp f inl = CategoryTheory.CategoryStruct.comp g inr)
:
(CategoryTheory.Limits.PushoutCocone.mk inl inr eq).pt = W
def
CategoryTheory.Limits.PushoutCocone.mk
{C : Type u}
[CategoryTheory.Category.{v, u} C]
{X : C}
{Y : C}
{Z : C}
{f : X ⟶ Y}
{g : X ⟶ Z}
{W : C}
(inl : Y ⟶ W)
(inr : Z ⟶ W)
(eq : CategoryTheory.CategoryStruct.comp f inl = CategoryTheory.CategoryStruct.comp g inr)
:
A pushout cocone on f and g is determined by morphisms inl : Y ⟶ W and inr : Z ⟶ W such
that f ≫ inl = g ↠ inr.
Instances For
@[simp]
theorem
CategoryTheory.Limits.PushoutCocone.mk_ι_app_left
{C : Type u}
[CategoryTheory.Category.{v, u} C]
{X : C}
{Y : C}
{Z : C}
{f : X ⟶ Y}
{g : X ⟶ Z}
{W : C}
(inl : Y ⟶ W)
(inr : Z ⟶ W)
(eq : CategoryTheory.CategoryStruct.comp f inl = CategoryTheory.CategoryStruct.comp g inr)
:
(CategoryTheory.Limits.PushoutCocone.mk inl inr eq).ι.app CategoryTheory.Limits.WalkingSpan.left = inl
@[simp]
theorem
CategoryTheory.Limits.PushoutCocone.mk_ι_app_right
{C : Type u}
[CategoryTheory.Category.{v, u} C]
{X : C}
{Y : C}
{Z : C}
{f : X ⟶ Y}
{g : X ⟶ Z}
{W : C}
(inl : Y ⟶ W)
(inr : Z ⟶ W)
(eq : CategoryTheory.CategoryStruct.comp f inl = CategoryTheory.CategoryStruct.comp g inr)
:
(CategoryTheory.Limits.PushoutCocone.mk inl inr eq).ι.app CategoryTheory.Limits.WalkingSpan.right = inr
@[simp]
theorem
CategoryTheory.Limits.PushoutCocone.mk_ι_app_zero
{C : Type u}
[CategoryTheory.Category.{v, u} C]
{X : C}
{Y : C}
{Z : C}
{f : X ⟶ Y}
{g : X ⟶ Z}
{W : C}
(inl : Y ⟶ W)
(inr : Z ⟶ W)
(eq : CategoryTheory.CategoryStruct.comp f inl = CategoryTheory.CategoryStruct.comp g inr)
:
(CategoryTheory.Limits.PushoutCocone.mk inl inr eq).ι.app CategoryTheory.Limits.WalkingSpan.zero = CategoryTheory.CategoryStruct.comp f inl
@[simp]
theorem
CategoryTheory.Limits.PushoutCocone.mk_inl
{C : Type u}
[CategoryTheory.Category.{v, u} C]
{X : C}
{Y : C}
{Z : C}
{f : X ⟶ Y}
{g : X ⟶ Z}
{W : C}
(inl : Y ⟶ W)
(inr : Z ⟶ W)
(eq : CategoryTheory.CategoryStruct.comp f inl = CategoryTheory.CategoryStruct.comp g inr)
:
@[simp]
theorem
CategoryTheory.Limits.PushoutCocone.mk_inr
{C : Type u}
[CategoryTheory.Category.{v, u} C]
{X : C}
{Y : C}
{Z : C}
{f : X ⟶ Y}
{g : X ⟶ Z}
{W : C}
(inl : Y ⟶ W)
(inr : Z ⟶ W)
(eq : CategoryTheory.CategoryStruct.comp f inl = CategoryTheory.CategoryStruct.comp g inr)
:
theorem
CategoryTheory.Limits.PushoutCocone.condition_assoc
{C : Type u}
[CategoryTheory.Category.{v, u} C]
{X : C}
{Y : C}
{Z : C}
{f : X ⟶ Y}
{g : X ⟶ Z}
(t : CategoryTheory.Limits.PushoutCocone f g)
{Z : C}
(h : t.pt ⟶ Z)
:
theorem
CategoryTheory.Limits.PushoutCocone.condition
{C : Type u}
[CategoryTheory.Category.{v, u} C]
{X : C}
{Y : C}
{Z : C}
{f : X ⟶ Y}
{g : X ⟶ Z}
(t : CategoryTheory.Limits.PushoutCocone f g)
:
theorem
CategoryTheory.Limits.PushoutCocone.coequalizer_ext
{C : Type u}
[CategoryTheory.Category.{v, u} C]
{X : C}
{Y : C}
{Z : C}
{f : X ⟶ Y}
{g : X ⟶ Z}
(t : CategoryTheory.Limits.PushoutCocone f g)
{W : C}
{k : t.pt ⟶ W}
{l : t.pt ⟶ W}
(h₀ : CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.PushoutCocone.inl t) k = CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.PushoutCocone.inl t) l)
(h₁ : CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.PushoutCocone.inr t) k = CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.PushoutCocone.inr t) l)
(j : CategoryTheory.Limits.WalkingSpan)
:
CategoryTheory.CategoryStruct.comp (t.ι.app j) k = CategoryTheory.CategoryStruct.comp (t.ι.app j) l
To check whether a morphism is coequalized by the maps of a pushout cocone, it suffices to check
it for inl t and inr t
theorem
CategoryTheory.Limits.PushoutCocone.IsColimit.hom_ext
{C : Type u}
[CategoryTheory.Category.{v, u} C]
{X : C}
{Y : C}
{Z : C}
{f : X ⟶ Y}
{g : X ⟶ Z}
{t : CategoryTheory.Limits.PushoutCocone f g}
(ht : CategoryTheory.Limits.IsColimit t)
{W : C}
{k : t.pt ⟶ W}
{l : t.pt ⟶ W}
(h₀ : CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.PushoutCocone.inl t) k = CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.PushoutCocone.inl t) l)
(h₁ : CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.PushoutCocone.inr t) k = CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.PushoutCocone.inr t) l)
:
k = l
def
CategoryTheory.Limits.PushoutCocone.IsColimit.desc
{C : Type u}
[CategoryTheory.Category.{v, u} C]
{X : C}
{Y : C}
{Z : C}
{f : X ⟶ Y}
{g : X ⟶ Z}
{t : CategoryTheory.Limits.PushoutCocone f g}
(ht : CategoryTheory.Limits.IsColimit t)
{W : C}
(h : Y ⟶ W)
(k : Z ⟶ W)
(w : CategoryTheory.CategoryStruct.comp f h = CategoryTheory.CategoryStruct.comp g k)
:
t.pt ⟶ W
If t is a colimit pushout cocone over f and g and h : Y ⟶ W and k : Z ⟶ W are
morphisms satisfying f ≫ h = g ≫ k, then we have a factorization l : t.pt ⟶ W such that
inl t ≫ l = h and inr t ≫ l = k, see IsColimit.inl_desc and IsColimit.inr_desc
Instances For
@[simp]
theorem
CategoryTheory.Limits.PushoutCocone.IsColimit.inl_desc_assoc
{C : Type u}
[CategoryTheory.Category.{v, u} C]
{X : C}
{Y : C}
{Z : C}
{f : X ⟶ Y}
{g : X ⟶ Z}
{t : CategoryTheory.Limits.PushoutCocone f g}
(ht : CategoryTheory.Limits.IsColimit t)
{W : C}
(h : Y ⟶ W)
(k : Z ⟶ W)
(w : CategoryTheory.CategoryStruct.comp f h = CategoryTheory.CategoryStruct.comp g k)
{Z : C}
(h : W ⟶ Z)
:
@[simp]
theorem
CategoryTheory.Limits.PushoutCocone.IsColimit.inl_desc
{C : Type u}
[CategoryTheory.Category.{v, u} C]
{X : C}
{Y : C}
{Z : C}
{f : X ⟶ Y}
{g : X ⟶ Z}
{t : CategoryTheory.Limits.PushoutCocone f g}
(ht : CategoryTheory.Limits.IsColimit t)
{W : C}
(h : Y ⟶ W)
(k : Z ⟶ W)
(w : CategoryTheory.CategoryStruct.comp f h = CategoryTheory.CategoryStruct.comp g k)
:
@[simp]
theorem
CategoryTheory.Limits.PushoutCocone.IsColimit.inr_desc_assoc
{C : Type u}
[CategoryTheory.Category.{v, u} C]
{X : C}
{Y : C}
{Z : C}
{f : X ⟶ Y}
{g : X ⟶ Z}
{t : CategoryTheory.Limits.PushoutCocone f g}
(ht : CategoryTheory.Limits.IsColimit t)
{W : C}
(h : Y ⟶ W)
(k : Z ⟶ W)
(w : CategoryTheory.CategoryStruct.comp f h = CategoryTheory.CategoryStruct.comp g k)
{Z : C}
(h : W ⟶ Z)
:
@[simp]
theorem
CategoryTheory.Limits.PushoutCocone.IsColimit.inr_desc
{C : Type u}
[CategoryTheory.Category.{v, u} C]
{X : C}
{Y : C}
{Z : C}
{f : X ⟶ Y}
{g : X ⟶ Z}
{t : CategoryTheory.Limits.PushoutCocone f g}
(ht : CategoryTheory.Limits.IsColimit t)
{W : C}
(h : Y ⟶ W)
(k : Z ⟶ W)
(w : CategoryTheory.CategoryStruct.comp f h = CategoryTheory.CategoryStruct.comp g k)
:
def
CategoryTheory.Limits.PushoutCocone.IsColimit.desc'
{C : Type u}
[CategoryTheory.Category.{v, u} C]
{X : C}
{Y : C}
{Z : C}
{f : X ⟶ Y}
{g : X ⟶ Z}
{t : CategoryTheory.Limits.PushoutCocone f g}
(ht : CategoryTheory.Limits.IsColimit t)
{W : C}
(h : Y ⟶ W)
(k : Z ⟶ W)
(w : CategoryTheory.CategoryStruct.comp f h = CategoryTheory.CategoryStruct.comp g k)
:
If t is a colimit pushout cocone over f and g and h : Y ⟶ W and k : Z ⟶ W are
morphisms satisfying f ≫ h = g ≫ k, then we have a factorization l : t.pt ⟶ W such that
inl t ≫ l = h and inr t ≫ l = k.
Instances For
theorem
CategoryTheory.Limits.PushoutCocone.epi_inr_of_is_pushout_of_epi
{C : Type u}
[CategoryTheory.Category.{v, u} C]
{X : C}
{Y : C}
{Z : C}
{f : X ⟶ Y}
{g : X ⟶ Z}
{t : CategoryTheory.Limits.PushoutCocone f g}
(ht : CategoryTheory.Limits.IsColimit t)
[CategoryTheory.Epi f]
:
theorem
CategoryTheory.Limits.PushoutCocone.epi_inl_of_is_pushout_of_epi
{C : Type u}
[CategoryTheory.Category.{v, u} C]
{X : C}
{Y : C}
{Z : C}
{f : X ⟶ Y}
{g : X ⟶ Z}
{t : CategoryTheory.Limits.PushoutCocone f g}
(ht : CategoryTheory.Limits.IsColimit t)
[CategoryTheory.Epi g]
:
def
CategoryTheory.Limits.PushoutCocone.ext
{C : Type u}
[CategoryTheory.Category.{v, u} C]
{X : C}
{Y : C}
{Z : C}
{f : X ⟶ Y}
{g : X ⟶ Z}
{s : CategoryTheory.Limits.PushoutCocone f g}
{t : CategoryTheory.Limits.PushoutCocone f g}
(i : s.pt ≅ t.pt)
(w₁ : CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.PushoutCocone.inl s) i.hom = CategoryTheory.Limits.PushoutCocone.inl t)
(w₂ : CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.PushoutCocone.inr s) i.hom = CategoryTheory.Limits.PushoutCocone.inr t)
:
s ≅ t
To construct an isomorphism of pushout cocones, it suffices to construct an isomorphism
of the cocone points and check it commutes with inl and inr.
Instances For
def
CategoryTheory.Limits.PushoutCocone.IsColimit.mk
{C : Type u}
[CategoryTheory.Category.{v, u} C]
{X : C}
{Y : C}
{Z : C}
{f : X ⟶ Y}
{g : X ⟶ Z}
{W : C}
{inl : Y ⟶ W}
{inr : Z ⟶ W}
(eq : CategoryTheory.CategoryStruct.comp f inl = CategoryTheory.CategoryStruct.comp g inr)
(desc : (s : CategoryTheory.Limits.PushoutCocone f g) → W ⟶ s.pt)
(fac_left : ∀ (s : CategoryTheory.Limits.PushoutCocone f g),
CategoryTheory.CategoryStruct.comp inl (desc s) = CategoryTheory.Limits.PushoutCocone.inl s)
(fac_right : ∀ (s : CategoryTheory.Limits.PushoutCocone f g),
CategoryTheory.CategoryStruct.comp inr (desc s) = CategoryTheory.Limits.PushoutCocone.inr s)
(uniq : ∀ (s : CategoryTheory.Limits.PushoutCocone f g) (m : W ⟶ s.pt),
CategoryTheory.CategoryStruct.comp inl m = CategoryTheory.Limits.PushoutCocone.inl s →
CategoryTheory.CategoryStruct.comp inr m = CategoryTheory.Limits.PushoutCocone.inr s → m = desc s)
:
This is a more convenient formulation to show that a PushoutCocone constructed using
PushoutCocone.mk is a colimit cocone.
Instances For
def
CategoryTheory.Limits.PushoutCocone.flipIsColimit
{C : Type u}
[CategoryTheory.Category.{v, u} C]
{X : C}
{Y : C}
{Z : C}
{f : X ⟶ Y}
{g : X ⟶ Z}
{W : C}
{h : Y ⟶ W}
{k : Z ⟶ W}
{comm : CategoryTheory.CategoryStruct.comp f h = CategoryTheory.CategoryStruct.comp g k}
(t : CategoryTheory.Limits.IsColimit
(CategoryTheory.Limits.PushoutCocone.mk k h
(_ : CategoryTheory.CategoryStruct.comp g k = CategoryTheory.CategoryStruct.comp f h)))
:
The flip of a pushout square is a pushout square.
Instances For
def
CategoryTheory.Limits.PushoutCocone.isColimitMkIdId
{C : Type u}
[CategoryTheory.Category.{v, u} C]
{X : C}
{Y : C}
(f : X ⟶ Y)
[CategoryTheory.Epi f]
:
CategoryTheory.Limits.IsColimit
(CategoryTheory.Limits.PushoutCocone.mk (CategoryTheory.CategoryStruct.id Y) (CategoryTheory.CategoryStruct.id Y)
(_ :
CategoryTheory.CategoryStruct.comp f (CategoryTheory.CategoryStruct.id Y) = CategoryTheory.CategoryStruct.comp f (CategoryTheory.CategoryStruct.id Y)))
The pushout cocone (𝟙 X, 𝟙 X) for the pair (f, f) is a colimit if f is an epi. The converse is
shown in epi_of_isColimit_mk_id_id.
Instances For
theorem
CategoryTheory.Limits.PushoutCocone.epi_of_isColimitMkIdId
{C : Type u}
[CategoryTheory.Category.{v, u} C]
{X : C}
{Y : C}
(f : X ⟶ Y)
(t : CategoryTheory.Limits.IsColimit
(CategoryTheory.Limits.PushoutCocone.mk (CategoryTheory.CategoryStruct.id Y) (CategoryTheory.CategoryStruct.id Y)
(_ :
CategoryTheory.CategoryStruct.comp f (CategoryTheory.CategoryStruct.id Y) = CategoryTheory.CategoryStruct.comp f (CategoryTheory.CategoryStruct.id Y))))
:
f is an epi if the pushout cocone (𝟙 X, 𝟙 X) is a colimit for the pair (f, f).
The converse is given in PushoutCocone.isColimitMkIdId.
def
CategoryTheory.Limits.PushoutCocone.isColimitOfFactors
{C : Type u}
[CategoryTheory.Category.{v, u} C]
{W : C}
{X : C}
{Y : C}
{Z : C}
(f : X ⟶ Y)
(g : X ⟶ Z)
(h : X ⟶ W)
[CategoryTheory.Epi h]
(x : W ⟶ Y)
(y : W ⟶ Z)
(hhx : CategoryTheory.CategoryStruct.comp h x = f)
(hhy : CategoryTheory.CategoryStruct.comp h y = g)
(s : CategoryTheory.Limits.PushoutCocone f g)
(hs : CategoryTheory.Limits.IsColimit s)
:
let_fun reassoc₁ :=
(_ :
CategoryTheory.CategoryStruct.comp h
(CategoryTheory.CategoryStruct.comp x (CategoryTheory.Limits.PushoutCocone.inl s)) = CategoryTheory.CategoryStruct.comp f (CategoryTheory.Limits.PushoutCocone.inl s));
let_fun reassoc₂ :=
(_ :
CategoryTheory.CategoryStruct.comp h
(CategoryTheory.CategoryStruct.comp y (CategoryTheory.Limits.PushoutCocone.inr s)) = CategoryTheory.CategoryStruct.comp g (CategoryTheory.Limits.PushoutCocone.inr s));
CategoryTheory.Limits.IsColimit
(CategoryTheory.Limits.PushoutCocone.mk (CategoryTheory.Limits.PushoutCocone.inl s)
(CategoryTheory.Limits.PushoutCocone.inr s)
(_ :
CategoryTheory.CategoryStruct.comp x (CategoryTheory.Limits.PushoutCocone.inl s) = CategoryTheory.CategoryStruct.comp y (CategoryTheory.Limits.PushoutCocone.inr s)))
Suppose f and g are two morphisms with a common domain and s is a colimit cocone over the
diagram formed by f and g. Suppose f and g both factor through an epimorphism h via
x and y, respectively. Then s is also a colimit cocone over the diagram formed by x and
y.
Instances For
def
CategoryTheory.Limits.PushoutCocone.isColimitOfEpiComp
{C : Type u}
[CategoryTheory.Category.{v, u} C]
{W : C}
{X : C}
{Y : C}
{Z : C}
(f : X ⟶ Y)
(g : X ⟶ Z)
(h : W ⟶ X)
[CategoryTheory.Epi h]
(s : CategoryTheory.Limits.PushoutCocone f g)
(H : CategoryTheory.Limits.IsColimit s)
:
CategoryTheory.Limits.IsColimit
(CategoryTheory.Limits.PushoutCocone.mk (CategoryTheory.Limits.PushoutCocone.inl s)
(CategoryTheory.Limits.PushoutCocone.inr s)
(_ :
CategoryTheory.CategoryStruct.comp (CategoryTheory.CategoryStruct.comp h f)
(CategoryTheory.Limits.PushoutCocone.inl s) = CategoryTheory.CategoryStruct.comp (CategoryTheory.CategoryStruct.comp h g)
(CategoryTheory.Limits.PushoutCocone.inr s)))
If W is the pushout of f, g,
it is also the pushout of h ≫ f, h ≫ g for any epi h.
Instances For
@[simp]
theorem
CategoryTheory.Limits.Cone.ofPullbackCone_pt
{C : Type u}
[CategoryTheory.Category.{v, u} C]
{F : CategoryTheory.Functor CategoryTheory.Limits.WalkingCospan C}
(t : CategoryTheory.Limits.PullbackCone (F.map CategoryTheory.Limits.WalkingCospan.Hom.inl)
(F.map CategoryTheory.Limits.WalkingCospan.Hom.inr))
:
(CategoryTheory.Limits.Cone.ofPullbackCone t).pt = t.pt
@[simp]
theorem
CategoryTheory.Limits.Cone.ofPullbackCone_π
{C : Type u}
[CategoryTheory.Category.{v, u} C]
{F : CategoryTheory.Functor CategoryTheory.Limits.WalkingCospan C}
(t : CategoryTheory.Limits.PullbackCone (F.map CategoryTheory.Limits.WalkingCospan.Hom.inl)
(F.map CategoryTheory.Limits.WalkingCospan.Hom.inr))
:
def
CategoryTheory.Limits.Cone.ofPullbackCone
{C : Type u}
[CategoryTheory.Category.{v, u} C]
{F : CategoryTheory.Functor CategoryTheory.Limits.WalkingCospan C}
(t : CategoryTheory.Limits.PullbackCone (F.map CategoryTheory.Limits.WalkingCospan.Hom.inl)
(F.map CategoryTheory.Limits.WalkingCospan.Hom.inr))
:
This is a helper construction that can be useful when verifying that a category has all
pullbacks. Given F : WalkingCospan ⥤ C, which is really the same as
cospan (F.map inl) (F.map inr), and a pullback cone on F.map inl and F.map inr, we
get a cone on F.
If you're thinking about using this, have a look at hasPullbacks_of_hasLimit_cospan,
which you may find to be an easier way of achieving your goal.
Instances For
@[simp]
theorem
CategoryTheory.Limits.Cocone.ofPushoutCocone_pt
{C : Type u}
[CategoryTheory.Category.{v, u} C]
{F : CategoryTheory.Functor CategoryTheory.Limits.WalkingSpan C}
(t : CategoryTheory.Limits.PushoutCocone (F.map CategoryTheory.Limits.WalkingSpan.Hom.fst)
(F.map CategoryTheory.Limits.WalkingSpan.Hom.snd))
:
(CategoryTheory.Limits.Cocone.ofPushoutCocone t).pt = t.pt
@[simp]
theorem
CategoryTheory.Limits.Cocone.ofPushoutCocone_ι
{C : Type u}
[CategoryTheory.Category.{v, u} C]
{F : CategoryTheory.Functor CategoryTheory.Limits.WalkingSpan C}
(t : CategoryTheory.Limits.PushoutCocone (F.map CategoryTheory.Limits.WalkingSpan.Hom.fst)
(F.map CategoryTheory.Limits.WalkingSpan.Hom.snd))
:
def
CategoryTheory.Limits.Cocone.ofPushoutCocone
{C : Type u}
[CategoryTheory.Category.{v, u} C]
{F : CategoryTheory.Functor CategoryTheory.Limits.WalkingSpan C}
(t : CategoryTheory.Limits.PushoutCocone (F.map CategoryTheory.Limits.WalkingSpan.Hom.fst)
(F.map CategoryTheory.Limits.WalkingSpan.Hom.snd))
:
This is a helper construction that can be useful when verifying that a category has all
pushout. Given F : WalkingSpan ⥤ C, which is really the same as
span (F.map fst) (F.map snd), and a pushout cocone on F.map fst and F.map snd,
we get a cocone on F.
If you're thinking about using this, have a look at hasPushouts_of_hasColimit_span, which
you may find to be an easier way of achieving your goal.
Instances For
@[simp]
theorem
CategoryTheory.Limits.PullbackCone.ofCone_pt
{C : Type u}
[CategoryTheory.Category.{v, u} C]
{F : CategoryTheory.Functor CategoryTheory.Limits.WalkingCospan C}
(t : CategoryTheory.Limits.Cone F)
:
(CategoryTheory.Limits.PullbackCone.ofCone t).pt = t.pt
@[simp]
theorem
CategoryTheory.Limits.PullbackCone.ofCone_π
{C : Type u}
[CategoryTheory.Category.{v, u} C]
{F : CategoryTheory.Functor CategoryTheory.Limits.WalkingCospan C}
(t : CategoryTheory.Limits.Cone F)
:
def
CategoryTheory.Limits.PullbackCone.ofCone
{C : Type u}
[CategoryTheory.Category.{v, u} C]
{F : CategoryTheory.Functor CategoryTheory.Limits.WalkingCospan C}
(t : CategoryTheory.Limits.Cone F)
:
Given F : WalkingCospan ⥤ C, which is really the same as cospan (F.map inl) (F.map inr),
and a cone on F, we get a pullback cone on F.map inl and F.map inr.
Instances For
@[simp]
theorem
CategoryTheory.Limits.PullbackCone.isoMk_hom_hom
{C : Type u}
[CategoryTheory.Category.{v, u} C]
{F : CategoryTheory.Functor CategoryTheory.Limits.WalkingCospan C}
(t : CategoryTheory.Limits.Cone F)
:
(CategoryTheory.Limits.PullbackCone.isoMk t).hom.hom = CategoryTheory.CategoryStruct.id t.pt
@[simp]
theorem
CategoryTheory.Limits.PullbackCone.isoMk_inv_hom
{C : Type u}
[CategoryTheory.Category.{v, u} C]
{F : CategoryTheory.Functor CategoryTheory.Limits.WalkingCospan C}
(t : CategoryTheory.Limits.Cone F)
:
(CategoryTheory.Limits.PullbackCone.isoMk t).inv.hom = CategoryTheory.CategoryStruct.id t.pt
def
CategoryTheory.Limits.PullbackCone.isoMk
{C : Type u}
[CategoryTheory.Category.{v, u} C]
{F : CategoryTheory.Functor CategoryTheory.Limits.WalkingCospan C}
(t : CategoryTheory.Limits.Cone F)
:
(CategoryTheory.Limits.Cones.postcompose (CategoryTheory.Limits.diagramIsoCospan F).hom).obj t ≅ CategoryTheory.Limits.PullbackCone.mk (t.π.app CategoryTheory.Limits.WalkingCospan.left)
(t.π.app CategoryTheory.Limits.WalkingCospan.right)
(_ :
CategoryTheory.CategoryStruct.comp (t.π.app CategoryTheory.Limits.WalkingCospan.left)
(F.map CategoryTheory.Limits.WalkingCospan.Hom.inl) = CategoryTheory.CategoryStruct.comp (t.π.app CategoryTheory.Limits.WalkingCospan.right)
(F.map CategoryTheory.Limits.WalkingCospan.Hom.inr))
A diagram WalkingCospan ⥤ C is isomorphic to some PullbackCone.mk after
composing with diagramIsoCospan.
Instances For
@[simp]
theorem
CategoryTheory.Limits.PushoutCocone.ofCocone_ι
{C : Type u}
[CategoryTheory.Category.{v, u} C]
{F : CategoryTheory.Functor CategoryTheory.Limits.WalkingSpan C}
(t : CategoryTheory.Limits.Cocone F)
:
@[simp]
theorem
CategoryTheory.Limits.PushoutCocone.ofCocone_pt
{C : Type u}
[CategoryTheory.Category.{v, u} C]
{F : CategoryTheory.Functor CategoryTheory.Limits.WalkingSpan C}
(t : CategoryTheory.Limits.Cocone F)
:
(CategoryTheory.Limits.PushoutCocone.ofCocone t).pt = t.pt
def
CategoryTheory.Limits.PushoutCocone.ofCocone
{C : Type u}
[CategoryTheory.Category.{v, u} C]
{F : CategoryTheory.Functor CategoryTheory.Limits.WalkingSpan C}
(t : CategoryTheory.Limits.Cocone F)
:
Given F : WalkingSpan ⥤ C, which is really the same as span (F.map fst) (F.map snd),
and a cocone on F, we get a pushout cocone on F.map fst and F.map snd.
Instances For
@[simp]
theorem
CategoryTheory.Limits.PushoutCocone.isoMk_inv_hom
{C : Type u}
[CategoryTheory.Category.{v, u} C]
{F : CategoryTheory.Functor CategoryTheory.Limits.WalkingSpan C}
(t : CategoryTheory.Limits.Cocone F)
:
(CategoryTheory.Limits.PushoutCocone.isoMk t).inv.hom = CategoryTheory.CategoryStruct.id t.pt
@[simp]
theorem
CategoryTheory.Limits.PushoutCocone.isoMk_hom_hom
{C : Type u}
[CategoryTheory.Category.{v, u} C]
{F : CategoryTheory.Functor CategoryTheory.Limits.WalkingSpan C}
(t : CategoryTheory.Limits.Cocone F)
:
(CategoryTheory.Limits.PushoutCocone.isoMk t).hom.hom = CategoryTheory.CategoryStruct.id t.pt
def
CategoryTheory.Limits.PushoutCocone.isoMk
{C : Type u}
[CategoryTheory.Category.{v, u} C]
{F : CategoryTheory.Functor CategoryTheory.Limits.WalkingSpan C}
(t : CategoryTheory.Limits.Cocone F)
:
(CategoryTheory.Limits.Cocones.precompose (CategoryTheory.Limits.diagramIsoSpan F).inv).obj t ≅ CategoryTheory.Limits.PushoutCocone.mk (t.ι.app CategoryTheory.Limits.WalkingSpan.left)
(t.ι.app CategoryTheory.Limits.WalkingSpan.right)
(_ :
CategoryTheory.CategoryStruct.comp (F.map CategoryTheory.Limits.WalkingSpan.Hom.fst)
(t.ι.app CategoryTheory.Limits.WalkingSpan.left) = CategoryTheory.CategoryStruct.comp (F.map CategoryTheory.Limits.WalkingSpan.Hom.snd)
(t.ι.app CategoryTheory.Limits.WalkingSpan.right))
A diagram WalkingSpan ⥤ C is isomorphic to some PushoutCocone.mk after composing with
diagramIsoSpan.
Instances For
@[inline, reducible]
abbrev
CategoryTheory.Limits.HasPullback
{C : Type u}
[CategoryTheory.Category.{v, u} C]
{X : C}
{Y : C}
{Z : C}
(f : X ⟶ Z)
(g : Y ⟶ Z)
:
HasPullback f g represents a particular choice of limiting cone
for the pair of morphisms f : X ⟶ Z and g : Y ⟶ Z.
Instances For
@[inline, reducible]
abbrev
CategoryTheory.Limits.HasPushout
{C : Type u}
[CategoryTheory.Category.{v, u} C]
{X : C}
{Y : C}
{Z : C}
(f : X ⟶ Y)
(g : X ⟶ Z)
:
HasPushout f g represents a particular choice of colimiting cocone
for the pair of morphisms f : X ⟶ Y and g : X ⟶ Z.
Instances For
@[inline, reducible]
abbrev
CategoryTheory.Limits.pullback
{C : Type u}
[CategoryTheory.Category.{v, u} C]
{X : C}
{Y : C}
{Z : C}
(f : X ⟶ Z)
(g : Y ⟶ Z)
[CategoryTheory.Limits.HasPullback f g]
:
C
pullback f g computes the pullback of a pair of morphisms with the same target.
Instances For
@[inline, reducible]
abbrev
CategoryTheory.Limits.pushout
{C : Type u}
[CategoryTheory.Category.{v, u} C]
{X : C}
{Y : C}
{Z : C}
(f : X ⟶ Y)
(g : X ⟶ Z)
[CategoryTheory.Limits.HasPushout f g]
:
C
pushout f g computes the pushout of a pair of morphisms with the same source.
Instances For
@[inline, reducible]
abbrev
CategoryTheory.Limits.pullback.fst
{C : Type u}
[CategoryTheory.Category.{v, u} C]
{X : C}
{Y : C}
{Z : C}
{f : X ⟶ Z}
{g : Y ⟶ Z}
[CategoryTheory.Limits.HasPullback f g]
:
The first projection of the pullback of f and g.
Instances For
@[inline, reducible]
abbrev
CategoryTheory.Limits.pullback.snd
{C : Type u}
[CategoryTheory.Category.{v, u} C]
{X : C}
{Y : C}
{Z : C}
{f : X ⟶ Z}
{g : Y ⟶ Z}
[CategoryTheory.Limits.HasPullback f g]
:
The second projection of the pullback of f and g.
Instances For
@[inline, reducible]
abbrev
CategoryTheory.Limits.pushout.inl
{C : Type u}
[CategoryTheory.Category.{v, u} C]
{X : C}
{Y : C}
{Z : C}
{f : X ⟶ Y}
{g : X ⟶ Z}
[CategoryTheory.Limits.HasPushout f g]
:
The first inclusion into the pushout of f and g.
Instances For
@[inline, reducible]
abbrev
CategoryTheory.Limits.pushout.inr
{C : Type u}
[CategoryTheory.Category.{v, u} C]
{X : C}
{Y : C}
{Z : C}
{f : X ⟶ Y}
{g : X ⟶ Z}
[CategoryTheory.Limits.HasPushout f g]
:
The second inclusion into the pushout of f and g.
Instances For
@[inline, reducible]
abbrev
CategoryTheory.Limits.pullback.lift
{C : Type u}
[CategoryTheory.Category.{v, u} C]
{W : C}
{X : C}
{Y : C}
{Z : C}
{f : X ⟶ Z}
{g : Y ⟶ Z}
[CategoryTheory.Limits.HasPullback f g]
(h : W ⟶ X)
(k : W ⟶ Y)
(w : CategoryTheory.CategoryStruct.comp h f = CategoryTheory.CategoryStruct.comp k g)
:
A pair of morphisms h : W ⟶ X and k : W ⟶ Y satisfying h ≫ f = k ≫ g induces a morphism
pullback.lift : W ⟶ pullback f g.
Instances For
@[inline, reducible]
abbrev
CategoryTheory.Limits.pushout.desc
{C : Type u}
[CategoryTheory.Category.{v, u} C]
{W : C}
{X : C}
{Y : C}
{Z : C}
{f : X ⟶ Y}
{g : X ⟶ Z}
[CategoryTheory.Limits.HasPushout f g]
(h : Y ⟶ W)
(k : Z ⟶ W)
(w : CategoryTheory.CategoryStruct.comp f h = CategoryTheory.CategoryStruct.comp g k)
:
A pair of morphisms h : Y ⟶ W and k : Z ⟶ W satisfying f ≫ h = g ≫ k induces a morphism
pushout.desc : pushout f g ⟶ W.
Instances For
@[simp]
theorem
CategoryTheory.Limits.PullbackCone.fst_colimit_cocone
{C : Type u}
[CategoryTheory.Category.{v, u} C]
{X : C}
{Y : C}
{Z : C}
(f : X ⟶ Z)
(g : Y ⟶ Z)
[CategoryTheory.Limits.HasLimit (CategoryTheory.Limits.cospan f g)]
:
CategoryTheory.Limits.PullbackCone.fst (CategoryTheory.Limits.limit.cone (CategoryTheory.Limits.cospan f g)) = CategoryTheory.Limits.pullback.fst
@[simp]
theorem
CategoryTheory.Limits.PullbackCone.snd_colimit_cocone
{C : Type u}
[CategoryTheory.Category.{v, u} C]
{X : C}
{Y : C}
{Z : C}
(f : X ⟶ Z)
(g : Y ⟶ Z)
[CategoryTheory.Limits.HasLimit (CategoryTheory.Limits.cospan f g)]
:
CategoryTheory.Limits.PullbackCone.snd (CategoryTheory.Limits.limit.cone (CategoryTheory.Limits.cospan f g)) = CategoryTheory.Limits.pullback.snd
theorem
CategoryTheory.Limits.PushoutCocone.inl_colimit_cocone
{C : Type u}
[CategoryTheory.Category.{v, u} C]
{X : C}
{Y : C}
{Z : C}
(f : Z ⟶ X)
(g : Z ⟶ Y)
[CategoryTheory.Limits.HasColimit (CategoryTheory.Limits.span f g)]
:
CategoryTheory.Limits.PushoutCocone.inl (CategoryTheory.Limits.colimit.cocone (CategoryTheory.Limits.span f g)) = CategoryTheory.Limits.pushout.inl
theorem
CategoryTheory.Limits.PushoutCocone.inr_colimit_cocone
{C : Type u}
[CategoryTheory.Category.{v, u} C]
{X : C}
{Y : C}
{Z : C}
(f : Z ⟶ X)
(g : Z ⟶ Y)
[CategoryTheory.Limits.HasColimit (CategoryTheory.Limits.span f g)]
:
CategoryTheory.Limits.PushoutCocone.inr (CategoryTheory.Limits.colimit.cocone (CategoryTheory.Limits.span f g)) = CategoryTheory.Limits.pushout.inr
theorem
CategoryTheory.Limits.pullback.lift_fst_assoc
{C : Type u}
[CategoryTheory.Category.{v, u} C]
{W : C}
{X : C}
{Y : C}
{Z : C}
{f : X ⟶ Z}
{g : Y ⟶ Z}
[CategoryTheory.Limits.HasPullback f g]
(h : W ⟶ X)
(k : W ⟶ Y)
(w : CategoryTheory.CategoryStruct.comp h f = CategoryTheory.CategoryStruct.comp k g)
{Z : C}
(h : X ⟶ Z)
:
CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.pullback.lift h k w)
(CategoryTheory.CategoryStruct.comp CategoryTheory.Limits.pullback.fst h) = CategoryTheory.CategoryStruct.comp h h
theorem
CategoryTheory.Limits.pullback.lift_fst
{C : Type u}
[CategoryTheory.Category.{v, u} C]
{W : C}
{X : C}
{Y : C}
{Z : C}
{f : X ⟶ Z}
{g : Y ⟶ Z}
[CategoryTheory.Limits.HasPullback f g]
(h : W ⟶ X)
(k : W ⟶ Y)
(w : CategoryTheory.CategoryStruct.comp h f = CategoryTheory.CategoryStruct.comp k g)
:
CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.pullback.lift h k w) CategoryTheory.Limits.pullback.fst = h
theorem
CategoryTheory.Limits.pullback.lift_snd_assoc
{C : Type u}
[CategoryTheory.Category.{v, u} C]
{W : C}
{X : C}
{Y : C}
{Z : C}
{f : X ⟶ Z}
{g : Y ⟶ Z}
[CategoryTheory.Limits.HasPullback f g]
(h : W ⟶ X)
(k : W ⟶ Y)
(w : CategoryTheory.CategoryStruct.comp h f = CategoryTheory.CategoryStruct.comp k g)
{Z : C}
(h : Y ⟶ Z)
:
CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.pullback.lift h k w)
(CategoryTheory.CategoryStruct.comp CategoryTheory.Limits.pullback.snd h) = CategoryTheory.CategoryStruct.comp k h
theorem
CategoryTheory.Limits.pullback.lift_snd
{C : Type u}
[CategoryTheory.Category.{v, u} C]
{W : C}
{X : C}
{Y : C}
{Z : C}
{f : X ⟶ Z}
{g : Y ⟶ Z}
[CategoryTheory.Limits.HasPullback f g]
(h : W ⟶ X)
(k : W ⟶ Y)
(w : CategoryTheory.CategoryStruct.comp h f = CategoryTheory.CategoryStruct.comp k g)
:
CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.pullback.lift h k w) CategoryTheory.Limits.pullback.snd = k
theorem
CategoryTheory.Limits.pushout.inl_desc_assoc
{C : Type u}
[CategoryTheory.Category.{v, u} C]
{W : C}
{X : C}
{Y : C}
{Z : C}
{f : X ⟶ Y}
{g : X ⟶ Z}
[CategoryTheory.Limits.HasPushout f g]
(h : Y ⟶ W)
(k : Z ⟶ W)
(w : CategoryTheory.CategoryStruct.comp f h = CategoryTheory.CategoryStruct.comp g k)
{Z : C}
(h : W ⟶ Z)
:
CategoryTheory.CategoryStruct.comp CategoryTheory.Limits.pushout.inl
(CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.pushout.desc h k w) h) = CategoryTheory.CategoryStruct.comp h h
theorem
CategoryTheory.Limits.pushout.inl_desc
{C : Type u}
[CategoryTheory.Category.{v, u} C]
{W : C}
{X : C}
{Y : C}
{Z : C}
{f : X ⟶ Y}
{g : X ⟶ Z}
[CategoryTheory.Limits.HasPushout f g]
(h : Y ⟶ W)
(k : Z ⟶ W)
(w : CategoryTheory.CategoryStruct.comp f h = CategoryTheory.CategoryStruct.comp g k)
:
CategoryTheory.CategoryStruct.comp CategoryTheory.Limits.pushout.inl (CategoryTheory.Limits.pushout.desc h k w) = h
theorem
CategoryTheory.Limits.pushout.inr_desc_assoc
{C : Type u}
[CategoryTheory.Category.{v, u} C]
{W : C}
{X : C}
{Y : C}
{Z : C}
{f : X ⟶ Y}
{g : X ⟶ Z}
[CategoryTheory.Limits.HasPushout f g]
(h : Y ⟶ W)
(k : Z ⟶ W)
(w : CategoryTheory.CategoryStruct.comp f h = CategoryTheory.CategoryStruct.comp g k)
{Z : C}
(h : W ⟶ Z)
:
CategoryTheory.CategoryStruct.comp CategoryTheory.Limits.pushout.inr
(CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.pushout.desc h k w) h) = CategoryTheory.CategoryStruct.comp k h
theorem
CategoryTheory.Limits.pushout.inr_desc
{C : Type u}
[CategoryTheory.Category.{v, u} C]
{W : C}
{X : C}
{Y : C}
{Z : C}
{f : X ⟶ Y}
{g : X ⟶ Z}
[CategoryTheory.Limits.HasPushout f g]
(h : Y ⟶ W)
(k : Z ⟶ W)
(w : CategoryTheory.CategoryStruct.comp f h = CategoryTheory.CategoryStruct.comp g k)
:
CategoryTheory.CategoryStruct.comp CategoryTheory.Limits.pushout.inr (CategoryTheory.Limits.pushout.desc h k w) = k
def
CategoryTheory.Limits.pullback.lift'
{C : Type u}
[CategoryTheory.Category.{v, u} C]
{W : C}
{X : C}
{Y : C}
{Z : C}
{f : X ⟶ Z}
{g : Y ⟶ Z}
[CategoryTheory.Limits.HasPullback f g]
(h : W ⟶ X)
(k : W ⟶ Y)
(w : CategoryTheory.CategoryStruct.comp h f = CategoryTheory.CategoryStruct.comp k g)
:
{ l //
CategoryTheory.CategoryStruct.comp l CategoryTheory.Limits.pullback.fst = h ∧ CategoryTheory.CategoryStruct.comp l CategoryTheory.Limits.pullback.snd = k }
A pair of morphisms h : W ⟶ X and k : W ⟶ Y satisfying h ≫ f = k ≫ g induces a morphism
l : W ⟶ pullback f g such that l ≫ pullback.fst = h and l ≫ pullback.snd = k.
Instances For
def
CategoryTheory.Limits.pullback.desc'
{C : Type u}
[CategoryTheory.Category.{v, u} C]
{W : C}
{X : C}
{Y : C}
{Z : C}
{f : X ⟶ Y}
{g : X ⟶ Z}
[CategoryTheory.Limits.HasPushout f g]
(h : Y ⟶ W)
(k : Z ⟶ W)
(w : CategoryTheory.CategoryStruct.comp f h = CategoryTheory.CategoryStruct.comp g k)
:
{ l //
CategoryTheory.CategoryStruct.comp CategoryTheory.Limits.pushout.inl l = h ∧ CategoryTheory.CategoryStruct.comp CategoryTheory.Limits.pushout.inr l = k }
A pair of morphisms h : Y ⟶ W and k : Z ⟶ W satisfying f ≫ h = g ≫ k induces a morphism
l : pushout f g ⟶ W such that pushout.inl ≫ l = h and pushout.inr ≫ l = k.
Instances For
theorem
CategoryTheory.Limits.pullback.condition_assoc
{C : Type u}
[CategoryTheory.Category.{v, u} C]
{X : C}
{Y : C}
{Z : C}
{f : X ⟶ Z}
{g : Y ⟶ Z}
[CategoryTheory.Limits.HasPullback f g]
{Z : C}
(h : Z ⟶ Z)
:
CategoryTheory.CategoryStruct.comp CategoryTheory.Limits.pullback.fst (CategoryTheory.CategoryStruct.comp f h) = CategoryTheory.CategoryStruct.comp CategoryTheory.Limits.pullback.snd (CategoryTheory.CategoryStruct.comp g h)
theorem
CategoryTheory.Limits.pullback.condition
{C : Type u}
[CategoryTheory.Category.{v, u} C]
{X : C}
{Y : C}
{Z : C}
{f : X ⟶ Z}
{g : Y ⟶ Z}
[CategoryTheory.Limits.HasPullback f g]
:
CategoryTheory.CategoryStruct.comp CategoryTheory.Limits.pullback.fst f = CategoryTheory.CategoryStruct.comp CategoryTheory.Limits.pullback.snd g
theorem
CategoryTheory.Limits.pushout.condition_assoc
{C : Type u}
[CategoryTheory.Category.{v, u} C]
{X : C}
{Y : C}
{Z : C}
{f : X ⟶ Y}
{g : X ⟶ Z}
[CategoryTheory.Limits.HasPushout f g]
{Z : C}
(h : CategoryTheory.Limits.pushout f g ⟶ Z)
:
CategoryTheory.CategoryStruct.comp f (CategoryTheory.CategoryStruct.comp CategoryTheory.Limits.pushout.inl h) = CategoryTheory.CategoryStruct.comp g (CategoryTheory.CategoryStruct.comp CategoryTheory.Limits.pushout.inr h)
theorem
CategoryTheory.Limits.pushout.condition
{C : Type u}
[CategoryTheory.Category.{v, u} C]
{X : C}
{Y : C}
{Z : C}
{f : X ⟶ Y}
{g : X ⟶ Z}
[CategoryTheory.Limits.HasPushout f g]
:
CategoryTheory.CategoryStruct.comp f CategoryTheory.Limits.pushout.inl = CategoryTheory.CategoryStruct.comp g CategoryTheory.Limits.pushout.inr
@[inline, reducible]
abbrev
CategoryTheory.Limits.pullback.map
{C : Type u}
[CategoryTheory.Category.{v, u} C]
{W : C}
{X : C}
{Y : C}
{Z : C}
{S : C}
{T : C}
(f₁ : W ⟶ S)
(f₂ : X ⟶ S)
[CategoryTheory.Limits.HasPullback f₁ f₂]
(g₁ : Y ⟶ T)
(g₂ : Z ⟶ T)
[CategoryTheory.Limits.HasPullback g₁ g₂]
(i₁ : W ⟶ Y)
(i₂ : X ⟶ Z)
(i₃ : S ⟶ T)
(eq₁ : CategoryTheory.CategoryStruct.comp f₁ i₃ = CategoryTheory.CategoryStruct.comp i₁ g₁)
(eq₂ : CategoryTheory.CategoryStruct.comp f₂ i₃ = CategoryTheory.CategoryStruct.comp i₂ g₂)
:
Given such a diagram, then there is a natural morphism W ×ₛ X ⟶ Y ×ₜ Z.
W ⟶ Y ↘ ↘ S ⟶ T ↗ ↗ X ⟶ Z
Instances For
@[inline, reducible]
abbrev
CategoryTheory.Limits.pullback.mapDesc
{C : Type u}
[CategoryTheory.Category.{v, u} C]
{X : C}
{Y : C}
{S : C}
{T : C}
(f : X ⟶ S)
(g : Y ⟶ S)
(i : S ⟶ T)
[CategoryTheory.Limits.HasPullback f g]
[CategoryTheory.Limits.HasPullback (CategoryTheory.CategoryStruct.comp f i) (CategoryTheory.CategoryStruct.comp g i)]
:
The canonical map X ×ₛ Y ⟶ X ×ₜ Y given S ⟶ T.
Instances For
@[inline, reducible]
abbrev
CategoryTheory.Limits.pushout.map
{C : Type u}
[CategoryTheory.Category.{v, u} C]
{W : C}
{X : C}
{Y : C}
{Z : C}
{S : C}
{T : C}
(f₁ : S ⟶ W)
(f₂ : S ⟶ X)
[CategoryTheory.Limits.HasPushout f₁ f₂]
(g₁ : T ⟶ Y)
(g₂ : T ⟶ Z)
[CategoryTheory.Limits.HasPushout g₁ g₂]
(i₁ : W ⟶ Y)
(i₂ : X ⟶ Z)
(i₃ : S ⟶ T)
(eq₁ : CategoryTheory.CategoryStruct.comp f₁ i₁ = CategoryTheory.CategoryStruct.comp i₃ g₁)
(eq₂ : CategoryTheory.CategoryStruct.comp f₂ i₂ = CategoryTheory.CategoryStruct.comp i₃ g₂)
:
Given such a diagram, then there is a natural morphism W ⨿ₛ X ⟶ Y ⨿ₜ Z.
W ⟶ Y
↗ ↗ S ⟶ T ↘ ↘ X ⟶ Z
Instances For
@[inline, reducible]
abbrev
CategoryTheory.Limits.pushout.mapLift
{C : Type u}
[CategoryTheory.Category.{v, u} C]
{X : C}
{Y : C}
{S : C}
{T : C}
(f : T ⟶ X)
(g : T ⟶ Y)
(i : S ⟶ T)
[CategoryTheory.Limits.HasPushout f g]
[CategoryTheory.Limits.HasPushout (CategoryTheory.CategoryStruct.comp i f) (CategoryTheory.CategoryStruct.comp i g)]
:
The canonical map X ⨿ₛ Y ⟶ X ⨿ₜ Y given S ⟶ T.
Instances For
theorem
CategoryTheory.Limits.pullback.hom_ext
{C : Type u}
[CategoryTheory.Category.{v, u} C]
{X : C}
{Y : C}
{Z : C}
{f : X ⟶ Z}
{g : Y ⟶ Z}
[CategoryTheory.Limits.HasPullback f g]
{W : C}
{k : W ⟶ CategoryTheory.Limits.pullback f g}
{l : W ⟶ CategoryTheory.Limits.pullback f g}
(h₀ : CategoryTheory.CategoryStruct.comp k CategoryTheory.Limits.pullback.fst = CategoryTheory.CategoryStruct.comp l CategoryTheory.Limits.pullback.fst)
(h₁ : CategoryTheory.CategoryStruct.comp k CategoryTheory.Limits.pullback.snd = CategoryTheory.CategoryStruct.comp l CategoryTheory.Limits.pullback.snd)
:
k = l
Two morphisms into a pullback are equal if their compositions with the pullback morphisms are equal
def
CategoryTheory.Limits.pullbackIsPullback
{C : Type u}
[CategoryTheory.Category.{v, u} C]
{X : C}
{Y : C}
{Z : C}
(f : X ⟶ Z)
(g : Y ⟶ Z)
[CategoryTheory.Limits.HasPullback f g]
:
CategoryTheory.Limits.IsLimit
(CategoryTheory.Limits.PullbackCone.mk CategoryTheory.Limits.pullback.fst CategoryTheory.Limits.pullback.snd
(_ :
CategoryTheory.CategoryStruct.comp CategoryTheory.Limits.pullback.fst f = CategoryTheory.CategoryStruct.comp CategoryTheory.Limits.pullback.snd g))
The pullback cone built from the pullback projections is a pullback.
Instances For
instance
CategoryTheory.Limits.pullback.fst_of_mono
{C : Type u}
[CategoryTheory.Category.{v, u} C]
{X : C}
{Y : C}
{Z : C}
{f : X ⟶ Z}
{g : Y ⟶ Z}
[CategoryTheory.Limits.HasPullback f g]
[CategoryTheory.Mono g]
:
CategoryTheory.Mono CategoryTheory.Limits.pullback.fst
The pullback of a monomorphism is a monomorphism
instance
CategoryTheory.Limits.pullback.snd_of_mono
{C : Type u}
[CategoryTheory.Category.{v, u} C]
{X : C}
{Y : C}
{Z : C}
{f : X ⟶ Z}
{g : Y ⟶ Z}
[CategoryTheory.Limits.HasPullback f g]
[CategoryTheory.Mono f]
:
CategoryTheory.Mono CategoryTheory.Limits.pullback.snd
The pullback of a monomorphism is a monomorphism
instance
CategoryTheory.Limits.mono_pullback_to_prod
{C : Type u_1}
[CategoryTheory.Category.{u_2, u_1} C]
{X : C}
{Y : C}
{Z : C}
(f : X ⟶ Z)
(g : Y ⟶ Z)
[CategoryTheory.Limits.HasPullback f g]
[CategoryTheory.Limits.HasBinaryProduct X Y]
:
CategoryTheory.Mono
(CategoryTheory.Limits.prod.lift CategoryTheory.Limits.pullback.fst CategoryTheory.Limits.pullback.snd)
The map X ×[Z] Y ⟶ X × Y is mono.
theorem
CategoryTheory.Limits.pushout.hom_ext
{C : Type u}
[CategoryTheory.Category.{v, u} C]
{X : C}
{Y : C}
{Z : C}
{f : X ⟶ Y}
{g : X ⟶ Z}
[CategoryTheory.Limits.HasPushout f g]
{W : C}
{k : CategoryTheory.Limits.pushout f g ⟶ W}
{l : CategoryTheory.Limits.pushout f g ⟶ W}
(h₀ : CategoryTheory.CategoryStruct.comp CategoryTheory.Limits.pushout.inl k = CategoryTheory.CategoryStruct.comp CategoryTheory.Limits.pushout.inl l)
(h₁ : CategoryTheory.CategoryStruct.comp CategoryTheory.Limits.pushout.inr k = CategoryTheory.CategoryStruct.comp CategoryTheory.Limits.pushout.inr l)
:
k = l
Two morphisms out of a pushout are equal if their compositions with the pushout morphisms are equal
def
CategoryTheory.Limits.pushoutIsPushout
{C : Type u}
[CategoryTheory.Category.{v, u} C]
{X : C}
{Y : C}
{Z : C}
(f : X ⟶ Y)
(g : X ⟶ Z)
[CategoryTheory.Limits.HasPushout f g]
:
CategoryTheory.Limits.IsColimit
(CategoryTheory.Limits.PushoutCocone.mk CategoryTheory.Limits.pushout.inl CategoryTheory.Limits.pushout.inr
(_ :
CategoryTheory.CategoryStruct.comp f CategoryTheory.Limits.pushout.inl = CategoryTheory.CategoryStruct.comp g CategoryTheory.Limits.pushout.inr))
The pushout cocone built from the pushout coprojections is a pushout.
Instances For
instance
CategoryTheory.Limits.pushout.inl_of_epi
{C : Type u}
[CategoryTheory.Category.{v, u} C]
{X : C}
{Y : C}
{Z : C}
{f : X ⟶ Y}
{g : X ⟶ Z}
[CategoryTheory.Limits.HasPushout f g]
[CategoryTheory.Epi g]
:
CategoryTheory.Epi CategoryTheory.Limits.pushout.inl
The pushout of an epimorphism is an epimorphism
instance
CategoryTheory.Limits.pushout.inr_of_epi
{C : Type u}
[CategoryTheory.Category.{v, u} C]
{X : C}
{Y : C}
{Z : C}
{f : X ⟶ Y}
{g : X ⟶ Z}
[CategoryTheory.Limits.HasPushout f g]
[CategoryTheory.Epi f]
:
CategoryTheory.Epi CategoryTheory.Limits.pushout.inr
The pushout of an epimorphism is an epimorphism
instance
CategoryTheory.Limits.epi_coprod_to_pushout
{C : Type u_1}
[CategoryTheory.Category.{u_2, u_1} C]
{X : C}
{Y : C}
{Z : C}
(f : X ⟶ Y)
(g : X ⟶ Z)
[CategoryTheory.Limits.HasPushout f g]
[CategoryTheory.Limits.HasBinaryCoproduct Y Z]
:
CategoryTheory.Epi
(CategoryTheory.Limits.coprod.desc CategoryTheory.Limits.pushout.inl CategoryTheory.Limits.pushout.inr)
The map X ⨿ Y ⟶ X ⨿[Z] Y is epi.
instance
CategoryTheory.Limits.pullback.map_isIso
{C : Type u}
[CategoryTheory.Category.{v, u} C]
{W : C}
{X : C}
{Y : C}
{Z : C}
{S : C}
{T : C}
(f₁ : W ⟶ S)
(f₂ : X ⟶ S)
[CategoryTheory.Limits.HasPullback f₁ f₂]
(g₁ : Y ⟶ T)
(g₂ : Z ⟶ T)
[CategoryTheory.Limits.HasPullback g₁ g₂]
(i₁ : W ⟶ Y)
(i₂ : X ⟶ Z)
(i₃ : S ⟶ T)
(eq₁ : CategoryTheory.CategoryStruct.comp f₁ i₃ = CategoryTheory.CategoryStruct.comp i₁ g₁)
(eq₂ : CategoryTheory.CategoryStruct.comp f₂ i₃ = CategoryTheory.CategoryStruct.comp i₂ g₂)
[CategoryTheory.IsIso i₁]
[CategoryTheory.IsIso i₂]
[CategoryTheory.IsIso i₃]
:
CategoryTheory.IsIso (CategoryTheory.Limits.pullback.map f₁ f₂ g₁ g₂ i₁ i₂ i₃ eq₁ eq₂)
@[simp]
theorem
CategoryTheory.Limits.pullback.congrHom_hom
{C : Type u}
[CategoryTheory.Category.{v, u} C]
{X : C}
{Y : C}
{Z : C}
{f₁ : X ⟶ Z}
{f₂ : X ⟶ Z}
{g₁ : Y ⟶ Z}
{g₂ : Y ⟶ Z}
(h₁ : f₁ = f₂)
(h₂ : g₁ = g₂)
[CategoryTheory.Limits.HasPullback f₁ g₁]
[CategoryTheory.Limits.HasPullback f₂ g₂]
:
(CategoryTheory.Limits.pullback.congrHom h₁ h₂).hom = CategoryTheory.Limits.pullback.map f₁ g₁ f₂ g₂ (CategoryTheory.CategoryStruct.id X)
(CategoryTheory.CategoryStruct.id Y) (CategoryTheory.CategoryStruct.id Z)
(_ :
CategoryTheory.CategoryStruct.comp f₁ (CategoryTheory.CategoryStruct.id Z) = CategoryTheory.CategoryStruct.comp (CategoryTheory.CategoryStruct.id X) f₂)
(_ :
CategoryTheory.CategoryStruct.comp g₁ (CategoryTheory.CategoryStruct.id Z) = CategoryTheory.CategoryStruct.comp (CategoryTheory.CategoryStruct.id Y) g₂)
def
CategoryTheory.Limits.pullback.congrHom
{C : Type u}
[CategoryTheory.Category.{v, u} C]
{X : C}
{Y : C}
{Z : C}
{f₁ : X ⟶ Z}
{f₂ : X ⟶ Z}
{g₁ : Y ⟶ Z}
{g₂ : Y ⟶ Z}
(h₁ : f₁ = f₂)
(h₂ : g₁ = g₂)
[CategoryTheory.Limits.HasPullback f₁ g₁]
[CategoryTheory.Limits.HasPullback f₂ g₂]
:
If f₁ = f₂ and g₁ = g₂, we may construct a canonical
isomorphism pullback f₁ g₁ ≅ pullback f₂ g₂
Instances For
@[simp]
theorem
CategoryTheory.Limits.pullback.congrHom_inv
{C : Type u}
[CategoryTheory.Category.{v, u} C]
{X : C}
{Y : C}
{Z : C}
{f₁ : X ⟶ Z}
{f₂ : X ⟶ Z}
{g₁ : Y ⟶ Z}
{g₂ : Y ⟶ Z}
(h₁ : f₁ = f₂)
(h₂ : g₁ = g₂)
[CategoryTheory.Limits.HasPullback f₁ g₁]
[CategoryTheory.Limits.HasPullback f₂ g₂]
:
(CategoryTheory.Limits.pullback.congrHom h₁ h₂).inv = CategoryTheory.Limits.pullback.map f₂ g₂ f₁ g₁ (CategoryTheory.CategoryStruct.id X)
(CategoryTheory.CategoryStruct.id Y) (CategoryTheory.CategoryStruct.id Z)
(_ :
CategoryTheory.CategoryStruct.comp f₂ (CategoryTheory.CategoryStruct.id Z) = CategoryTheory.CategoryStruct.comp (CategoryTheory.CategoryStruct.id X) f₁)
(_ :
CategoryTheory.CategoryStruct.comp g₂ (CategoryTheory.CategoryStruct.id Z) = CategoryTheory.CategoryStruct.comp (CategoryTheory.CategoryStruct.id Y) g₁)
instance
CategoryTheory.Limits.pushout.map_isIso
{C : Type u}
[CategoryTheory.Category.{v, u} C]
{W : C}
{X : C}
{Y : C}
{Z : C}
{S : C}
{T : C}
(f₁ : S ⟶ W)
(f₂ : S ⟶ X)
[CategoryTheory.Limits.HasPushout f₁ f₂]
(g₁ : T ⟶ Y)
(g₂ : T ⟶ Z)
[CategoryTheory.Limits.HasPushout g₁ g₂]
(i₁ : W ⟶ Y)
(i₂ : X ⟶ Z)
(i₃ : S ⟶ T)
(eq₁ : CategoryTheory.CategoryStruct.comp f₁ i₁ = CategoryTheory.CategoryStruct.comp i₃ g₁)
(eq₂ : CategoryTheory.CategoryStruct.comp f₂ i₂ = CategoryTheory.CategoryStruct.comp i₃ g₂)
[CategoryTheory.IsIso i₁]
[CategoryTheory.IsIso i₂]
[CategoryTheory.IsIso i₃]
:
CategoryTheory.IsIso (CategoryTheory.Limits.pushout.map f₁ f₂ g₁ g₂ i₁ i₂ i₃ eq₁ eq₂)
theorem
CategoryTheory.Limits.pullback.mapDesc_comp
{C : Type u}
[CategoryTheory.Category.{v, u} C]
{X : C}
{Y : C}
{S : C}
{T : C}
{S' : C}
(f : X ⟶ T)
(g : Y ⟶ T)
(i : T ⟶ S)
(i' : S ⟶ S')
[CategoryTheory.Limits.HasPullback f g]
[CategoryTheory.Limits.HasPullback (CategoryTheory.CategoryStruct.comp f i) (CategoryTheory.CategoryStruct.comp g i)]
[CategoryTheory.Limits.HasPullback (CategoryTheory.CategoryStruct.comp f (CategoryTheory.CategoryStruct.comp i i'))
(CategoryTheory.CategoryStruct.comp g (CategoryTheory.CategoryStruct.comp i i'))]
[CategoryTheory.Limits.HasPullback (CategoryTheory.CategoryStruct.comp (CategoryTheory.CategoryStruct.comp f i) i')
(CategoryTheory.CategoryStruct.comp (CategoryTheory.CategoryStruct.comp g i) i')]
:
CategoryTheory.Limits.pullback.mapDesc f g (CategoryTheory.CategoryStruct.comp i i') = CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.pullback.mapDesc f g i)
(CategoryTheory.CategoryStruct.comp
(CategoryTheory.Limits.pullback.mapDesc (CategoryTheory.CategoryStruct.comp f i)
(CategoryTheory.CategoryStruct.comp g i) i')
(CategoryTheory.Limits.pullback.congrHom
(_ :
CategoryTheory.CategoryStruct.comp (CategoryTheory.CategoryStruct.comp f i) i' = CategoryTheory.CategoryStruct.comp f (CategoryTheory.CategoryStruct.comp i i'))
(_ :
CategoryTheory.CategoryStruct.comp (CategoryTheory.CategoryStruct.comp g i) i' = CategoryTheory.CategoryStruct.comp g (CategoryTheory.CategoryStruct.comp i i'))).hom)
@[simp]
theorem
CategoryTheory.Limits.pushout.congrHom_hom
{C : Type u}
[CategoryTheory.Category.{v, u} C]
{X : C}
{Y : C}
{Z : C}
{f₁ : X ⟶ Y}
{f₂ : X ⟶ Y}
{g₁ : X ⟶ Z}
{g₂ : X ⟶ Z}
(h₁ : f₁ = f₂)
(h₂ : g₁ = g₂)
[CategoryTheory.Limits.HasPushout f₁ g₁]
[CategoryTheory.Limits.HasPushout f₂ g₂]
:
(CategoryTheory.Limits.pushout.congrHom h₁ h₂).hom = CategoryTheory.Limits.pushout.map f₁ g₁ f₂ g₂ (CategoryTheory.CategoryStruct.id Y)
(CategoryTheory.CategoryStruct.id Z) (CategoryTheory.CategoryStruct.id X)
(_ :
CategoryTheory.CategoryStruct.comp f₁ (CategoryTheory.CategoryStruct.id Y) = CategoryTheory.CategoryStruct.comp (CategoryTheory.CategoryStruct.id X) f₂)
(_ :
CategoryTheory.CategoryStruct.comp g₁ (CategoryTheory.CategoryStruct.id Z) = CategoryTheory.CategoryStruct.comp (CategoryTheory.CategoryStruct.id X) g₂)
def
CategoryTheory.Limits.pushout.congrHom
{C : Type u}
[CategoryTheory.Category.{v, u} C]
{X : C}
{Y : C}
{Z : C}
{f₁ : X ⟶ Y}
{f₂ : X ⟶ Y}
{g₁ : X ⟶ Z}
{g₂ : X ⟶ Z}
(h₁ : f₁ = f₂)
(h₂ : g₁ = g₂)
[CategoryTheory.Limits.HasPushout f₁ g₁]
[CategoryTheory.Limits.HasPushout f₂ g₂]
:
If f₁ = f₂ and g₁ = g₂, we may construct a canonical
isomorphism pushout f₁ g₁ ≅ pullback f₂ g₂
Instances For
@[simp]
theorem
CategoryTheory.Limits.pushout.congrHom_inv
{C : Type u}
[CategoryTheory.Category.{v, u} C]
{X : C}
{Y : C}
{Z : C}
{f₁ : X ⟶ Y}
{f₂ : X ⟶ Y}
{g₁ : X ⟶ Z}
{g₂ : X ⟶ Z}
(h₁ : f₁ = f₂)
(h₂ : g₁ = g₂)
[CategoryTheory.Limits.HasPushout f₁ g₁]
[CategoryTheory.Limits.HasPushout f₂ g₂]
:
(CategoryTheory.Limits.pushout.congrHom h₁ h₂).inv = CategoryTheory.Limits.pushout.map f₂ g₂ f₁ g₁ (CategoryTheory.CategoryStruct.id Y)
(CategoryTheory.CategoryStruct.id Z) (CategoryTheory.CategoryStruct.id X)
(_ :
CategoryTheory.CategoryStruct.comp f₂ (CategoryTheory.CategoryStruct.id Y) = CategoryTheory.CategoryStruct.comp (CategoryTheory.CategoryStruct.id X) f₁)
(_ :
CategoryTheory.CategoryStruct.comp g₂ (CategoryTheory.CategoryStruct.id Z) = CategoryTheory.CategoryStruct.comp (CategoryTheory.CategoryStruct.id X) g₁)
theorem
CategoryTheory.Limits.pushout.mapLift_comp
{C : Type u}
[CategoryTheory.Category.{v, u} C]
{X : C}
{Y : C}
{S : C}
{T : C}
{S' : C}
(f : T ⟶ X)
(g : T ⟶ Y)
(i : S ⟶ T)
(i' : S' ⟶ S)
[CategoryTheory.Limits.HasPushout f g]
[CategoryTheory.Limits.HasPushout (CategoryTheory.CategoryStruct.comp i f) (CategoryTheory.CategoryStruct.comp i g)]
[CategoryTheory.Limits.HasPushout (CategoryTheory.CategoryStruct.comp i' (CategoryTheory.CategoryStruct.comp i f))
(CategoryTheory.CategoryStruct.comp i' (CategoryTheory.CategoryStruct.comp i g))]
[CategoryTheory.Limits.HasPushout (CategoryTheory.CategoryStruct.comp (CategoryTheory.CategoryStruct.comp i' i) f)
(CategoryTheory.CategoryStruct.comp (CategoryTheory.CategoryStruct.comp i' i) g)]
:
CategoryTheory.Limits.pushout.mapLift f g (CategoryTheory.CategoryStruct.comp i' i) = CategoryTheory.CategoryStruct.comp
(CategoryTheory.Limits.pushout.congrHom
(_ :
CategoryTheory.CategoryStruct.comp (CategoryTheory.CategoryStruct.comp i' i) f = CategoryTheory.CategoryStruct.comp i' (CategoryTheory.CategoryStruct.comp i f))
(_ :
CategoryTheory.CategoryStruct.comp (CategoryTheory.CategoryStruct.comp i' i) g = CategoryTheory.CategoryStruct.comp i' (CategoryTheory.CategoryStruct.comp i g))).hom
(CategoryTheory.CategoryStruct.comp
(CategoryTheory.Limits.pushout.mapLift (CategoryTheory.CategoryStruct.comp i f)
(CategoryTheory.CategoryStruct.comp i g) i')
(CategoryTheory.Limits.pushout.mapLift f g i))
def
CategoryTheory.Limits.pullbackComparison
{C : Type u}
[CategoryTheory.Category.{v, u} C]
{D : Type u₂}
[CategoryTheory.Category.{v₂, u₂} D]
{X : C}
{Y : C}
{Z : C}
(G : CategoryTheory.Functor C D)
(f : X ⟶ Z)
(g : Y ⟶ Z)
[CategoryTheory.Limits.HasPullback f g]
[CategoryTheory.Limits.HasPullback (G.map f) (G.map g)]
:
G.obj (CategoryTheory.Limits.pullback f g) ⟶ CategoryTheory.Limits.pullback (G.map f) (G.map g)
The comparison morphism for the pullback of f,g.
This is an isomorphism iff G preserves the pullback of f,g; see
CategoryTheory/Limits/Preserves/Shapes/Pullbacks.lean
Instances For
@[simp]
theorem
CategoryTheory.Limits.pullbackComparison_comp_fst_assoc
{C : Type u}
[CategoryTheory.Category.{v, u} C]
{D : Type u₂}
[CategoryTheory.Category.{v₂, u₂} D]
{X : C}
{Y : C}
{Z : C}
(G : CategoryTheory.Functor C D)
(f : X ⟶ Z)
(g : Y ⟶ Z)
[CategoryTheory.Limits.HasPullback f g]
[CategoryTheory.Limits.HasPullback (G.map f) (G.map g)]
{Z : D}
(h : G.obj X ⟶ Z)
:
CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.pullbackComparison G f g)
(CategoryTheory.CategoryStruct.comp CategoryTheory.Limits.pullback.fst h) = CategoryTheory.CategoryStruct.comp (G.map CategoryTheory.Limits.pullback.fst) h
@[simp]
theorem
CategoryTheory.Limits.pullbackComparison_comp_fst
{C : Type u}
[CategoryTheory.Category.{v, u} C]
{D : Type u₂}
[CategoryTheory.Category.{v₂, u₂} D]
{X : C}
{Y : C}
{Z : C}
(G : CategoryTheory.Functor C D)
(f : X ⟶ Z)
(g : Y ⟶ Z)
[CategoryTheory.Limits.HasPullback f g]
[CategoryTheory.Limits.HasPullback (G.map f) (G.map g)]
:
CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.pullbackComparison G f g) CategoryTheory.Limits.pullback.fst = G.map CategoryTheory.Limits.pullback.fst
@[simp]
theorem
CategoryTheory.Limits.pullbackComparison_comp_snd_assoc
{C : Type u}
[CategoryTheory.Category.{v, u} C]
{D : Type u₂}
[CategoryTheory.Category.{v₂, u₂} D]
{X : C}
{Y : C}
{Z : C}
(G : CategoryTheory.Functor C D)
(f : X ⟶ Z)
(g : Y ⟶ Z)
[CategoryTheory.Limits.HasPullback f g]
[CategoryTheory.Limits.HasPullback (G.map f) (G.map g)]
{Z : D}
(h : G.obj Y ⟶ Z)
:
CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.pullbackComparison G f g)
(CategoryTheory.CategoryStruct.comp CategoryTheory.Limits.pullback.snd h) = CategoryTheory.CategoryStruct.comp (G.map CategoryTheory.Limits.pullback.snd) h
@[simp]
theorem
CategoryTheory.Limits.pullbackComparison_comp_snd
{C : Type u}
[CategoryTheory.Category.{v, u} C]
{D : Type u₂}
[CategoryTheory.Category.{v₂, u₂} D]
{X : C}
{Y : C}
{Z : C}
(G : CategoryTheory.Functor C D)
(f : X ⟶ Z)
(g : Y ⟶ Z)
[CategoryTheory.Limits.HasPullback f g]
[CategoryTheory.Limits.HasPullback (G.map f) (G.map g)]
:
CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.pullbackComparison G f g) CategoryTheory.Limits.pullback.snd = G.map CategoryTheory.Limits.pullback.snd
@[simp]
theorem
CategoryTheory.Limits.map_lift_pullbackComparison_assoc
{C : Type u}
[CategoryTheory.Category.{v, u} C]
{D : Type u₂}
[CategoryTheory.Category.{v₂, u₂} D]
{X : C}
{Y : C}
{Z : C}
(G : CategoryTheory.Functor C D)
(f : X ⟶ Z)
(g : Y ⟶ Z)
[CategoryTheory.Limits.HasPullback f g]
[CategoryTheory.Limits.HasPullback (G.map f) (G.map g)]
{W : C}
{h : W ⟶ X}
{k : W ⟶ Y}
(w : CategoryTheory.CategoryStruct.comp h f = CategoryTheory.CategoryStruct.comp k g)
{Z : D}
(h : CategoryTheory.Limits.pullback (G.map f) (G.map g) ⟶ Z)
:
CategoryTheory.CategoryStruct.comp (G.map (CategoryTheory.Limits.pullback.lift h k w))
(CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.pullbackComparison G f g) h) = CategoryTheory.CategoryStruct.comp
(CategoryTheory.Limits.pullback.lift (G.map h) (G.map k)
(_ :
CategoryTheory.CategoryStruct.comp (G.map h) (G.map f) = CategoryTheory.CategoryStruct.comp (G.map k) (G.map g)))
h
@[simp]
theorem
CategoryTheory.Limits.map_lift_pullbackComparison
{C : Type u}
[CategoryTheory.Category.{v, u} C]
{D : Type u₂}
[CategoryTheory.Category.{v₂, u₂} D]
{X : C}
{Y : C}
{Z : C}
(G : CategoryTheory.Functor C D)
(f : X ⟶ Z)
(g : Y ⟶ Z)
[CategoryTheory.Limits.HasPullback f g]
[CategoryTheory.Limits.HasPullback (G.map f) (G.map g)]
{W : C}
{h : W ⟶ X}
{k : W ⟶ Y}
(w : CategoryTheory.CategoryStruct.comp h f = CategoryTheory.CategoryStruct.comp k g)
:
CategoryTheory.CategoryStruct.comp (G.map (CategoryTheory.Limits.pullback.lift h k w))
(CategoryTheory.Limits.pullbackComparison G f g) = CategoryTheory.Limits.pullback.lift (G.map h) (G.map k)
(_ :
CategoryTheory.CategoryStruct.comp (G.map h) (G.map f) = CategoryTheory.CategoryStruct.comp (G.map k) (G.map g))
def
CategoryTheory.Limits.pushoutComparison
{C : Type u}
[CategoryTheory.Category.{v, u} C]
{D : Type u₂}
[CategoryTheory.Category.{v₂, u₂} D]
{X : C}
{Y : C}
{Z : C}
(G : CategoryTheory.Functor C D)
(f : X ⟶ Y)
(g : X ⟶ Z)
[CategoryTheory.Limits.HasPushout f g]
[CategoryTheory.Limits.HasPushout (G.map f) (G.map g)]
:
CategoryTheory.Limits.pushout (G.map f) (G.map g) ⟶ G.obj (CategoryTheory.Limits.pushout f g)
The comparison morphism for the pushout of f,g.
This is an isomorphism iff G preserves the pushout of f,g; see
CategoryTheory/Limits/Preserves/Shapes/Pullbacks.lean
Instances For
@[simp]
theorem
CategoryTheory.Limits.inl_comp_pushoutComparison_assoc
{C : Type u}
[CategoryTheory.Category.{v, u} C]
{D : Type u₂}
[CategoryTheory.Category.{v₂, u₂} D]
{X : C}
{Y : C}
{Z : C}
(G : CategoryTheory.Functor C D)
(f : X ⟶ Y)
(g : X ⟶ Z)
[CategoryTheory.Limits.HasPushout f g]
[CategoryTheory.Limits.HasPushout (G.map f) (G.map g)]
{Z : D}
(h : G.obj (CategoryTheory.Limits.pushout f g) ⟶ Z)
:
CategoryTheory.CategoryStruct.comp CategoryTheory.Limits.pushout.inl
(CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.pushoutComparison G f g) h) = CategoryTheory.CategoryStruct.comp (G.map CategoryTheory.Limits.pushout.inl) h
@[simp]
theorem
CategoryTheory.Limits.inl_comp_pushoutComparison
{C : Type u}
[CategoryTheory.Category.{v, u} C]
{D : Type u₂}
[CategoryTheory.Category.{v₂, u₂} D]
{X : C}
{Y : C}
{Z : C}
(G : CategoryTheory.Functor C D)
(f : X ⟶ Y)
(g : X ⟶ Z)
[CategoryTheory.Limits.HasPushout f g]
[CategoryTheory.Limits.HasPushout (G.map f) (G.map g)]
:
CategoryTheory.CategoryStruct.comp CategoryTheory.Limits.pushout.inl (CategoryTheory.Limits.pushoutComparison G f g) = G.map CategoryTheory.Limits.pushout.inl
@[simp]
theorem
CategoryTheory.Limits.inr_comp_pushoutComparison_assoc
{C : Type u}
[CategoryTheory.Category.{v, u} C]
{D : Type u₂}
[CategoryTheory.Category.{v₂, u₂} D]
{X : C}
{Y : C}
{Z : C}
(G : CategoryTheory.Functor C D)
(f : X ⟶ Y)
(g : X ⟶ Z)
[CategoryTheory.Limits.HasPushout f g]
[CategoryTheory.Limits.HasPushout (G.map f) (G.map g)]
{Z : D}
(h : G.obj (CategoryTheory.Limits.pushout f g) ⟶ Z)
:
CategoryTheory.CategoryStruct.comp CategoryTheory.Limits.pushout.inr
(CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.pushoutComparison G f g) h) = CategoryTheory.CategoryStruct.comp (G.map CategoryTheory.Limits.pushout.inr) h
@[simp]
theorem
CategoryTheory.Limits.inr_comp_pushoutComparison
{C : Type u}
[CategoryTheory.Category.{v, u} C]
{D : Type u₂}
[CategoryTheory.Category.{v₂, u₂} D]
{X : C}
{Y : C}
{Z : C}
(G : CategoryTheory.Functor C D)
(f : X ⟶ Y)
(g : X ⟶ Z)
[CategoryTheory.Limits.HasPushout f g]
[CategoryTheory.Limits.HasPushout (G.map f) (G.map g)]
:
CategoryTheory.CategoryStruct.comp CategoryTheory.Limits.pushout.inr (CategoryTheory.Limits.pushoutComparison G f g) = G.map CategoryTheory.Limits.pushout.inr
@[simp]
theorem
CategoryTheory.Limits.pushoutComparison_map_desc_assoc
{C : Type u}
[CategoryTheory.Category.{v, u} C]
{D : Type u₂}
[CategoryTheory.Category.{v₂, u₂} D]
{X : C}
{Y : C}
{Z : C}
(G : CategoryTheory.Functor C D)
(f : X ⟶ Y)
(g : X ⟶ Z)
[CategoryTheory.Limits.HasPushout f g]
[CategoryTheory.Limits.HasPushout (G.map f) (G.map g)]
{W : C}
{h : Y ⟶ W}
{k : Z ⟶ W}
(w : CategoryTheory.CategoryStruct.comp f h = CategoryTheory.CategoryStruct.comp g k)
{Z : D}
(h : G.obj W ⟶ Z)
:
CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.pushoutComparison G f g)
(CategoryTheory.CategoryStruct.comp (G.map (CategoryTheory.Limits.pushout.desc h k w)) h) = CategoryTheory.CategoryStruct.comp
(CategoryTheory.Limits.pushout.desc (G.map h) (G.map k)
(_ :
CategoryTheory.CategoryStruct.comp (G.map f) (G.map h) = CategoryTheory.CategoryStruct.comp (G.map g) (G.map k)))
h
@[simp]
theorem
CategoryTheory.Limits.pushoutComparison_map_desc
{C : Type u}
[CategoryTheory.Category.{v, u} C]
{D : Type u₂}
[CategoryTheory.Category.{v₂, u₂} D]
{X : C}
{Y : C}
{Z : C}
(G : CategoryTheory.Functor C D)
(f : X ⟶ Y)
(g : X ⟶