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.
@[match_pattern, inline, reducible]
The left point of the walking cospan.
@[match_pattern, inline, reducible]
The right point of the walking cospan.
@[match_pattern, inline, reducible]
The central point of the walking cospan.
Equations
@[inline, reducible]
The type of objects for the diagram indexing a pushout, defined as a special case of
WidePushoutShape.
@[match_pattern, inline, reducible]
The left point of the walking span.
@[match_pattern, inline, reducible]
The right point of the walking span.
@[match_pattern, inline, reducible]
The central point of the walking span.
Equations
@[inline, reducible]
The type of arrows for the diagram indexing a pullback.
Equations
- CategoryTheory.Limits.WalkingCospan.Hom = CategoryTheory.Limits.WidePullbackShape.Hom
@[match_pattern, inline, reducible]
The left arrow of the walking cospan.
@[match_pattern, inline, reducible]
The right arrow of the walking cospan.
@[match_pattern, inline, reducible]
The identity arrows of the walking cospan.
@[inline, reducible]
The type of arrows for the diagram indexing a pushout.
Equations
- CategoryTheory.Limits.WalkingSpan.Hom = CategoryTheory.Limits.WidePushoutShape.Hom
@[match_pattern, inline, reducible]
The left arrow of the walking span.
@[match_pattern, inline, reducible]
The right arrow of the walking span.
@[match_pattern, inline, reducible]
The identity arrows of the walking span.
instance
CategoryTheory.Limits.WalkingSpan.instSubsingletonHomWalkingSpanToQuiverStructWalkingPair
(X : CategoryTheory.Limits.WalkingSpan)
(Y : CategoryTheory.Limits.WalkingSpan)
:
Subsingleton (X ⟶ Y)
Equations
- ⋯ = ⋯
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.
Equations
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.
Equations
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.
Equations
- One or more equations did not get rendered due to their size.
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.
Equations
- One or more equations did not get rendered due to their size.
@[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 ⋯
@[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 ⋯
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
Equations
@[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 ⋯
@[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 ⋯
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
Equations
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.
Equations
- One or more equations did not get rendered due to their size.
@[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.
Equations
- One or more equations did not get rendered due to their size.
@[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.
Equations
- One or more equations did not get rendered due to their size.
@[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.
Equations
- One or more equations did not get rendered due to their size.
@[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.
@[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.
Equations
@[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.
Equations
@[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
Equations
- CategoryTheory.Limits.PullbackCone.isLimitAux t lift fac_left fac_right uniq = { lift := lift, fac := ⋯, uniq := uniq }
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 : s.pt ⟶ t.pt //
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.
Equations
- CategoryTheory.Limits.PullbackCone.isLimitAux' t create = CategoryTheory.Limits.PullbackCone.isLimitAux t (fun (s : CategoryTheory.Limits.PullbackCone f g) => ↑(create s)) ⋯ ⋯ ⋯
@[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) =>
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.
Equations
- One or more equations did not get rendered due to their size.
@[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.
Equations
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.
Equations
- CategoryTheory.Limits.PullbackCone.IsLimit.lift ht h k w = ht.lift (CategoryTheory.Limits.PullbackCone.mk h k w)
@[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)
:
{ l : W ⟶ t.pt //
CategoryTheory.CategoryStruct.comp l (CategoryTheory.Limits.PullbackCone.fst t) = h ∧ CategoryTheory.CategoryStruct.comp l (CategoryTheory.Limits.PullbackCone.snd t) = k }
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.
Equations
- CategoryTheory.Limits.PullbackCone.IsLimit.lift' ht h k w = { val := CategoryTheory.Limits.PullbackCone.IsLimit.lift ht h k w, property := ⋯ }
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.
Equations
- One or more equations did not get rendered due to their size.
def
CategoryTheory.Limits.PullbackCone.flip
{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)
:
@[simp]
theorem
CategoryTheory.Limits.PullbackCone.flip_pt
{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)
:
(CategoryTheory.Limits.PullbackCone.flip t).pt = t.pt
@[simp]
theorem
CategoryTheory.Limits.PullbackCone.flip_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)
:
@[simp]
theorem
CategoryTheory.Limits.PullbackCone.flip_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)
:
def
CategoryTheory.Limits.PullbackCone.flipFlipIso
{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)
:
Flipping a pullback cone twice gives an isomorphic cone.
Equations
- One or more equations did not get rendered due to their size.
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}
{t : CategoryTheory.Limits.PullbackCone f g}
(ht : CategoryTheory.Limits.IsLimit t)
:
The flip of a pullback square is a pullback square.
Equations
- One or more equations did not get rendered due to their size.
def
CategoryTheory.Limits.PullbackCone.isLimitOfFlip
{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 (CategoryTheory.Limits.PullbackCone.flip t))
:
A square is a pullback square if its flip is.
Equations
- One or more equations did not get rendered due to their size.
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.
Equations
- One or more equations did not get rendered due to their size.
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) ⋯))
:
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)
:
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.
Equations
- One or more equations did not get rendered due to their size.
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)
:
If W is the pullback of f, g,
it is also the pullback of f ≫ i, g ≫ i for any mono i.
Equations
- One or more equations did not get rendered due to their size.
@[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.
@[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.
Equations
@[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.
Equations
@[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
Equations
- CategoryTheory.Limits.PushoutCocone.isColimitAux t desc fac_left fac_right uniq = { desc := desc, fac := ⋯, uniq := uniq }
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 : t.pt ⟶ s.pt //
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.
Equations
- CategoryTheory.Limits.PushoutCocone.isColimitAux' t create = CategoryTheory.Limits.PushoutCocone.isColimitAux t (fun (s : CategoryTheory.Limits.PushoutCocone f g) => ↑(create s)) ⋯ ⋯ ⋯
@[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
@[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) =>
CategoryTheory.Limits.WalkingPair.casesOn j' inl inr
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.
Equations
- One or more equations did not get rendered due to their size.
@[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
Equations
- CategoryTheory.Limits.PushoutCocone.IsColimit.desc ht h k w = ht.desc (CategoryTheory.Limits.PushoutCocone.mk h k w)
@[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)
:
{ l : t.pt ⟶ W //
CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.PushoutCocone.inl t) l = h ∧ CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.PushoutCocone.inr t) l = 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.
Equations
- CategoryTheory.Limits.PushoutCocone.IsColimit.desc' ht h k w = { val := CategoryTheory.Limits.PushoutCocone.IsColimit.desc ht h k w, property := ⋯ }
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.
Equations
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.
Equations
- One or more equations did not get rendered due to their size.
def
CategoryTheory.Limits.PushoutCocone.flip
{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)
:
@[simp]
theorem
CategoryTheory.Limits.PushoutCocone.flip_pt
{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)
:
(CategoryTheory.Limits.PushoutCocone.flip t).pt = t.pt
@[simp]
theorem
CategoryTheory.Limits.PushoutCocone.flip_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)
:
@[simp]
theorem
CategoryTheory.Limits.PushoutCocone.flip_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)
:
def
CategoryTheory.Limits.PushoutCocone.flipFlipIso
{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)
:
Flipping a pushout cocone twice gives an isomorphic cocone.
Equations
- One or more equations did not get rendered due to their size.
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}
{t : CategoryTheory.Limits.PushoutCocone f g}
(ht : CategoryTheory.Limits.IsColimit t)
:
The flip of a pushout square is a pushout square.
Equations
- One or more equations did not get rendered due to their size.
def
CategoryTheory.Limits.PushoutCocone.isColimitOfFlip
{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 (CategoryTheory.Limits.PushoutCocone.flip t))
:
A square is a pushout square if its flip is.
Equations
- One or more equations did not get rendered due to their size.
def
CategoryTheory.Limits.PushoutCocone.isColimitMkIdId
{C : Type u}
[CategoryTheory.Category.{v, u} C]
{X : C}
{Y : C}
(f : X ⟶ Y)
[CategoryTheory.Epi f]
:
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.
Equations
- One or more equations did not get rendered due to their size.
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) ⋯))
:
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₁ := ⋯;
let_fun reassoc₂ := ⋯;
CategoryTheory.Limits.IsColimit
(CategoryTheory.Limits.PushoutCocone.mk (CategoryTheory.Limits.PushoutCocone.inl s)
(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.
Equations
- One or more equations did not get rendered due to their size.
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)
:
If W is the pushout of f, g,
it is also the pushout of h ≫ f, h ≫ g for any epi h.
Equations
- One or more equations did not get rendered due to their size.
@[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.
Equations
- CategoryTheory.Limits.Cone.ofPullbackCone t = { pt := t.pt, π := CategoryTheory.CategoryStruct.comp t.π (CategoryTheory.Limits.diagramIsoCospan F).inv }
@[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))
:
@[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
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.
Equations
- CategoryTheory.Limits.Cocone.ofPushoutCocone t = { pt := t.pt, ι := CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.diagramIsoSpan F).hom t.ι }
@[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.
Equations
- CategoryTheory.Limits.PullbackCone.ofCone t = { pt := t.pt, π := CategoryTheory.CategoryStruct.comp t.π (CategoryTheory.Limits.diagramIsoCospan F).hom }
@[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)
:
A diagram WalkingCospan ⥤ C is isomorphic to some PullbackCone.mk after
composing with diagramIsoCospan.
Equations
- One or more equations did not get rendered due to their size.
@[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
@[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)
:
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.
Equations
- CategoryTheory.Limits.PushoutCocone.ofCocone t = { pt := t.pt, ι := CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.diagramIsoSpan F).inv t.ι }
@[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)
:
A diagram WalkingSpan ⥤ C is isomorphic to some PushoutCocone.mk after composing with
diagramIsoSpan.
Equations
- One or more equations did not get rendered due to their size.
@[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.
@[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.
@[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.
Equations
@[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.
Equations
@[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.
Equations
- CategoryTheory.Limits.pullback.fst = CategoryTheory.Limits.limit.π (CategoryTheory.Limits.cospan f g) CategoryTheory.Limits.WalkingCospan.left
@[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.
Equations
- CategoryTheory.Limits.pullback.snd = CategoryTheory.Limits.limit.π (CategoryTheory.Limits.cospan f g) CategoryTheory.Limits.WalkingCospan.right
@[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.
Equations
- CategoryTheory.Limits.pushout.inl = CategoryTheory.Limits.colimit.ι (CategoryTheory.Limits.span f g) CategoryTheory.Limits.WalkingSpan.left
@[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.
Equations
- CategoryTheory.Limits.pushout.inr = CategoryTheory.Limits.colimit.ι (CategoryTheory.Limits.span f g) CategoryTheory.Limits.WalkingSpan.right
@[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.
@[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.
@[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 : W ⟶ CategoryTheory.Limits.pullback f g //
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.
Equations
- CategoryTheory.Limits.pullback.lift' h k w = { val := CategoryTheory.Limits.pullback.lift h k w, property := ⋯ }
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.Limits.pushout f g ⟶ W //
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.
Equations
- CategoryTheory.Limits.pullback.desc' h k w = { val := CategoryTheory.Limits.pushout.desc h k w, property := ⋯ }
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
Equations
- One or more equations did not get rendered due to their size.
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.
Equations
- One or more equations did not get rendered due to their size.
@[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
Equations
- One or more equations did not get rendered due to their size.
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.
Equations
- One or more equations did not get rendered due to their size.
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 ⋯)
The pullback cone built from the pullback projections is a pullback.
Equations
- One or more equations did not get rendered due to their size.
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
Equations
- ⋯ = ⋯
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
Equations
- ⋯ = ⋯
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.
Equations
- ⋯ = ⋯
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 ⋯)
The pushout cocone built from the pushout coprojections is a pushout.
Equations
- One or more equations did not get rendered due to their size.
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
Equations
- ⋯ = ⋯
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
Equations
- ⋯ = ⋯
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.
Equations
- ⋯ = ⋯
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₂)
Equations
- ⋯ = ⋯
@[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) ⋯ ⋯
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₂
Equations
- One or more equations did not get rendered due to their size.
@[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) ⋯ ⋯
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₂)
Equations
- ⋯ = ⋯
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 ⋯ ⋯).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) ⋯ ⋯
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₂
Equations
- One or more equations did not get rendered due to their size.
@[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) ⋯ ⋯
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 ⋯ ⋯).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
Mathlib/CategoryTheory/Limits/Preserves/Shapes/Pullbacks.lean
Equations
- CategoryTheory.Limits.pullbackComparison G f g = CategoryTheory.Limits.pullback.lift (G.map CategoryTheory.Limits.pullback.fst) (G.map CategoryTheory.Limits.pullback.snd) ⋯
@[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) ⋯) 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) ⋯
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
Mathlib/CategoryTheory/Limits/Preserves/Shapes/Pullbacks.lean
Equations
- CategoryTheory.Limits.pushoutComparison G f g = CategoryTheory.Limits.pushout.desc (G.map CategoryTheory.Limits.pushout.inl) (G.map CategoryTheory.Limits.pushout.inr) ⋯
@[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) ⋯) 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 ⟶ 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)
:
CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.pushoutComparison G f g)
(G.map (CategoryTheory.Limits.pushout.desc h k w)) = CategoryTheory.Limits.pushout.desc (G.map h) (G.map k) ⋯
theorem
CategoryTheory.Limits.hasPullback_symmetry
{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]
:
Making this a global instance would make the typeclass search go in an infinite loop.
def
CategoryTheory.Limits.pullbackSymmetry
{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 isomorphism X ×[Z] Y ≅ Y ×[Z] X.
Equations
- One or more equations did not get rendered due to their size.
@[simp]
theorem
CategoryTheory.Limits.pullbackSymmetry_hom_comp_fst_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 : Y ⟶ Z)
:
CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.pullbackSymmetry f g).hom
(CategoryTheory.CategoryStruct.comp CategoryTheory.Limits.pullback.fst h) = CategoryTheory.CategoryStruct.comp CategoryTheory.Limits.pullback.snd h
@[simp]
theorem
CategoryTheory.Limits.pullbackSymmetry_hom_comp_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]
:
CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.pullbackSymmetry f g).hom CategoryTheory.Limits.pullback.fst = CategoryTheory.Limits.pullback.snd
@[simp]
theorem
CategoryTheory.Limits.pullbackSymmetry_hom_comp_snd_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 : X ⟶ Z)
:
CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.pullbackSymmetry f g).hom
(CategoryTheory.CategoryStruct.comp CategoryTheory.Limits.pullback.snd h) = CategoryTheory.CategoryStruct.comp CategoryTheory.Limits.pullback.fst h
@[simp]
theorem
CategoryTheory.Limits.pullbackSymmetry_hom_comp_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]
:
CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.pullbackSymmetry f g).hom CategoryTheory.Limits.pullback.snd = CategoryTheory.Limits.pullback.fst
@[simp]
theorem
CategoryTheory.Limits.pullbackSymmetry_inv_comp_fst_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 : X ⟶ Z)
:
CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.pullbackSymmetry f g).inv
(CategoryTheory.CategoryStruct.comp CategoryTheory.Limits.pullback.fst h) = CategoryTheory.CategoryStruct.comp CategoryTheory.Limits.pullback.snd h
@[simp]
theorem
CategoryTheory.Limits.pullbackSymmetry_inv_comp_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]
:
CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.pullbackSymmetry f g).inv CategoryTheory.Limits.pullback.fst = CategoryTheory.Limits.pullback.snd
@[simp]
theorem
CategoryTheory.Limits.pullbackSymmetry_inv_comp_snd_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 : Y ⟶ Z)
:
CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.pullbackSymmetry f g).inv
(CategoryTheory.CategoryStruct.comp CategoryTheory.Limits.pullback.snd h) = CategoryTheory.CategoryStruct.comp CategoryTheory.Limits.pullback.fst h
@[simp]
theorem
CategoryTheory.Limits.pullbackSymmetry_inv_comp_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]
:
CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.pullbackSymmetry f g).inv CategoryTheory.Limits.pullback.snd = CategoryTheory.Limits.pullback.fst
theorem
CategoryTheory.Limits.hasPushout_symmetry
{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]
:
Making this a global instance would make the typeclass search go in an infinite loop.
def
CategoryTheory.Limits.pushoutSymmetry
{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 isomorphism Y ⨿[X] Z ≅ Z ⨿[X] Y.
Equations
- One or more equations did not get rendered due to their size.
@[simp]
theorem
CategoryTheory.Limits.inl_comp_pushoutSymmetry_hom_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 g f ⟶ Z)
:
CategoryTheory.CategoryStruct.comp CategoryTheory.Limits.pushout.inl
(CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.pushoutSymmetry f g).hom h) = CategoryTheory.CategoryStruct.comp CategoryTheory.Limits.pushout.inr h
@[simp]
theorem
CategoryTheory.Limits.inl_comp_pushoutSymmetry_hom
{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 CategoryTheory.Limits.pushout.inl (CategoryTheory.Limits.pushoutSymmetry f g).hom = CategoryTheory.Limits.pushout.inr
@[simp]
theorem
CategoryTheory.Limits.inr_comp_pushoutSymmetry_hom_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 g f ⟶ Z)
:
CategoryTheory.CategoryStruct.comp CategoryTheory.Limits.pushout.inr
(CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.pushoutSymmetry f g).hom h) = CategoryTheory.CategoryStruct.comp CategoryTheory.Limits.pushout.inl h
@[simp]
theorem
CategoryTheory.Limits.inr_comp_pushoutSymmetry_hom
{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 CategoryTheory.Limits.pushout.inr (CategoryTheory.Limits.pushoutSymmetry f g).hom = CategoryTheory.Limits.pushout.inl
@[simp]
theorem
CategoryTheory.Limits.inl_comp_pushoutSymmetry_inv_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 CategoryTheory.Limits.pushout.inl
(CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.pushoutSymmetry f g).inv h) = CategoryTheory.CategoryStruct.comp CategoryTheory.Limits.pushout.inr h
@[simp]
theorem
CategoryTheory.Limits.inl_comp_pushoutSymmetry_inv
{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 CategoryTheory.Limits.pushout.inl (CategoryTheory.Limits.pushoutSymmetry f g).inv = CategoryTheory.Limits.pushout.inr
@[simp]
theorem
CategoryTheory.Limits.inr_comp_pushoutSymmetry_inv_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 CategoryTheory.Limits.pushout.inr
(CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.pushoutSymmetry f g).inv h) = CategoryTheory.CategoryStruct.comp CategoryTheory.Limits.pushout.inl h
@[simp]
theorem
CategoryTheory.Limits.inr_comp_pushoutSymmetry_inv
{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 CategoryTheory.Limits.pushout.inr (CategoryTheory.Limits.pushoutSymmetry f g).inv = CategoryTheory.Limits.pushout.inl
noncomputable def
CategoryTheory.Limits.pullbackIsPullbackOfCompMono
{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]
[CategoryTheory.Limits.HasPullback f g]
:
CategoryTheory.Limits.IsLimit
(CategoryTheory.Limits.PullbackCone.mk CategoryTheory.Limits.pullback.fst CategoryTheory.Limits.pullback.snd ⋯)
The pullback of f, g is also the pullback of f ≫ i, g ≫ i for any mono i.
Equations
- One or more equations did not get rendered due to their size.
instance
CategoryTheory.Limits.hasPullback_of_comp_mono
{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]
[CategoryTheory.Limits.HasPullback f g]
:
Equations
- ⋯ = ⋯
def
CategoryTheory.Limits.pullbackConeOfLeftIso
{C : Type u}
[CategoryTheory.Category.{v, u} C]
{X : C}
{Y : C}
{Z : C}
(f : X ⟶ Z)
(g : Y ⟶ Z)
[CategoryTheory.IsIso f]
:
If f : X ⟶ Z is iso, then X ×[Z] Y ≅ Y. This is the explicit limit cone.
@[simp]
theorem
CategoryTheory.Limits.pullbackConeOfLeftIso_x
{C : Type u}
[CategoryTheory.Category.{v, u} C]
{X : C}
{Y : C}
{Z : C}
(f : X ⟶ Z)
(g : Y ⟶ Z)
[CategoryTheory.IsIso f]
:
(CategoryTheory.Limits.pullbackConeOfLeftIso f g).pt = Y
@[simp]
theorem
CategoryTheory.Limits.pullbackConeOfLeftIso_fst
{C : Type u}
[CategoryTheory.Category.{v, u} C]
{X : C}
{Y : C}
{Z : C}
(f : X ⟶ Z)
(g : Y ⟶ Z)
[CategoryTheory.IsIso f]
:
@[simp]
theorem
CategoryTheory.Limits.pullbackConeOfLeftIso_snd
{C : Type u}
[CategoryTheory.Category.{v, u} C]
{X : C}
{Y : C}
{Z : C}
(f : X ⟶ Z)
(g : Y ⟶ Z)
[CategoryTheory.IsIso f]
:
theorem
CategoryTheory.Limits.pullbackConeOfLeftIso_π_app_none
{C : Type u}
[CategoryTheory.Category.{v, u} C]
{X : C}
{Y : C}
{Z : C}
(f : X ⟶ Z)
(g : Y ⟶ Z)
[CategoryTheory.IsIso f]
:
(CategoryTheory.Limits.pullbackConeOfLeftIso f g).π.app none = g
@[simp]
theorem
CategoryTheory.Limits.pullbackConeOfLeftIso_π_app_left
{C : Type u}
[CategoryTheory.Category.{v, u} C]
{X : C}
{Y : C}
{Z : C}
(f : X ⟶ Z)
(g : Y ⟶ Z)
[CategoryTheory.IsIso f]
:
@[simp]
theorem
CategoryTheory.Limits.pullbackConeOfLeftIso_π_app_right
{C : Type u}
[CategoryTheory.Category.{v, u} C]
{X : C}
{Y : C}
{Z : C}
(f : X ⟶ Z)
(g : Y ⟶ Z)
[CategoryTheory.IsIso f]
:
(CategoryTheory.Limits.pullbackConeOfLeftIso f g).π.app CategoryTheory.Limits.WalkingCospan.right = CategoryTheory.CategoryStruct.id
(((CategoryTheory.Functor.const CategoryTheory.Limits.WalkingCospan).obj
(CategoryTheory.Limits.pullbackConeOfLeftIso f g).pt).obj
CategoryTheory.Limits.WalkingCospan.right)
def
CategoryTheory.Limits.pullbackConeOfLeftIsoIsLimit
{C : Type u}
[CategoryTheory.Category.{v, u} C]
{X : C}
{Y : C}
{Z : C}
(f : X ⟶ Z)
(g : Y ⟶ Z)
[CategoryTheory.IsIso f]
:
Verify that the constructed limit cone is indeed a limit.
Equations
- One or more equations did not get rendered due to their size.
theorem
CategoryTheory.Limits.hasPullback_of_left_iso
{C : Type u}
[CategoryTheory.Category.{v, u} C]
{X : C}
{Y : C}
{Z : C}
(f : X ⟶ Z)
(g : Y ⟶ Z)
[CategoryTheory.IsIso f]
:
instance
CategoryTheory.Limits.pullback_snd_iso_of_left_iso
{C : Type u}
[CategoryTheory.Category.{v, u} C]
{X : C}
{Y : C}
{Z : C}
(f : X ⟶ Z)
(g : Y ⟶ Z)
[CategoryTheory.IsIso f]
:
CategoryTheory.IsIso CategoryTheory.Limits.pullback.snd
Equations
- ⋯ = ⋯
instance
CategoryTheory.Limits.hasPullback_of_right_factors_mono
{C : Type u}
[CategoryTheory.Category.{v, u} C]
{W : C}
{X : C}
{Z : C}
(i : Z ⟶ W)
[CategoryTheory.Mono i]
(f : X ⟶ Z)
:
Equations
- ⋯ = ⋯
instance
CategoryTheory.Limits.pullback_snd_iso_of_right_factors_mono
{C : Type u}
[CategoryTheory.Category.{v, u} C]
{W : C}
{X : C}
{Z : C}
(i : Z ⟶ W)
[CategoryTheory.Mono i]
(f : X ⟶ Z)
:
CategoryTheory.IsIso CategoryTheory.Limits.pullback.snd
Equations
- ⋯ = ⋯
def
CategoryTheory.Limits.pullbackConeOfRightIso
{C : Type u}
[CategoryTheory.Category.{v, u} C]
{X : C}
{Y : C}
{Z : C}
(f : X ⟶ Z)
(g : Y ⟶ Z)
[CategoryTheory.IsIso g]
:
If g : Y ⟶ Z is iso, then X ×[Z] Y ≅ X. This is the explicit limit cone.
@[simp]
theorem
CategoryTheory.Limits.pullbackConeOfRightIso_x
{C : Type u}
[CategoryTheory.Category.{v, u} C]
{X : C}
{Y : C}
{Z : C}
(f : X ⟶ Z)
(g : Y ⟶ Z)
[CategoryTheory.IsIso g]
:
(CategoryTheory.Limits.pullbackConeOfRightIso f g).pt = X
@[simp]
theorem
CategoryTheory.Limits.pullbackConeOfRightIso_fst
{C : Type u}
[CategoryTheory.Category.{v, u} C]
{X : C}
{Y : C}
{Z : C}
(f : X ⟶ Z)
(g : Y ⟶ Z)
[CategoryTheory.IsIso g]
:
@[simp]
theorem
CategoryTheory.Limits.pullbackConeOfRightIso_snd
{C : Type u}
[CategoryTheory.Category.{v, u} C]
{X : C}
{Y : C}
{Z : C}
(f : X ⟶ Z)
(g : Y ⟶ Z)
[CategoryTheory.IsIso g]
:
theorem
CategoryTheory.Limits.pullbackConeOfRightIso_π_app_none
{C : Type u}
[CategoryTheory.Category.{v, u} C]
{X : C}
{Y : C}
{Z : C}
(f : X ⟶ Z)
(g : Y ⟶ Z)
[CategoryTheory.IsIso g]
:
(CategoryTheory.Limits.pullbackConeOfRightIso f g).π.app none = f
@[simp]
theorem
CategoryTheory.Limits.pullbackConeOfRightIso_π_app_left
{C : Type u}
[CategoryTheory.Category.{v, u} C]
{X : C}
{Y : C}
{Z : C}
(f : X ⟶ Z)
(g : Y ⟶ Z)
[CategoryTheory.IsIso g]
:
(CategoryTheory.Limits.pullbackConeOfRightIso f g).π.app CategoryTheory.Limits.WalkingCospan.left = CategoryTheory.CategoryStruct.id
(((CategoryTheory.Functor.const CategoryTheory.Limits.WalkingCospan).obj
(CategoryTheory.Limits.pullbackConeOfRightIso f g).pt).obj
CategoryTheory.Limits.WalkingCospan.left)
@[simp]
theorem
CategoryTheory.Limits.pullbackConeOfRightIso_π_app_right
{C : Type u}
[CategoryTheory.Category.{v, u} C]
{X : C}
{Y : C}
{Z : C}
(f : X ⟶ Z)
(g : Y ⟶ Z)
[CategoryTheory.IsIso g]
:
def
CategoryTheory.Limits.pullbackConeOfRightIsoIsLimit
{C : Type u}
[CategoryTheory.Category.{v, u} C]
{X : C}
{Y : C}
{Z : C}
(f : X ⟶ Z)
(g : Y ⟶ Z)
[CategoryTheory.IsIso g]
:
Verify that the constructed limit cone is indeed a limit.
Equations
- One or more equations did not get rendered due to their size.
theorem
CategoryTheory.Limits.hasPullback_of_right_iso
{C : Type u}
[CategoryTheory.Category.{v, u} C]
{X : C}
{Y : C}
{Z : C}
(f : X ⟶ Z)
(g : Y ⟶ Z)
[CategoryTheory.IsIso g]
:
instance
CategoryTheory.Limits.pullback_snd_iso_of_right_iso
{C : Type u}
[CategoryTheory.Category.{v, u} C]
{X : C}
{Y : C}
{Z : C}
(f : X ⟶ Z)
(g : Y ⟶ Z)
[CategoryTheory.IsIso g]
:
CategoryTheory.IsIso CategoryTheory.Limits.pullback.fst
Equations
- ⋯ = ⋯
instance
CategoryTheory.Limits.hasPullback_of_left_factors_mono
{C : Type u}
[CategoryTheory.Category.{v, u} C]
{W : C}
{X : C}
{Z : C}
(i : Z ⟶ W)
[CategoryTheory.Mono i]
(f : X ⟶ Z)
:
Equations
- ⋯ = ⋯
instance
CategoryTheory.Limits.pullback_snd_iso_of_left_factors_mono
{C : Type u}
[CategoryTheory.Category.{v, u} C]
{W : C}
{X : C}
{Z : C}
(i : Z ⟶ W)
[CategoryTheory.Mono i]
(f : X ⟶ Z)
:
CategoryTheory.IsIso CategoryTheory.Limits.pullback.fst
Equations
- ⋯ = ⋯
noncomputable def
CategoryTheory.Limits.pushoutIsPushoutOfEpiComp
{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]
[CategoryTheory.Limits.HasPushout f g]
:
CategoryTheory.Limits.IsColimit
(CategoryTheory.Limits.PushoutCocone.mk CategoryTheory.Limits.pushout.inl CategoryTheory.Limits.pushout.inr ⋯)
The pushout of f, g is also the pullback of h ≫ f, h ≫ g for any epi h.
Equations
- One or more equations did not get rendered due to their size.
instance
CategoryTheory.Limits.hasPushout_of_epi_comp
{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]
[CategoryTheory.Limits.HasPushout f g]
:
Equations
- ⋯ = ⋯
def
CategoryTheory.Limits.pushoutCoconeOfLeftIso
{C : Type u}
[CategoryTheory.Category.{v, u} C]
{X : C}
{Y : C}
{Z : C}
(f : X ⟶ Y)
(g : X ⟶ Z)
[CategoryTheory.IsIso f]
:
If f : X ⟶ Y is iso, then Y ⨿[X] Z ≅ Z. This is the explicit colimit cocone.
@[simp]
theorem
CategoryTheory.Limits.pushoutCoconeOfLeftIso_x
{C : Type u}
[CategoryTheory.Category.{v, u} C]
{X : C}
{Y : C}
{Z : C}
(f : X ⟶ Y)
(g : X ⟶ Z)
[CategoryTheory.IsIso f]
:
(CategoryTheory.Limits.pushoutCoconeOfLeftIso f g).pt = Z
@[simp]
theorem
CategoryTheory.Limits.pushoutCoconeOfLeftIso_inl
{C : Type u}
[CategoryTheory.Category.{v, u} C]
{X : C}
{Y : C}
{Z : C}
(f : X ⟶ Y)
(g : X ⟶ Z)
[CategoryTheory.IsIso f]
:
@[simp]
theorem
CategoryTheory.Limits.pushoutCoconeOfLeftIso_inr
{C : Type u}
[CategoryTheory.Category.{v, u} C]
{X : C}
{Y : C}
{Z : C}
(f : X ⟶ Y)
(g : X ⟶ Z)
[CategoryTheory.IsIso f]
:
theorem
CategoryTheory.Limits.pushoutCoconeOfLeftIso_ι_app_none
{C : Type u}
[CategoryTheory.Category.{v, u} C]
{X : C}
{Y : C}
{Z : C}
(f : X ⟶ Y)
(g : X ⟶ Z)
[CategoryTheory.IsIso f]
:
(CategoryTheory.Limits.pushoutCoconeOfLeftIso f g).ι.app none = g
@[simp]
theorem
CategoryTheory.Limits.pushoutCoconeOfLeftIso_ι_app_left
{C : Type u}
[CategoryTheory.Category.{v, u} C]
{X : C}
{Y : C}
{Z : C}
(f : X ⟶ Y)
(g : X ⟶ Z)
[CategoryTheory.IsIso f]
:
@[simp]
theorem
CategoryTheory.Limits.pushoutCoconeOfLeftIso_ι_app_right
{C : Type u}
[CategoryTheory.Category.{v, u} C]
{X : C}
{Y : C}
{Z : C}
(f : X ⟶ Y)
(g : X ⟶ Z)
[CategoryTheory.IsIso f]
:
def
CategoryTheory.Limits.pushoutCoconeOfLeftIsoIsLimit
{C : Type u}
[CategoryTheory.Category.{v, u} C]
{X : C}
{Y : C}
{Z : C}
(f : X ⟶ Y)
(g : X ⟶ Z)
[CategoryTheory.IsIso f]
:
Verify that the constructed cocone is indeed a colimit.
Equations
- One or more equations did not get rendered due to their size.
theorem
CategoryTheory.Limits.hasPushout_of_left_iso
{C : Type u}
[CategoryTheory.Category.{v, u} C]
{X : C}
{Y : C}
{Z : C}
(f : X ⟶ Y)
(g : X ⟶ Z)
[CategoryTheory.IsIso f]
:
instance
CategoryTheory.Limits.pushout_inr_iso_of_left_iso
{C : Type u}
[CategoryTheory.Category.{v, u} C]
{X : C}
{Y : C}
{Z : C}
(f : X ⟶ Y)
(g : X ⟶ Z)
[CategoryTheory.IsIso f]
:
CategoryTheory.IsIso CategoryTheory.Limits.pushout.inr
Equations
- ⋯ = ⋯
instance
CategoryTheory.Limits.hasPushout_of_right_factors_epi
{C : Type u}
[CategoryTheory.Category.{v, u} C]
{W : C}
{X : C}
{Y : C}
(h : W ⟶ X)
[CategoryTheory.Epi h]
(f : X ⟶ Y)
:
Equations
- ⋯ = ⋯
instance
CategoryTheory.Limits.pushout_inr_iso_of_right_factors_epi
{C : Type u}
[CategoryTheory.Category.{v, u} C]
{W : C}
{X : C}
{Y : C}
(h : W ⟶ X)
[CategoryTheory.Epi h]
(f : X ⟶ Y)
:
CategoryTheory.IsIso CategoryTheory.Limits.pushout.inr
Equations
- ⋯ = ⋯
def
CategoryTheory.Limits.pushoutCoconeOfRightIso
{C : Type u}
[CategoryTheory.Category.{v, u} C]
{X : C}
{Y : C}
{Z : C}
(f : X ⟶ Y)
(g : X ⟶ Z)
[CategoryTheory.IsIso g]
:
If f : X ⟶ Z is iso, then Y ⨿[X] Z ≅ Y. This is the explicit colimit cocone.
@[simp]
theorem
CategoryTheory.Limits.pushoutCoconeOfRightIso_x
{C : Type u}
[CategoryTheory.Category.{v, u} C]
{X : C}
{Y : C}
{Z : C}
(f : X ⟶ Y)
(g : X ⟶ Z)
[CategoryTheory.IsIso g]
:
(CategoryTheory.Limits.pushoutCoconeOfRightIso f g).pt = Y
@[simp]
theorem
CategoryTheory.Limits.pushoutCoconeOfRightIso_inl
{C : Type u}
[CategoryTheory.Category.{v, u} C]
{X : C}
{Y : C}
{Z : C}
(f : X ⟶ Y)
(g : X ⟶ Z)
[CategoryTheory.IsIso g]
:
@[simp]
theorem
CategoryTheory.Limits.pushoutCoconeOfRightIso_inr
{C : Type u}
[CategoryTheory.Category.{v, u} C]
{X : C}
{Y : C}
{Z : C}
(f : X ⟶ Y)
(g : X ⟶ Z)
[CategoryTheory.IsIso g]
:
theorem
CategoryTheory.Limits.pushoutCoconeOfRightIso_ι_app_none
{C : Type u}
[CategoryTheory.Category.{v, u} C]
{X : C}
{Y : C}
{Z : C}
(f : X ⟶ Y)
(g : X ⟶ Z)
[CategoryTheory.IsIso g]
:
(CategoryTheory.Limits.pushoutCoconeOfRightIso f g).ι.app none = f
@[simp]
theorem
CategoryTheory.Limits.pushoutCoconeOfRightIso_ι_app_left
{C : Type u}
[CategoryTheory.Category.{v, u} C]
{X : C}
{Y : C}
{Z : C}
(f : X ⟶ Y)
(g : X ⟶ Z)
[CategoryTheory.IsIso g]
:
@[simp]
theorem
CategoryTheory.Limits.pushoutCoconeOfRightIso_ι_app_right
{C : Type u}
[CategoryTheory.Category.{v, u} C]
{X : C}
{Y : C}
{Z : C}
(f : X ⟶ Y)
(g : X ⟶ Z)
[CategoryTheory.IsIso g]
:
def
CategoryTheory.Limits.pushoutCoconeOfRightIsoIsLimit
{C : Type u}
[CategoryTheory.Category.{v, u} C]
{X : C}
{Y : C}
{Z : C}
(f : X ⟶ Y)
(g : X ⟶ Z)
[CategoryTheory.IsIso g]
:
Verify that the constructed cocone is indeed a colimit.
Equations
- One or more equations did not get rendered due to their size.
theorem
CategoryTheory.Limits.hasPushout_of_right_iso
{C : Type u}
[CategoryTheory.Category.{v, u} C]
{X : C}
{Y : C}
{Z : C}
(f : X ⟶ Y)
(g : X ⟶ Z)
[CategoryTheory.IsIso g]
:
instance
CategoryTheory.Limits.pushout_inl_iso_of_right_iso
{C : Type u}
[CategoryTheory.Category.{v, u} C]
{X : C}
{Y : C}
{Z : C}
(f : X ⟶ Y)
(g : X ⟶ Z)
[CategoryTheory.IsIso g]
:
CategoryTheory.IsIso CategoryTheory.Limits.pushout.inl
Equations
- ⋯ = ⋯
instance
CategoryTheory.Limits.hasPushout_of_left_factors_epi
{C : Type u}
[CategoryTheory.Category.{v, u} C]
{W : C}
{X : C}
{Y : C}
(h : W ⟶ X)
[CategoryTheory.Epi h]
(f : X ⟶ Y)
:
Equations
- ⋯ = ⋯
instance
CategoryTheory.Limits.pushout_inl_iso_of_left_factors_epi
{C : Type u}
[CategoryTheory.Category.{v, u} C]
{W : C}
{X : C}
{Y : C}
(h : W ⟶ X)
[CategoryTheory.Epi h]
(f : X ⟶ Y)
:
CategoryTheory.IsIso CategoryTheory.Limits.pushout.inl
Equations
- ⋯ = ⋯
instance
CategoryTheory.Limits.has_kernel_pair_of_mono
{C : Type u}
[CategoryTheory.Category.{v, u} C]
{X : C}
{Y : C}
(f : X ⟶ Y)
[CategoryTheory.Mono f]
:
Equations
- ⋯ = ⋯
theorem
CategoryTheory.Limits.fst_eq_snd_of_mono_eq
{C : Type u}
[CategoryTheory.Category.{v, u} C]
{X : C}
{Y : C}
(f : X ⟶ Y)
[CategoryTheory.Mono f]
:
CategoryTheory.Limits.pullback.fst = CategoryTheory.Limits.pullback.snd
@[simp]
theorem
CategoryTheory.Limits.pullbackSymmetry_hom_of_mono_eq
{C : Type u}
[CategoryTheory.Category.{v, u} C]
{X : C}
{Y : C}
(f : X ⟶ Y)
[CategoryTheory.Mono f]
:
instance
CategoryTheory.Limits.fst_iso_of_mono_eq
{C : Type u}
[CategoryTheory.Category.{v, u} C]
{X : C}
{Y : C}
(f : X ⟶ Y)
[CategoryTheory.Mono f]
:
CategoryTheory.IsIso CategoryTheory.Limits.pullback.fst
Equations
- ⋯ = ⋯
instance
CategoryTheory.Limits.snd_iso_of_mono_eq
{C : Type u}
[CategoryTheory.Category.{v, u} C]
{X : C}
{Y : C}
(f : X ⟶ Y)
[CategoryTheory.Mono f]
:
CategoryTheory.IsIso CategoryTheory.Limits.pullback.snd
Equations
- ⋯ = ⋯
instance
CategoryTheory.Limits.has_cokernel_pair_of_epi
{C : Type u}
[CategoryTheory.Category.{v, u} C]
{X : C}
{Y : C}
(f : X ⟶ Y)
[CategoryTheory.Epi f]
:
Equations
- ⋯ = ⋯
theorem
CategoryTheory.Limits.inl_eq_inr_of_epi_eq
{C : Type u}
[CategoryTheory.Category.{v, u} C]
{X : C}
{Y : C}
(f : X ⟶ Y)
[CategoryTheory.Epi f]
:
CategoryTheory.Limits.pushout.inl = CategoryTheory.Limits.pushout.inr
@[simp]
theorem
CategoryTheory.Limits.pullback_symmetry_hom_of_epi_eq
{C : Type u}
[CategoryTheory.Category.{v, u} C]
{X : C}
{Y : C}
(f : X ⟶ Y)
[CategoryTheory.Epi f]
:
instance
CategoryTheory.Limits.inl_iso_of_epi_eq
{C : Type u}
[CategoryTheory.Category.{v, u} C]
{X : C}
{Y : C}
(f : X ⟶ Y)
[CategoryTheory.Epi f]
:
CategoryTheory.IsIso CategoryTheory.Limits.pushout.inl
Equations
- ⋯ = ⋯
instance
CategoryTheory.Limits.inr_iso_of_epi_eq
{C : Type u}
[CategoryTheory.Category.{v, u} C]
{X : C}
{Y : C}
(f : X ⟶ Y)
[CategoryTheory.Epi f]
:
CategoryTheory.IsIso CategoryTheory.Limits.pushout.inr
Equations
- ⋯ = ⋯
def
CategoryTheory.Limits.bigSquareIsPullback
{C : Type u}
[CategoryTheory.Category.{v, u} C]
{X₁ : C}
{X₂ : C}
{X₃ : C}
{Y₁ : C}
{Y₂ : C}
{Y₃ : C}
(f₁ : X₁ ⟶ X₂)
(f₂ : X₂ ⟶ X₃)
(g₁ : Y₁ ⟶ Y₂)
(g₂ : Y₂ ⟶ Y₃)
(i₁ : X₁ ⟶ Y₁)
(i₂ : X₂ ⟶ Y₂)
(i₃ : X₃ ⟶ Y₃)
(h₁ : CategoryTheory.CategoryStruct.comp i₁ g₁ = CategoryTheory.CategoryStruct.comp f₁ i₂)
(h₂ : CategoryTheory.CategoryStruct.comp i₂ g₂ = CategoryTheory.CategoryStruct.comp f₂ i₃)
(H : CategoryTheory.Limits.IsLimit (CategoryTheory.Limits.PullbackCone.mk i₂ f₂ h₂))
(H' : CategoryTheory.Limits.IsLimit (CategoryTheory.Limits.PullbackCone.mk i₁ f₁ h₁))
:
Given
X₁ - f₁ -> X₂ - f₂ -> X₃ | | | i₁ i₂ i₃ ∨ ∨ ∨ Y₁ - g₁ -> Y₂ - g₂ -> Y₃
Then the big square is a pullback if both the small squares are.
Equations
- One or more equations did not get rendered due to their size.
def
CategoryTheory.Limits.bigSquareIsPushout
{C : Type u}
[CategoryTheory.Category.{v, u} C]
{X₁ : C}
{X₂ : C}
{X₃ : C}
{Y₁ : C}
{Y₂ : C}
{Y₃ : C}
(f₁ : X₁ ⟶ X₂)
(f₂ : X₂ ⟶ X₃)
(g₁ : Y₁ ⟶ Y₂)
(g₂ : Y₂ ⟶ Y₃)
(i₁ : X₁ ⟶ Y₁)
(i₂ : X₂ ⟶ Y₂)
(i₃ : X₃ ⟶ Y₃)
(h₁ : CategoryTheory.CategoryStruct.comp i₁ g₁ = CategoryTheory.CategoryStruct.comp f₁ i₂)
(h₂ : CategoryTheory.CategoryStruct.comp i₂ g₂ = CategoryTheory.CategoryStruct.comp f₂ i₃)
(H : CategoryTheory.Limits.IsColimit (CategoryTheory.Limits.PushoutCocone.mk g₂ i₃ h₂))
(H' : CategoryTheory.Limits.IsColimit (CategoryTheory.Limits.PushoutCocone.mk g₁ i₂ h₁))
:
Given
X₁ - f₁ -> X₂ - f₂ -> X₃ | | | i₁ i₂ i₃ ∨ ∨ ∨ Y₁ - g₁ -> Y₂ - g₂ -> Y₃
Then the big square is a pushout if both the small squares are.
Equations
- One or more equations did not get rendered due to their size.
def
CategoryTheory.Limits.leftSquareIsPullback
{C : Type u}
[CategoryTheory.Category.{v, u} C]
{X₁ : C}
{X₂ : C}
{X₃ : C}
{Y₁ : C}
{Y₂ : C}
{Y₃ : C}
(f₁ : X₁ ⟶ X₂)
(f₂ : X₂ ⟶ X₃)
(g₁ : Y₁ ⟶ Y₂)
(g₂ : Y₂ ⟶ Y₃)
(i₁ : X₁ ⟶ Y₁)
(i₂ : X₂ ⟶ Y₂)
(i₃ : X₃ ⟶ Y₃)
(h₁ : CategoryTheory.CategoryStruct.comp i₁ g₁ = CategoryTheory.CategoryStruct.comp f₁ i₂)
(h₂ : CategoryTheory.CategoryStruct.comp i₂ g₂ = CategoryTheory.CategoryStruct.comp f₂ i₃)
(H : CategoryTheory.Limits.IsLimit (CategoryTheory.Limits.PullbackCone.mk i₂ f₂ h₂))
(H' : CategoryTheory.Limits.IsLimit (CategoryTheory.Limits.PullbackCone.mk i₁ (CategoryTheory.CategoryStruct.comp f₁ f₂) ⋯))
:
Given
X₁ - f₁ -> X₂ - f₂ -> X₃ | | | i₁ i₂ i₃ ∨ ∨ ∨ Y₁ - g₁ -> Y₂ - g₂ -> Y₃
Then the left square is a pullback if the right square and the big square are.
Equations
- One or more equations did not get rendered due to their size.
def
CategoryTheory.Limits.rightSquareIsPushout
{C : Type u}
[CategoryTheory.Category.{v, u} C]
{X₁ : C}
{X₂ : C}
{X₃ : C}
{Y₁ : C}
{Y₂ : C}
{Y₃ : C}
(f₁ : X₁ ⟶ X₂)
(f₂ : X₂ ⟶ X₃)
(g₁ : Y₁ ⟶ Y₂)
(g₂ : Y₂ ⟶ Y₃)
(i₁ : X₁ ⟶ Y₁)
(i₂ : X₂ ⟶ Y₂)
(i₃ : X₃ ⟶ Y₃)
(h₁ : CategoryTheory.CategoryStruct.comp i₁ g₁ = CategoryTheory.CategoryStruct.comp f₁ i₂)
(h₂ : CategoryTheory.CategoryStruct.comp i₂ g₂ = CategoryTheory.CategoryStruct.comp f₂ i₃)
(H : CategoryTheory.Limits.IsColimit (CategoryTheory.Limits.PushoutCocone.mk g₁ i₂ h₁))
(H' : CategoryTheory.Limits.IsColimit (CategoryTheory.Limits.PushoutCocone.mk (CategoryTheory.CategoryStruct.comp g₁ g₂) i₃ ⋯))
:
Given
X₁ - f₁ -> X₂ - f₂ -> X₃ | | | i₁ i₂ i₃ ∨ ∨ ∨ Y₁ - g₁ -> Y₂ - g₂ -> Y₃
Then the right square is a pushout if the left square and the big square are.
Equations
- One or more equations did not get rendered due to their size.
noncomputable def
CategoryTheory.Limits.pullbackRightPullbackFstIso
{C : Type u}
[CategoryTheory.Category.{v, u} C]
{W : C}
{X : C}
{Y : C}
{Z : C}
(f : X ⟶ Z)
(g : Y ⟶ Z)
(f' : W ⟶ X)
[CategoryTheory.Limits.HasPullback f g]
[CategoryTheory.Limits.HasPullback f' CategoryTheory.Limits.pullback.fst]
[CategoryTheory.Limits.HasPullback (CategoryTheory.CategoryStruct.comp f' f) g]
:
CategoryTheory.Limits.pullback f' CategoryTheory.Limits.pullback.fst ≅ CategoryTheory.Limits.pullback (CategoryTheory.CategoryStruct.comp f' f) g
The canonical isomorphism W ×[X] (X ×[Z] Y) ≅ W ×[Z] Y
Equations
- One or more equations did not get rendered due to their size.
@[simp]
theorem
CategoryTheory.Limits.pullbackRightPullbackFstIso_hom_fst_assoc
{C : Type u}
[CategoryTheory.Category.{v, u} C]
{W : C}
{X : C}
{Y : C}
{Z : C}
(f : X ⟶ Z✝)
(g : Y ⟶ Z✝)
(f' : W ⟶ X)
[CategoryTheory.Limits.HasPullback f g]
[CategoryTheory.Limits.HasPullback f' CategoryTheory.Limits.pullback.fst]
[CategoryTheory.Limits.HasPullback (CategoryTheory.CategoryStruct.comp f' f) g]
{Z : C}
(h : W ⟶ Z)
:
CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.pullbackRightPullbackFstIso f g f').hom
(CategoryTheory.CategoryStruct.comp CategoryTheory.Limits.pullback.fst h) = CategoryTheory.CategoryStruct.comp CategoryTheory.Limits.pullback.fst h
@[simp]
theorem
CategoryTheory.Limits.pullbackRightPullbackFstIso_hom_fst
{C : Type u}
[CategoryTheory.Category.{v, u} C]
{W : C}
{X : C}
{Y : C}
{Z : C}
(f : X ⟶ Z)
(g : Y ⟶ Z)
(f' : W ⟶ X)
[CategoryTheory.Limits.HasPullback f g]
[CategoryTheory.Limits.HasPullback f' CategoryTheory.Limits.pullback.fst]
[CategoryTheory.Limits.HasPullback (CategoryTheory.CategoryStruct.comp f' f) g]
:
CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.pullbackRightPullbackFstIso f g f').hom
CategoryTheory.Limits.pullback.fst = CategoryTheory.Limits.pullback.fst
@[simp]
theorem
CategoryTheory.Limits.pullbackRightPullbackFstIso_hom_snd_assoc
{C : Type u}
[CategoryTheory.Category.{v, u} C]
{W : C}
{X : C}
{Y : C}
{Z : C}
(f : X ⟶ Z✝)
(g : Y ⟶ Z✝)
(f' : W ⟶ X)
[CategoryTheory.Limits.HasPullback f g]
[CategoryTheory.Limits.HasPullback f' CategoryTheory.Limits.pullback.fst]
[CategoryTheory.Limits.HasPullback (CategoryTheory.CategoryStruct.comp f' f) g]
{Z : C}
(h : Y ⟶ Z)
:
CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.pullbackRightPullbackFstIso f g f').hom
(CategoryTheory.CategoryStruct.comp CategoryTheory.Limits.pullback.snd h) = CategoryTheory.CategoryStruct.comp CategoryTheory.Limits.pullback.snd
(CategoryTheory.CategoryStruct.comp CategoryTheory.Limits.pullback.snd h)
@[simp]
theorem
CategoryTheory.Limits.pullbackRightPullbackFstIso_hom_snd
{C : Type u}
[CategoryTheory.Category.{v, u} C]
{W : C}
{X : C}
{Y : C}
{Z : C}
(f : X ⟶ Z)
(g : Y ⟶ Z)
(f' : W ⟶ X)
[CategoryTheory.Limits.HasPullback f g]
[CategoryTheory.Limits.HasPullback f' CategoryTheory.Limits.pullback.fst]
[CategoryTheory.Limits.HasPullback (CategoryTheory.CategoryStruct.comp f' f) g]
:
CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.pullbackRightPullbackFstIso f g f').hom
CategoryTheory.Limits.pullback.snd = CategoryTheory.CategoryStruct.comp CategoryTheory.Limits.pullback.snd CategoryTheory.Limits.pullback.snd
@[simp]
theorem
CategoryTheory.Limits.pullbackRightPullbackFstIso_inv_fst_assoc
{C : Type u}
[CategoryTheory.Category.{v, u} C]
{W : C}
{X : C}
{Y : C}
{Z : C}
(f : X ⟶ Z✝)
(g : Y ⟶ Z✝)
(f' : W ⟶ X)
[CategoryTheory.Limits.HasPullback f g]
[CategoryTheory.Limits.HasPullback f' CategoryTheory.Limits.pullback.fst]
[CategoryTheory.Limits.HasPullback (CategoryTheory.CategoryStruct.comp f' f) g]
{Z : C}
(h : W ⟶ Z)
:
CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.pullbackRightPullbackFstIso f g f').inv
(CategoryTheory.CategoryStruct.comp CategoryTheory.Limits.pullback.fst h) = CategoryTheory.CategoryStruct.comp CategoryTheory.Limits.pullback.fst h
@[simp]
theorem
CategoryTheory.Limits.pullbackRightPullbackFstIso_inv_fst
{C : Type u}
[CategoryTheory.Category.{v, u} C]
{W : C}
{X : C}
{Y : C}
{Z : C}
(f : X ⟶ Z)
(g : Y ⟶ Z)
(f' : W ⟶ X)
[CategoryTheory.Limits.HasPullback f g]
[CategoryTheory.Limits.HasPullback f' CategoryTheory.Limits.pullback.fst]
[CategoryTheory.Limits.HasPullback (CategoryTheory.CategoryStruct.comp f' f) g]
:
CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.pullbackRightPullbackFstIso f g f').inv
CategoryTheory.Limits.pullback.fst = CategoryTheory.Limits.pullback.fst
@[simp]
theorem
CategoryTheory.Limits.pullbackRightPullbackFstIso_inv_snd_snd_assoc
{C : Type u}
[CategoryTheory.Category.{v, u} C]
{W : C}
{X : C}
{Y : C}
{Z : C}
(f : X ⟶ Z✝)
(g : Y ⟶ Z✝)
(f' : W ⟶ X)
[CategoryTheory.Limits.HasPullback f g]
[CategoryTheory.Limits.HasPullback f' CategoryTheory.Limits.pullback.fst]
[CategoryTheory.Limits.HasPullback (CategoryTheory.CategoryStruct.comp f' f) g]
{Z : C}
(h : Y ⟶ Z)
:
CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.pullbackRightPullbackFstIso f g f').inv
(CategoryTheory.CategoryStruct.comp CategoryTheory.Limits.pullback.snd
(CategoryTheory.CategoryStruct.comp CategoryTheory.Limits.pullback.snd h)) = CategoryTheory.CategoryStruct.comp CategoryTheory.Limits.pullback.snd h
@[simp]
theorem
CategoryTheory.Limits.pullbackRightPullbackFstIso_inv_snd_snd
{C : Type u}
[CategoryTheory.Category.{v, u} C]
{W : C}
{X : C}
{Y : C}
{Z : C}
(f : X ⟶ Z)
(g : Y ⟶ Z)
(f' : W ⟶ X)
[CategoryTheory.Limits.HasPullback f g]
[CategoryTheory.Limits.HasPullback f' CategoryTheory.Limits.pullback.fst]
[CategoryTheory.Limits.HasPullback (CategoryTheory.CategoryStruct.comp f' f) g]
:
CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.pullbackRightPullbackFstIso f g f').inv
(CategoryTheory.CategoryStruct.comp CategoryTheory.Limits.pullback.snd CategoryTheory.Limits.pullback.snd) = CategoryTheory.Limits.pullback.snd
@[simp]
theorem
CategoryTheory.Limits.pullbackRightPullbackFstIso_inv_snd_fst_assoc
{C : Type u}
[CategoryTheory.Category.{v, u} C]
{W : C}
{X : C}
{Y : C}
{Z : C}
(f : X ⟶ Z✝)
(g : Y ⟶ Z✝)
(f' : W ⟶ X)
[CategoryTheory.Limits.HasPullback f g]
[CategoryTheory.Limits.HasPullback f' CategoryTheory.Limits.pullback.fst]
[CategoryTheory.Limits.HasPullback (CategoryTheory.CategoryStruct.comp f' f) g]
{Z : C}
(h : X ⟶ Z)
:
CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.pullbackRightPullbackFstIso f g f').inv
(CategoryTheory.CategoryStruct.comp CategoryTheory.Limits.pullback.snd
(CategoryTheory.CategoryStruct.comp CategoryTheory.Limits.pullback.fst h)) = CategoryTheory.CategoryStruct.comp CategoryTheory.Limits.pullback.fst (CategoryTheory.CategoryStruct.comp f' h)
@[simp]
theorem
CategoryTheory.Limits.pullbackRightPullbackFstIso_inv_snd_fst
{C : Type u}
[CategoryTheory.Category.{v, u} C]
{W : C}
{X : C}
{Y : C}
{Z : C}
(f : X ⟶ Z)
(g : Y ⟶ Z)
(f' : W ⟶ X)
[CategoryTheory.Limits.HasPullback f g]
[CategoryTheory.Limits.HasPullback f' CategoryTheory.Limits.pullback.fst]
[CategoryTheory.Limits.HasPullback (CategoryTheory.CategoryStruct.comp f' f) g]
:
CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.pullbackRightPullbackFstIso f g f').inv
(CategoryTheory.CategoryStruct.comp CategoryTheory.Limits.pullback.snd CategoryTheory.Limits.pullback.fst) = CategoryTheory.CategoryStruct.comp CategoryTheory.Limits.pullback.fst f'
noncomputable def
CategoryTheory.Limits.pushoutLeftPushoutInrIso
{C : Type u}
[CategoryTheory.Category.{v, u} C]
{W : C}
{X : C}
{Y : C}
{Z : C}
(f : X ⟶ Y)
(g : X ⟶ Z)
(g' : Z ⟶ W)
[CategoryTheory.Limits.HasPushout f g]
[CategoryTheory.Limits.HasPushout CategoryTheory.Limits.pushout.inr g']
[CategoryTheory.Limits.HasPushout f (CategoryTheory.CategoryStruct.comp g g')]
:
CategoryTheory.Limits.pushout CategoryTheory.Limits.pushout.inr g' ≅ CategoryTheory.Limits.pushout f (CategoryTheory.CategoryStruct.comp g g')
The canonical isomorphism (Y ⨿[X] Z) ⨿[Z] W ≅ Y ×[X] W
Equations
- One or more equations did not get rendered due to their size.
@[simp]
theorem
CategoryTheory.Limits.inl_pushoutLeftPushoutInrIso_inv_assoc
{C : Type u}
[CategoryTheory.Category.{v, u} C]
{W : C}
{X : C}
{Y : C}
{Z : C}
(f : X ⟶ Y)
(g : X ⟶ Z✝)
(g' : Z✝ ⟶ W)
[CategoryTheory.Limits.HasPushout f g]
[CategoryTheory.Limits.HasPushout CategoryTheory.Limits.pushout.inr g']
[CategoryTheory.Limits.HasPushout f (CategoryTheory.CategoryStruct.comp g g')]
{Z : C}
(h : CategoryTheory.Limits.pushout CategoryTheory.Limits.pushout.inr g' ⟶ Z)
:
CategoryTheory.CategoryStruct.comp CategoryTheory.Limits.pushout.inl
(CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.pushoutLeftPushoutInrIso f g g').inv h) = CategoryTheory.CategoryStruct.comp CategoryTheory.Limits.pushout.inl
(CategoryTheory.CategoryStruct.comp CategoryTheory.Limits.pushout.inl h)
@[simp]
theorem
CategoryTheory.Limits.inl_pushoutLeftPushoutInrIso_inv
{C : Type u}
[CategoryTheory.Category.{v, u} C]
{W : C}
{X : C}
{Y : C}
{Z : C}
(f : X ⟶ Y)
(g : X ⟶ Z)
(g' : Z ⟶ W)
[CategoryTheory.Limits.HasPushout f g]
[CategoryTheory.Limits.HasPushout CategoryTheory.Limits.pushout.inr g']
[CategoryTheory.Limits.HasPushout f (CategoryTheory.CategoryStruct.comp g g')]
:
CategoryTheory.CategoryStruct.comp CategoryTheory.Limits.pushout.inl
(CategoryTheory.Limits.pushoutLeftPushoutInrIso f g g').inv = CategoryTheory.CategoryStruct.comp CategoryTheory.Limits.pushout.inl CategoryTheory.Limits.pushout.inl
@[simp]
theorem
CategoryTheory.Limits.inr_pushoutLeftPushoutInrIso_hom_assoc
{C : Type u}
[CategoryTheory.Category.{v, u} C]
{W : C}
{X : C}
{Y : C}
{Z : C}
(f : X ⟶ Y)
(g : X ⟶ Z✝)
(g' : Z✝ ⟶ W)
[CategoryTheory.Limits.HasPushout f g]
[CategoryTheory.Limits.HasPushout CategoryTheory.Limits.pushout.inr g']
[CategoryTheory.Limits.HasPushout f (CategoryTheory.CategoryStruct.comp g g')]
{Z : C}
(h : CategoryTheory.Limits.pushout f (CategoryTheory.CategoryStruct.comp g g') ⟶ Z)
:
CategoryTheory.CategoryStruct.comp CategoryTheory.Limits.pushout.inr
(CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.pushoutLeftPushoutInrIso f g g').hom h) = CategoryTheory.CategoryStruct.comp CategoryTheory.Limits.pushout.inr h
@[simp]
theorem
CategoryTheory.Limits.inr_pushoutLeftPushoutInrIso_hom
{C : Type u}
[CategoryTheory.Category.{v, u} C]
{W : C}
{X : C}
{Y : C}
{Z : C}
(f : X ⟶ Y)
(g : X ⟶ Z)
(g' : Z ⟶ W)
[CategoryTheory.Limits.HasPushout f g]
[CategoryTheory.Limits.HasPushout CategoryTheory.Limits.pushout.inr g']
[CategoryTheory.Limits.HasPushout f (CategoryTheory.CategoryStruct.comp g g')]
:
CategoryTheory.CategoryStruct.comp CategoryTheory.Limits.pushout.inr
(CategoryTheory.Limits.pushoutLeftPushoutInrIso f g g').hom = CategoryTheory.Limits.pushout.inr
@[simp]
theorem
CategoryTheory.Limits.inr_pushoutLeftPushoutInrIso_inv_assoc
{C : Type u}
[CategoryTheory.Category.{v, u} C]
{W : C}
{X : C}
{Y : C}
{Z : C}
(f : X ⟶ Y)
(g : X ⟶ Z✝)
(g' : Z✝ ⟶ W)
[CategoryTheory.Limits.HasPushout f g]
[CategoryTheory.Limits.HasPushout CategoryTheory.Limits.pushout.inr g']
[CategoryTheory.Limits.HasPushout f (CategoryTheory.CategoryStruct.comp g g')]
{Z : C}
(h : CategoryTheory.Limits.pushout CategoryTheory.Limits.pushout.inr g' ⟶ Z)
:
CategoryTheory.CategoryStruct.comp CategoryTheory.Limits.pushout.inr
(CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.pushoutLeftPushoutInrIso f g g').inv h) = CategoryTheory.CategoryStruct.comp CategoryTheory.Limits.pushout.inr h
@[simp]
theorem
CategoryTheory.Limits.inr_pushoutLeftPushoutInrIso_inv
{C : Type u}
[CategoryTheory.Category.{v, u} C]
{W : C}
{X : C}
{Y : C}
{Z : C}
(f : X ⟶ Y)
(g : X ⟶ Z)
(g' : Z ⟶ W)
[CategoryTheory.Limits.HasPushout f g]
[CategoryTheory.Limits.HasPushout CategoryTheory.Limits.pushout.inr g']
[CategoryTheory.Limits.HasPushout f (CategoryTheory.CategoryStruct.comp g g')]
:
CategoryTheory.CategoryStruct.comp CategoryTheory.Limits.pushout.inr
(CategoryTheory.Limits.pushoutLeftPushoutInrIso f g g').inv = CategoryTheory.Limits.pushout.inr
@[simp]
theorem
CategoryTheory.Limits.inl_inl_pushoutLeftPushoutInrIso_hom_assoc
{C : Type u}
[CategoryTheory.Category.{v, u} C]
{W : C}
{X : C}
{Y : C}
{Z : C}
(f : X ⟶ Y)
(g : X ⟶ Z✝)
(g' : Z✝ ⟶ W)
[CategoryTheory.Limits.HasPushout f g]
[CategoryTheory.Limits.HasPushout CategoryTheory.Limits.pushout.inr g']
[CategoryTheory.Limits.HasPushout f (CategoryTheory.CategoryStruct.comp g g')]
{Z : C}
(h : CategoryTheory.Limits.pushout f (CategoryTheory.CategoryStruct.comp g g') ⟶ Z)
:
CategoryTheory.CategoryStruct.comp CategoryTheory.Limits.pushout.inl
(CategoryTheory.CategoryStruct.comp CategoryTheory.Limits.pushout.inl
(CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.pushoutLeftPushoutInrIso f g g').hom h)) = CategoryTheory.CategoryStruct.comp CategoryTheory.Limits.pushout.inl h
@[simp]
theorem
CategoryTheory.Limits.inl_inl_pushoutLeftPushoutInrIso_hom
{C : Type u}
[CategoryTheory.Category.{v, u} C]
{W : C}
{X : C}
{Y : C}
{Z : C}
(f : X ⟶ Y)
(g : X ⟶ Z)
(g' : Z ⟶ W)
[CategoryTheory.Limits.HasPushout f g]
[CategoryTheory.Limits.HasPushout CategoryTheory.Limits.pushout.inr g']
[CategoryTheory.Limits.HasPushout f (CategoryTheory.CategoryStruct.comp g g')]
:
CategoryTheory.CategoryStruct.comp CategoryTheory.Limits.pushout.inl
(CategoryTheory.CategoryStruct.comp CategoryTheory.Limits.pushout.inl
(CategoryTheory.Limits.pushoutLeftPushoutInrIso f g g').hom) = CategoryTheory.Limits.pushout.inl
@[simp]
theorem
CategoryTheory.Limits.inr_inl_pushoutLeftPushoutInrIso_hom_assoc
{C : Type u}
[CategoryTheory.Category.{v, u} C]
{W : C}
{X : C}
{Y : C}
{Z : C}
(f : X ⟶ Y)
(g : X ⟶ Z✝)
(g' : Z✝ ⟶ W)
[CategoryTheory.Limits.HasPushout f g]
[CategoryTheory.Limits.HasPushout CategoryTheory.Limits.pushout.inr g']
[CategoryTheory.Limits.HasPushout f (CategoryTheory.CategoryStruct.comp g g')]
{Z : C}
(h : CategoryTheory.Limits.pushout f (CategoryTheory.CategoryStruct.comp g g') ⟶ Z)
:
CategoryTheory.CategoryStruct.comp CategoryTheory.Limits.pushout.inr
(CategoryTheory.CategoryStruct.comp CategoryTheory.Limits.pushout.inl
(CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.pushoutLeftPushoutInrIso f g g').hom h)) = CategoryTheory.CategoryStruct.comp g' (CategoryTheory.CategoryStruct.comp CategoryTheory.Limits.pushout.inr h)
@[simp]
theorem
CategoryTheory.Limits.inr_inl_pushoutLeftPushoutInrIso_hom
{C : Type u}
[CategoryTheory.Category.{v, u} C]
{W : C}
{X : C}
{Y : C}
{Z : C}
(f : X ⟶ Y)
(g : X ⟶ Z)
(g' : Z ⟶ W)
[CategoryTheory.Limits.HasPushout f g]
[CategoryTheory.Limits.HasPushout CategoryTheory.Limits.pushout.inr g']
[CategoryTheory.Limits.HasPushout f (CategoryTheory.CategoryStruct.comp g g')]
:
CategoryTheory.CategoryStruct.comp CategoryTheory.Limits.pushout.inr
(CategoryTheory.CategoryStruct.comp CategoryTheory.Limits.pushout.inl
(CategoryTheory.Limits.pushoutLeftPushoutInrIso f g g').hom) = CategoryTheory.CategoryStruct.comp g' CategoryTheory.Limits.pushout.inr
def
CategoryTheory.Limits.pullbackPullbackLeftIsPullback
{C : Type u}
[CategoryTheory.Category.{v, u} C]
{X₁ : C}
{X₂ : C}
{X₃ : C}
{Y₁ : C}
{Y₂ : C}
(f₁ : X₁ ⟶ Y₁)
(f₂ : X₂ ⟶ Y₁)
(f₃ : X₂ ⟶ Y₂)
(f₄ : X₃ ⟶ Y₂)
[CategoryTheory.Limits.HasPullback f₁ f₂]
[CategoryTheory.Limits.HasPullback f₃ f₄]
[CategoryTheory.Limits.HasPullback (CategoryTheory.CategoryStruct.comp CategoryTheory.Limits.pullback.snd f₃) f₄]
:
CategoryTheory.Limits.IsLimit
(CategoryTheory.Limits.PullbackCone.mk CategoryTheory.Limits.pullback.fst
(CategoryTheory.Limits.pullback.lift
(CategoryTheory.CategoryStruct.comp CategoryTheory.Limits.pullback.fst CategoryTheory.Limits.pullback.snd)
CategoryTheory.Limits.pullback.snd ⋯)
⋯)
(X₁ ×[Y₁] X₂) ×[Y₂] X₃ is the pullback (X₁ ×[Y₁] X₂) ×[X₂] (X₂ ×[Y₂] X₃).
Equations
- One or more equations did not get rendered due to their size.
def
CategoryTheory.Limits.pullbackAssocIsPullback
{C : Type u}
[CategoryTheory.Category.{v, u} C]
{X₁ : C}
{X₂ : C}
{X₃ : C}
{Y₁ : C}
{Y₂ : C}
(f₁ : X₁ ⟶ Y₁)
(f₂ : X₂ ⟶ Y₁)
(f₃ : X₂ ⟶ Y₂)
(f₄ : X₃ ⟶ Y₂)
[CategoryTheory.Limits.HasPullback f₁ f₂]
[CategoryTheory.Limits.HasPullback f₃ f₄]
[CategoryTheory.Limits.HasPullback (CategoryTheory.CategoryStruct.comp CategoryTheory.Limits.pullback.snd f₃) f₄]
:
CategoryTheory.Limits.IsLimit
(CategoryTheory.Limits.PullbackCone.mk
(CategoryTheory.CategoryStruct.comp CategoryTheory.Limits.pullback.fst CategoryTheory.Limits.pullback.fst)
(CategoryTheory.Limits.pullback.lift
(CategoryTheory.CategoryStruct.comp CategoryTheory.Limits.pullback.fst CategoryTheory.Limits.pullback.snd)
CategoryTheory.Limits.pullback.snd ⋯)
⋯)
(X₁ ×[Y₁] X₂) ×[Y₂] X₃ is the pullback X₁ ×[Y₁] (X₂ ×[Y₂] X₃).
Equations
- One or more equations did not get rendered due to their size.
theorem
CategoryTheory.Limits.hasPullback_assoc
{C : Type u}
[CategoryTheory.Category.{v, u} C]
{X₁ : C}
{X₂ : C}
{X₃ : C}
{Y₁ : C}
{Y₂ : C}
(f₁ : X₁ ⟶ Y₁)
(f₂ : X₂ ⟶ Y₁)
(f₃ : X₂ ⟶ Y₂)
(f₄ : X₃ ⟶ Y₂)
[CategoryTheory.Limits.HasPullback f₁ f₂]
[CategoryTheory.Limits.HasPullback f₃ f₄]
[CategoryTheory.Limits.HasPullback (CategoryTheory.CategoryStruct.comp CategoryTheory.Limits.pullback.snd f₃) f₄]
:
CategoryTheory.Limits.HasPullback f₁ (CategoryTheory.CategoryStruct.comp CategoryTheory.Limits.pullback.fst f₂)
def
CategoryTheory.Limits.pullbackPullbackRightIsPullback
{C : Type u}
[CategoryTheory.Category.{v, u} C]
{X₁ : C}
{X₂ : C}
{X₃ : C}
{Y₁ : C}
{Y₂ : C}
(f₁ : X₁ ⟶ Y₁)
(f₂ : X₂ ⟶ Y₁)
(f₃ : X₂ ⟶ Y₂)
(f₄ : X₃ ⟶ Y₂)
[CategoryTheory.Limits.HasPullback f₁ f₂]
[CategoryTheory.Limits.HasPullback f₃ f₄]
[CategoryTheory.Limits.HasPullback f₁ (CategoryTheory.CategoryStruct.comp CategoryTheory.Limits.pullback.fst f₂)]
:
CategoryTheory.Limits.IsLimit
(CategoryTheory.Limits.PullbackCone.mk
(CategoryTheory.Limits.pullback.lift CategoryTheory.Limits.pullback.fst
(CategoryTheory.CategoryStruct.comp CategoryTheory.Limits.pullback.snd CategoryTheory.Limits.pullback.fst) ⋯)
CategoryTheory.Limits.pullback.snd ⋯)
X₁ ×[Y₁] (X₂ ×[Y₂] X₃) is the pullback (X₁ ×[Y₁] X₂) ×[X₂] (X₂ ×[Y₂] X₃).
Equations
- One or more equations did not get rendered due to their size.
def
CategoryTheory.Limits.pullbackAssocSymmIsPullback
{C : Type u}
[CategoryTheory.Category.{v, u} C]
{X₁ : C}
{X₂ : C}
{X₃ : C}
{Y₁ : C}
{Y₂ : C}
(f₁ : X₁ ⟶ Y₁)
(f₂ : X₂ ⟶ Y₁)
(f₃ : X₂ ⟶ Y₂)
(f₄ : X₃ ⟶ Y₂)
[CategoryTheory.Limits.HasPullback f₁ f₂]
[CategoryTheory.Limits.HasPullback f₃ f₄]
[CategoryTheory.Limits.HasPullback f₁ (CategoryTheory.CategoryStruct.comp CategoryTheory.Limits.pullback.fst f₂)]
:
CategoryTheory.Limits.IsLimit
(CategoryTheory.Limits.PullbackCone.mk
(CategoryTheory.Limits.pullback.lift CategoryTheory.Limits.pullback.fst
(CategoryTheory.CategoryStruct.comp CategoryTheory.Limits.pullback.snd CategoryTheory.Limits.pullback.fst) ⋯)
(CategoryTheory.CategoryStruct.comp CategoryTheory.Limits.pullback.snd CategoryTheory.Limits.pullback.snd) ⋯)
X₁ ×[Y₁] (X₂ ×[Y₂] X₃) is the pullback (X₁ ×[Y₁] X₂) ×[Y₂] X₃.
Equations
- One or more equations did not get rendered due to their size.
theorem
CategoryTheory.Limits.hasPullback_assoc_symm
{C : Type u}
[CategoryTheory.Category.{v, u} C]
{X₁ : C}
{X₂ : C}
{X₃ : C}
{Y₁ : C}
{Y₂ : C}
(f₁ : X₁ ⟶ Y₁)
(f₂ : X₂ ⟶ Y₁)
(f₃ : X₂ ⟶ Y₂)
(f₄ : X₃ ⟶ Y₂)
[CategoryTheory.Limits.HasPullback f₁ f₂]
[CategoryTheory.Limits.HasPullback f₃ f₄]
[CategoryTheory.Limits.HasPullback f₁ (CategoryTheory.CategoryStruct.comp CategoryTheory.Limits.pullback.fst f₂)]
:
CategoryTheory.Limits.HasPullback (CategoryTheory.CategoryStruct.comp CategoryTheory.Limits.pullback.snd f₃) f₄
noncomputable def
CategoryTheory.Limits.pullbackAssoc
{C : Type u}
[CategoryTheory.Category.{v, u} C]
{X₁ : C}
{X₂ : C}
{X₃ : C}
{Y₁ : C}
{Y₂ : C}
(f₁ : X₁ ⟶ Y₁)
(f₂ : X₂ ⟶ Y₁)
(f₃ : X₂ ⟶ Y₂)
(f₄ : X₃ ⟶ Y₂)
[CategoryTheory.Limits.HasPullback f₁ f₂]
[CategoryTheory.Limits.HasPullback f₃ f₄]
[CategoryTheory.Limits.HasPullback (CategoryTheory.CategoryStruct.comp CategoryTheory.Limits.pullback.snd f₃) f₄]
[CategoryTheory.Limits.HasPullback f₁ (CategoryTheory.CategoryStruct.comp CategoryTheory.Limits.pullback.fst f₂)]
:
CategoryTheory.Limits.pullback (CategoryTheory.CategoryStruct.comp CategoryTheory.Limits.pullback.snd f₃) f₄ ≅ CategoryTheory.Limits.pullback f₁ (CategoryTheory.CategoryStruct.comp CategoryTheory.Limits.pullback.fst f₂)
The canonical isomorphism (X₁ ×[Y₁] X₂) ×[Y₂] X₃ ≅ X₁ ×[Y₁] (X₂ ×[Y₂] X₃).
Equations
- One or more equations did not get rendered due to their size.
@[simp]
theorem
CategoryTheory.Limits.pullbackAssoc_inv_fst_fst_assoc
{C : Type u}
[CategoryTheory.Category.{v, u} C]
{X₁ : C}
{X₂ : C}
{X₃ : C}
{Y₁ : C}
{Y₂ : C}
(f₁ : X₁ ⟶ Y₁)
(f₂ : X₂ ⟶ Y₁)
(f₃ : X₂ ⟶ Y₂)
(f₄ : X₃ ⟶ Y₂)
[CategoryTheory.Limits.HasPullback f₁ f₂]
[CategoryTheory.Limits.HasPullback f₃ f₄]
[CategoryTheory.Limits.HasPullback (CategoryTheory.CategoryStruct.comp CategoryTheory.Limits.pullback.snd f₃) f₄]
[CategoryTheory.Limits.HasPullback f₁ (CategoryTheory.CategoryStruct.comp CategoryTheory.Limits.pullback.fst f₂)]
{Z : C}
(h : X₁ ⟶ Z)
:
CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.pullbackAssoc f₁ f₂ f₃ f₄).inv
(CategoryTheory.CategoryStruct.comp CategoryTheory.Limits.pullback.fst
(CategoryTheory.CategoryStruct.comp CategoryTheory.Limits.pullback.fst h)) = CategoryTheory.CategoryStruct.comp CategoryTheory.Limits.pullback.fst h
@[simp]
theorem
CategoryTheory.Limits.pullbackAssoc_inv_fst_fst
{C : Type u}
[CategoryTheory.Category.{v, u} C]
{X₁ : C}
{X₂ : C}
{X₃ : C}
{Y₁ : C}
{Y₂ : C}
(f₁ : X₁ ⟶ Y₁)
(f₂ : X₂ ⟶ Y₁)
(f₃ : X₂ ⟶ Y₂)
(f₄ : X₃ ⟶ Y₂)
[CategoryTheory.Limits.HasPullback f₁ f₂]
[CategoryTheory.Limits.HasPullback f₃ f₄]
[CategoryTheory.Limits.HasPullback (CategoryTheory.CategoryStruct.comp CategoryTheory.Limits.pullback.snd f₃) f₄]
[CategoryTheory.Limits.HasPullback f₁ (CategoryTheory.CategoryStruct.comp CategoryTheory.Limits.pullback.fst f₂)]
:
CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.pullbackAssoc f₁ f₂ f₃ f₄).inv
(CategoryTheory.CategoryStruct.comp CategoryTheory.Limits.pullback.fst CategoryTheory.Limits.pullback.fst) = CategoryTheory.Limits.pullback.fst
@[simp]
theorem
CategoryTheory.Limits.pullbackAssoc_hom_fst_assoc
{C : Type u}
[CategoryTheory.Category.{v, u} C]
{X₁ : C}
{X₂ : C}
{X₃ : C}
{Y₁ : C}
{Y₂ : C}
(f₁ : X₁ ⟶ Y₁)
(f₂ : X₂ ⟶ Y₁)
(f₃ : X₂ ⟶ Y₂)
(f₄ : X₃ ⟶ Y₂)
[CategoryTheory.Limits.HasPullback f₁ f₂]
[CategoryTheory.Limits.HasPullback f₃ f₄]
[CategoryTheory.Limits.HasPullback (CategoryTheory.CategoryStruct.comp CategoryTheory.Limits.pullback.snd f₃) f₄]
[CategoryTheory.Limits.HasPullback f₁ (CategoryTheory.CategoryStruct.comp CategoryTheory.Limits.pullback.fst f₂)]
{Z : C}
(h : X₁ ⟶ Z)
:
CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.pullbackAssoc f₁ f₂ f₃ f₄).hom
(CategoryTheory.CategoryStruct.comp CategoryTheory.Limits.pullback.fst h) = CategoryTheory.CategoryStruct.comp CategoryTheory.Limits.pullback.fst
(CategoryTheory.CategoryStruct.comp CategoryTheory.Limits.pullback.fst h)
@[simp]
theorem
CategoryTheory.Limits.pullbackAssoc_hom_fst
{C : Type u}
[CategoryTheory.Category.{v, u} C]
{X₁ : C}
{X₂ : C}
{X₃ : C}
{Y₁ : C}
{Y₂ : C}
(f₁ : X₁ ⟶ Y₁)
(f₂ : X₂ ⟶ Y₁)
(f₃ : X₂ ⟶ Y₂)
(f₄ : X₃ ⟶ Y₂)
[CategoryTheory.Limits.HasPullback f₁ f₂]
[CategoryTheory.Limits.HasPullback f₃ f₄]
[CategoryTheory.Limits.HasPullback (CategoryTheory.CategoryStruct.comp CategoryTheory.Limits.pullback.snd f₃) f₄]
[CategoryTheory.Limits.HasPullback f₁ (CategoryTheory.CategoryStruct.comp CategoryTheory.Limits.pullback.fst f₂)]
:
CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.pullbackAssoc f₁ f₂ f₃ f₄).hom
CategoryTheory.Limits.pullback.fst = CategoryTheory.CategoryStruct.comp CategoryTheory.Limits.pullback.fst CategoryTheory.Limits.pullback.fst
@[simp]
theorem
CategoryTheory.Limits.pullbackAssoc_hom_snd_fst_assoc
{C : Type u}
[CategoryTheory.Category.{v, u} C]
{X₁ : C}
{X₂ : C}
{X₃ : C}
{Y₁ : C}
{Y₂ : C}
(f₁ : X₁ ⟶ Y₁)
(f₂ : X₂ ⟶ Y₁)
(f₃ : X₂ ⟶ Y₂)
(f₄ : X₃ ⟶ Y₂)
[CategoryTheory.Limits.HasPullback f₁ f₂]
[CategoryTheory.Limits.HasPullback f₃ f₄]
[CategoryTheory.Limits.HasPullback (CategoryTheory.CategoryStruct.comp CategoryTheory.Limits.pullback.snd f₃) f₄]
[CategoryTheory.Limits.HasPullback f₁ (CategoryTheory.CategoryStruct.comp CategoryTheory.Limits.pullback.fst f₂)]
{Z : C}
(h : X₂ ⟶ Z)
:
CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.pullbackAssoc f₁ f₂ f₃ f₄).hom
(CategoryTheory.CategoryStruct.comp CategoryTheory.Limits.pullback.snd
(CategoryTheory.CategoryStruct.comp CategoryTheory.Limits.pullback.fst h)) = CategoryTheory.CategoryStruct.comp CategoryTheory.Limits.pullback.fst
(CategoryTheory.CategoryStruct.comp CategoryTheory.Limits.pullback.snd h)
@[simp]
theorem
CategoryTheory.Limits.pullbackAssoc_hom_snd_fst
{C : Type u}
[CategoryTheory.Category.{v, u} C]
{X₁ : C}
{X₂ : C}
{X₃ : C}
{Y₁ : C}
{Y₂ : C}
(f₁ : X₁ ⟶ Y₁)
(f₂ : X₂ ⟶ Y₁)
(f₃ : X₂ ⟶ Y₂)
(f₄ : X₃ ⟶ Y₂)
[CategoryTheory.Limits.HasPullback f₁ f₂]
[CategoryTheory.Limits.HasPullback f₃ f₄]
[CategoryTheory.Limits.HasPullback (CategoryTheory.CategoryStruct.comp CategoryTheory.Limits.pullback.snd f₃) f₄]
[CategoryTheory.Limits.HasPullback f₁ (CategoryTheory.CategoryStruct.comp CategoryTheory.Limits.pullback.fst f₂)]
:
CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.pullbackAssoc f₁ f₂ f₃ f₄).hom
(CategoryTheory.CategoryStruct.comp CategoryTheory.Limits.pullback.snd CategoryTheory.Limits.pullback.fst) = CategoryTheory.CategoryStruct.comp CategoryTheory.Limits.pullback.fst CategoryTheory.Limits.pullback.snd
@[simp]
theorem
CategoryTheory.Limits.pullbackAssoc_hom_snd_snd_assoc
{C : Type u}
[CategoryTheory.Category.{v, u} C]
{X₁ : C}
{X₂ : C}
{X₃ : C}
{Y₁ : C}
{Y₂ : C}
(f₁ : X₁ ⟶ Y₁)
(f₂ : X₂ ⟶ Y₁)
(f₃ : X₂ ⟶ Y₂)
(f₄ : X₃ ⟶ Y₂)
[CategoryTheory.Limits.HasPullback f₁ f₂]
[CategoryTheory.Limits.HasPullback f₃ f₄]
[CategoryTheory.Limits.HasPullback (CategoryTheory.CategoryStruct.comp CategoryTheory.Limits.pullback.snd f₃) f₄]
[CategoryTheory.Limits.HasPullback f₁ (CategoryTheory.CategoryStruct.comp CategoryTheory.Limits.pullback.fst f₂)]
{Z : C}
(h : X₃ ⟶ Z)
:
CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.pullbackAssoc f₁ f₂ f₃ f₄).hom
(CategoryTheory.CategoryStruct.comp CategoryTheory.Limits.pullback.snd
(CategoryTheory.CategoryStruct.comp CategoryTheory.Limits.pullback.snd h)) = CategoryTheory.CategoryStruct.comp CategoryTheory.Limits.pullback.snd h
@[simp]
theorem
CategoryTheory.Limits.pullbackAssoc_hom_snd_snd
{C : Type u}
[CategoryTheory.Category.{v, u} C]
{X₁ : C}
{X₂ : C}
{X₃ : C}
{Y₁ : C}
{Y₂ : C}
(f₁ : X₁ ⟶ Y₁)
(f₂ : X₂ ⟶ Y₁)
(f₃ : X₂ ⟶ Y₂)
(f₄ : X₃ ⟶ Y₂)
[CategoryTheory.Limits.HasPullback f₁ f₂]
[CategoryTheory.Limits.HasPullback f₃ f₄]
[CategoryTheory.Limits.HasPullback (CategoryTheory.CategoryStruct.comp CategoryTheory.Limits.pullback.snd f₃) f₄]
[CategoryTheory.Limits.HasPullback f₁ (CategoryTheory.CategoryStruct.comp CategoryTheory.Limits.pullback.fst f₂)]
:
CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.pullbackAssoc f₁ f₂ f₃ f₄).hom
(CategoryTheory.CategoryStruct.comp CategoryTheory.Limits.pullback.snd CategoryTheory.Limits.pullback.snd) = CategoryTheory.Limits.pullback.snd
@[simp]
theorem
CategoryTheory.Limits.pullbackAssoc_inv_fst_snd_assoc
{C : Type u}
[CategoryTheory.Category.{v, u} C]
{X₁ : C}
{X₂ : C}
{X₃ : C}
{Y₁ : C}
{Y₂ : C}
(f₁ : X₁ ⟶ Y₁)
(f₂ : X₂ ⟶ Y₁)
(f₃ : X₂ ⟶ Y₂)
(f₄ : X₃ ⟶ Y₂)
[CategoryTheory.Limits.HasPullback f₁ f₂]
[CategoryTheory.Limits.HasPullback f₃ f₄]
[CategoryTheory.Limits.HasPullback (CategoryTheory.CategoryStruct.comp CategoryTheory.Limits.pullback.snd f₃) f₄]
[CategoryTheory.Limits.HasPullback f₁ (CategoryTheory.CategoryStruct.comp CategoryTheory.Limits.pullback.fst f₂)]
{Z : C}
(h : X₂ ⟶ Z)
:
CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.pullbackAssoc f₁ f₂ f₃ f₄).inv
(CategoryTheory.CategoryStruct.comp CategoryTheory.Limits.pullback.fst
(CategoryTheory.CategoryStruct.comp CategoryTheory.Limits.pullback.snd h)) = CategoryTheory.CategoryStruct.comp CategoryTheory.Limits.pullback.snd
(CategoryTheory.CategoryStruct.comp CategoryTheory.Limits.pullback.fst h)
@[simp]
theorem
CategoryTheory.Limits.pullbackAssoc_inv_fst_snd
{C : Type u}
[CategoryTheory.Category.{v, u} C]
{X₁ : C}
{X₂ : C}
{X₃ : C}
{Y₁ : C}
{Y₂ : C}
(f₁ : X₁ ⟶ Y₁)
(f₂ : X₂ ⟶ Y₁)
(f₃ : X₂ ⟶ Y₂)
(f₄ : X₃ ⟶ Y₂)
[CategoryTheory.Limits.HasPullback f₁ f₂]
[CategoryTheory.Limits.HasPullback f₃ f₄]
[CategoryTheory.Limits.HasPullback (CategoryTheory.CategoryStruct.comp CategoryTheory.Limits.pullback.snd f₃) f₄]
[CategoryTheory.Limits.HasPullback f₁ (CategoryTheory.CategoryStruct.comp CategoryTheory.Limits.pullback.fst f₂)]
:
CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.pullbackAssoc f₁ f₂ f₃ f₄).inv
(CategoryTheory.CategoryStruct.comp CategoryTheory.Limits.pullback.fst CategoryTheory.Limits.pullback.snd) = CategoryTheory.CategoryStruct.comp CategoryTheory.Limits.pullback.snd CategoryTheory.Limits.pullback.fst
@[simp]
theorem
CategoryTheory.Limits.pullbackAssoc_inv_snd_assoc
{C : Type u}
[CategoryTheory.Category.{v, u} C]
{X₁ : C}
{X₂ : C}
{X₃ : C}
{Y₁ : C}
{Y₂ : C}
(f₁ : X₁ ⟶ Y₁)
(f₂ : X₂ ⟶ Y₁)
(f₃ : X₂ ⟶ Y₂)
(f₄ : X₃ ⟶ Y₂)
[CategoryTheory.Limits.HasPullback f₁ f₂]
[CategoryTheory.Limits.HasPullback f₃ f₄]
[CategoryTheory.Limits.HasPullback (CategoryTheory.CategoryStruct.comp CategoryTheory.Limits.pullback.snd f₃) f₄]
[CategoryTheory.Limits.HasPullback f₁ (CategoryTheory.CategoryStruct.comp CategoryTheory.Limits.pullback.fst f₂)]
{Z : C}
(h : X₃ ⟶ Z)
:
CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.pullbackAssoc f₁ f₂ f₃ f₄).inv
(CategoryTheory.CategoryStruct.comp CategoryTheory.Limits.pullback.snd h) = CategoryTheory.CategoryStruct.comp CategoryTheory.Limits.pullback.snd
(CategoryTheory.CategoryStruct.comp CategoryTheory.Limits.pullback.snd h)
@[simp]
theorem
CategoryTheory.Limits.pullbackAssoc_inv_snd
{C : Type u}
[CategoryTheory.Category.{v, u} C]
{X₁ : C}
{X₂ : C}
{X₃ : C}
{Y₁ : C}
{Y₂ : C}
(f₁ : X₁ ⟶ Y₁)
(f₂ : X₂ ⟶ Y₁)
(f₃ : X₂ ⟶ Y₂)
(f₄ : X₃ ⟶ Y₂)
[CategoryTheory.Limits.HasPullback f₁ f₂]
[CategoryTheory.Limits.HasPullback f₃ f₄]
[CategoryTheory.Limits.HasPullback (CategoryTheory.CategoryStruct.comp CategoryTheory.Limits.pullback.snd f₃) f₄]
[CategoryTheory.Limits.HasPullback f₁ (CategoryTheory.CategoryStruct.comp CategoryTheory.Limits.pullback.fst f₂)]
:
CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.pullbackAssoc f₁ f₂ f₃ f₄).inv
CategoryTheory.Limits.pullback.snd = CategoryTheory.CategoryStruct.comp CategoryTheory.Limits.pullback.snd CategoryTheory.Limits.pullback.snd
def
CategoryTheory.Limits.pushoutPushoutLeftIsPushout
{C : Type u}
[CategoryTheory.Category.{v, u} C]
{X₁ : C}
{X₂ : C}
{X₃ : C}
{Z₁ : C}
{Z₂ : C}
(g₁ : Z₁ ⟶ X₁)
(g₂ : Z₁ ⟶ X₂)
(g₃ : Z₂ ⟶ X₂)
(g₄ : Z₂ ⟶ X₃)
[CategoryTheory.Limits.HasPushout g₁ g₂]
[CategoryTheory.Limits.HasPushout g₃ g₄]
[CategoryTheory.Limits.HasPushout (CategoryTheory.CategoryStruct.comp g₃ CategoryTheory.Limits.pushout.inr) g₄]
:
CategoryTheory.Limits.IsColimit
(CategoryTheory.Limits.PushoutCocone.mk CategoryTheory.Limits.pushout.inl
(CategoryTheory.Limits.pushout.desc
(CategoryTheory.CategoryStruct.comp CategoryTheory.Limits.pushout.inr CategoryTheory.Limits.pushout.inl)
CategoryTheory.Limits.pushout.inr ⋯)
⋯)
(X₁ ⨿[Z₁] X₂) ⨿[Z₂] X₃ is the pushout (X₁ ⨿[Z₁] X₂) ×[X₂] (X₂ ⨿[Z₂] X₃).
Equations
- One or more equations did not get rendered due to their size.
def
CategoryTheory.Limits.pushoutAssocIsPushout
{C : Type u}
[CategoryTheory.Category.{v, u} C]
{X₁ : C}
{X₂ : C}
{X₃ : C}
{Z₁ : C}
{Z₂ : C}
(g₁ : Z₁ ⟶ X₁)
(g₂ : Z₁ ⟶ X₂)
(g₃ : Z₂ ⟶ X₂)
(g₄ : Z₂ ⟶ X₃)
[CategoryTheory.Limits.HasPushout g₁ g₂]
[CategoryTheory.Limits.HasPushout g₃ g₄]
[CategoryTheory.Limits.HasPushout (CategoryTheory.CategoryStruct.comp g₃ CategoryTheory.Limits.pushout.inr) g₄]
:
CategoryTheory.Limits.IsColimit
(CategoryTheory.Limits.PushoutCocone.mk
(CategoryTheory.CategoryStruct.comp CategoryTheory.Limits.pushout.inl CategoryTheory.Limits.pushout.inl)
(CategoryTheory.Limits.pushout.desc
(CategoryTheory.CategoryStruct.comp CategoryTheory.Limits.pushout.inr CategoryTheory.Limits.pushout.inl)
CategoryTheory.Limits.pushout.inr ⋯)
⋯)
(X₁ ⨿[Z₁] X₂) ⨿[Z₂] X₃ is the pushout X₁ ⨿[Z₁] (X₂ ⨿[Z₂] X₃).
Equations
- One or more equations did not get rendered due to their size.
theorem
CategoryTheory.Limits.hasPushout_assoc
{C : Type u}
[CategoryTheory.Category.{v, u} C]
{X₁ : C}
{X₂ : C}
{X₃ : C}
{Z₁ : C}
{Z₂ : C}
(g₁ : Z₁ ⟶ X₁)
(g₂ : Z₁ ⟶ X₂)
(g₃ : Z₂ ⟶ X₂)
(g₄ : Z₂ ⟶ X₃)
[CategoryTheory.Limits.HasPushout g₁ g₂]
[CategoryTheory.Limits.HasPushout g₃ g₄]
[CategoryTheory.Limits.HasPushout (CategoryTheory.CategoryStruct.comp g₃ CategoryTheory.Limits.pushout.inr) g₄]
:
CategoryTheory.Limits.HasPushout g₁ (CategoryTheory.CategoryStruct.comp g₂ CategoryTheory.Limits.pushout.inl)
def
CategoryTheory.Limits.pushoutPushoutRightIsPushout
{C : Type u}
[CategoryTheory.Category.{v, u} C]
{X₁ : C}
{X₂ : C}
{X₃ : C}
{Z₁ : C}
{Z₂ : C}
(g₁ : Z₁ ⟶ X₁)
(g₂ : Z₁ ⟶ X₂)
(g₃ : Z₂ ⟶ X₂)
(g₄ : Z₂ ⟶ X₃)
[CategoryTheory.Limits.HasPushout g₁ g₂]
[CategoryTheory.Limits.HasPushout g₃ g₄]
[CategoryTheory.Limits.HasPushout g₁ (CategoryTheory.CategoryStruct.comp g₂ CategoryTheory.Limits.pushout.inl)]
:
CategoryTheory.Limits.IsColimit
(CategoryTheory.Limits.PushoutCocone.mk
(CategoryTheory.Limits.pushout.desc CategoryTheory.Limits.pushout.inl
(CategoryTheory.CategoryStruct.comp CategoryTheory.Limits.pushout.inl CategoryTheory.Limits.pushout.inr) ⋯)
CategoryTheory.Limits.pushout.inr ⋯)
X₁ ⨿[Z₁] (X₂ ⨿[Z₂] X₃) is the pushout (X₁ ⨿[Z₁] X₂) ×[X₂] (X₂ ⨿[Z₂] X₃).
Equations
- One or more equations did not get rendered due to their size.
def
CategoryTheory.Limits.pushoutAssocSymmIsPushout
{C : Type u}
[CategoryTheory.Category.{v, u} C]
{X₁ : C}
{X₂ : C}
{X₃ : C}
{Z₁ : C}
{Z₂ : C}
(g₁ : Z₁ ⟶ X₁)
(g₂ : Z₁ ⟶ X₂)
(g₃ : Z₂ ⟶ X₂)
(g₄ : Z₂ ⟶ X₃)
[CategoryTheory.Limits.HasPushout g₁ g₂]
[CategoryTheory.Limits.HasPushout g₃ g₄]
[CategoryTheory.Limits.HasPushout g₁ (CategoryTheory.CategoryStruct.comp g₂ CategoryTheory.Limits.pushout.inl)]
:
CategoryTheory.Limits.IsColimit
(CategoryTheory.Limits.PushoutCocone.mk
(CategoryTheory.Limits.pushout.desc CategoryTheory.Limits.pushout.inl
(CategoryTheory.CategoryStruct.comp CategoryTheory.Limits.pushout.inl CategoryTheory.Limits.pushout.inr) ⋯)
(CategoryTheory.CategoryStruct.comp CategoryTheory.Limits.pushout.inr CategoryTheory.Limits.pushout.inr) ⋯)
X₁ ⨿[Z₁] (X₂ ⨿[Z₂] X₃) is the pushout (X₁ ⨿[Z₁] X₂) ⨿[Z₂] X₃.
Equations
- One or more equations did not get rendered due to their size.
theorem
CategoryTheory.Limits.hasPushout_assoc_symm
{C : Type u}
[CategoryTheory.Category.{v, u} C]
{X₁ : C}
{X₂ : C}
{X₃ : C}
{Z₁ : C}
{Z₂ : C}
(g₁ : Z₁ ⟶ X₁)
(g₂ : Z₁ ⟶ X₂)
(g₃ : Z₂ ⟶ X₂)
(g₄ : Z₂ ⟶ X₃)
[CategoryTheory.Limits.HasPushout g₁ g₂]
[CategoryTheory.Limits.HasPushout g₃ g₄]
[CategoryTheory.Limits.HasPushout g₁ (CategoryTheory.CategoryStruct.comp g₂ CategoryTheory.Limits.pushout.inl)]
:
CategoryTheory.Limits.HasPushout (CategoryTheory.CategoryStruct.comp g₃ CategoryTheory.Limits.pushout.inr) g₄
noncomputable def
CategoryTheory.Limits.pushoutAssoc
{C : Type u}
[CategoryTheory.Category.{v, u} C]
{X₁ : C}
{X₂ : C}
{X₃ : C}
{Z₁ : C}
{Z₂ : C}
(g₁ : Z₁ ⟶ X₁)
(g₂ : Z₁ ⟶ X₂)
(g₃ : Z₂ ⟶ X₂)
(g₄ : Z₂ ⟶ X₃)
[CategoryTheory.Limits.HasPushout g₁ g₂]
[CategoryTheory.Limits.HasPushout g₃ g₄]
[CategoryTheory.Limits.HasPushout (CategoryTheory.CategoryStruct.comp g₃ CategoryTheory.Limits.pushout.inr) g₄]
[CategoryTheory.Limits.HasPushout g₁ (CategoryTheory.CategoryStruct.comp g₂ CategoryTheory.Limits.pushout.inl)]
:
CategoryTheory.Limits.pushout (CategoryTheory.CategoryStruct.comp g₃ CategoryTheory.Limits.pushout.inr) g₄ ≅ CategoryTheory.Limits.pushout g₁ (CategoryTheory.CategoryStruct.comp g₂ CategoryTheory.Limits.pushout.inl)
The canonical isomorphism (X₁ ⨿[Z₁] X₂) ⨿[Z₂] X₃ ≅ X₁ ⨿[Z₁] (X₂ ⨿[Z₂] X₃).
Equations
- One or more equations did not get rendered due to their size.
@[simp]
theorem
CategoryTheory.Limits.inl_inl_pushoutAssoc_hom_assoc
{C : Type u}
[CategoryTheory.Category.{v, u} C]
{X₁ : C}
{X₂ : C}
{X₃ : C}
{Z₁ : C}
{Z₂ : C}
(g₁ : Z₁ ⟶ X₁)
(g₂ : Z₁ ⟶ X₂)
(g₃ : Z₂ ⟶ X₂)
(g₄ : Z₂ ⟶ X₃)
[CategoryTheory.Limits.HasPushout g₁ g₂]
[CategoryTheory.Limits.HasPushout g₃ g₄]
[CategoryTheory.Limits.HasPushout (CategoryTheory.CategoryStruct.comp g₃ CategoryTheory.Limits.pushout.inr) g₄]
[CategoryTheory.Limits.HasPushout g₁ (CategoryTheory.CategoryStruct.comp g₂ CategoryTheory.Limits.pushout.inl)]
{Z : C}
(h : CategoryTheory.Limits.pushout g₁ (CategoryTheory.CategoryStruct.comp g₂ CategoryTheory.Limits.pushout.inl) ⟶ Z)
:
CategoryTheory.CategoryStruct.comp CategoryTheory.Limits.pushout.inl
(CategoryTheory.CategoryStruct.comp CategoryTheory.Limits.pushout.inl
(CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.pushoutAssoc g₁ g₂ g₃ g₄).hom h)) = CategoryTheory.CategoryStruct.comp CategoryTheory.Limits.pushout.inl h
@[simp]
theorem
CategoryTheory.Limits.inl_inl_pushoutAssoc_hom
{C : Type u}
[CategoryTheory.Category.{v, u} C]
{X₁ : C}
{X₂ : C}
{X₃ : C}
{Z₁ : C}
{Z₂ : C}
(g₁ : Z₁ ⟶ X₁)
(g₂ : Z₁ ⟶ X₂)
(g₃ : Z₂ ⟶ X₂)
(g₄ : Z₂ ⟶ X₃)
[CategoryTheory.Limits.HasPushout g₁ g₂]
[CategoryTheory.Limits.HasPushout g₃ g₄]
[CategoryTheory.Limits.HasPushout (CategoryTheory.CategoryStruct.comp g₃ CategoryTheory.Limits.pushout.inr) g₄]
[CategoryTheory.Limits.HasPushout g₁ (CategoryTheory.CategoryStruct.comp g₂ CategoryTheory.Limits.pushout.inl)]
:
CategoryTheory.CategoryStruct.comp CategoryTheory.Limits.pushout.inl
(CategoryTheory.CategoryStruct.comp CategoryTheory.Limits.pushout.inl
(CategoryTheory.Limits.pushoutAssoc g₁ g₂ g₃ g₄).hom) = CategoryTheory.Limits.pushout.inl
@[simp]
theorem
CategoryTheory.Limits.inr_inl_pushoutAssoc_hom_assoc
{C : Type u}
[CategoryTheory.Category.{v, u} C]
{X₁ : C}
{X₂ : C}
{X₃ : C}
{Z₁ : C}
{Z₂ : C}
(g₁ : Z₁ ⟶ X₁)
(g₂ : Z₁ ⟶ X₂)
(g₃ : Z₂ ⟶ X₂)
(g₄ : Z₂ ⟶ X₃)
[CategoryTheory.Limits.HasPushout g₁ g₂]
[CategoryTheory.Limits.HasPushout g₃ g₄]
[CategoryTheory.Limits.HasPushout (CategoryTheory.CategoryStruct.comp g₃ CategoryTheory.Limits.pushout.inr) g₄]
[CategoryTheory.Limits.HasPushout g₁ (CategoryTheory.CategoryStruct.comp g₂ CategoryTheory.Limits.pushout.inl)]
{Z : C}
(h : CategoryTheory.Limits.pushout g₁ (CategoryTheory.CategoryStruct.comp g₂ CategoryTheory.Limits.pushout.inl) ⟶ Z)
:
CategoryTheory.CategoryStruct.comp CategoryTheory.Limits.pushout.inr
(CategoryTheory.CategoryStruct.comp CategoryTheory.Limits.pushout.inl
(CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.pushoutAssoc g₁ g₂ g₃ g₄).hom h)) = CategoryTheory.CategoryStruct.comp CategoryTheory.Limits.pushout.inl
(CategoryTheory.CategoryStruct.comp CategoryTheory.Limits.pushout.inr h)
@[simp]
theorem
CategoryTheory.Limits.inr_inl_pushoutAssoc_hom
{C : Type u}
[CategoryTheory.Category.{v, u} C]
{X₁ : C}
{X₂ : C}
{X₃ : C}
{Z₁ : C}
{Z₂ : C}
(g₁ : Z₁ ⟶ X₁)
(g₂ : Z₁ ⟶ X₂)
(g₃ : Z₂ ⟶ X₂)
(g₄ : Z₂ ⟶ X₃)
[CategoryTheory.Limits.HasPushout g₁ g₂]
[CategoryTheory.Limits.HasPushout g₃ g₄]
[CategoryTheory.Limits.HasPushout (CategoryTheory.CategoryStruct.comp g₃ CategoryTheory.Limits.pushout.inr) g₄]
[CategoryTheory.Limits.HasPushout g₁ (CategoryTheory.CategoryStruct.comp g₂ CategoryTheory.Limits.pushout.inl)]
:
CategoryTheory.CategoryStruct.comp CategoryTheory.Limits.pushout.inr
(CategoryTheory.CategoryStruct.comp CategoryTheory.Limits.pushout.inl
(CategoryTheory.Limits.pushoutAssoc g₁ g₂ g₃ g₄).hom) = CategoryTheory.CategoryStruct.comp CategoryTheory.Limits.pushout.inl CategoryTheory.Limits.pushout.inr
@[simp]
theorem
CategoryTheory.Limits.inr_inr_pushoutAssoc_inv_assoc
{C : Type u}
[CategoryTheory.Category.{v, u} C]
{X₁ : C}
{X₂ : C}
{X₃ : C}
{Z₁ : C}
{Z₂ : C}
(g₁ : Z₁ ⟶ X₁)
(g₂ : Z₁ ⟶ X₂)
(g₃ : Z₂ ⟶ X₂)
(g₄ : Z₂ ⟶ X₃)
[CategoryTheory.Limits.HasPushout g₁ g₂]
[CategoryTheory.Limits.HasPushout g₃ g₄]
[CategoryTheory.Limits.HasPushout (CategoryTheory.CategoryStruct.comp g₃ CategoryTheory.Limits.pushout.inr) g₄]
[CategoryTheory.Limits.HasPushout g₁ (CategoryTheory.CategoryStruct.comp g₂ CategoryTheory.Limits.pushout.inl)]
{Z : C}
(h : CategoryTheory.Limits.pushout (CategoryTheory.CategoryStruct.comp g₃ CategoryTheory.Limits.pushout.inr) g₄ ⟶ Z)
:
CategoryTheory.CategoryStruct.comp CategoryTheory.Limits.pushout.inr
(CategoryTheory.CategoryStruct.comp CategoryTheory.Limits.pushout.inr
(CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.pushoutAssoc g₁ g₂ g₃ g₄).inv h)) = CategoryTheory.CategoryStruct.comp CategoryTheory.Limits.pushout.inr h
@[simp]
theorem
CategoryTheory.Limits.inr_inr_pushoutAssoc_inv
{C : Type u}
[CategoryTheory.Category.{v, u} C]
{X₁ : C}
{X₂ : C}
{X₃ : C}
{Z₁ : C}
{Z₂ : C}
(g₁ : Z₁ ⟶ X₁)
(g₂ : Z₁ ⟶ X₂)
(g₃ : Z₂ ⟶ X₂)
(g₄ : Z₂ ⟶ X₃)
[CategoryTheory.Limits.HasPushout g₁ g₂]
[CategoryTheory.Limits.HasPushout g₃ g₄]
[CategoryTheory.Limits.HasPushout (CategoryTheory.CategoryStruct.comp g₃ CategoryTheory.Limits.pushout.inr) g₄]
[CategoryTheory.Limits.HasPushout g₁ (CategoryTheory.CategoryStruct.comp g₂ CategoryTheory.Limits.pushout.inl)]
:
CategoryTheory.CategoryStruct.comp CategoryTheory.Limits.pushout.inr
(CategoryTheory.CategoryStruct.comp CategoryTheory.Limits.pushout.inr
(CategoryTheory.Limits.pushoutAssoc g₁ g₂ g₃ g₄).inv) = CategoryTheory.Limits.pushout.inr
@[simp]
theorem
CategoryTheory.Limits.inl_pushoutAssoc_inv_assoc
{C : Type u}
[CategoryTheory.Category.{v, u} C]
{X₁ : C}
{X₂ : C}
{X₃ : C}
{Z₁ : C}
{Z₂ : C}
(g₁ : Z₁ ⟶ X₁)
(g₂ : Z₁ ⟶ X₂)
(g₃ : Z₂ ⟶ X₂)
(g₄ : Z₂ ⟶ X₃)
[CategoryTheory.Limits.HasPushout g₁ g₂]
[CategoryTheory.Limits.HasPushout g₃ g₄]
[CategoryTheory.Limits.HasPushout (CategoryTheory.CategoryStruct.comp g₃ CategoryTheory.Limits.pushout.inr) g₄]
[CategoryTheory.Limits.HasPushout g₁ (CategoryTheory.CategoryStruct.comp g₂ CategoryTheory.Limits.pushout.inl)]
{Z : C}
(h : CategoryTheory.Limits.pushout (CategoryTheory.CategoryStruct.comp g₃ CategoryTheory.Limits.pushout.inr) g₄ ⟶ Z)
:
CategoryTheory.CategoryStruct.comp CategoryTheory.Limits.pushout.inl
(CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.pushoutAssoc g₁ g₂ g₃ g₄).inv h) = CategoryTheory.CategoryStruct.comp CategoryTheory.Limits.pushout.inl
(CategoryTheory.CategoryStruct.comp CategoryTheory.Limits.pushout.inl h)
@[simp]
theorem
CategoryTheory.Limits.inl_pushoutAssoc_inv
{C : Type u}
[CategoryTheory.Category.{v, u} C]
{X₁ : C}
{X₂ : C}
{X₃ : C}
{Z₁ : C}
{Z₂ : C}
(g₁ : Z₁ ⟶ X₁)
(g₂ : Z₁ ⟶ X₂)
(g₃ : Z₂ ⟶ X₂)
(g₄ : Z₂ ⟶ X₃)
[CategoryTheory.Limits.HasPushout g₁ g₂]
[CategoryTheory.Limits.HasPushout g₃ g₄]
[CategoryTheory.Limits.HasPushout (CategoryTheory.CategoryStruct.comp g₃ CategoryTheory.Limits.pushout.inr) g₄]
[CategoryTheory.Limits.HasPushout g₁ (CategoryTheory.CategoryStruct.comp g₂ CategoryTheory.Limits.pushout.inl)]
:
CategoryTheory.CategoryStruct.comp CategoryTheory.Limits.pushout.inl
(CategoryTheory.Limits.pushoutAssoc g₁ g₂ g₃ g₄).inv = CategoryTheory.CategoryStruct.comp CategoryTheory.Limits.pushout.inl CategoryTheory.Limits.pushout.inl
@[simp]
theorem
CategoryTheory.Limits.inl_inr_pushoutAssoc_inv_assoc
{C : Type u}
[CategoryTheory.Category.{v, u} C]
{X₁ : C}
{X₂ : C}
{X₃ : C}
{Z₁ : C}
{Z₂ : C}
(g₁ : Z₁ ⟶ X₁)
(g₂ : Z₁ ⟶ X₂)
(g₃ : Z₂ ⟶ X₂)
(g₄ : Z₂ ⟶ X₃)
[CategoryTheory.Limits.HasPushout g₁ g₂]
[CategoryTheory.Limits.HasPushout g₃ g₄]
[CategoryTheory.Limits.HasPushout (CategoryTheory.CategoryStruct.comp g₃ CategoryTheory.Limits.pushout.inr) g₄]
[CategoryTheory.Limits.HasPushout g₁ (CategoryTheory.CategoryStruct.comp g₂ CategoryTheory.Limits.pushout.inl)]
{Z : C}
(h : CategoryTheory.Limits.pushout (CategoryTheory.CategoryStruct.comp g₃ CategoryTheory.Limits.pushout.inr) g₄ ⟶ Z)
:
CategoryTheory.CategoryStruct.comp CategoryTheory.Limits.pushout.inl
(CategoryTheory.CategoryStruct.comp CategoryTheory.Limits.pushout.inr
(CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.pushoutAssoc g₁ g₂ g₃ g₄).inv h)) = CategoryTheory.CategoryStruct.comp CategoryTheory.Limits.pushout.inr
(CategoryTheory.CategoryStruct.comp CategoryTheory.Limits.pushout.inl h)
@[simp]
theorem
CategoryTheory.Limits.inl_inr_pushoutAssoc_inv
{C : Type u}
[CategoryTheory.Category.{v, u} C]
{X₁ : C}
{X₂ : C}
{X₃ : C}
{Z₁ : C}
{Z₂ : C}
(g₁ : Z₁ ⟶ X₁)
(g₂ : Z₁ ⟶ X₂)
(g₃ : Z₂ ⟶ X₂)
(g₄ : Z₂ ⟶ X₃)
[CategoryTheory.Limits.HasPushout g₁ g₂]
[CategoryTheory.Limits.HasPushout g₃ g₄]
[CategoryTheory.Limits.HasPushout (CategoryTheory.CategoryStruct.comp g₃ CategoryTheory.Limits.pushout.inr) g₄]
[CategoryTheory.Limits.HasPushout g₁ (CategoryTheory.CategoryStruct.comp g₂ CategoryTheory.Limits.pushout.inl)]
:
CategoryTheory.CategoryStruct.comp CategoryTheory.Limits.pushout.inl
(CategoryTheory.CategoryStruct.comp CategoryTheory.Limits.pushout.inr
(CategoryTheory.Limits.pushoutAssoc g₁ g₂ g₃ g₄).inv) = CategoryTheory.CategoryStruct.comp CategoryTheory.Limits.pushout.inr CategoryTheory.Limits.pushout.inl
@[simp]
theorem
CategoryTheory.Limits.inr_pushoutAssoc_hom_assoc
{C : Type u}
[CategoryTheory.Category.{v, u} C]
{X₁ : C}
{X₂ : C}
{X₃ : C}
{Z₁ : C}
{Z₂ : C}
(g₁ : Z₁ ⟶ X₁)
(g₂ : Z₁ ⟶ X₂)
(g₃ : Z₂ ⟶ X₂)
(g₄ : Z₂ ⟶ X₃)
[CategoryTheory.Limits.HasPushout g₁ g₂]
[CategoryTheory.Limits.HasPushout g₃ g₄]
[CategoryTheory.Limits.HasPushout (CategoryTheory.CategoryStruct.comp g₃ CategoryTheory.Limits.pushout.inr) g₄]
[CategoryTheory.Limits.HasPushout g₁ (CategoryTheory.CategoryStruct.comp g₂ CategoryTheory.Limits.pushout.inl)]
{Z : C}
(h : CategoryTheory.Limits.pushout g₁ (CategoryTheory.CategoryStruct.comp g₂ CategoryTheory.Limits.pushout.inl) ⟶ Z)
:
CategoryTheory.CategoryStruct.comp CategoryTheory.Limits.pushout.inr
(CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.pushoutAssoc g₁ g₂ g₃ g₄).hom h) = CategoryTheory.CategoryStruct.comp CategoryTheory.Limits.pushout.inr
(CategoryTheory.CategoryStruct.comp CategoryTheory.Limits.pushout.inr h)
@[simp]
theorem
CategoryTheory.Limits.inr_pushoutAssoc_hom
{C : Type u}
[CategoryTheory.Category.{v, u} C]
{X₁ : C}
{X₂ : C}
{X₃ : C}
{Z₁ : C}
{Z₂ : C}
(g₁ : Z₁ ⟶ X₁)
(g₂ : Z₁ ⟶ X₂)
(g₃ : Z₂ ⟶ X₂)
(g₄ : Z₂ ⟶ X₃)
[CategoryTheory.Limits.HasPushout g₁ g₂]
[CategoryTheory.Limits.HasPushout g₃ g₄]
[CategoryTheory.Limits.HasPushout (CategoryTheory.CategoryStruct.comp g₃ CategoryTheory.Limits.pushout.inr) g₄]
[CategoryTheory.Limits.HasPushout g₁ (CategoryTheory.CategoryStruct.comp g₂ CategoryTheory.Limits.pushout.inl)]
:
CategoryTheory.CategoryStruct.comp CategoryTheory.Limits.pushout.inr
(CategoryTheory.Limits.pushoutAssoc g₁ g₂ g₃ g₄).hom = CategoryTheory.CategoryStruct.comp CategoryTheory.Limits.pushout.inr CategoryTheory.Limits.pushout.inr
@[inline, reducible]
HasPushouts represents a choice of pushout for every pair of morphisms
theorem
CategoryTheory.Limits.hasPullbacks_of_hasLimit_cospan
(C : Type u)
[CategoryTheory.Category.{v, u} C]
[∀ {X Y Z : C} {f : X ⟶ Z} {g : Y ⟶ Z}, CategoryTheory.Limits.HasLimit (CategoryTheory.Limits.cospan f g)]
:
If C has all limits of diagrams cospan f g, then it has all pullbacks
theorem
CategoryTheory.Limits.hasPushouts_of_hasColimit_span
(C : Type u)
[CategoryTheory.Category.{v, u} C]
[∀ {X Y Z : C} {f : X ⟶ Y} {g : X ⟶ Z}, CategoryTheory.Limits.HasColimit (CategoryTheory.Limits.span f g)]
:
If C has all colimits of diagrams span f g, then it has all pushouts
@[simp]
theorem
CategoryTheory.Limits.walkingSpanOpEquiv_inverse_map
{X₁ : CategoryTheory.Limits.WidePullbackShape CategoryTheory.Limits.WalkingPair}
{X₂ : CategoryTheory.Limits.WidePullbackShape CategoryTheory.Limits.WalkingPair}
:
∀ (a : X₁ ⟶ X₂),
CategoryTheory.Limits.walkingSpanOpEquiv.inverse.map a = CategoryTheory.Limits.widePullbackShapeOpMap CategoryTheory.Limits.WalkingPair X₁ X₂ a
@[simp]
theorem
CategoryTheory.Limits.walkingSpanOpEquiv_functor_obj
(X : (CategoryTheory.Limits.WidePushoutShape CategoryTheory.Limits.WalkingPair)ᵒᵖ)
:
CategoryTheory.Limits.walkingSpanOpEquiv.functor.obj X = X.unop
@[simp]
theorem
CategoryTheory.Limits.walkingSpanOpEquiv_functor_map :
∀ {X Y : (CategoryTheory.Limits.WidePushoutShape CategoryTheory.Limits.WalkingPair)ᵒᵖ} (f : X ⟶ Y),
CategoryTheory.Limits.walkingSpanOpEquiv.functor.map f = (CategoryTheory.Limits.widePushoutShapeOpMap CategoryTheory.Limits.WalkingPair Y.unop X.unop f.unop).unop
The duality equivalence WalkingSpanᵒᵖ ≌ WalkingCospan
@[simp]
theorem
CategoryTheory.Limits.walkingCospanOpEquiv_inverse_map
{X : CategoryTheory.Limits.WidePushoutShape CategoryTheory.Limits.WalkingPair}
{Y : CategoryTheory.Limits.WidePushoutShape CategoryTheory.Limits.WalkingPair}
:
∀ (a : X ⟶ Y),
CategoryTheory.Limits.walkingCospanOpEquiv.inverse.map a = CategoryTheory.Limits.widePushoutShapeOpMap CategoryTheory.Limits.WalkingPair X Y a
@[simp]
theorem
CategoryTheory.Limits.walkingCospanOpEquiv_functor_map :
∀ {X Y : (CategoryTheory.Limits.WidePullbackShape CategoryTheory.Limits.WalkingPair)ᵒᵖ} (f : X ⟶ Y),
CategoryTheory.Limits.walkingCospanOpEquiv.functor.map f = (CategoryTheory.Limits.widePullbackShapeOpMap CategoryTheory.Limits.WalkingPair Y.unop X.unop f.unop).unop
@[simp]
The duality equivalence WalkingCospanᵒᵖ ≌ WalkingSpan
instance
CategoryTheory.Limits.hasPullbacks_of_hasWidePullbacks
(D : Type u)
[h : CategoryTheory.Category.{v, u} D]
[h' : CategoryTheory.Limits.HasWidePullbacks D]
:
Having wide pullback at any universe level implies having binary pullbacks.
Equations
- ⋯ = ⋯
instance
CategoryTheory.Limits.hasPushouts_of_hasWidePushouts
(D : Type u)
[h : CategoryTheory.Category.{v, u} D]
[h' : CategoryTheory.Limits.HasWidePushouts D]
:
Having wide pushout at any universe level implies having binary pushouts.
Equations
- ⋯ = ⋯
@[simp]
theorem
CategoryTheory.Limits.baseChange_map_left
{C : Type u}
[CategoryTheory.Category.{v, u} C]
[CategoryTheory.Limits.HasPullbacks C]
{X : C}
{Y : C}
(f : X ⟶ Y)
:
∀ {X_1 Y_1 : CategoryTheory.Over Y} (i : X_1 ⟶ Y_1),
((CategoryTheory.Limits.baseChange f).map i).left = CategoryTheory.Limits.pullback.map X_1.hom f Y_1.hom f i.left (CategoryTheory.CategoryStruct.id X)
(CategoryTheory.CategoryStruct.id Y) ⋯ ⋯
@[simp]
theorem
CategoryTheory.Limits.baseChange_obj_left
{C : Type u}
[CategoryTheory.Category.{v, u} C]
[CategoryTheory.Limits.HasPullbacks C]
{X : C}
{Y : C}
(f : X ⟶ Y)
(g : CategoryTheory.Over Y)
:
((CategoryTheory.Limits.baseChange f).obj g).left = CategoryTheory.Limits.pullback g.hom f
@[simp]
theorem
CategoryTheory.Limits.baseChange_obj_hom
{C : Type u}
[CategoryTheory.Category.{v, u} C]
[CategoryTheory.Limits.HasPullbacks C]
{X : C}
{Y : C}
(f : X ⟶ Y)
(g : CategoryTheory.Over Y)
:
((CategoryTheory.Limits.baseChange f).obj g).hom = CategoryTheory.Limits.pullback.snd
def
CategoryTheory.Limits.baseChange
{C : Type u}
[CategoryTheory.Category.{v, u} C]
[CategoryTheory.Limits.HasPullbacks C]
{X : C}
{Y : C}
(f : X ⟶ Y)
:
Given a morphism f : X ⟶ Y, we can take morphisms over Y to morphisms over X via
pullbacks. This is right adjoint to over.map (TODO)
Equations
- One or more equations did not get rendered due to their size.