Pullbacks #
THIS FILE IS SYNCHRONIZED WITH MATHLIB4. Any changes to this file require a corresponding PR to mathlib4.
We define a category walking_cospan (resp. walking_span), 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 #
@[reducible]
The type of objects for the diagram indexing a pullback, defined as a special case of
wide_pullback_shape.
@[reducible]
The left point of the walking cospan.
@[reducible]
The right point of the walking cospan.
@[reducible]
The central point of the walking cospan.
@[reducible]
The type of objects for the diagram indexing a pushout, defined as a special case of
wide_pushout_shape.
@[reducible]
The left point of the walking span.
@[reducible]
The right point of the walking span.
@[reducible]
The central point of the walking span.
@[reducible]
The type of arrows for the diagram indexing a pullback.
@[reducible]
The left arrow of the walking cospan.
@[reducible]
The right arrow of the walking cospan.
@[reducible]
def
category_theory.limits.walking_cospan.hom.id
(X : category_theory.limits.walking_cospan) :
X ⟶ X
The identity arrows of the walking cospan.
@[protected, instance]
@[reducible]
The type of arrows for the diagram indexing a pushout.
@[reducible]
The identity arrows of the walking span.
@[protected, instance]
def
category_theory.limits.walking_cospan.ext
{C : Type u}
[category_theory.category C]
{F : category_theory.limits.walking_cospan ⥤ C}
{s t : category_theory.limits.cone F}
(i : s.X ≅ t.X)
(w₁ : s.π.app category_theory.limits.walking_cospan.left = i.hom ≫ t.π.app category_theory.limits.walking_cospan.left)
(w₂ : s.π.app category_theory.limits.walking_cospan.right = i.hom ≫ t.π.app category_theory.limits.walking_cospan.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
category_theory.limits.walking_span.ext
{C : Type u}
[category_theory.category C]
{F : category_theory.limits.walking_span ⥤ C}
{s t : category_theory.limits.cocone F}
(i : s.X ≅ t.X)
(w₁ : s.ι.app category_theory.limits.walking_cospan.left ≫ i.hom = t.ι.app category_theory.limits.walking_cospan.left)
(w₂ : s.ι.app category_theory.limits.walking_cospan.right ≫ i.hom = t.ι.app category_theory.limits.walking_cospan.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
category_theory.limits.cospan
{C : Type u}
[category_theory.category C]
{X Y Z : C}
(f : X ⟶ Z)
(g : Y ⟶ Z) :
cospan f g is the functor from the walking cospan hitting f and g.
Equations
- category_theory.limits.cospan f g = category_theory.limits.wide_pullback_shape.wide_cospan Z (λ (j : category_theory.limits.walking_pair), j.cases_on X Y) (λ (j : category_theory.limits.walking_pair), j.cases_on f g)
Instances for category_theory.limits.cospan
- category_theory.adhesive.has_pullback_of_mono_left
- category_theory.limits.has_pullback_of_comp_mono
- category_theory.limits.has_pullback_of_right_factors_mono
- category_theory.limits.has_pullback_of_left_factors_mono
- category_theory.limits.has_kernel_pair_of_mono
- category_theory.glue_data.f_has_pullback
- category_theory.glue_data.category_theory.functor.map.category_theory.limits.has_pullback
- category_theory.limits.has_pullback_over_zero
- category_theory.is_pullback.has_pullback_biprod_fst_biprod_snd
- algebraic_geometry.PresheafedSpace.is_open_immersion.has_pullback_of_left
- algebraic_geometry.PresheafedSpace.is_open_immersion.has_pullback_of_right
- algebraic_geometry.PresheafedSpace.is_open_immersion.forget_preserves_limits_of_left
- algebraic_geometry.PresheafedSpace.is_open_immersion.forget_preserves_limits_of_right
- algebraic_geometry.SheafedSpace.is_open_immersion.has_limit_cospan_forget_of_left'
- algebraic_geometry.SheafedSpace.is_open_immersion.has_limit_cospan_forget_of_right'
- algebraic_geometry.SheafedSpace.is_open_immersion.forget_creates_pullback_of_left
- algebraic_geometry.SheafedSpace.is_open_immersion.forget_creates_pullback_of_right
- algebraic_geometry.SheafedSpace.is_open_immersion.SheafedSpace_forget_preserves_of_left
- algebraic_geometry.SheafedSpace.is_open_immersion.SheafedSpace_forget_preserves_of_right
- algebraic_geometry.SheafedSpace.is_open_immersion.SheafedSpace_has_pullback_of_left
- algebraic_geometry.SheafedSpace.is_open_immersion.SheafedSpace_has_pullback_of_right
- algebraic_geometry.LocallyRingedSpace.is_open_immersion.has_pullback_of_left
- algebraic_geometry.LocallyRingedSpace.is_open_immersion.has_pullback_of_right
- algebraic_geometry.LocallyRingedSpace.is_open_immersion.forget_preserves_pullback_of_left
- algebraic_geometry.LocallyRingedSpace.is_open_immersion.forget_to_PresheafedSpace_preserves_pullback_of_left
- algebraic_geometry.LocallyRingedSpace.is_open_immersion.forget_to_Top_preserves_pullback_of_left
- algebraic_geometry.LocallyRingedSpace.is_open_immersion.forget_reflects_pullback_of_left
- algebraic_geometry.LocallyRingedSpace.is_open_immersion.forget_preserves_pullback_of_right
- algebraic_geometry.LocallyRingedSpace.is_open_immersion.forget_to_PresheafedSpace_preserves_pullback_of_right
- algebraic_geometry.LocallyRingedSpace.is_open_immersion.forget_reflects_pullback_of_right
- algebraic_geometry.LocallyRingedSpace.is_open_immersion.forget_to_PresheafedSpace_reflects_pullback_of_left
- algebraic_geometry.LocallyRingedSpace.is_open_immersion.forget_to_PresheafedSpace_reflects_pullback_of_right
- algebraic_geometry.LocallyRingedSpace.glue_data.algebraic_geometry.LocallyRingedSpace.forget_to_SheafedSpace.category_theory.limits.preserves_limit
- algebraic_geometry.is_open_immersion.has_limit_cospan_forget_of_left'
- algebraic_geometry.is_open_immersion.has_limit_cospan_forget_of_right'
- algebraic_geometry.is_open_immersion.forget_creates_pullback_of_left
- algebraic_geometry.is_open_immersion.forget_creates_pullback_of_right
- algebraic_geometry.is_open_immersion.forget_preserves_of_left
- algebraic_geometry.is_open_immersion.forget_preserves_of_right
- algebraic_geometry.is_open_immersion.has_pullback_of_left
- algebraic_geometry.is_open_immersion.has_pullback_of_right
- algebraic_geometry.is_open_immersion.forget_to_Top_preserves_of_left
- algebraic_geometry.is_open_immersion.forget_to_Top_preserves_of_right
- algebraic_geometry.Scheme.pullback.affine_has_pullback
- algebraic_geometry.Scheme.pullback.base_affine_has_pullback
- algebraic_geometry.Scheme.pullback.left_affine_comp_pullback_has_pullback
- algebraic_geometry.Scheme.pullback.category_theory.limits.has_pullback
def
category_theory.limits.span
{C : Type u}
[category_theory.category C]
{X Y Z : C}
(f : X ⟶ Y)
(g : X ⟶ Z) :
span f g is the functor from the walking span hitting f and g.
Equations
- category_theory.limits.span f g = category_theory.limits.wide_pushout_shape.wide_span X (λ (j : category_theory.limits.walking_pair), j.cases_on Y Z) (λ (j : category_theory.limits.walking_pair), j.cases_on f g)
Instances for category_theory.limits.span
- category_theory.adhesive.has_pushout_of_mono_left
- category_theory.limits.has_pushout_of_epi_comp
- category_theory.limits.has_pushout_of_right_factors_epi
- category_theory.limits.has_pushout_of_left_factors_epi
- category_theory.limits.has_cokernel_pair_of_epi
- category_theory.limits.has_pushout_over_zero
- category_theory.is_pushout.has_pushout_biprod_fst_biprod_snd
@[simp]
theorem
category_theory.limits.cospan_left
{C : Type u}
[category_theory.category C]
{X Y Z : C}
(f : X ⟶ Z)
(g : Y ⟶ Z) :
@[simp]
theorem
category_theory.limits.span_left
{C : Type u}
[category_theory.category C]
{X Y Z : C}
(f : X ⟶ Y)
(g : X ⟶ Z) :
@[simp]
theorem
category_theory.limits.cospan_right
{C : Type u}
[category_theory.category C]
{X Y Z : C}
(f : X ⟶ Z)
(g : Y ⟶ Z) :
@[simp]
theorem
category_theory.limits.span_right
{C : Type u}
[category_theory.category C]
{X Y Z : C}
(f : X ⟶ Y)
(g : X ⟶ Z) :
@[simp]
theorem
category_theory.limits.cospan_one
{C : Type u}
[category_theory.category C]
{X Y Z : C}
(f : X ⟶ Z)
(g : Y ⟶ Z) :
@[simp]
theorem
category_theory.limits.span_zero
{C : Type u}
[category_theory.category C]
{X Y Z : C}
(f : X ⟶ Y)
(g : X ⟶ Z) :
@[simp]
theorem
category_theory.limits.cospan_map_inl
{C : Type u}
[category_theory.category C]
{X Y Z : C}
(f : X ⟶ Z)
(g : Y ⟶ Z) :
@[simp]
theorem
category_theory.limits.span_map_fst
{C : Type u}
[category_theory.category C]
{X Y Z : C}
(f : X ⟶ Y)
(g : X ⟶ Z) :
@[simp]
theorem
category_theory.limits.cospan_map_inr
{C : Type u}
[category_theory.category C]
{X Y Z : C}
(f : X ⟶ Z)
(g : Y ⟶ Z) :
@[simp]
theorem
category_theory.limits.span_map_snd
{C : Type u}
[category_theory.category C]
{X Y Z : C}
(f : X ⟶ Y)
(g : X ⟶ Z) :
theorem
category_theory.limits.cospan_map_id
{C : Type u}
[category_theory.category C]
{X Y Z : C}
(f : X ⟶ Z)
(g : Y ⟶ Z)
(w : category_theory.limits.walking_cospan) :
theorem
category_theory.limits.span_map_id
{C : Type u}
[category_theory.category C]
{X Y Z : C}
(f : X ⟶ Y)
(g : X ⟶ Z)
(w : category_theory.limits.walking_span) :
(category_theory.limits.span f g).map (category_theory.limits.walking_span.hom.id w) = 𝟙 ((category_theory.limits.span f g).obj w)
def
category_theory.limits.diagram_iso_cospan
{C : Type u}
[category_theory.category C]
(F : category_theory.limits.walking_cospan ⥤ C) :
Every diagram indexing an pullback is naturally isomorphic (actually, equal) to a cospan
@[simp]
theorem
category_theory.limits.diagram_iso_cospan_hom_app
{C : Type u}
[category_theory.category C]
(F : category_theory.limits.walking_cospan ⥤ C)
(X : category_theory.limits.walking_cospan) :
(category_theory.limits.diagram_iso_cospan F).hom.app X = ((λ (j : category_theory.limits.walking_cospan), category_theory.eq_to_iso _) X).hom
@[simp]
theorem
category_theory.limits.diagram_iso_cospan_inv_app
{C : Type u}
[category_theory.category C]
(F : category_theory.limits.walking_cospan ⥤ C)
(X : category_theory.limits.walking_cospan) :
(category_theory.limits.diagram_iso_cospan F).inv.app X = ((λ (j : category_theory.limits.walking_cospan), category_theory.eq_to_iso _) X).inv
@[simp]
theorem
category_theory.limits.diagram_iso_span_inv_app
{C : Type u}
[category_theory.category C]
(F : category_theory.limits.walking_span ⥤ C)
(X : category_theory.limits.walking_span) :
(category_theory.limits.diagram_iso_span F).inv.app X = ((λ (j : category_theory.limits.walking_span), category_theory.eq_to_iso _) X).inv
@[simp]
theorem
category_theory.limits.diagram_iso_span_hom_app
{C : Type u}
[category_theory.category C]
(F : category_theory.limits.walking_span ⥤ C)
(X : category_theory.limits.walking_span) :
(category_theory.limits.diagram_iso_span F).hom.app X = ((λ (j : category_theory.limits.walking_span), category_theory.eq_to_iso _) X).hom
def
category_theory.limits.diagram_iso_span
{C : Type u}
[category_theory.category C]
(F : category_theory.limits.walking_span ⥤ C) :
Every diagram indexing a pushout is naturally isomorphic (actually, equal) to a span
def
category_theory.limits.cospan_comp_iso
{C : Type u}
[category_theory.category C]
{D : Type u₂}
[category_theory.category D]
(F : C ⥤ D)
{X Y Z : C}
(f : X ⟶ Z)
(g : Y ⟶ Z) :
category_theory.limits.cospan f g ⋙ F ≅ category_theory.limits.cospan (F.map f) (F.map g)
A functor applied to a cospan is a cospan.
Equations
- category_theory.limits.cospan_comp_iso F f g = category_theory.nat_iso.of_components (λ (X_1 : category_theory.limits.walking_cospan), option.cases_on X_1 (category_theory.iso.refl ((category_theory.limits.cospan f g ⋙ F).obj option.none)) (λ (X_1 : category_theory.limits.walking_pair), X_1.cases_on (category_theory.iso.refl ((category_theory.limits.cospan f g ⋙ F).obj (option.some category_theory.limits.walking_pair.left))) (category_theory.iso.refl ((category_theory.limits.cospan f g ⋙ F).obj (option.some category_theory.limits.walking_pair.right))))) _
@[simp]
theorem
category_theory.limits.cospan_comp_iso_app_left
{C : Type u}
[category_theory.category C]
{D : Type u₂}
[category_theory.category D]
(F : C ⥤ D)
{X Y Z : C}
(f : X ⟶ Z)
(g : Y ⟶ Z) :
@[simp]
theorem
category_theory.limits.cospan_comp_iso_app_right
{C : Type u}
[category_theory.category C]
{D : Type u₂}
[category_theory.category D]
(F : C ⥤ D)
{X Y Z : C}
(f : X ⟶ Z)
(g : Y ⟶ Z) :
@[simp]
theorem
category_theory.limits.cospan_comp_iso_app_one
{C : Type u}
[category_theory.category C]
{D : Type u₂}
[category_theory.category D]
(F : C ⥤ D)
{X Y Z : C}
(f : X ⟶ Z)
(g : Y ⟶ Z) :
@[simp]
theorem
category_theory.limits.cospan_comp_iso_hom_app_left
{C : Type u}
[category_theory.category C]
{D : Type u₂}
[category_theory.category D]
(F : C ⥤ D)
{X Y Z : C}
(f : X ⟶ Z)
(g : Y ⟶ Z) :
@[simp]
theorem
category_theory.limits.cospan_comp_iso_hom_app_right
{C : Type u}
[category_theory.category C]
{D : Type u₂}
[category_theory.category D]
(F : C ⥤ D)
{X Y Z : C}
(f : X ⟶ Z)
(g : Y ⟶ Z) :
@[simp]
theorem
category_theory.limits.cospan_comp_iso_hom_app_one
{C : Type u}
[category_theory.category C]
{D : Type u₂}
[category_theory.category D]
(F : C ⥤ D)
{X Y Z : C}
(f : X ⟶ Z)
(g : Y ⟶ Z) :
@[simp]
theorem
category_theory.limits.cospan_comp_iso_inv_app_left
{C : Type u}
[category_theory.category C]
{D : Type u₂}
[category_theory.category D]
(F : C ⥤ D)
{X Y Z : C}
(f : X ⟶ Z)
(g : Y ⟶ Z) :
@[simp]
theorem
category_theory.limits.cospan_comp_iso_inv_app_right
{C : Type u}
[category_theory.category C]
{D : Type u₂}
[category_theory.category D]
(F : C ⥤ D)
{X Y Z : C}
(f : X ⟶ Z)
(g : Y ⟶ Z) :
@[simp]
theorem
category_theory.limits.cospan_comp_iso_inv_app_one
{C : Type u}
[category_theory.category C]
{D : Type u₂}
[category_theory.category D]
(F : C ⥤ D)
{X Y Z : C}
(f : X ⟶ Z)
(g : Y ⟶ Z) :
def
category_theory.limits.span_comp_iso
{C : Type u}
[category_theory.category C]
{D : Type u₂}
[category_theory.category D]
(F : C ⥤ D)
{X Y Z : C}
(f : X ⟶ Y)
(g : X ⟶ Z) :
category_theory.limits.span f g ⋙ F ≅ category_theory.limits.span (F.map f) (F.map g)
A functor applied to a span is a span.
Equations
- category_theory.limits.span_comp_iso F f g = category_theory.nat_iso.of_components (λ (X_1 : category_theory.limits.walking_span), option.cases_on X_1 (category_theory.iso.refl ((category_theory.limits.span f g ⋙ F).obj option.none)) (λ (X_1 : category_theory.limits.walking_pair), X_1.cases_on (category_theory.iso.refl ((category_theory.limits.span f g ⋙ F).obj (option.some category_theory.limits.walking_pair.left))) (category_theory.iso.refl ((category_theory.limits.span f g ⋙ F).obj (option.some category_theory.limits.walking_pair.right))))) _
@[simp]
theorem
category_theory.limits.span_comp_iso_app_left
{C : Type u}
[category_theory.category C]
{D : Type u₂}
[category_theory.category D]
(F : C ⥤ D)
{X Y Z : C}
(f : X ⟶ Y)
(g : X ⟶ Z) :
@[simp]
theorem
category_theory.limits.span_comp_iso_app_right
{C : Type u}
[category_theory.category C]
{D : Type u₂}
[category_theory.category D]
(F : C ⥤ D)
{X Y Z : C}
(f : X ⟶ Y)
(g : X ⟶ Z) :
@[simp]
theorem
category_theory.limits.span_comp_iso_app_zero
{C : Type u}
[category_theory.category C]
{D : Type u₂}
[category_theory.category D]
(F : C ⥤ D)
{X Y Z : C}
(f : X ⟶ Y)
(g : X ⟶ Z) :
@[simp]
theorem
category_theory.limits.span_comp_iso_hom_app_left
{C : Type u}
[category_theory.category C]
{D : Type u₂}
[category_theory.category D]
(F : C ⥤ D)
{X Y Z : C}
(f : X ⟶ Y)
(g : X ⟶ Z) :
@[simp]
theorem
category_theory.limits.span_comp_iso_hom_app_right
{C : Type u}
[category_theory.category C]
{D : Type u₂}
[category_theory.category D]
(F : C ⥤ D)
{X Y Z : C}
(f : X ⟶ Y)
(g : X ⟶ Z) :
@[simp]
theorem
category_theory.limits.span_comp_iso_hom_app_zero
{C : Type u}
[category_theory.category C]
{D : Type u₂}
[category_theory.category D]
(F : C ⥤ D)
{X Y Z : C}
(f : X ⟶ Y)
(g : X ⟶ Z) :
@[simp]
theorem
category_theory.limits.span_comp_iso_inv_app_left
{C : Type u}
[category_theory.category C]
{D : Type u₂}
[category_theory.category D]
(F : C ⥤ D)
{X Y Z : C}
(f : X ⟶ Y)
(g : X ⟶ Z) :
@[simp]
theorem
category_theory.limits.span_comp_iso_inv_app_right
{C : Type u}
[category_theory.category C]
{D : Type u₂}
[category_theory.category D]
(F : C ⥤ D)
{X Y Z : C}
(f : X ⟶ Y)
(g : X ⟶ Z) :
@[simp]
theorem
category_theory.limits.span_comp_iso_inv_app_zero
{C : Type u}
[category_theory.category C]
{D : Type u₂}
[category_theory.category D]
(F : C ⥤ D)
{X Y Z : C}
(f : X ⟶ Y)
(g : X ⟶ Z) :
def
category_theory.limits.cospan_ext
{C : Type u}
[category_theory.category C]
{X Y Z X' Y' Z' : C}
(iX : X ≅ X')
(iY : Y ≅ Y')
(iZ : Z ≅ Z')
{f : X ⟶ Z}
{g : Y ⟶ Z}
{f' : X' ⟶ Z'}
{g' : Y' ⟶ Z'}
(wf : iX.hom ≫ f' = f ≫ iZ.hom)
(wg : iY.hom ≫ g' = g ≫ iZ.hom) :
Construct an isomorphism of cospans from components.
Equations
- category_theory.limits.cospan_ext iX iY iZ wf wg = category_theory.nat_iso.of_components (λ (X_1 : category_theory.limits.walking_cospan), option.cases_on X_1 iZ (λ (X_1 : category_theory.limits.walking_pair), X_1.cases_on iX iY)) _
@[simp]
theorem
category_theory.limits.cospan_ext_app_left
{C : Type u}
[category_theory.category C]
{X Y Z X' Y' Z' : C}
(iX : X ≅ X')
(iY : Y ≅ Y')
(iZ : Z ≅ Z')
{f : X ⟶ Z}
{g : Y ⟶ Z}
{f' : X' ⟶ Z'}
{g' : Y' ⟶ Z'}
(wf : iX.hom ≫ f' = f ≫ iZ.hom)
(wg : iY.hom ≫ g' = g ≫ iZ.hom) :
(category_theory.limits.cospan_ext iX iY iZ wf wg).app category_theory.limits.walking_cospan.left = iX
@[simp]
theorem
category_theory.limits.cospan_ext_app_right
{C : Type u}
[category_theory.category C]
{X Y Z X' Y' Z' : C}
(iX : X ≅ X')
(iY : Y ≅ Y')
(iZ : Z ≅ Z')
{f : X ⟶ Z}
{g : Y ⟶ Z}
{f' : X' ⟶ Z'}
{g' : Y' ⟶ Z'}
(wf : iX.hom ≫ f' = f ≫ iZ.hom)
(wg : iY.hom ≫ g' = g ≫ iZ.hom) :
(category_theory.limits.cospan_ext iX iY iZ wf wg).app category_theory.limits.walking_cospan.right = iY
@[simp]
theorem
category_theory.limits.cospan_ext_app_one
{C : Type u}
[category_theory.category C]
{X Y Z X' Y' Z' : C}
(iX : X ≅ X')
(iY : Y ≅ Y')
(iZ : Z ≅ Z')
{f : X ⟶ Z}
{g : Y ⟶ Z}
{f' : X' ⟶ Z'}
{g' : Y' ⟶ Z'}
(wf : iX.hom ≫ f' = f ≫ iZ.hom)
(wg : iY.hom ≫ g' = g ≫ iZ.hom) :
(category_theory.limits.cospan_ext iX iY iZ wf wg).app category_theory.limits.walking_cospan.one = iZ
@[simp]
theorem
category_theory.limits.cospan_ext_hom_app_left
{C : Type u}
[category_theory.category C]
{X Y Z X' Y' Z' : C}
(iX : X ≅ X')
(iY : Y ≅ Y')
(iZ : Z ≅ Z')
{f : X ⟶ Z}
{g : Y ⟶ Z}
{f' : X' ⟶ Z'}
{g' : Y' ⟶ Z'}
(wf : iX.hom ≫ f' = f ≫ iZ.hom)
(wg : iY.hom ≫ g' = g ≫ iZ.hom) :
(category_theory.limits.cospan_ext iX iY iZ wf wg).hom.app category_theory.limits.walking_cospan.left = iX.hom
@[simp]
theorem
category_theory.limits.cospan_ext_hom_app_right
{C : Type u}
[category_theory.category C]
{X Y Z X' Y' Z' : C}
(iX : X ≅ X')
(iY : Y ≅ Y')
(iZ : Z ≅ Z')
{f : X ⟶ Z}
{g : Y ⟶ Z}
{f' : X' ⟶ Z'}
{g' : Y' ⟶ Z'}
(wf : iX.hom ≫ f' = f ≫ iZ.hom)
(wg : iY.hom ≫ g' = g ≫ iZ.hom) :
(category_theory.limits.cospan_ext iX iY iZ wf wg).hom.app category_theory.limits.walking_cospan.right = iY.hom
@[simp]
theorem
category_theory.limits.cospan_ext_hom_app_one
{C : Type u}
[category_theory.category C]
{X Y Z X' Y' Z' : C}
(iX : X ≅ X')
(iY : Y ≅ Y')
(iZ : Z ≅ Z')
{f : X ⟶ Z}
{g : Y ⟶ Z}
{f' : X' ⟶ Z'}
{g' : Y' ⟶ Z'}
(wf : iX.hom ≫ f' = f ≫ iZ.hom)
(wg : iY.hom ≫ g' = g ≫ iZ.hom) :
(category_theory.limits.cospan_ext iX iY iZ wf wg).hom.app category_theory.limits.walking_cospan.one = iZ.hom
@[simp]
theorem
category_theory.limits.cospan_ext_inv_app_left
{C : Type u}
[category_theory.category C]
{X Y Z X' Y' Z' : C}
(iX : X ≅ X')
(iY : Y ≅ Y')
(iZ : Z ≅ Z')
{f : X ⟶ Z}
{g : Y ⟶ Z}
{f' : X' ⟶ Z'}
{g' : Y' ⟶ Z'}
(wf : iX.hom ≫ f' = f ≫ iZ.hom)
(wg : iY.hom ≫ g' = g ≫ iZ.hom) :
(category_theory.limits.cospan_ext iX iY iZ wf wg).inv.app category_theory.limits.walking_cospan.left = iX.inv
@[simp]
theorem
category_theory.limits.cospan_ext_inv_app_right
{C : Type u}
[category_theory.category C]
{X Y Z X' Y' Z' : C}
(iX : X ≅ X')
(iY : Y ≅ Y')
(iZ : Z ≅ Z')
{f : X ⟶ Z}
{g : Y ⟶ Z}
{f' : X' ⟶ Z'}
{g' : Y' ⟶ Z'}
(wf : iX.hom ≫ f' = f ≫ iZ.hom)
(wg : iY.hom ≫ g' = g ≫ iZ.hom) :
(category_theory.limits.cospan_ext iX iY iZ wf wg).inv.app category_theory.limits.walking_cospan.right = iY.inv
@[simp]
theorem
category_theory.limits.cospan_ext_inv_app_one
{C : Type u}
[category_theory.category C]
{X Y Z X' Y' Z' : C}
(iX : X ≅ X')
(iY : Y ≅ Y')
(iZ : Z ≅ Z')
{f : X ⟶ Z}
{g : Y ⟶ Z}
{f' : X' ⟶ Z'}
{g' : Y' ⟶ Z'}
(wf : iX.hom ≫ f' = f ≫ iZ.hom)
(wg : iY.hom ≫ g' = g ≫ iZ.hom) :
(category_theory.limits.cospan_ext iX iY iZ wf wg).inv.app category_theory.limits.walking_cospan.one = iZ.inv
def
category_theory.limits.span_ext
{C : Type u}
[category_theory.category C]
{X Y Z X' Y' Z' : C}
(iX : X ≅ X')
(iY : Y ≅ Y')
(iZ : Z ≅ Z')
{f : X ⟶ Y}
{g : X ⟶ Z}
{f' : X' ⟶ Y'}
{g' : X' ⟶ Z'}
(wf : iX.hom ≫ f' = f ≫ iY.hom)
(wg : iX.hom ≫ g' = g ≫ iZ.hom) :
Construct an isomorphism of spans from components.
Equations
- category_theory.limits.span_ext iX iY iZ wf wg = category_theory.nat_iso.of_components (λ (X_1 : category_theory.limits.walking_span), option.cases_on X_1 iX (λ (X_1 : category_theory.limits.walking_pair), X_1.cases_on iY iZ)) _
@[simp]
theorem
category_theory.limits.span_ext_app_left
{C : Type u}
[category_theory.category C]
{X Y Z X' Y' Z' : C}
(iX : X ≅ X')
(iY : Y ≅ Y')
(iZ : Z ≅ Z')
{f : X ⟶ Y}
{g : X ⟶ Z}
{f' : X' ⟶ Y'}
{g' : X' ⟶ Z'}
(wf : iX.hom ≫ f' = f ≫ iY.hom)
(wg : iX.hom ≫ g' = g ≫ iZ.hom) :
(category_theory.limits.span_ext iX iY iZ wf wg).app category_theory.limits.walking_span.left = iY
@[simp]
theorem
category_theory.limits.span_ext_app_right
{C : Type u}
[category_theory.category C]
{X Y Z X' Y' Z' : C}
(iX : X ≅ X')
(iY : Y ≅ Y')
(iZ : Z ≅ Z')
{f : X ⟶ Y}
{g : X ⟶ Z}
{f' : X' ⟶ Y'}
{g' : X' ⟶ Z'}
(wf : iX.hom ≫ f' = f ≫ iY.hom)
(wg : iX.hom ≫ g' = g ≫ iZ.hom) :
(category_theory.limits.span_ext iX iY iZ wf wg).app category_theory.limits.walking_span.right = iZ
@[simp]
theorem
category_theory.limits.span_ext_app_one
{C : Type u}
[category_theory.category C]
{X Y Z X' Y' Z' : C}
(iX : X ≅ X')
(iY : Y ≅ Y')
(iZ : Z ≅ Z')
{f : X ⟶ Y}
{g : X ⟶ Z}
{f' : X' ⟶ Y'}
{g' : X' ⟶ Z'}
(wf : iX.hom ≫ f' = f ≫ iY.hom)
(wg : iX.hom ≫ g' = g ≫ iZ.hom) :
(category_theory.limits.span_ext iX iY iZ wf wg).app category_theory.limits.walking_span.zero = iX
@[simp]
theorem
category_theory.limits.span_ext_hom_app_left
{C : Type u}
[category_theory.category C]
{X Y Z X' Y' Z' : C}
(iX : X ≅ X')
(iY : Y ≅ Y')
(iZ : Z ≅ Z')
{f : X ⟶ Y}
{g : X ⟶ Z}
{f' : X' ⟶ Y'}
{g' : X' ⟶ Z'}
(wf : iX.hom ≫ f' = f ≫ iY.hom)
(wg : iX.hom ≫ g' = g ≫ iZ.hom) :
(category_theory.limits.span_ext iX iY iZ wf wg).hom.app category_theory.limits.walking_span.left = iY.hom
@[simp]
theorem
category_theory.limits.span_ext_hom_app_right
{C : Type u}
[category_theory.category C]
{X Y Z X' Y' Z' : C}
(iX : X ≅ X')
(iY : Y ≅ Y')
(iZ : Z ≅ Z')
{f : X ⟶ Y}
{g : X ⟶ Z}
{f' : X' ⟶ Y'}
{g' : X' ⟶ Z'}
(wf : iX.hom ≫ f' = f ≫ iY.hom)
(wg : iX.hom ≫ g' = g ≫ iZ.hom) :
(category_theory.limits.span_ext iX iY iZ wf wg).hom.app category_theory.limits.walking_span.right = iZ.hom
@[simp]
theorem
category_theory.limits.span_ext_hom_app_zero
{C : Type u}
[category_theory.category C]
{X Y Z X' Y' Z' : C}
(iX : X ≅ X')
(iY : Y ≅ Y')
(iZ : Z ≅ Z')
{f : X ⟶ Y}
{g : X ⟶ Z}
{f' : X' ⟶ Y'}
{g' : X' ⟶ Z'}
(wf : iX.hom ≫ f' = f ≫ iY.hom)
(wg : iX.hom ≫ g' = g ≫ iZ.hom) :
(category_theory.limits.span_ext iX iY iZ wf wg).hom.app category_theory.limits.walking_span.zero = iX.hom
@[simp]
theorem
category_theory.limits.span_ext_inv_app_left
{C : Type u}
[category_theory.category C]
{X Y Z X' Y' Z' : C}
(iX : X ≅ X')
(iY : Y ≅ Y')
(iZ : Z ≅ Z')
{f : X ⟶ Y}
{g : X ⟶ Z}
{f' : X' ⟶ Y'}
{g' : X' ⟶ Z'}
(wf : iX.hom ≫ f' = f ≫ iY.hom)
(wg : iX.hom ≫ g' = g ≫ iZ.hom) :
(category_theory.limits.span_ext iX iY iZ wf wg).inv.app category_theory.limits.walking_span.left = iY.inv
@[simp]
theorem
category_theory.limits.span_ext_inv_app_right
{C : Type u}
[category_theory.category C]
{X Y Z X' Y' Z' : C}
(iX : X ≅ X')
(iY : Y ≅ Y')
(iZ : Z ≅ Z')
{f : X ⟶ Y}
{g : X ⟶ Z}
{f' : X' ⟶ Y'}
{g' : X' ⟶ Z'}
(wf : iX.hom ≫ f' = f ≫ iY.hom)
(wg : iX.hom ≫ g' = g ≫ iZ.hom) :
(category_theory.limits.span_ext iX iY iZ wf wg).inv.app category_theory.limits.walking_span.right = iZ.inv
@[simp]
theorem
category_theory.limits.span_ext_inv_app_zero
{C : Type u}
[category_theory.category C]
{X Y Z X' Y' Z' : C}
(iX : X ≅ X')
(iY : Y ≅ Y')
(iZ : Z ≅ Z')
{f : X ⟶ Y}
{g : X ⟶ Z}
{f' : X' ⟶ Y'}
{g' : X' ⟶ Z'}
(wf : iX.hom ≫ f' = f ≫ iY.hom)
(wg : iX.hom ≫ g' = g ≫ iZ.hom) :
(category_theory.limits.span_ext iX iY iZ wf wg).inv.app category_theory.limits.walking_span.zero = iX.inv
@[reducible]
def
category_theory.limits.pullback_cone
{C : Type u}
[category_theory.category C]
{X Y 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.
@[reducible]
def
category_theory.limits.pullback_cone.fst
{C : Type u}
[category_theory.category C]
{X Y Z : C}
{f : X ⟶ Z}
{g : Y ⟶ Z}
(t : category_theory.limits.pullback_cone f g) :
The first projection of a pullback cone.
@[reducible]
def
category_theory.limits.pullback_cone.snd
{C : Type u}
[category_theory.category C]
{X Y Z : C}
{f : X ⟶ Z}
{g : Y ⟶ Z}
(t : category_theory.limits.pullback_cone f g) :
The second projection of a pullback cone.
@[simp]
theorem
category_theory.limits.pullback_cone.π_app_left
{C : Type u}
[category_theory.category C]
{X Y Z : C}
{f : X ⟶ Z}
{g : Y ⟶ Z}
(c : category_theory.limits.pullback_cone f g) :
@[simp]
theorem
category_theory.limits.pullback_cone.π_app_right
{C : Type u}
[category_theory.category C]
{X Y Z : C}
{f : X ⟶ Z}
{g : Y ⟶ Z}
(c : category_theory.limits.pullback_cone f g) :
@[simp]
theorem
category_theory.limits.pullback_cone.condition_one
{C : Type u}
[category_theory.category C]
{X Y Z : C}
{f : X ⟶ Z}
{g : Y ⟶ Z}
(t : category_theory.limits.pullback_cone f g) :
def
category_theory.limits.pullback_cone.is_limit_aux
{C : Type u}
[category_theory.category C]
{X Y Z : C}
{f : X ⟶ Z}
{g : Y ⟶ Z}
(t : category_theory.limits.pullback_cone f g)
(lift : Π (s : category_theory.limits.pullback_cone f g), s.X ⟶ t.X)
(fac_left : ∀ (s : category_theory.limits.pullback_cone f g), lift s ≫ t.fst = s.fst)
(fac_right : ∀ (s : category_theory.limits.pullback_cone f g), lift s ≫ t.snd = s.snd)
(uniq : ∀ (s : category_theory.limits.pullback_cone f g) (m : s.X ⟶ t.X), (∀ (j : category_theory.limits.walking_cospan), 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
def
category_theory.limits.pullback_cone.is_limit_aux'
{C : Type u}
[category_theory.category C]
{X Y Z : C}
{f : X ⟶ Z}
{g : Y ⟶ Z}
(t : category_theory.limits.pullback_cone f g)
(create : Π (s : category_theory.limits.pullback_cone f g), {l // l ≫ t.fst = s.fst ∧ l ≫ t.snd = s.snd ∧ ∀ {m : s.X ⟶ t.X}, m ≫ t.fst = s.fst → m ≫ t.snd = s.snd → 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
- t.is_limit_aux' create = t.is_limit_aux (λ (s : category_theory.limits.pullback_cone f g), (create s).val) _ _ _
def
category_theory.limits.pullback_cone.mk
{C : Type u}
[category_theory.category C]
{X Y Z : C}
{f : X ⟶ Z}
{g : Y ⟶ Z}
{W : C}
(fst : W ⟶ X)
(snd : W ⟶ Y)
(eq : fst ≫ f = 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
- category_theory.limits.pullback_cone.mk fst snd eq = {X := W, π := {app := λ (j : category_theory.limits.walking_cospan), option.cases_on j (fst ≫ f) (λ (j' : category_theory.limits.walking_pair), j'.cases_on fst snd), naturality' := _}}
@[simp]
theorem
category_theory.limits.pullback_cone.mk_X
{C : Type u}
[category_theory.category C]
{X Y Z : C}
{f : X ⟶ Z}
{g : Y ⟶ Z}
{W : C}
(fst : W ⟶ X)
(snd : W ⟶ Y)
(eq : fst ≫ f = snd ≫ g) :
(category_theory.limits.pullback_cone.mk fst snd eq).X = W
@[simp]
theorem
category_theory.limits.pullback_cone.mk_π_app
{C : Type u}
[category_theory.category C]
{X Y Z : C}
{f : X ⟶ Z}
{g : Y ⟶ Z}
{W : C}
(fst : W ⟶ X)
(snd : W ⟶ Y)
(eq : fst ≫ f = snd ≫ g)
(j : category_theory.limits.walking_cospan) :
(category_theory.limits.pullback_cone.mk fst snd eq).π.app j = option.cases_on j (fst ≫ f) (λ (j' : category_theory.limits.walking_pair), j'.cases_on fst snd)
@[simp]
theorem
category_theory.limits.pullback_cone.mk_π_app_left
{C : Type u}
[category_theory.category C]
{X Y Z : C}
{f : X ⟶ Z}
{g : Y ⟶ Z}
{W : C}
(fst : W ⟶ X)
(snd : W ⟶ Y)
(eq : fst ≫ f = snd ≫ g) :
@[simp]
theorem
category_theory.limits.pullback_cone.mk_π_app_right
{C : Type u}
[category_theory.category C]
{X Y Z : C}
{f : X ⟶ Z}
{g : Y ⟶ Z}
{W : C}
(fst : W ⟶ X)
(snd : W ⟶ Y)
(eq : fst ≫ f = snd ≫ g) :
@[simp]
theorem
category_theory.limits.pullback_cone.mk_π_app_one
{C : Type u}
[category_theory.category C]
{X Y Z : C}
{f : X ⟶ Z}
{g : Y ⟶ Z}
{W : C}
(fst : W ⟶ X)
(snd : W ⟶ Y)
(eq : fst ≫ f = snd ≫ g) :
(category_theory.limits.pullback_cone.mk fst snd eq).π.app category_theory.limits.walking_cospan.one = fst ≫ f
@[simp]
theorem
category_theory.limits.pullback_cone.mk_fst
{C : Type u}
[category_theory.category C]
{X Y Z : C}
{f : X ⟶ Z}
{g : Y ⟶ Z}
{W : C}
(fst : W ⟶ X)
(snd : W ⟶ Y)
(eq : fst ≫ f = snd ≫ g) :
(category_theory.limits.pullback_cone.mk fst snd eq).fst = fst
@[simp]
theorem
category_theory.limits.pullback_cone.mk_snd
{C : Type u}
[category_theory.category C]
{X Y Z : C}
{f : X ⟶ Z}
{g : Y ⟶ Z}
{W : C}
(fst : W ⟶ X)
(snd : W ⟶ Y)
(eq : fst ≫ f = snd ≫ g) :
(category_theory.limits.pullback_cone.mk fst snd eq).snd = snd
theorem
category_theory.limits.pullback_cone.condition
{C : Type u}
[category_theory.category C]
{X Y Z : C}
{f : X ⟶ Z}
{g : Y ⟶ Z}
(t : category_theory.limits.pullback_cone f g) :
theorem
category_theory.limits.pullback_cone.condition_assoc
{C : Type u}
[category_theory.category C]
{X Y Z : C}
{f : X ⟶ Z}
{g : Y ⟶ Z}
(t : category_theory.limits.pullback_cone f g)
{X' : C}
(f' : Z ⟶ X') :
theorem
category_theory.limits.pullback_cone.equalizer_ext
{C : Type u}
[category_theory.category C]
{X Y Z : C}
{f : X ⟶ Z}
{g : Y ⟶ Z}
(t : category_theory.limits.pullback_cone f g)
{W : C}
{k l : W ⟶ t.X}
(h₀ : k ≫ t.fst = l ≫ t.fst)
(h₁ : k ≫ t.snd = l ≫ t.snd)
(j : category_theory.limits.walking_cospan) :
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
category_theory.limits.pullback_cone.is_limit.hom_ext
{C : Type u}
[category_theory.category C]
{X Y Z : C}
{f : X ⟶ Z}
{g : Y ⟶ Z}
{t : category_theory.limits.pullback_cone f g}
(ht : category_theory.limits.is_limit t)
{W : C}
{k l : W ⟶ t.X}
(h₀ : k ≫ t.fst = l ≫ t.fst)
(h₁ : k ≫ t.snd = l ≫ t.snd) :
k = l
theorem
category_theory.limits.pullback_cone.mono_snd_of_is_pullback_of_mono
{C : Type u}
[category_theory.category C]
{X Y Z : C}
{f : X ⟶ Z}
{g : Y ⟶ Z}
{t : category_theory.limits.pullback_cone f g}
(ht : category_theory.limits.is_limit t)
[category_theory.mono f] :
theorem
category_theory.limits.pullback_cone.mono_fst_of_is_pullback_of_mono
{C : Type u}
[category_theory.category C]
{X Y Z : C}
{f : X ⟶ Z}
{g : Y ⟶ Z}
{t : category_theory.limits.pullback_cone f g}
(ht : category_theory.limits.is_limit t)
[category_theory.mono g] :
def
category_theory.limits.pullback_cone.ext
{C : Type u}
[category_theory.category C]
{X Y Z : C}
{f : X ⟶ Z}
{g : Y ⟶ Z}
{s t : category_theory.limits.pullback_cone f g}
(i : s.X ≅ t.X)
(w₁ : s.fst = i.hom ≫ t.fst)
(w₂ : s.snd = i.hom ≫ t.snd) :
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
category_theory.limits.pullback_cone.is_limit.lift'
{C : Type u}
[category_theory.category C]
{X Y Z : C}
{f : X ⟶ Z}
{g : Y ⟶ Z}
{t : category_theory.limits.pullback_cone f g}
(ht : category_theory.limits.is_limit t)
{W : C}
(h : W ⟶ X)
(k : W ⟶ Y)
(w : h ≫ f = k ≫ g) :
If t is a limit pullback cone over f and g and h : W ⟶ X and k : W ⟶ Y are such that
h ≫ f = k ≫ g, then we have l : W ⟶ t.X satisfying l ≫ fst t = h and l ≫ snd t = k.
Equations
- category_theory.limits.pullback_cone.is_limit.lift' ht h k w = ⟨ht.lift (category_theory.limits.pullback_cone.mk h k w), _⟩
def
category_theory.limits.pullback_cone.is_limit.mk
{C : Type u}
[category_theory.category C]
{X Y Z : C}
{f : X ⟶ Z}
{g : Y ⟶ Z}
{W : C}
{fst : W ⟶ X}
{snd : W ⟶ Y}
(eq : fst ≫ f = snd ≫ g)
(lift : Π (s : category_theory.limits.pullback_cone f g), s.X ⟶ W)
(fac_left : ∀ (s : category_theory.limits.pullback_cone f g), lift s ≫ fst = s.fst)
(fac_right : ∀ (s : category_theory.limits.pullback_cone f g), lift s ≫ snd = s.snd)
(uniq : ∀ (s : category_theory.limits.pullback_cone f g) (m : s.X ⟶ W), m ≫ fst = s.fst → m ≫ snd = s.snd → m = lift s) :
This is a more convenient formulation to show that a pullback_cone constructed using
pullback_cone.mk is a limit cone.
Equations
- category_theory.limits.pullback_cone.is_limit.mk eq lift fac_left fac_right uniq = (category_theory.limits.pullback_cone.mk fst snd eq).is_limit_aux lift fac_left fac_right _
def
category_theory.limits.pullback_cone.flip_is_limit
{C : Type u}
[category_theory.category C]
{X Y Z : C}
{f : X ⟶ Z}
{g : Y ⟶ Z}
{W : C}
{h : W ⟶ X}
{k : W ⟶ Y}
{comm : h ≫ f = k ≫ g}
(t : category_theory.limits.is_limit (category_theory.limits.pullback_cone.mk k h category_theory.limits.pullback_cone.flip_is_limit._proof_1)) :
The flip of a pullback square is a pullback square.
Equations
- category_theory.limits.pullback_cone.flip_is_limit t = (category_theory.limits.pullback_cone.mk h k comm).is_limit_aux' (λ (s : category_theory.limits.pullback_cone f g), ⟨(category_theory.limits.pullback_cone.is_limit.lift' t s.snd s.fst _).val, _⟩)
def
category_theory.limits.pullback_cone.is_limit_mk_id_id
{C : Type u}
[category_theory.category C]
{X Y : C}
(f : X ⟶ Y)
[category_theory.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
theorem
category_theory.limits.pullback_cone.mono_of_is_limit_mk_id_id
{C : Type u}
[category_theory.category C]
{X Y : C}
(f : X ⟶ Y)
(t : category_theory.limits.is_limit (category_theory.limits.pullback_cone.mk (𝟙 X) (𝟙 X) rfl)) :
f is a mono if the pullback cone (𝟙 X, 𝟙 X) is a limit for the pair (f, f). The converse is
given in pullback_cone.is_id_of_mono.
def
category_theory.limits.pullback_cone.is_limit_of_factors
{C : Type u}
[category_theory.category C]
{W X Y Z : C}
(f : X ⟶ Z)
(g : Y ⟶ Z)
(h : W ⟶ Z)
[category_theory.mono h]
(x : X ⟶ W)
(y : Y ⟶ W)
(hxh : x ≫ h = f)
(hyh : y ≫ h = g)
(s : category_theory.limits.pullback_cone f g)
(hs : category_theory.limits.is_limit 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
- category_theory.limits.pullback_cone.is_limit_of_factors f g h x y hxh hyh s hs = (category_theory.limits.pullback_cone.mk s.fst s.snd _).is_limit_aux' (λ (t : category_theory.limits.pullback_cone x y), ⟨hs.lift (category_theory.limits.pullback_cone.mk t.fst t.snd _), _⟩)
def
category_theory.limits.pullback_cone.is_limit_of_comp_mono
{C : Type u}
[category_theory.category C]
{W X Y Z : C}
(f : X ⟶ W)
(g : Y ⟶ W)
(i : W ⟶ Z)
[category_theory.mono i]
(s : category_theory.limits.pullback_cone f g)
(H : category_theory.limits.is_limit s) :
If W is the pullback of f, g,
it is also the pullback of f ≫ i, g ≫ i for any mono i.
Equations
- category_theory.limits.pullback_cone.is_limit_of_comp_mono f g i s H = (category_theory.limits.pullback_cone.mk s.fst s.snd _).is_limit_aux' (λ (s_1 : category_theory.limits.pullback_cone (f ≫ i) (g ≫ i)), (category_theory.limits.pullback_cone.is_limit.lift' H s_1.fst s_1.snd _).cases_on (λ (l : s_1.X ⟶ s.X) (property : l ≫ s.fst = s_1.fst ∧ l ≫ s.snd = s_1.snd), property.dcases_on (λ (h₁ : l ≫ s.fst = s_1.fst) (h₂ : l ≫ s.snd = s_1.snd), ⟨l, _⟩)))
@[reducible]
def
category_theory.limits.pushout_cocone
{C : Type u}
[category_theory.category C]
{X Y 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.
@[reducible]
def
category_theory.limits.pushout_cocone.inl
{C : Type u}
[category_theory.category C]
{X Y Z : C}
{f : X ⟶ Y}
{g : X ⟶ Z}
(t : category_theory.limits.pushout_cocone f g) :
The first inclusion of a pushout cocone.
@[reducible]
def
category_theory.limits.pushout_cocone.inr
{C : Type u}
[category_theory.category C]
{X Y Z : C}
{f : X ⟶ Y}
{g : X ⟶ Z}
(t : category_theory.limits.pushout_cocone f g) :
The second inclusion of a pushout cocone.
@[simp]
theorem
category_theory.limits.pushout_cocone.ι_app_left
{C : Type u}
[category_theory.category C]
{X Y Z : C}
{f : X ⟶ Y}
{g : X ⟶ Z}
(c : category_theory.limits.pushout_cocone f g) :
@[simp]
theorem
category_theory.limits.pushout_cocone.ι_app_right
{C : Type u}
[category_theory.category C]
{X Y Z : C}
{f : X ⟶ Y}
{g : X ⟶ Z}
(c : category_theory.limits.pushout_cocone f g) :
@[simp]
theorem
category_theory.limits.pushout_cocone.condition_zero
{C : Type u}
[category_theory.category C]
{X Y Z : C}
{f : X ⟶ Y}
{g : X ⟶ Z}
(t : category_theory.limits.pushout_cocone f g) :
def
category_theory.limits.pushout_cocone.is_colimit_aux
{C : Type u}
[category_theory.category C]
{X Y Z : C}
{f : X ⟶ Y}
{g : X ⟶ Z}
(t : category_theory.limits.pushout_cocone f g)
(desc : Π (s : category_theory.limits.pushout_cocone f g), t.X ⟶ s.X)
(fac_left : ∀ (s : category_theory.limits.pushout_cocone f g), t.inl ≫ desc s = s.inl)
(fac_right : ∀ (s : category_theory.limits.pushout_cocone f g), t.inr ≫ desc s = s.inr)
(uniq : ∀ (s : category_theory.limits.pushout_cocone f g) (m : t.X ⟶ s.X), (∀ (j : category_theory.limits.walking_span), 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
def
category_theory.limits.pushout_cocone.is_colimit_aux'
{C : Type u}
[category_theory.category C]
{X Y Z : C}
{f : X ⟶ Y}
{g : X ⟶ Z}
(t : category_theory.limits.pushout_cocone f g)
(create : Π (s : category_theory.limits.pushout_cocone f g), {l // t.inl ≫ l = s.inl ∧ t.inr ≫ l = s.inr ∧ ∀ {m : t.X ⟶ s.X}, t.inl ≫ m = s.inl → t.inr ≫ m = s.inr → 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
- t.is_colimit_aux' create = t.is_colimit_aux (λ (s : category_theory.limits.pushout_cocone f g), (create s).val) _ _ _
@[simp]
theorem
category_theory.limits.pushout_cocone.mk_ι_app
{C : Type u}
[category_theory.category C]
{X Y Z : C}
{f : X ⟶ Y}
{g : X ⟶ Z}
{W : C}
(inl : Y ⟶ W)
(inr : Z ⟶ W)
(eq : f ≫ inl = g ≫ inr)
(j : category_theory.limits.walking_span) :
(category_theory.limits.pushout_cocone.mk inl inr eq).ι.app j = option.cases_on j (f ≫ inl) (λ (j' : category_theory.limits.walking_pair), j'.cases_on inl inr)
def
category_theory.limits.pushout_cocone.mk
{C : Type u}
[category_theory.category C]
{X Y Z : C}
{f : X ⟶ Y}
{g : X ⟶ Z}
{W : C}
(inl : Y ⟶ W)
(inr : Z ⟶ W)
(eq : f ≫ inl = 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
- category_theory.limits.pushout_cocone.mk inl inr eq = {X := W, ι := {app := λ (j : category_theory.limits.walking_span), option.cases_on j (f ≫ inl) (λ (j' : category_theory.limits.walking_pair), j'.cases_on inl inr), naturality' := _}}
@[simp]
theorem
category_theory.limits.pushout_cocone.mk_X
{C : Type u}
[category_theory.category C]
{X Y Z : C}
{f : X ⟶ Y}
{g : X ⟶ Z}
{W : C}
(inl : Y ⟶ W)
(inr : Z ⟶ W)
(eq : f ≫ inl = g ≫ inr) :
(category_theory.limits.pushout_cocone.mk inl inr eq).X = W
@[simp]
theorem
category_theory.limits.pushout_cocone.mk_ι_app_left
{C : Type u}
[category_theory.category C]
{X Y Z : C}
{f : X ⟶ Y}
{g : X ⟶ Z}
{W : C}
(inl : Y ⟶ W)
(inr : Z ⟶ W)
(eq : f ≫ inl = g ≫ inr) :
@[simp]
theorem
category_theory.limits.pushout_cocone.mk_ι_app_right
{C : Type u}
[category_theory.category C]
{X Y Z : C}
{f : X ⟶ Y}
{g : X ⟶ Z}
{W : C}
(inl : Y ⟶ W)
(inr : Z ⟶ W)
(eq : f ≫ inl = g ≫ inr) :
@[simp]
theorem
category_theory.limits.pushout_cocone.mk_ι_app_zero
{C : Type u}
[category_theory.category C]
{X Y Z : C}
{f : X ⟶ Y}
{g : X ⟶ Z}
{W : C}
(inl : Y ⟶ W)
(inr : Z ⟶ W)
(eq : f ≫ inl = g ≫ inr) :
(category_theory.limits.pushout_cocone.mk inl inr eq).ι.app category_theory.limits.walking_span.zero = f ≫ inl
@[simp]
theorem
category_theory.limits.pushout_cocone.mk_inl
{C : Type u}
[category_theory.category C]
{X Y Z : C}
{f : X ⟶ Y}
{g : X ⟶ Z}
{W : C}
(inl : Y ⟶ W)
(inr : Z ⟶ W)
(eq : f ≫ inl = g ≫ inr) :
(category_theory.limits.pushout_cocone.mk inl inr eq).inl = inl
@[simp]
theorem
category_theory.limits.pushout_cocone.mk_inr
{C : Type u}
[category_theory.category C]
{X Y Z : C}
{f : X ⟶ Y}
{g : X ⟶ Z}
{W : C}
(inl : Y ⟶ W)
(inr : Z ⟶ W)
(eq : f ≫ inl = g ≫ inr) :
(category_theory.limits.pushout_cocone.mk inl inr eq).inr = inr
theorem
category_theory.limits.pushout_cocone.condition
{C : Type u}
[category_theory.category C]
{X Y Z : C}
{f : X ⟶ Y}
{g : X ⟶ Z}
(t : category_theory.limits.pushout_cocone f g) :
theorem
category_theory.limits.pushout_cocone.coequalizer_ext
{C : Type u}
[category_theory.category C]
{X Y Z : C}
{f : X ⟶ Y}
{g : X ⟶ Z}
(t : category_theory.limits.pushout_cocone f g)
{W : C}
{k l : t.X ⟶ W}
(h₀ : t.inl ≫ k = t.inl ≫ l)
(h₁ : t.inr ≫ k = t.inr ≫ l)
(j : category_theory.limits.walking_span) :
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
category_theory.limits.pushout_cocone.is_colimit.hom_ext
{C : Type u}
[category_theory.category C]
{X Y Z : C}
{f : X ⟶ Y}
{g : X ⟶ Z}
{t : category_theory.limits.pushout_cocone f g}
(ht : category_theory.limits.is_colimit t)
{W : C}
{k l : t.X ⟶ W}
(h₀ : t.inl ≫ k = t.inl ≫ l)
(h₁ : t.inr ≫ k = t.inr ≫ l) :
k = l
def
category_theory.limits.pushout_cocone.is_colimit.desc'
{C : Type u}
[category_theory.category C]
{X Y Z : C}
{f : X ⟶ Y}
{g : X ⟶ Z}
{t : category_theory.limits.pushout_cocone f g}
(ht : category_theory.limits.is_colimit t)
{W : C}
(h : Y ⟶ W)
(k : Z ⟶ W)
(w : f ≫ h = g ≫ k) :
If t is a colimit pushout cocone over f and g and h : Y ⟶ W and k : Z ⟶ W are
morphisms satisfying f ≫ h = g ≫ k, then we have a factorization l : t.X ⟶ W such that
inl t ≫ l = h and inr t ≫ l = k.
Equations
- category_theory.limits.pushout_cocone.is_colimit.desc' ht h k w = ⟨ht.desc (category_theory.limits.pushout_cocone.mk h k w), _⟩
theorem
category_theory.limits.pushout_cocone.epi_inr_of_is_pushout_of_epi
{C : Type u}
[category_theory.category C]
{X Y Z : C}
{f : X ⟶ Y}
{g : X ⟶ Z}
{t : category_theory.limits.pushout_cocone f g}
(ht : category_theory.limits.is_colimit t)
[category_theory.epi f] :
theorem
category_theory.limits.pushout_cocone.epi_inl_of_is_pushout_of_epi
{C : Type u}
[category_theory.category C]
{X Y Z : C}
{f : X ⟶ Y}
{g : X ⟶ Z}
{t : category_theory.limits.pushout_cocone f g}
(ht : category_theory.limits.is_colimit t)
[category_theory.epi g] :
def
category_theory.limits.pushout_cocone.ext
{C : Type u}
[category_theory.category C]
{X Y Z : C}
{f : X ⟶ Y}
{g : X ⟶ Z}
{s t : category_theory.limits.pushout_cocone f g}
(i : s.X ≅ t.X)
(w₁ : s.inl ≫ i.hom = t.inl)
(w₂ : s.inr ≫ i.hom = t.inr) :
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
category_theory.limits.pushout_cocone.is_colimit.mk
{C : Type u}
[category_theory.category C]
{X Y Z : C}
{f : X ⟶ Y}
{g : X ⟶ Z}
{W : C}
{inl : Y ⟶ W}
{inr : Z ⟶ W}
(eq : f ≫ inl = g ≫ inr)
(desc : Π (s : category_theory.limits.pushout_cocone f g), W ⟶ s.X)
(fac_left : ∀ (s : category_theory.limits.pushout_cocone f g), inl ≫ desc s = s.inl)
(fac_right : ∀ (s : category_theory.limits.pushout_cocone f g), inr ≫ desc s = s.inr)
(uniq : ∀ (s : category_theory.limits.pushout_cocone f g) (m : W ⟶ s.X), inl ≫ m = s.inl → inr ≫ m = s.inr → m = desc s) :
This is a more convenient formulation to show that a pushout_cocone constructed using
pushout_cocone.mk is a colimit cocone.
Equations
- category_theory.limits.pushout_cocone.is_colimit.mk eq desc fac_left fac_right uniq = (category_theory.limits.pushout_cocone.mk inl inr eq).is_colimit_aux desc fac_left fac_right _
def
category_theory.limits.pushout_cocone.flip_is_colimit
{C : Type u}
[category_theory.category C]
{X Y Z : C}
{f : X ⟶ Y}
{g : X ⟶ Z}
{W : C}
{h : Y ⟶ W}
{k : Z ⟶ W}
{comm : f ≫ h = g ≫ k}
(t : category_theory.limits.is_colimit (category_theory.limits.pushout_cocone.mk k h category_theory.limits.pushout_cocone.flip_is_colimit._proof_1)) :
The flip of a pushout square is a pushout square.
Equations
def
category_theory.limits.pushout_cocone.is_colimit_mk_id_id
{C : Type u}
[category_theory.category C]
{X Y : C}
(f : X ⟶ Y)
[category_theory.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_is_colimit_mk_id_id.
Equations
theorem
category_theory.limits.pushout_cocone.epi_of_is_colimit_mk_id_id
{C : Type u}
[category_theory.category C]
{X Y : C}
(f : X ⟶ Y)
(t : category_theory.limits.is_colimit (category_theory.limits.pushout_cocone.mk (𝟙 Y) (𝟙 Y) rfl)) :
f is an epi if the pushout cocone (𝟙 X, 𝟙 X) is a colimit for the pair (f, f).
The converse is given in pushout_cocone.is_colimit_mk_id_id.
def
category_theory.limits.pushout_cocone.is_colimit_of_factors
{C : Type u}
[category_theory.category C]
{W X Y Z : C}
(f : X ⟶ Y)
(g : X ⟶ Z)
(h : X ⟶ W)
[category_theory.epi h]
(x : W ⟶ Y)
(y : W ⟶ Z)
(hhx : h ≫ x = f)
(hhy : h ≫ y = g)
(s : category_theory.limits.pushout_cocone f g)
(hs : category_theory.limits.is_colimit 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
- category_theory.limits.pushout_cocone.is_colimit_of_factors f g h x y hhx hhy s hs = (category_theory.limits.pushout_cocone.mk s.inl s.inr _).is_colimit_aux' (λ (t : category_theory.limits.pushout_cocone x y), ⟨hs.desc (category_theory.limits.pushout_cocone.mk t.inl t.inr _), _⟩)
def
category_theory.limits.pushout_cocone.is_colimit_of_epi_comp
{C : Type u}
[category_theory.category C]
{W X Y Z : C}
(f : X ⟶ Y)
(g : X ⟶ Z)
(h : W ⟶ X)
[category_theory.epi h]
(s : category_theory.limits.pushout_cocone f g)
(H : category_theory.limits.is_colimit s) :
If W is the pushout of f, g,
it is also the pushout of h ≫ f, h ≫ g for any epi h.
Equations
- category_theory.limits.pushout_cocone.is_colimit_of_epi_comp f g h s H = (category_theory.limits.pushout_cocone.mk s.inl s.inr _).is_colimit_aux' (λ (s_1 : category_theory.limits.pushout_cocone (h ≫ f) (h ≫ g)), (category_theory.limits.pushout_cocone.is_colimit.desc' H s_1.inl s_1.inr _).cases_on (λ (l : s.X ⟶ s_1.X) (property : s.inl ≫ l = s_1.inl ∧ s.inr ≫ l = s_1.inr), property.dcases_on (λ (h₁ : s.inl ≫ l = s_1.inl) (h₂ : s.inr ≫ l = s_1.inr), ⟨l, _⟩)))
def
category_theory.limits.cone.of_pullback_cone
{C : Type u}
[category_theory.category C]
{F : category_theory.limits.walking_cospan ⥤ C}
(t : category_theory.limits.pullback_cone (F.map category_theory.limits.walking_cospan.hom.inl) (F.map category_theory.limits.walking_cospan.hom.inr)) :
This is a helper construction that can be useful when verifying that a category has all
pullbacks. Given F : walking_cospan ⥤ 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 has_pullbacks_of_has_limit_cospan,
which you may find to be an easier way of achieving your goal.
Equations
- category_theory.limits.cone.of_pullback_cone t = {X := t.X, π := t.π ≫ (category_theory.limits.diagram_iso_cospan F).inv}
@[simp]
@[simp]
@[simp]
@[simp]
def
category_theory.limits.cocone.of_pushout_cocone
{C : Type u}
[category_theory.category C]
{F : category_theory.limits.walking_span ⥤ C}
(t : category_theory.limits.pushout_cocone (F.map category_theory.limits.walking_span.hom.fst) (F.map category_theory.limits.walking_span.hom.snd)) :
This is a helper construction that can be useful when verifying that a category has all
pushout. Given F : walking_span ⥤ C, which is really the same as
span (F.map fst) (F.mal 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 has_pushouts_of_has_colimit_span, which
you may find to be an easiery way of achieving your goal.
Equations
- category_theory.limits.cocone.of_pushout_cocone t = {X := t.X, ι := (category_theory.limits.diagram_iso_span F).hom ≫ t.ι}
def
category_theory.limits.pullback_cone.of_cone
{C : Type u}
[category_theory.category C]
{F : category_theory.limits.walking_cospan ⥤ C}
(t : category_theory.limits.cone F) :
Given F : walking_cospan ⥤ 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
- category_theory.limits.pullback_cone.of_cone t = {X := t.X, π := t.π ≫ (category_theory.limits.diagram_iso_cospan F).hom}
@[simp]
theorem
category_theory.limits.pullback_cone.of_cone_π
{C : Type u}
[category_theory.category C]
{F : category_theory.limits.walking_cospan ⥤ C}
(t : category_theory.limits.cone F) :
@[simp]
theorem
category_theory.limits.pullback_cone.of_cone_X
{C : Type u}
[category_theory.category C]
{F : category_theory.limits.walking_cospan ⥤ C}
(t : category_theory.limits.cone F) :
@[simp]
theorem
category_theory.limits.pullback_cone.iso_mk_hom_hom
{C : Type u}
[category_theory.category C]
{F : category_theory.limits.walking_cospan ⥤ C}
(t : category_theory.limits.cone F) :
@[simp]
theorem
category_theory.limits.pullback_cone.iso_mk_inv_hom
{C : Type u}
[category_theory.category C]
{F : category_theory.limits.walking_cospan ⥤ C}
(t : category_theory.limits.cone F) :
def
category_theory.limits.pullback_cone.iso_mk
{C : Type u}
[category_theory.category C]
{F : category_theory.limits.walking_cospan ⥤ C}
(t : category_theory.limits.cone F) :
A diagram walking_cospan ⥤ C is isomorphic to some pullback_cone.mk after
composing with diagram_iso_cospan.
@[simp]
theorem
category_theory.limits.pushout_cocone.of_cocone_ι
{C : Type u}
[category_theory.category C]
{F : category_theory.limits.walking_span ⥤ C}
(t : category_theory.limits.cocone F) :
def
category_theory.limits.pushout_cocone.of_cocone
{C : Type u}
[category_theory.category C]
{F : category_theory.limits.walking_span ⥤ C}
(t : category_theory.limits.cocone F) :
Given F : walking_span ⥤ 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
- category_theory.limits.pushout_cocone.of_cocone t = {X := t.X, ι := (category_theory.limits.diagram_iso_span F).inv ≫ t.ι}
@[simp]
theorem
category_theory.limits.pushout_cocone.of_cocone_X
{C : Type u}
[category_theory.category C]
{F : category_theory.limits.walking_span ⥤ C}
(t : category_theory.limits.cocone F) :
def
category_theory.limits.pushout_cocone.iso_mk
{C : Type u}
[category_theory.category C]
{F : category_theory.limits.walking_span ⥤ C}
(t : category_theory.limits.cocone F) :
A diagram walking_span ⥤ C is isomorphic to some pushout_cocone.mk after composing with
diagram_iso_span.
@[simp]
theorem
category_theory.limits.pushout_cocone.iso_mk_inv_hom
{C : Type u}
[category_theory.category C]
{F : category_theory.limits.walking_span ⥤ C}
(t : category_theory.limits.cocone F) :
@[simp]
theorem
category_theory.limits.pushout_cocone.iso_mk_hom_hom
{C : Type u}
[category_theory.category C]
{F : category_theory.limits.walking_span ⥤ C}
(t : category_theory.limits.cocone F) :
@[reducible]
def
category_theory.limits.has_pullback
{C : Type u}
[category_theory.category C]
{X Y Z : C}
(f : X ⟶ Z)
(g : Y ⟶ Z) :
Prop
has_pullback f g represents a particular choice of limiting cone
for the pair of morphisms f : X ⟶ Z and g : Y ⟶ Z.
@[reducible]
def
category_theory.limits.has_pushout
{C : Type u}
[category_theory.category C]
{X Y Z : C}
(f : X ⟶ Y)
(g : X ⟶ Z) :
Prop
has_pushout f g represents a particular choice of colimiting cocone
for the pair of morphisms f : X ⟶ Y and g : X ⟶ Z.
@[reducible]
noncomputable
def
category_theory.limits.pullback
{C : Type u}
[category_theory.category C]
{X Y Z : C}
(f : X ⟶ Z)
(g : Y ⟶ Z)
[category_theory.limits.has_pullback f g] :
C
pullback f g computes the pullback of a pair of morphisms with the same target.
@[reducible]
noncomputable
def
category_theory.limits.pushout
{C : Type u}
[category_theory.category C]
{X Y Z : C}
(f : X ⟶ Y)
(g : X ⟶ Z)
[category_theory.limits.has_pushout f g] :
C
pushout f g computes the pushout of a pair of morphisms with the same source.
@[reducible]
noncomputable
def
category_theory.limits.pullback.fst
{C : Type u}
[category_theory.category C]
{X Y Z : C}
{f : X ⟶ Z}
{g : Y ⟶ Z}
[category_theory.limits.has_pullback f g] :
The first projection of the pullback of f and g.
@[reducible]
noncomputable
def
category_theory.limits.pullback.snd
{C : Type u}
[category_theory.category C]
{X Y Z : C}
{f : X ⟶ Z}
{g : Y ⟶ Z}
[category_theory.limits.has_pullback f g] :
The second projection of the pullback of f and g.
@[reducible]
noncomputable
def
category_theory.limits.pushout.inl
{C : Type u}
[category_theory.category C]
{X Y Z : C}
{f : X ⟶ Y}
{g : X ⟶ Z}
[category_theory.limits.has_pushout f g] :
The first inclusion into the pushout of f and g.
@[reducible]
noncomputable
def
category_theory.limits.pushout.inr
{C : Type u}
[category_theory.category C]
{X Y Z : C}
{f : X ⟶ Y}
{g : X ⟶ Z}
[category_theory.limits.has_pushout f g] :
The second inclusion into the pushout of f and g.
@[reducible]
noncomputable
def
category_theory.limits.pullback.lift
{C : Type u}
[category_theory.category C]
{W X Y Z : C}
{f : X ⟶ Z}
{g : Y ⟶ Z}
[category_theory.limits.has_pullback f g]
(h : W ⟶ X)
(k : W ⟶ Y)
(w : h ≫ f = 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.
@[reducible]
noncomputable
def
category_theory.limits.pushout.desc
{C : Type u}
[category_theory.category C]
{W X Y Z : C}
{f : X ⟶ Y}
{g : X ⟶ Z}
[category_theory.limits.has_pushout f g]
(h : Y ⟶ W)
(k : Z ⟶ W)
(w : f ≫ h = 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
category_theory.limits.pullback_cone.fst_colimit_cocone
{C : Type u}
[category_theory.category C]
{X Y Z : C}
(f : X ⟶ Z)
(g : Y ⟶ Z)
[category_theory.limits.has_limit (category_theory.limits.cospan f g)] :
@[simp]
theorem
category_theory.limits.pullback_cone.snd_colimit_cocone
{C : Type u}
[category_theory.category C]
{X Y Z : C}
(f : X ⟶ Z)
(g : Y ⟶ Z)
[category_theory.limits.has_limit (category_theory.limits.cospan f g)] :
@[simp]
theorem
category_theory.limits.pushout_cocone.inl_colimit_cocone
{C : Type u}
[category_theory.category C]
{X Y Z : C}
(f : Z ⟶ X)
(g : Z ⟶ Y)
[category_theory.limits.has_colimit (category_theory.limits.span f g)] :
@[simp]
theorem
category_theory.limits.pushout_cocone.inr_colimit_cocone
{C : Type u}
[category_theory.category C]
{X Y Z : C}
(f : Z ⟶ X)
(g : Z ⟶ Y)
[category_theory.limits.has_colimit (category_theory.limits.span f g)] :
@[simp]
theorem
category_theory.limits.pullback.lift_fst_assoc
{C : Type u}
[category_theory.category C]
{W X Y Z : C}
{f : X ⟶ Z}
{g : Y ⟶ Z}
[category_theory.limits.has_pullback f g]
(h : W ⟶ X)
(k : W ⟶ Y)
(w : h ≫ f = k ≫ g)
{X' : C}
(f' : X ⟶ X') :
category_theory.limits.pullback.lift h k w ≫ category_theory.limits.pullback.fst ≫ f' = h ≫ f'
@[simp]
theorem
category_theory.limits.pullback.lift_fst
{C : Type u}
[category_theory.category C]
{W X Y Z : C}
{f : X ⟶ Z}
{g : Y ⟶ Z}
[category_theory.limits.has_pullback f g]
(h : W ⟶ X)
(k : W ⟶ Y)
(w : h ≫ f = k ≫ g) :
@[simp]
theorem
category_theory.limits.pullback.lift_snd
{C : Type u}
[category_theory.category C]
{W X Y Z : C}
{f : X ⟶ Z}
{g : Y ⟶ Z}
[category_theory.limits.has_pullback f g]
(h : W ⟶ X)
(k : W ⟶ Y)
(w : h ≫ f = k ≫ g) :
@[simp]
theorem
category_theory.limits.pullback.lift_snd_assoc
{C : Type u}
[category_theory.category C]
{W X Y Z : C}
{f : X ⟶ Z}
{g : Y ⟶ Z}
[category_theory.limits.has_pullback f g]
(h : W ⟶ X)
(k : W ⟶ Y)
(w : h ≫ f = k ≫ g)
{X' : C}
(f' : Y ⟶ X') :
category_theory.limits.pullback.lift h k w ≫ category_theory.limits.pullback.snd ≫ f' = k ≫ f'
@[simp]
theorem
category_theory.limits.pushout.inl_desc_assoc
{C : Type u}
[category_theory.category C]
{W X Y Z : C}
{f : X ⟶ Y}
{g : X ⟶ Z}
[category_theory.limits.has_pushout f g]
(h : Y ⟶ W)
(k : Z ⟶ W)
(w : f ≫ h = g ≫ k)
{X' : C}
(f' : W ⟶ X') :
category_theory.limits.pushout.inl ≫ category_theory.limits.pushout.desc h k w ≫ f' = h ≫ f'
@[simp]
theorem
category_theory.limits.pushout.inl_desc
{C : Type u}
[category_theory.category C]
{W X Y Z : C}
{f : X ⟶ Y}
{g : X ⟶ Z}
[category_theory.limits.has_pushout f g]
(h : Y ⟶ W)
(k : Z ⟶ W)
(w : f ≫ h = g ≫ k) :
@[simp]
theorem
category_theory.limits.pushout.inr_desc_assoc
{C : Type u}
[category_theory.category C]
{W X Y Z : C}
{f : X ⟶ Y}
{g : X ⟶ Z}
[category_theory.limits.has_pushout f g]
(h : Y ⟶ W)
(k : Z ⟶ W)
(w : f ≫ h = g ≫ k)
{X' : C}
(f' : W ⟶ X') :
category_theory.limits.pushout.inr ≫ category_theory.limits.pushout.desc h k w ≫ f' = k ≫ f'
@[simp]
theorem
category_theory.limits.pushout.inr_desc
{C : Type u}
[category_theory.category C]
{W X Y Z : C}
{f : X ⟶ Y}
{g : X ⟶ Z}
[category_theory.limits.has_pushout f g]
(h : Y ⟶ W)
(k : Z ⟶ W)
(w : f ≫ h = g ≫ k) :
noncomputable
def
category_theory.limits.pullback.lift'
{C : Type u}
[category_theory.category C]
{W X Y Z : C}
{f : X ⟶ Z}
{g : Y ⟶ Z}
[category_theory.limits.has_pullback f g]
(h : W ⟶ X)
(k : W ⟶ Y)
(w : h ≫ f = k ≫ g) :
{l // l ≫ category_theory.limits.pullback.fst = h ∧ l ≫ category_theory.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
noncomputable
def
category_theory.limits.pullback.desc'
{C : Type u}
[category_theory.category C]
{W X Y Z : C}
{f : X ⟶ Y}
{g : X ⟶ Z}
[category_theory.limits.has_pushout f g]
(h : Y ⟶ W)
(k : Z ⟶ W)
(w : f ≫ h = g ≫ k) :
{l // category_theory.limits.pushout.inl ≫ l = h ∧ category_theory.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
theorem
category_theory.limits.pullback.condition
{C : Type u}
[category_theory.category C]
{X Y Z : C}
{f : X ⟶ Z}
{g : Y ⟶ Z}
[category_theory.limits.has_pullback f g] :
theorem
category_theory.limits.pullback.condition_assoc
{C : Type u}
[category_theory.category C]
{X Y Z : C}
{f : X ⟶ Z}
{g : Y ⟶ Z}
[category_theory.limits.has_pullback f g]
{X' : C}
(f' : Z ⟶ X') :
theorem
category_theory.limits.pushout.condition
{C : Type u}
[category_theory.category C]
{X Y Z : C}
{f : X ⟶ Y}
{g : X ⟶ Z}
[category_theory.limits.has_pushout f g] :
theorem
category_theory.limits.pushout.condition_assoc
{C : Type u}
[category_theory.category C]
{X Y Z : C}
{f : X ⟶ Y}
{g : X ⟶ Z}
[category_theory.limits.has_pushout f g]
{X' : C}
(f' : category_theory.limits.pushout f g ⟶ X') :
@[reducible]
noncomputable
def
category_theory.limits.pullback.map
{C : Type u}
[category_theory.category C]
{W X Y Z S T : C}
(f₁ : W ⟶ S)
(f₂ : X ⟶ S)
[category_theory.limits.has_pullback f₁ f₂]
(g₁ : Y ⟶ T)
(g₂ : Z ⟶ T)
[category_theory.limits.has_pullback g₁ g₂]
(i₁ : W ⟶ Y)
(i₂ : X ⟶ Z)
(i₃ : S ⟶ T)
(eq₁ : f₁ ≫ i₃ = i₁ ≫ g₁)
(eq₂ : f₂ ≫ i₃ = i₂ ≫ g₂) :
Given such a diagram, then there is a natural morphism W ×ₛ X ⟶ Y ×ₜ Z.
W ⟶ Y
↘ ↘
S ⟶ T
↗ ↗
X ⟶ Z
@[reducible]
noncomputable
def
category_theory.limits.pullback.map_desc
{C : Type u}
[category_theory.category C]
{X Y S T : C}
(f : X ⟶ S)
(g : Y ⟶ S)
(i : S ⟶ T)
[category_theory.limits.has_pullback f g]
[category_theory.limits.has_pullback (f ≫ i) (g ≫ i)] :
category_theory.limits.pullback f g ⟶ category_theory.limits.pullback (f ≫ i) (g ≫ i)
The canonical map X ×ₛ Y ⟶ X ×ₜ Y given S ⟶ T.
@[reducible]
noncomputable
def
category_theory.limits.pushout.map
{C : Type u}
[category_theory.category C]
{W X Y Z S T : C}
(f₁ : S ⟶ W)
(f₂ : S ⟶ X)
[category_theory.limits.has_pushout f₁ f₂]
(g₁ : T ⟶ Y)
(g₂ : T ⟶ Z)
[category_theory.limits.has_pushout g₁ g₂]
(i₁ : W ⟶ Y)
(i₂ : X ⟶ Z)
(i₃ : S ⟶ T)
(eq₁ : f₁ ≫ i₁ = i₃ ≫ g₁)
(eq₂ : f₂ ≫ i₂ = i₃ ≫ g₂) :
Given such a diagram, then there is a natural morphism W ⨿ₛ X ⟶ Y ⨿ₜ Z.
W ⟶ Y
↗ ↗
S ⟶ T
↘ ↘
X ⟶ Z
@[reducible]
noncomputable
def
category_theory.limits.pushout.map_lift
{C : Type u}
[category_theory.category C]
{X Y S T : C}
(f : T ⟶ X)
(g : T ⟶ Y)
(i : S ⟶ T)
[category_theory.limits.has_pushout f g]
[category_theory.limits.has_pushout (i ≫ f) (i ≫ g)] :
category_theory.limits.pushout (i ≫ f) (i ≫ g) ⟶ category_theory.limits.pushout f g
The canonical map X ⨿ₛ Y ⟶ X ⨿ₜ Y given S ⟶ T.
@[ext]
theorem
category_theory.limits.pullback.hom_ext
{C : Type u}
[category_theory.category C]
{X Y Z : C}
{f : X ⟶ Z}
{g : Y ⟶ Z}
[category_theory.limits.has_pullback f g]
{W : C}
{k l : W ⟶ category_theory.limits.pullback f g}
(h₀ : k ≫ category_theory.limits.pullback.fst = l ≫ category_theory.limits.pullback.fst)
(h₁ : k ≫ category_theory.limits.pullback.snd = l ≫ category_theory.limits.pullback.snd) :
k = l
Two morphisms into a pullback are equal if their compositions with the pullback morphisms are equal
noncomputable
def
category_theory.limits.pullback_is_pullback
{C : Type u}
[category_theory.category C]
{X Y Z : C}
(f : X ⟶ Z)
(g : Y ⟶ Z)
[category_theory.limits.has_pullback f g] :
The pullback cone built from the pullback projections is a pullback.
@[protected, instance]
def
category_theory.limits.pullback.fst_of_mono
{C : Type u}
[category_theory.category C]
{X Y Z : C}
{f : X ⟶ Z}
{g : Y ⟶ Z}
[category_theory.limits.has_pullback f g]
[category_theory.mono g] :
The pullback of a monomorphism is a monomorphism
@[protected, instance]
def
category_theory.limits.pullback.snd_of_mono
{C : Type u}
[category_theory.category C]
{X Y Z : C}
{f : X ⟶ Z}
{g : Y ⟶ Z}
[category_theory.limits.has_pullback f g]
[category_theory.mono f] :
The pullback of a monomorphism is a monomorphism
@[protected, instance]
def
category_theory.limits.mono_pullback_to_prod
{C : Type u_1}
[category_theory.category C]
{X Y Z : C}
(f : X ⟶ Z)
(g : Y ⟶ Z)
[category_theory.limits.has_pullback f g]
[category_theory.limits.has_binary_product X Y] :
The map X ×[Z] Y ⟶ X × Y is mono.
@[ext]
theorem
category_theory.limits.pushout.hom_ext
{C : Type u}
[category_theory.category C]
{X Y Z : C}
{f : X ⟶ Y}
{g : X ⟶ Z}
[category_theory.limits.has_pushout f g]
{W : C}
{k l : category_theory.limits.pushout f g ⟶ W}
(h₀ : category_theory.limits.pushout.inl ≫ k = category_theory.limits.pushout.inl ≫ l)
(h₁ : category_theory.limits.pushout.inr ≫ k = category_theory.limits.pushout.inr ≫ l) :
k = l
Two morphisms out of a pushout are equal if their compositions with the pushout morphisms are equal
noncomputable
def
category_theory.limits.pushout_is_pushout
{C : Type u}
[category_theory.category C]
{X Y Z : C}
(f : X ⟶ Y)
(g : X ⟶ Z)
[category_theory.limits.has_pushout f g] :
The pushout cocone built from the pushout coprojections is a pushout.
@[protected, instance]
def
category_theory.limits.pushout.inl_of_epi
{C : Type u}
[category_theory.category C]
{X Y Z : C}
{f : X ⟶ Y}
{g : X ⟶ Z}
[category_theory.limits.has_pushout f g]
[category_theory.epi g] :
The pushout of an epimorphism is an epimorphism
@[protected, instance]
def
category_theory.limits.pushout.inr_of_epi
{C : Type u}
[category_theory.category C]
{X Y Z : C}
{f : X ⟶ Y}
{g : X ⟶ Z}
[category_theory.limits.has_pushout f g]
[category_theory.epi f] :
The pushout of an epimorphism is an epimorphism
@[protected, instance]
def
category_theory.limits.epi_coprod_to_pushout
{C : Type u_1}
[category_theory.category C]
{X Y Z : C}
(f : X ⟶ Y)
(g : X ⟶ Z)
[category_theory.limits.has_pushout f g]
[category_theory.limits.has_binary_coproduct Y Z] :
The map X ⨿ Y ⟶ X ⨿[Z] Y is epi.
@[protected, instance]
def
category_theory.limits.pullback.map_is_iso
{C : Type u}
[category_theory.category C]
{W X Y Z S T : C}
(f₁ : W ⟶ S)
(f₂ : X ⟶ S)
[category_theory.limits.has_pullback f₁ f₂]
(g₁ : Y ⟶ T)
(g₂ : Z ⟶ T)
[category_theory.limits.has_pullback g₁ g₂]
(i₁ : W ⟶ Y)
(i₂ : X ⟶ Z)
(i₃ : S ⟶ T)
(eq₁ : f₁ ≫ i₃ = i₁ ≫ g₁)
(eq₂ : f₂ ≫ i₃ = i₂ ≫ g₂)
[category_theory.is_iso i₁]
[category_theory.is_iso i₂]
[category_theory.is_iso i₃] :
category_theory.is_iso (category_theory.limits.pullback.map f₁ f₂ g₁ g₂ i₁ i₂ i₃ eq₁ eq₂)
noncomputable
def
category_theory.limits.pullback.congr_hom
{C : Type u}
[category_theory.category C]
{X Y Z : C}
{f₁ f₂ : X ⟶ Z}
{g₁ g₂ : Y ⟶ Z}
(h₁ : f₁ = f₂)
(h₂ : g₁ = g₂)
[category_theory.limits.has_pullback f₁ g₁]
[category_theory.limits.has_pullback f₂ g₂] :
If f₁ = f₂ and g₁ = g₂, we may construct a canonical
isomorphism pullback f₁ g₁ ≅ pullback f₂ g₂
Equations
- category_theory.limits.pullback.congr_hom h₁ h₂ = category_theory.as_iso (category_theory.limits.pullback.map f₁ g₁ f₂ g₂ (𝟙 X) (𝟙 Y) (𝟙 Z) _ _)
@[simp]
theorem
category_theory.limits.pullback.congr_hom_hom
{C : Type u}
[category_theory.category C]
{X Y Z : C}
{f₁ f₂ : X ⟶ Z}
{g₁ g₂ : Y ⟶ Z}
(h₁ : f₁ = f₂)
(h₂ : g₁ = g₂)
[category_theory.limits.has_pullback f₁ g₁]
[category_theory.limits.has_pullback f₂ g₂] :
(category_theory.limits.pullback.congr_hom h₁ h₂).hom = category_theory.limits.pullback.map f₁ g₁ f₂ g₂ (𝟙 X) (𝟙 Y) (𝟙 Z) _ _
@[simp]
theorem
category_theory.limits.pullback.congr_hom_inv
{C : Type u}
[category_theory.category C]
{X Y Z : C}
{f₁ f₂ : X ⟶ Z}
{g₁ g₂ : Y ⟶ Z}
(h₁ : f₁ = f₂)
(h₂ : g₁ = g₂)
[category_theory.limits.has_pullback f₁ g₁]
[category_theory.limits.has_pullback f₂ g₂] :
(category_theory.limits.pullback.congr_hom h₁ h₂).inv = category_theory.limits.pullback.map f₂ g₂ f₁ g₁ (𝟙 X) (𝟙 Y) (𝟙 Z) _ _
@[protected, instance]
def
category_theory.limits.pushout.map_is_iso
{C : Type u}
[category_theory.category C]
{W X Y Z S T : C}
(f₁ : S ⟶ W)
(f₂ : S ⟶ X)
[category_theory.limits.has_pushout f₁ f₂]
(g₁ : T ⟶ Y)
(g₂ : T ⟶ Z)
[category_theory.limits.has_pushout g₁ g₂]
(i₁ : W ⟶ Y)
(i₂ : X ⟶ Z)
(i₃ : S ⟶ T)
(eq₁ : f₁ ≫ i₁ = i₃ ≫ g₁)
(eq₂ : f₂ ≫ i₂ = i₃ ≫ g₂)
[category_theory.is_iso i₁]
[category_theory.is_iso i₂]
[category_theory.is_iso i₃] :
category_theory.is_iso (category_theory.limits.pushout.map f₁ f₂ g₁ g₂ i₁ i₂ i₃ eq₁ eq₂)
theorem
category_theory.limits.pullback.map_desc_comp
{C : Type u}
[category_theory.category C]
{X Y S T S' : C}
(f : X ⟶ T)
(g : Y ⟶ T)
(i : T ⟶ S)
(i' : S ⟶ S')
[category_theory.limits.has_pullback f g]
[category_theory.limits.has_pullback (f ≫ i) (g ≫ i)]
[category_theory.limits.has_pullback (f ≫ i ≫ i') (g ≫ i ≫ i')]
[category_theory.limits.has_pullback ((f ≫ i) ≫ i') ((g ≫ i) ≫ i')] :
category_theory.limits.pullback.map_desc f g (i ≫ i') = category_theory.limits.pullback.map_desc f g i ≫ category_theory.limits.pullback.map_desc (f ≫ i) (g ≫ i) i' ≫ (category_theory.limits.pullback.congr_hom _ _).hom
@[simp]
theorem
category_theory.limits.pushout.congr_hom_hom
{C : Type u}
[category_theory.category C]
{X Y Z : C}
{f₁ f₂ : X ⟶ Y}
{g₁ g₂ : X ⟶ Z}
(h₁ : f₁ = f₂)
(h₂ : g₁ = g₂)
[category_theory.limits.has_pushout f₁ g₁]
[category_theory.limits.has_pushout f₂ g₂] :
(category_theory.limits.pushout.congr_hom h₁ h₂).hom = category_theory.limits.pushout.map f₁ g₁ f₂ g₂ (𝟙 Y) (𝟙 Z) (𝟙 X) _ _
noncomputable
def
category_theory.limits.pushout.congr_hom
{C : Type u}
[category_theory.category C]
{X Y Z : C}
{f₁ f₂ : X ⟶ Y}
{g₁ g₂ : X ⟶ Z}
(h₁ : f₁ = f₂)
(h₂ : g₁ = g₂)
[category_theory.limits.has_pushout f₁ g₁]
[category_theory.limits.has_pushout f₂ g₂] :
If f₁ = f₂ and g₁ = g₂, we may construct a canonical
isomorphism pushout f₁ g₁ ≅ pullback f₂ g₂
Equations
- category_theory.limits.pushout.congr_hom h₁ h₂ = category_theory.as_iso (category_theory.limits.pushout.map f₁ g₁ f₂ g₂ (𝟙 Y) (𝟙 Z) (𝟙 X) _ _)
@[simp]
theorem
category_theory.limits.pushout.congr_hom_inv
{C : Type u}
[category_theory.category C]
{X Y Z : C}
{f₁ f₂ : X ⟶ Y}
{g₁ g₂ : X ⟶ Z}
(h₁ : f₁ = f₂)
(h₂ : g₁ = g₂)
[category_theory.limits.has_pushout f₁ g₁]
[category_theory.limits.has_pushout f₂ g₂] :
(category_theory.limits.pushout.congr_hom h₁ h₂).inv = category_theory.limits.pushout.map f₂ g₂ f₁ g₁ (𝟙 Y) (𝟙 Z) (𝟙 X) _ _
theorem
category_theory.limits.pushout.map_lift_comp
{C : Type u}
[category_theory.category C]
{X Y S T S' : C}
(f : T ⟶ X)
(g : T ⟶ Y)
(i : S ⟶ T)
(i' : S' ⟶ S)
[category_theory.limits.has_pushout f g]
[category_theory.limits.has_pushout (i ≫ f) (i ≫ g)]
[category_theory.limits.has_pushout (i' ≫ i ≫ f) (i' ≫ i ≫ g)]
[category_theory.limits.has_pushout ((i' ≫ i) ≫ f) ((i' ≫ i) ≫ g)] :
category_theory.limits.pushout.map_lift f g (i' ≫ i) = (category_theory.limits.pushout.congr_hom _ _).hom ≫ category_theory.limits.pushout.map_lift (i ≫ f) (i ≫ g) i' ≫ category_theory.limits.pushout.map_lift f g i
noncomputable
def
category_theory.limits.pullback_comparison
{C : Type u}
[category_theory.category C]
{D : Type u₂}
[category_theory.category D]
{X Y Z : C}
(G : C ⥤ D)
(f : X ⟶ Z)
(g : Y ⟶ Z)
[category_theory.limits.has_pullback f g]
[category_theory.limits.has_pullback (G.map f) (G.map g)] :
G.obj (category_theory.limits.pullback f g) ⟶ category_theory.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
category_theory/limits/preserves/shapes/pullbacks.lean
Equations
Instances for category_theory.limits.pullback_comparison
@[simp]
theorem
category_theory.limits.pullback_comparison_comp_fst
{C : Type u}
[category_theory.category C]
{D : Type u₂}
[category_theory.category D]
{X Y Z : C}
(G : C ⥤ D)
(f : X ⟶ Z)
(g : Y ⟶ Z)
[category_theory.limits.has_pullback f g]
[category_theory.limits.has_pullback (G.map f) (G.map g)] :
@[simp]
theorem
category_theory.limits.pullback_comparison_comp_fst_assoc
{C : Type u}
[category_theory.category C]
{D : Type u₂}
[category_theory.category D]
{X Y Z : C}
(G : C ⥤ D)
(f : X ⟶ Z)
(g : Y ⟶ Z)
[category_theory.limits.has_pullback f g]
[category_theory.limits.has_pullback (G.map f) (G.map g)]
{X' : D}
(f' : G.obj X ⟶ X') :
@[simp]
theorem
category_theory.limits.pullback_comparison_comp_snd_assoc
{C : Type u}
[category_theory.category C]
{D : Type u₂}
[category_theory.category D]
{X Y Z : C}
(G : C ⥤ D)
(f : X ⟶ Z)
(g : Y ⟶ Z)
[category_theory.limits.has_pullback f g]
[category_theory.limits.has_pullback (G.map f) (G.map g)]
{X' : D}
(f' : G.obj Y ⟶ X') :
@[simp]
theorem
category_theory.limits.pullback_comparison_comp_snd
{C : Type u}
[category_theory.category C]
{D : Type u₂}
[category_theory.category D]
{X Y Z : C}
(G : C ⥤ D)
(f : X ⟶ Z)
(g : Y ⟶ Z)
[category_theory.limits.has_pullback f g]
[category_theory.limits.has_pullback (G.map f) (G.map g)] :
@[simp]
theorem
category_theory.limits.map_lift_pullback_comparison_assoc
{C : Type u}
[category_theory.category C]
{D : Type u₂}
[category_theory.category D]
{X Y Z : C}
(G : C ⥤ D)
(f : X ⟶ Z)
(g : Y ⟶ Z)
[category_theory.limits.has_pullback f g]
[category_theory.limits.has_pullback (G.map f) (G.map g)]
{W : C}
{h : W ⟶ X}
{k : W ⟶ Y}
(w : h ≫ f = k ≫ g)
{X' : D}
(f' : category_theory.limits.pullback (G.map f) (G.map g) ⟶ X') :
G.map (category_theory.limits.pullback.lift h k w) ≫ category_theory.limits.pullback_comparison G f g ≫ f' = category_theory.limits.pullback.lift (G.map h) (G.map k) _ ≫ f'
@[simp]
theorem
category_theory.limits.map_lift_pullback_comparison
{C : Type u}
[category_theory.category C]
{D : Type u₂}
[category_theory.category D]
{X Y Z : C}
(G : C ⥤ D)
(f : X ⟶ Z)
(g : Y ⟶ Z)
[category_theory.limits.has_pullback f g]
[category_theory.limits.has_pullback (G.map f) (G.map g)]
{W : C}
{h : W ⟶ X}
{k : W ⟶ Y}
(w : h ≫ f = k ≫ g) :
G.map (category_theory.limits.pullback.lift h k w) ≫ category_theory.limits.pullback_comparison G f g = category_theory.limits.pullback.lift (G.map h) (G.map k) _
noncomputable
def
category_theory.limits.pushout_comparison
{C : Type u}
[category_theory.category C]
{D : Type u₂}
[category_theory.category D]
{X Y Z : C}
(G : C ⥤ D)
(f : X ⟶ Y)
(g : X ⟶ Z)
[category_theory.limits.has_pushout f g]
[category_theory.limits.has_pushout (G.map f) (G.map g)] :
category_theory.limits.pushout (G.map f) (G.map g) ⟶ G.obj (category_theory.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
category_theory/limits/preserves/shapes/pullbacks.lean
Equations
Instances for category_theory.limits.pushout_comparison
@[simp]
theorem
category_theory.limits.inl_comp_pushout_comparison
{C : Type u}
[category_theory.category C]
{D : Type u₂}
[category_theory.category D]
{X Y Z : C}
(G : C ⥤ D)
(f : X ⟶ Y)
(g : X ⟶ Z)
[category_theory.limits.has_pushout f g]
[category_theory.limits.has_pushout (G.map f) (G.map g)] :
@[simp]
theorem
category_theory.limits.inl_comp_pushout_comparison_assoc
{C : Type u}
[category_theory.category C]
{D : Type u₂}
[category_theory.category D]
{X Y Z : C}
(G : C ⥤ D)
(f : X ⟶ Y)
(g : X ⟶ Z)
[category_theory.limits.has_pushout f g]
[category_theory.limits.has_pushout (G.map f) (G.map g)]
{X' : D}
(f' : G.obj (category_theory.limits.pushout f g) ⟶ X') :
@[simp]
theorem
category_theory.limits.inr_comp_pushout_comparison
{C : Type u}
[category_theory.category C]
{D : Type u₂}
[category_theory.category D]
{X Y Z : C}
(G : C ⥤ D)
(f : X ⟶ Y)
(g : X ⟶ Z)
[category_theory.limits.has_pushout f g]
[category_theory.limits.has_pushout (G.map f) (G.map g)] :
@[simp]
theorem
category_theory.limits.inr_comp_pushout_comparison_assoc
{C : Type u}
[category_theory.category C]
{D : Type u₂}
[category_theory.category D]
{X Y Z : C}
(G : C ⥤ D)
(f : X ⟶ Y)
(g : X ⟶ Z)
[category_theory.limits.has_pushout f g]
[category_theory.limits.has_pushout (G.map f) (G.map g)]
{X' : D}
(f' : G.obj (category_theory.limits.pushout f g) ⟶ X') :
@[simp]
theorem
category_theory.limits.pushout_comparison_map_desc_assoc
{C : Type u}
[category_theory.category C]
{D : Type u₂}
[category_theory.category D]
{X Y Z : C}
(G : C ⥤ D)
(f : X ⟶ Y)
(g : X ⟶ Z)
[category_theory.limits.has_pushout f g]
[category_theory.limits.has_pushout (G.map f) (G.map g)]
{W : C}
{h : Y ⟶ W}
{k : Z ⟶ W}
(w : f ≫ h = g ≫ k)
{X' : D}
(f' : G.obj W ⟶ X') :
category_theory.limits.pushout_comparison G f g ≫ G.map (category_theory.limits.pushout.desc h k w) ≫ f' = category_theory.limits.pushout.desc (G.map h) (G.map k) _ ≫ f'
@[simp]
theorem
category_theory.limits.pushout_comparison_map_desc
{C : Type u}
[category_theory.category C]
{D : Type u₂}
[category_theory.category D]
{X Y Z : C}
(G : C ⥤ D)
(f : X ⟶ Y)
(g : X ⟶ Z)
[category_theory.limits.has_pushout f g]
[category_theory.limits.has_pushout (G.map f) (G.map g)]
{W : C}
{h : Y ⟶ W}
{k : Z ⟶ W}
(w : f ≫ h = g ≫ k) :
category_theory.limits.pushout_comparison G f g ≫ G.map (category_theory.limits.pushout.desc h k w) = category_theory.limits.pushout.desc (G.map h) (G.map k) _
theorem
category_theory.limits.has_pullback_symmetry
{C : Type u}
[category_theory.category C]
{X Y Z : C}
(f : X ⟶ Z)
(g : Y ⟶ Z)
[category_theory.limits.has_pullback f g] :
Making this a global instance would make the typeclass seach go in an infinite loop.
noncomputable
def
category_theory.limits.pullback_symmetry
{C : Type u}
[category_theory.category C]
{X Y Z : C}
(f : X ⟶ Z)
(g : Y ⟶ Z)
[category_theory.limits.has_pullback f g] :
The isomorphism X ×[Z] Y ≅ Y ×[Z] X.
@[simp]
theorem
category_theory.limits.pullback_symmetry_hom_comp_fst_assoc
{C : Type u}
[category_theory.category C]
{X Y Z : C}
(f : X ⟶ Z)
(g : Y ⟶ Z)
[category_theory.limits.has_pullback f g]
{X' : C}
(f' : Y ⟶ X') :
@[simp]
theorem
category_theory.limits.pullback_symmetry_hom_comp_fst
{C : Type u}
[category_theory.category C]
{X Y Z : C}
(f : X ⟶ Z)
(g : Y ⟶ Z)
[category_theory.limits.has_pullback f g] :
@[simp]
theorem
category_theory.limits.pullback_symmetry_hom_comp_snd_assoc
{C : Type u}
[category_theory.category C]
{X Y Z : C}
(f : X ⟶ Z)
(g : Y ⟶ Z)
[category_theory.limits.has_pullback f g]
{X' : C}
(f' : X ⟶ X') :
@[simp]
theorem
category_theory.limits.pullback_symmetry_hom_comp_snd
{C : Type u}
[category_theory.category C]
{X Y Z : C}
(f : X ⟶ Z)
(g : Y ⟶ Z)
[category_theory.limits.has_pullback f g] :
@[simp]
theorem
category_theory.limits.pullback_symmetry_inv_comp_fst
{C : Type u}
[category_theory.category C]
{X Y Z : C}
(f : X ⟶ Z)
(g : Y ⟶ Z)
[category_theory.limits.has_pullback f g] :
@[simp]
theorem
category_theory.limits.pullback_symmetry_inv_comp_fst_assoc
{C : Type u}
[category_theory.category C]
{X Y Z : C}
(f : X ⟶ Z)
(g : Y ⟶ Z)
[category_theory.limits.has_pullback f g]
{X' : C}
(f' : X ⟶ X') :
@[simp]
theorem
category_theory.limits.pullback_symmetry_inv_comp_snd
{C : Type u}
[category_theory.category C]
{X Y Z : C}
(f : X ⟶ Z)
(g : Y ⟶ Z)
[category_theory.limits.has_pullback f g] :
@[simp]
theorem
category_theory.limits.pullback_symmetry_inv_comp_snd_assoc
{C : Type u}
[category_theory.category C]
{X Y Z : C}
(f : X ⟶ Z)
(g : Y ⟶ Z)
[category_theory.limits.has_pullback f g]
{X' : C}
(f' : Y ⟶ X') :
theorem
category_theory.limits.has_pushout_symmetry
{C : Type u}
[category_theory.category C]
{X Y Z : C}
(f : X ⟶ Y)
(g : X ⟶ Z)
[category_theory.limits.has_pushout f g] :
Making this a global instance would make the typeclass seach go in an infinite loop.
noncomputable
def
category_theory.limits.pushout_symmetry
{C : Type u}
[category_theory.category C]
{X Y Z : C}
(f : X ⟶ Y)
(g : X ⟶ Z)
[category_theory.limits.has_pushout f g] :
The isomorphism Y ⨿[X] Z ≅ Z ⨿[X] Y.
@[simp]
theorem
category_theory.limits.inl_comp_pushout_symmetry_hom
{C : Type u}
[category_theory.category C]
{X Y Z : C}
(f : X ⟶ Y)
(g : X ⟶ Z)
[category_theory.limits.has_pushout f g] :
@[simp]
theorem
category_theory.limits.inl_comp_pushout_symmetry_hom_assoc
{C : Type u}
[category_theory.category C]
{X Y Z : C}
(f : X ⟶ Y)
(g : X ⟶ Z)
[category_theory.limits.has_pushout f g]
{X' : C}
(f' : category_theory.limits.pushout g f ⟶ X') :
@[simp]
theorem
category_theory.limits.inr_comp_pushout_symmetry_hom_assoc
{C : Type u}
[category_theory.category C]
{X Y Z : C}
(f : X ⟶ Y)
(g : X ⟶ Z)
[category_theory.limits.has_pushout f g]
{X' : C}
(f' : category_theory.limits.pushout g f ⟶ X') :
@[simp]
theorem
category_theory.limits.inr_comp_pushout_symmetry_hom
{C : Type u}
[category_theory.category C]
{X Y Z : C}
(f : X ⟶ Y)
(g : X ⟶ Z)
[category_theory.limits.has_pushout f g] :
@[simp]
theorem
category_theory.limits.inl_comp_pushout_symmetry_inv_assoc
{C : Type u}
[category_theory.category C]
{X Y Z : C}
(f : X ⟶ Y)
(g : X ⟶ Z)
[category_theory.limits.has_pushout f g]
{X' : C}
(f' : category_theory.limits.pushout f g ⟶ X') :
@[simp]
theorem
category_theory.limits.inl_comp_pushout_symmetry_inv
{C : Type u}
[category_theory.category C]
{X Y Z : C}
(f : X ⟶ Y)
(g : X ⟶ Z)
[category_theory.limits.has_pushout f g] :
@[simp]
theorem
category_theory.limits.inr_comp_pushout_symmetry_inv_assoc
{C : Type u}
[category_theory.category C]
{X Y Z : C}
(f : X ⟶ Y)
(g : X ⟶ Z)
[category_theory.limits.has_pushout f g]
{X' : C}
(f' : category_theory.limits.pushout f g ⟶ X') :
@[simp]
theorem
category_theory.limits.inr_comp_pushout_symmetry_inv
{C : Type u}
[category_theory.category C]
{X Y Z : C}
(f : X ⟶ Y)
(g : X ⟶ Z)
[category_theory.limits.has_pushout f g] :
noncomputable
def
category_theory.limits.pullback_is_pullback_of_comp_mono
{C : Type u}
[category_theory.category C]
{W X Y Z : C}
(f : X ⟶ W)
(g : Y ⟶ W)
(i : W ⟶ Z)
[category_theory.mono i]
[category_theory.limits.has_pullback f g] :
The pullback of f, g is also the pullback of f ≫ i, g ≫ i for any mono i.
@[protected, instance]
def
category_theory.limits.has_pullback_of_comp_mono
{C : Type u}
[category_theory.category C]
{W X Y Z : C}
(f : X ⟶ W)
(g : Y ⟶ W)
(i : W ⟶ Z)
[category_theory.mono i]
[category_theory.limits.has_pullback f g] :
category_theory.limits.has_pullback (f ≫ i) (g ≫ i)
noncomputable
def
category_theory.limits.pullback_cone_of_left_iso
{C : Type u}
[category_theory.category C]
{X Y Z : C}
(f : X ⟶ Z)
(g : Y ⟶ Z)
[category_theory.is_iso f] :
If f : X ⟶ Z is iso, then X ×[Z] Y ≅ Y. This is the explicit limit cone.
Equations
@[simp]
theorem
category_theory.limits.pullback_cone_of_left_iso_X
{C : Type u}
[category_theory.category C]
{X Y Z : C}
(f : X ⟶ Z)
(g : Y ⟶ Z)
[category_theory.is_iso f] :
@[simp]
theorem
category_theory.limits.pullback_cone_of_left_iso_fst
{C : Type u}
[category_theory.category C]
{X Y Z : C}
(f : X ⟶ Z)
(g : Y ⟶ Z)
[category_theory.is_iso f] :
@[simp]
theorem
category_theory.limits.pullback_cone_of_left_iso_snd
{C : Type u}
[category_theory.category C]
{X Y Z : C}
(f : X ⟶ Z)
(g : Y ⟶ Z)
[category_theory.is_iso f] :
@[simp]
theorem
category_theory.limits.pullback_cone_of_left_iso_π_app_none
{C : Type u}
[category_theory.category C]
{X Y Z : C}
(f : X ⟶ Z)
(g : Y ⟶ Z)
[category_theory.is_iso f] :
@[simp]
theorem
category_theory.limits.pullback_cone_of_left_iso_π_app_left
{C : Type u}
[category_theory.category C]
{X Y Z : C}
(f : X ⟶ Z)
(g : Y ⟶ Z)
[category_theory.is_iso f] :
@[simp]
theorem
category_theory.limits.pullback_cone_of_left_iso_π_app_right
{C : Type u}
[category_theory.category C]
{X Y Z : C}
(f : X ⟶ Z)
(g : Y ⟶ Z)
[category_theory.is_iso f] :
noncomputable
def
category_theory.limits.pullback_cone_of_left_iso_is_limit
{C : Type u}
[category_theory.category C]
{X Y Z : C}
(f : X ⟶ Z)
(g : Y ⟶ Z)
[category_theory.is_iso f] :
Verify that the constructed limit cone is indeed a limit.
Equations
theorem
category_theory.limits.has_pullback_of_left_iso
{C : Type u}
[category_theory.category C]
{X Y Z : C}
(f : X ⟶ Z)
(g : Y ⟶ Z)
[category_theory.is_iso f] :
@[protected, instance]
def
category_theory.limits.pullback_snd_iso_of_left_iso
{C : Type u}
[category_theory.category C]
{X Y Z : C}
(f : X ⟶ Z)
(g : Y ⟶ Z)
[category_theory.is_iso f] :
@[protected, instance]
def
category_theory.limits.has_pullback_of_right_factors_mono
{C : Type u}
[category_theory.category C]
{W X Z : C}
(i : Z ⟶ W)
[category_theory.mono i]
(f : X ⟶ Z) :
category_theory.limits.has_pullback i (f ≫ i)
@[protected, instance]
def
category_theory.limits.pullback_snd_iso_of_right_factors_mono
{C : Type u}
[category_theory.category C]
{W X Z : C}
(i : Z ⟶ W)
[category_theory.mono i]
(f : X ⟶ Z) :
noncomputable
def
category_theory.limits.pullback_cone_of_right_iso
{C : Type u}
[category_theory.category C]
{X Y Z : C}
(f : X ⟶ Z)
(g : Y ⟶ Z)
[category_theory.is_iso g] :
If g : Y ⟶ Z is iso, then X ×[Z] Y ≅ X. This is the explicit limit cone.
Equations
@[simp]
theorem
category_theory.limits.pullback_cone_of_right_iso_X
{C : Type u}
[category_theory.category C]
{X Y Z : C}
(f : X ⟶ Z)
(g : Y ⟶ Z)
[category_theory.is_iso g] :
@[simp]
theorem
category_theory.limits.pullback_cone_of_right_iso_fst
{C : Type u}
[category_theory.category C]
{X Y Z : C}
(f : X ⟶ Z)
(g : Y ⟶ Z)
[category_theory.is_iso g] :
@[simp]
theorem
category_theory.limits.pullback_cone_of_right_iso_snd
{C : Type u}
[category_theory.category C]
{X Y Z : C}
(f : X ⟶ Z)
(g : Y ⟶ Z)
[category_theory.is_iso g] :
@[simp]
theorem
category_theory.limits.pullback_cone_of_right_iso_π_app_none
{C : Type u}
[category_theory.category C]
{X Y Z : C}
(f : X ⟶ Z)
(g : Y ⟶ Z)
[category_theory.is_iso g] :
@[simp]
theorem
category_theory.limits.pullback_cone_of_right_iso_π_app_left
{C : Type u}
[category_theory.category C]
{X Y Z : C}
(f : X ⟶ Z)
(g : Y ⟶ Z)
[category_theory.is_iso g] :
@[simp]
theorem
category_theory.limits.pullback_cone_of_right_iso_π_app_right
{C : Type u}
[category_theory.category C]
{X Y Z : C}
(f : X ⟶ Z)
(g : Y ⟶ Z)
[category_theory.is_iso g] :
noncomputable
def
category_theory.limits.pullback_cone_of_right_iso_is_limit
{C : Type u}
[category_theory.category C]
{X Y Z : C}
(f : X ⟶ Z)
(g : Y ⟶ Z)
[category_theory.is_iso g] :
Verify that the constructed limit cone is indeed a limit.
Equations
theorem
category_theory.limits.has_pullback_of_right_iso
{C : Type u}
[category_theory.category C]
{X Y Z : C}
(f : X ⟶ Z)
(g : Y ⟶ Z)
[category_theory.is_iso g] :
@[protected, instance]
def
category_theory.limits.pullback_snd_iso_of_right_iso
{C : Type u}
[category_theory.category C]
{X Y Z : C}
(f : X ⟶ Z)
(g : Y ⟶ Z)
[category_theory.is_iso g] :
@[protected, instance]
def
category_theory.limits.has_pullback_of_left_factors_mono
{C : Type u}
[category_theory.category C]
{W X Z : C}
(i : Z ⟶ W)
[category_theory.mono i]
(f : X ⟶ Z) :
category_theory.limits.has_pullback (f ≫ i) i
@[protected, instance]
def
category_theory.limits.pullback_snd_iso_of_left_factors_mono
{C : Type u}
[category_theory.category C]
{W X Z : C}
(i : Z ⟶ W)
[category_theory.mono i]
(f : X ⟶ Z) :
noncomputable
def
category_theory.limits.pushout_is_pushout_of_epi_comp
{C : Type u}
[category_theory.category C]
{W X Y Z : C}
(f : X ⟶ Y)
(g : X ⟶ Z)
(h : W ⟶ X)
[category_theory.epi h]
[category_theory.limits.has_pushout f g] :
The pushout of f, g is also the pullback of h ≫ f, h ≫ g for any epi h.
@[protected, instance]
def
category_theory.limits.has_pushout_of_epi_comp
{C : Type u}
[category_theory.category C]
{W X Y Z : C}
(f : X ⟶ Y)
(g : X ⟶ Z)
(h : W ⟶ X)
[category_theory.epi h]
[category_theory.limits.has_pushout f g] :
category_theory.limits.has_pushout (h ≫ f) (h ≫ g)
noncomputable
def
category_theory.limits.pushout_cocone_of_left_iso
{C : Type u}
[category_theory.category C]
{X Y Z : C}
(f : X ⟶ Y)
(g : X ⟶ Z)
[category_theory.is_iso f] :
If f : X ⟶ Y is iso, then Y ⨿[X] Z ≅ Z. This is the explicit colimit cocone.
Equations
@[simp]
theorem
category_theory.limits.pushout_cocone_of_left_iso_X
{C : Type u}
[category_theory.category C]
{X Y Z : C}
(f : X ⟶ Y)
(g : X ⟶ Z)
[category_theory.is_iso f] :
@[simp]
theorem
category_theory.limits.pushout_cocone_of_left_iso_inl
{C : Type u}
[category_theory.category C]
{X Y Z : C}
(f : X ⟶ Y)
(g : X ⟶ Z)
[category_theory.is_iso f] :
@[simp]
theorem
category_theory.limits.pushout_cocone_of_left_iso_inr
{C : Type u}
[category_theory.category C]
{X Y Z : C}
(f : X ⟶ Y)
(g : X ⟶ Z)
[category_theory.is_iso f] :
@[simp]
theorem
category_theory.limits.pushout_cocone_of_left_iso_ι_app_none
{C : Type u}
[category_theory.category C]
{X Y Z : C}
(f : X ⟶ Y)
(g : X ⟶ Z)
[category_theory.is_iso f] :
@[simp]
theorem
category_theory.limits.pushout_cocone_of_left_iso_ι_app_left
{C : Type u}
[category_theory.category C]
{X Y Z : C}
(f : X ⟶ Y)
(g : X ⟶ Z)
[category_theory.is_iso f] :
@[simp]
theorem
category_theory.limits.pushout_cocone_of_left_iso_ι_app_right
{C : Type u}
[category_theory.category C]
{X Y Z : C}
(f : X ⟶ Y)
(g : X ⟶ Z)
[category_theory.is_iso f] :
noncomputable
def
category_theory.limits.pushout_cocone_of_left_iso_is_limit
{C : Type u}
[category_theory.category C]
{X Y Z : C}
(f : X ⟶ Y)
(g : X ⟶ Z)
[category_theory.is_iso f] :
Verify that the constructed cocone is indeed a colimit.
Equations
theorem
category_theory.limits.has_pushout_of_left_iso
{C : Type u}
[category_theory.category C]
{X Y Z : C}
(f : X ⟶ Y)
(g : X ⟶ Z)
[category_theory.is_iso f] :
@[protected, instance]
def
category_theory.limits.pushout_inr_iso_of_left_iso
{C : Type u}
[category_theory.category C]
{X Y Z : C}
(f : X ⟶ Y)
(g : X ⟶ Z)
[category_theory.is_iso f] :
@[protected, instance]
def
category_theory.limits.has_pushout_of_right_factors_epi
{C : Type u}
[category_theory.category C]
{W X Y : C}
(h : W ⟶ X)
[category_theory.epi h]
(f : X ⟶ Y) :
category_theory.limits.has_pushout h (h ≫ f)
@[protected, instance]
def
category_theory.limits.pushout_inr_iso_of_right_factors_epi
{C : Type u}
[category_theory.category C]
{W X Y : C}
(h : W ⟶ X)
[category_theory.epi h]
(f : X ⟶ Y) :
noncomputable
def
category_theory.limits.pushout_cocone_of_right_iso
{C : Type u}
[category_theory.category C]
{X Y Z : C}
(f : X ⟶ Y)
(g : X ⟶ Z)
[category_theory.is_iso g] :
If f : X ⟶ Z is iso, then Y ⨿[X] Z ≅ Y. This is the explicit colimit cocone.
Equations
@[simp]
theorem
category_theory.limits.pushout_cocone_of_right_iso_X
{C : Type u}
[category_theory.category C]
{X Y Z : C}
(f : X ⟶ Y)
(g : X ⟶ Z)
[category_theory.is_iso g] :
@[simp]
theorem
category_theory.limits.pushout_cocone_of_right_iso_inl
{C : Type u}
[category_theory.category C]
{X Y Z : C}
(f : X ⟶ Y)
(g : X ⟶ Z)
[category_theory.is_iso g] :
@[simp]
theorem
category_theory.limits.pushout_cocone_of_right_iso_inr
{C : Type u}
[category_theory.category C]
{X Y Z : C}
(f : X ⟶ Y)
(g : X ⟶ Z)
[category_theory.is_iso g] :
@[simp]
theorem
category_theory.limits.pushout_cocone_of_right_iso_ι_app_none
{C : Type u}
[category_theory.category C]
{X Y Z : C}
(f : X ⟶ Y)
(g : X ⟶ Z)
[category_theory.is_iso g] :
@[simp]
theorem
category_theory.limits.pushout_cocone_of_right_iso_ι_app_left
{C : Type u}
[category_theory.category C]
{X Y Z : C}
(f : X ⟶ Y)
(g : X ⟶ Z)
[category_theory.is_iso g] :
@[simp]
theorem
category_theory.limits.pushout_cocone_of_right_iso_ι_app_right
{C : Type u}
[category_theory.category C]
{X Y Z : C}
(f : X ⟶ Y)
(g : X ⟶ Z)
[category_theory.is_iso g] :
noncomputable
def
category_theory.limits.pushout_cocone_of_right_iso_is_limit
{C : Type u}
[category_theory.category C]
{X Y Z : C}
(f : X ⟶ Y)
(g : X ⟶ Z)
[category_theory.is_iso g] :
Verify that the constructed cocone is indeed a colimit.
Equations
theorem
category_theory.limits.has_pushout_of_right_iso
{C : Type u}
[category_theory.category C]
{X Y Z : C}
(f : X ⟶ Y)
(g : X ⟶ Z)
[category_theory.is_iso g] :
@[protected, instance]
def
category_theory.limits.pushout_inl_iso_of_right_iso
{C : Type u}
[category_theory.category C]
{X Y Z : C}
(f : X ⟶ Y)
(g : X ⟶ Z)
[category_theory.is_iso g] :
@[protected, instance]
def
category_theory.limits.has_pushout_of_left_factors_epi
{C : Type u}
[category_theory.category C]
{W X Y : C}
(h : W ⟶ X)
[category_theory.epi h]
(f : X ⟶ Y) :
category_theory.limits.has_pushout (h ≫ f) h
@[protected, instance]
def
category_theory.limits.pushout_inl_iso_of_left_factors_epi
{C : Type u}
[category_theory.category C]
{W X Y : C}
(h : W ⟶ X)
[category_theory.epi h]
(f : X ⟶ Y) :
@[protected, instance]
def
category_theory.limits.has_kernel_pair_of_mono
{C : Type u}
[category_theory.category C]
{X Y : C}
(f : X ⟶ Y)
[category_theory.mono f] :
theorem
category_theory.limits.fst_eq_snd_of_mono_eq
{C : Type u}
[category_theory.category C]
{X Y : C}
(f : X ⟶ Y)
[category_theory.mono f] :
@[simp]
theorem
category_theory.limits.pullback_symmetry_hom_of_mono_eq
{C : Type u}
[category_theory.category C]
{X Y : C}
(f : X ⟶ Y)
[category_theory.mono f] :
@[protected, instance]
def
category_theory.limits.fst_iso_of_mono_eq
{C : Type u}
[category_theory.category C]
{X Y : C}
(f : X ⟶ Y)
[category_theory.mono f] :
@[protected, instance]
def
category_theory.limits.snd_iso_of_mono_eq
{C : Type u}
[category_theory.category C]
{X Y : C}
(f : X ⟶ Y)
[category_theory.mono f] :
@[protected, instance]
def
category_theory.limits.has_cokernel_pair_of_epi
{C : Type u}
[category_theory.category C]
{X Y : C}
(f : X ⟶ Y)
[category_theory.epi f] :
theorem
category_theory.limits.inl_eq_inr_of_epi_eq
{C : Type u}
[category_theory.category C]
{X Y : C}
(f : X ⟶ Y)
[category_theory.epi f] :
@[simp]
theorem
category_theory.limits.pullback_symmetry_hom_of_epi_eq
{C : Type u}
[category_theory.category C]
{X Y : C}
(f : X ⟶ Y)
[category_theory.epi f] :
@[protected, instance]
def
category_theory.limits.inl_iso_of_epi_eq
{C : Type u}
[category_theory.category C]
{X Y : C}
(f : X ⟶ Y)
[category_theory.epi f] :
@[protected, instance]
def
category_theory.limits.inr_iso_of_epi_eq
{C : Type u}
[category_theory.category C]
{X Y : C}
(f : X ⟶ Y)
[category_theory.epi f] :
def
category_theory.limits.big_square_is_pullback
{C : Type u}
[category_theory.category C]
{X₁ X₂ X₃ Y₁ Y₂ Y₃ : C}
(f₁ : X₁ ⟶ X₂)
(f₂ : X₂ ⟶ X₃)
(g₁ : Y₁ ⟶ Y₂)
(g₂ : Y₂ ⟶ Y₃)
(i₁ : X₁ ⟶ Y₁)
(i₂ : X₂ ⟶ Y₂)
(i₃ : X₃ ⟶ Y₃)
(h₁ : i₁ ≫ g₁ = f₁ ≫ i₂)
(h₂ : i₂ ≫ g₂ = f₂ ≫ i₃)
(H : category_theory.limits.is_limit (category_theory.limits.pullback_cone.mk i₂ f₂ h₂))
(H' : category_theory.limits.is_limit (category_theory.limits.pullback_cone.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
- category_theory.limits.big_square_is_pullback f₁ f₂ g₁ g₂ i₁ i₂ i₃ h₁ h₂ H H' = (category_theory.limits.pullback_cone.mk i₁ (f₁ ≫ f₂) _).is_limit_aux' (λ (s : category_theory.limits.pullback_cone (g₁ ≫ g₂) i₃), (category_theory.limits.pullback_cone.is_limit.lift' H (s.fst ≫ g₁) s.snd _).cases_on (λ (l₁ : s.X ⟶ (category_theory.limits.pullback_cone.mk i₂ f₂ h₂).X) (property : l₁ ≫ (category_theory.limits.pullback_cone.mk i₂ f₂ h₂).fst = s.fst ≫ g₁ ∧ l₁ ≫ (category_theory.limits.pullback_cone.mk i₂ f₂ h₂).snd = s.snd), property.dcases_on (λ (hl₁ : l₁ ≫ (category_theory.limits.pullback_cone.mk i₂ f₂ h₂).fst = s.fst ≫ g₁) (hl₁' : l₁ ≫ (category_theory.limits.pullback_cone.mk i₂ f₂ h₂).snd = s.snd), (category_theory.limits.pullback_cone.is_limit.lift' H' s.fst l₁ _).cases_on (λ (l₂ : s.X ⟶ (category_theory.limits.pullback_cone.mk i₁ f₁ h₁).X) (property : l₂ ≫ (category_theory.limits.pullback_cone.mk i₁ f₁ h₁).fst = s.fst ∧ l₂ ≫ (category_theory.limits.pullback_cone.mk i₁ f₁ h₁).snd = l₁), property.dcases_on (λ (hl₂ : l₂ ≫ (category_theory.limits.pullback_cone.mk i₁ f₁ h₁).fst = s.fst) (hl₂' : l₂ ≫ (category_theory.limits.pullback_cone.mk i₁ f₁ h₁).snd = l₁), ⟨l₂, _⟩)))))
def
category_theory.limits.big_square_is_pushout
{C : Type u}
[category_theory.category C]
{X₁ X₂ X₃ Y₁ Y₂ Y₃ : C}
(f₁ : X₁ ⟶ X₂)
(f₂ : X₂ ⟶ X₃)
(g₁ : Y₁ ⟶ Y₂)
(g₂ : Y₂ ⟶ Y₃)
(i₁ : X₁ ⟶ Y₁)
(i₂ : X₂ ⟶ Y₂)
(i₃ : X₃ ⟶ Y₃)
(h₁ : i₁ ≫ g₁ = f₁ ≫ i₂)
(h₂ : i₂ ≫ g₂ = f₂ ≫ i₃)
(H : category_theory.limits.is_colimit (category_theory.limits.pushout_cocone.mk g₂ i₃ h₂))
(H' : category_theory.limits.is_colimit (category_theory.limits.pushout_cocone.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
- category_theory.limits.big_square_is_pushout f₁ f₂ g₁ g₂ i₁ i₂ i₃ h₁ h₂ H H' = (category_theory.limits.pushout_cocone.mk (g₁ ≫ g₂) i₃ _).is_colimit_aux' (λ (s : category_theory.limits.pushout_cocone i₁ (f₁ ≫ f₂)), (category_theory.limits.pushout_cocone.is_colimit.desc' H' s.inl (f₂ ≫ s.inr) _).cases_on (λ (l₁ : (category_theory.limits.pushout_cocone.mk g₁ i₂ h₁).X ⟶ s.X) (property : (category_theory.limits.pushout_cocone.mk g₁ i₂ h₁).inl ≫ l₁ = s.inl ∧ (category_theory.limits.pushout_cocone.mk g₁ i₂ h₁).inr ≫ l₁ = f₂ ≫ s.inr), property.dcases_on (λ (hl₁ : (category_theory.limits.pushout_cocone.mk g₁ i₂ h₁).inl ≫ l₁ = s.inl) (hl₁' : (category_theory.limits.pushout_cocone.mk g₁ i₂ h₁).inr ≫ l₁ = f₂ ≫ s.inr), (category_theory.limits.pushout_cocone.is_colimit.desc' H l₁ s.inr hl₁').cases_on (λ (l₂ : (category_theory.limits.pushout_cocone.mk g₂ i₃ h₂).X ⟶ s.X) (property : (category_theory.limits.pushout_cocone.mk g₂ i₃ h₂).inl ≫ l₂ = l₁ ∧ (category_theory.limits.pushout_cocone.mk g₂ i₃ h₂).inr ≫ l₂ = s.inr), property.dcases_on (λ (hl₂ : (category_theory.limits.pushout_cocone.mk g₂ i₃ h₂).inl ≫ l₂ = l₁) (hl₂' : (category_theory.limits.pushout_cocone.mk g₂ i₃ h₂).inr ≫ l₂ = s.inr), ⟨l₂, _⟩)))))
def
category_theory.limits.left_square_is_pullback
{C : Type u}
[category_theory.category C]
{X₁ X₂ X₃ Y₁ Y₂ Y₃ : C}
(f₁ : X₁ ⟶ X₂)
(f₂ : X₂ ⟶ X₃)
(g₁ : Y₁ ⟶ Y₂)
(g₂ : Y₂ ⟶ Y₃)
(i₁ : X₁ ⟶ Y₁)
(i₂ : X₂ ⟶ Y₂)
(i₃ : X₃ ⟶ Y₃)
(h₁ : i₁ ≫ g₁ = f₁ ≫ i₂)
(h₂ : i₂ ≫ g₂ = f₂ ≫ i₃)
(H : category_theory.limits.is_limit (category_theory.limits.pullback_cone.mk i₂ f₂ h₂))
(H' : category_theory.limits.is_limit (category_theory.limits.pullback_cone.mk i₁ (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
- category_theory.limits.left_square_is_pullback f₁ f₂ g₁ g₂ i₁ i₂ i₃ h₁ h₂ H H' = (category_theory.limits.pullback_cone.mk i₁ f₁ h₁).is_limit_aux' (λ (s : category_theory.limits.pullback_cone g₁ i₂), (category_theory.limits.pullback_cone.is_limit.lift' H' s.fst (s.snd ≫ f₂) _).cases_on (λ (l₁ : s.X ⟶ (category_theory.limits.pullback_cone.mk i₁ (f₁ ≫ f₂) _).X) (property : l₁ ≫ (category_theory.limits.pullback_cone.mk i₁ (f₁ ≫ f₂) _).fst = s.fst ∧ l₁ ≫ (category_theory.limits.pullback_cone.mk i₁ (f₁ ≫ f₂) _).snd = s.snd ≫ f₂), property.dcases_on (λ (hl₁ : l₁ ≫ (category_theory.limits.pullback_cone.mk i₁ (f₁ ≫ f₂) _).fst = s.fst) (hl₁' : l₁ ≫ (category_theory.limits.pullback_cone.mk i₁ (f₁ ≫ f₂) _).snd = s.snd ≫ f₂), ⟨l₁, _⟩)))
def
category_theory.limits.right_square_is_pushout
{C : Type u}
[category_theory.category C]
{X₁ X₂ X₃ Y₁ Y₂ Y₃ : C}
(f₁ : X₁ ⟶ X₂)
(f₂ : X₂ ⟶ X₃)
(g₁ : Y₁ ⟶ Y₂)
(g₂ : Y₂ ⟶ Y₃)
(i₁ : X₁ ⟶ Y₁)
(i₂ : X₂ ⟶ Y₂)
(i₃ : X₃ ⟶ Y₃)
(h₁ : i₁ ≫ g₁ = f₁ ≫ i₂)
(h₂ : i₂ ≫ g₂ = f₂ ≫ i₃)
(H : category_theory.limits.is_colimit (category_theory.limits.pushout_cocone.mk g₁ i₂ h₁))
(H' : category_theory.limits.is_colimit (category_theory.limits.pushout_cocone.mk (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
- category_theory.limits.right_square_is_pushout f₁ f₂ g₁ g₂ i₁ i₂ i₃ h₁ h₂ H H' = (category_theory.limits.pushout_cocone.mk g₂ i₃ h₂).is_colimit_aux' (λ (s : category_theory.limits.pushout_cocone i₂ f₂), (category_theory.limits.pushout_cocone.is_colimit.desc' H' (g₁ ≫ s.inl) s.inr _).cases_on (λ (l₁ : (category_theory.limits.pushout_cocone.mk (g₁ ≫ g₂) i₃ _).X ⟶ s.X) (property : (category_theory.limits.pushout_cocone.mk (g₁ ≫ g₂) i₃ _).inl ≫ l₁ = g₁ ≫ s.inl ∧ (category_theory.limits.pushout_cocone.mk (g₁ ≫ g₂) i₃ _).inr ≫ l₁ = s.inr), property.dcases_on (λ (hl₁ : (category_theory.limits.pushout_cocone.mk (g₁ ≫ g₂) i₃ _).inl ≫ l₁ = g₁ ≫ s.inl) (hl₁' : (category_theory.limits.pushout_cocone.mk (g₁ ≫ g₂) i₃ _).inr ≫ l₁ = s.inr), id (λ {X₁ X₂ X₃ Y₁ Y₂ Y₃ : C} (f₁ : X₁ ⟶ X₂) (f₂ : X₂ ⟶ X₃) (g₁ : Y₁ ⟶ Y₂) (g₂ : Y₂ ⟶ Y₃) (i₁ : X₁ ⟶ Y₁) (i₂ : X₂ ⟶ Y₂) (i₃ : X₃ ⟶ Y₃) (h₁ : i₁ ≫ g₁ = f₁ ≫ i₂) (h₂ : i₂ ≫ g₂ = f₂ ≫ i₃) (H : category_theory.limits.is_colimit (category_theory.limits.pushout_cocone.mk g₁ i₂ h₁)) (H' : category_theory.limits.is_colimit (category_theory.limits.pushout_cocone.mk (g₁ ≫ g₂) i₃ _)) (s : category_theory.limits.pushout_cocone i₂ f₂) (this : i₁ ≫ g₁ ≫ s.inl = (f₁ ≫ f₂) ≫ s.inr) (l₁ : Y₃ ⟶ s.X) (hl₁ : (g₁ ≫ g₂) ≫ l₁ = g₁ ≫ s.inl) (hl₁' : i₃ ≫ l₁ = s.inr), ⟨l₁, _⟩) f₁ f₂ g₁ g₂ i₁ i₂ i₃ h₁ h₂ H H' s _ l₁ hl₁ hl₁')))
noncomputable
def
category_theory.limits.pullback_right_pullback_fst_iso
{C : Type u}
[category_theory.category C]
{W X Y Z : C}
(f : X ⟶ Z)
(g : Y ⟶ Z)
(f' : W ⟶ X)
[category_theory.limits.has_pullback f g]
[category_theory.limits.has_pullback f' category_theory.limits.pullback.fst]
[category_theory.limits.has_pullback (f' ≫ f) g] :
The canonical isomorphism W ×[X] (X ×[Z] Y) ≅ W ×[Z] Y
Equations
- category_theory.limits.pullback_right_pullback_fst_iso f g f' = let this : category_theory.limits.is_limit (category_theory.limits.pullback_cone.mk category_theory.limits.pullback.fst (category_theory.limits.pullback.snd ≫ category_theory.limits.pullback.snd) _) := category_theory.limits.big_square_is_pullback category_theory.limits.pullback.snd category_theory.limits.pullback.snd f' f category_theory.limits.pullback.fst category_theory.limits.pullback.fst g _ category_theory.limits.pullback.condition (category_theory.limits.pullback_is_pullback f g) (category_theory.limits.pullback_is_pullback f' category_theory.limits.pullback.fst) in this.cone_point_unique_up_to_iso (category_theory.limits.pullback_is_pullback (f' ≫ f) g)
@[simp]
theorem
category_theory.limits.pullback_right_pullback_fst_iso_hom_fst
{C : Type u}
[category_theory.category C]
{W X Y Z : C}
(f : X ⟶ Z)
(g : Y ⟶ Z)
(f' : W ⟶ X)
[category_theory.limits.has_pullback f g]
[category_theory.limits.has_pullback f' category_theory.limits.pullback.fst]
[category_theory.limits.has_pullback (f' ≫ f) g] :
@[simp]
theorem
category_theory.limits.pullback_right_pullback_fst_iso_hom_fst_assoc
{C : Type u}
[category_theory.category C]
{W X Y Z : C}
(f : X ⟶ Z)
(g : Y ⟶ Z)
(f' : W ⟶ X)
[category_theory.limits.has_pullback f g]
[category_theory.limits.has_pullback f' category_theory.limits.pullback.fst]
[category_theory.limits.has_pullback (f' ≫ f) g]
{X' : C}
(f'_1 : W ⟶ X') :
@[simp]
theorem
category_theory.limits.pullback_right_pullback_fst_iso_hom_snd_assoc
{C : Type u}
[category_theory.category C]
{W X Y Z : C}
(f : X ⟶ Z)
(g : Y ⟶ Z)
(f' : W ⟶ X)
[category_theory.limits.has_pullback f g]
[category_theory.limits.has_pullback f' category_theory.limits.pullback.fst]
[category_theory.limits.has_pullback (f' ≫ f) g]
{X' : C}
(f'_1 : Y ⟶ X') :
@[simp]
theorem
category_theory.limits.pullback_right_pullback_fst_iso_hom_snd
{C : Type u}
[category_theory.category C]
{W X Y Z : C}
(f : X ⟶ Z)
(g : Y ⟶ Z)
(f' : W ⟶ X)
[category_theory.limits.has_pullback f g]
[category_theory.limits.has_pullback f' category_theory.limits.pullback.fst]
[category_theory.limits.has_pullback (f' ≫ f) g] :
@[simp]
theorem
category_theory.limits.pullback_right_pullback_fst_iso_inv_fst
{C : Type u}
[category_theory.category C]
{W X Y Z : C}
(f : X ⟶ Z)
(g : Y ⟶ Z)
(f' : W ⟶ X)
[category_theory.limits.has_pullback f g]
[category_theory.limits.has_pullback f' category_theory.limits.pullback.fst]
[category_theory.limits.has_pullback (f' ≫ f) g] :
@[simp]
theorem
category_theory.limits.pullback_right_pullback_fst_iso_inv_fst_assoc
{C : Type u}
[category_theory.category C]
{W X Y Z : C}
(f : X ⟶ Z)
(g : Y ⟶ Z)
(f' : W ⟶ X)
[category_theory.limits.has_pullback f g]
[category_theory.limits.has_pullback f' category_theory.limits.pullback.fst]
[category_theory.limits.has_pullback (f' ≫ f) g]
{X' : C}
(f'_1 : W ⟶ X') :
@[simp]
theorem
category_theory.limits.pullback_right_pullback_fst_iso_inv_snd_snd_assoc
{C : Type u}
[category_theory.category C]
{W X Y Z : C}
(f : X ⟶ Z)
(g : Y ⟶ Z)
(f' : W ⟶ X)
[category_theory.limits.has_pullback f g]
[category_theory.limits.has_pullback f' category_theory.limits.pullback.fst]
[category_theory.limits.has_pullback (f' ≫ f) g]
{X' : C}
(f'_1 : Y ⟶ X') :
@[simp]
theorem
category_theory.limits.pullback_right_pullback_fst_iso_inv_snd_snd
{C : Type u}
[category_theory.category C]
{W X Y Z : C}
(f : X ⟶ Z)
(g : Y ⟶ Z)
(f' : W ⟶ X)
[category_theory.limits.has_pullback f g]
[category_theory.limits.has_pullback f' category_theory.limits.pullback.fst]
[category_theory.limits.has_pullback (f' ≫ f) g] :
@[simp]
theorem
category_theory.limits.pullback_right_pullback_fst_iso_inv_snd_fst_assoc
{C : Type u}
[category_theory.category C]
{W X Y Z : C}
(f : X ⟶ Z)
(g : Y ⟶ Z)
(f' : W ⟶ X)
[category_theory.limits.has_pullback f g]
[category_theory.limits.has_pullback f' category_theory.limits.pullback.fst]
[category_theory.limits.has_pullback (f' ≫ f) g]
{X' : C}
(f'_1 : X ⟶ X') :
@[simp]
theorem
category_theory.limits.pullback_right_pullback_fst_iso_inv_snd_fst
{C : Type u}
[category_theory.category C]
{W X Y Z : C}
(f : X ⟶ Z)
(g : Y ⟶ Z)
(f' : W ⟶ X)
[category_theory.limits.has_pullback f g]
[category_theory.limits.has_pullback f' category_theory.limits.pullback.fst]
[category_theory.limits.has_pullback (f' ≫ f) g] :
noncomputable
def
category_theory.limits.pushout_left_pushout_inr_iso
{C : Type u}
[category_theory.category C]
{W X Y Z : C}
(f : X ⟶ Y)
(g : X ⟶ Z)
(g' : Z ⟶ W)
[category_theory.limits.has_pushout f g]
[category_theory.limits.has_pushout category_theory.limits.pushout.inr g']
[category_theory.limits.has_pushout f (g ≫ g')] :
The canonical isomorphism (Y ⨿[X] Z) ⨿[Z] W ≅ Y ×[X] W
Equations
- category_theory.limits.pushout_left_pushout_inr_iso f g g' = (category_theory.limits.big_square_is_pushout g g' category_theory.limits.pushout.inl category_theory.limits.pushout.inl f category_theory.limits.pushout.inr category_theory.limits.pushout.inr category_theory.limits.pushout.condition _ (category_theory.limits.pushout_is_pushout category_theory.limits.pushout.inr g') (category_theory.limits.pushout_is_pushout f g)).cocone_point_unique_up_to_iso (category_theory.limits.pushout_is_pushout f (g ≫ g'))
@[simp]
theorem
category_theory.limits.inl_pushout_left_pushout_inr_iso_inv
{C : Type u}
[category_theory.category C]
{W X Y Z : C}
(f : X ⟶ Y)
(g : X ⟶ Z)
(g' : Z ⟶ W)
[category_theory.limits.has_pushout f g]
[category_theory.limits.has_pushout category_theory.limits.pushout.inr g']
[category_theory.limits.has_pushout f (g ≫ g')] :
@[simp]
theorem
category_theory.limits.inl_pushout_left_pushout_inr_iso_inv_assoc
{C : Type u}
[category_theory.category C]
{W X Y Z : C}
(f : X ⟶ Y)
(g : X ⟶ Z)
(g' : Z ⟶ W)
[category_theory.limits.has_pushout f g]
[category_theory.limits.has_pushout category_theory.limits.pushout.inr g']
[category_theory.limits.has_pushout f (g ≫ g')]
{X' : C}
(f' : category_theory.limits.pushout category_theory.limits.pushout.inr g' ⟶ X') :
@[simp]
theorem
category_theory.limits.inr_pushout_left_pushout_inr_iso_hom
{C : Type u}
[category_theory.category C]
{W X Y Z : C}
(f : X ⟶ Y)
(g : X ⟶ Z)
(g' : Z ⟶ W)
[category_theory.limits.has_pushout f g]
[category_theory.limits.has_pushout category_theory.limits.pushout.inr g']
[category_theory.limits.has_pushout f (g ≫ g')] :
@[simp]
theorem
category_theory.limits.inr_pushout_left_pushout_inr_iso_hom_assoc
{C : Type u}
[category_theory.category C]
{W X Y Z : C}
(f : X ⟶ Y)
(g : X ⟶ Z)
(g' : Z ⟶ W)
[category_theory.limits.has_pushout f g]
[category_theory.limits.has_pushout category_theory.limits.pushout.inr g']
[category_theory.limits.has_pushout f (g ≫ g')]
{X' : C}
(f' : category_theory.limits.pushout f (g ≫ g') ⟶ X') :
@[simp]
theorem
category_theory.limits.inr_pushout_left_pushout_inr_iso_inv
{C : Type u}
[category_theory.category C]
{W X Y Z : C}
(f : X ⟶ Y)
(g : X ⟶ Z)
(g' : Z ⟶ W)
[category_theory.limits.has_pushout f g]
[category_theory.limits.has_pushout category_theory.limits.pushout.inr g']
[category_theory.limits.has_pushout f (g ≫ g')] :
@[simp]
theorem
category_theory.limits.inr_pushout_left_pushout_inr_iso_inv_assoc
{C : Type u}
[category_theory.category C]
{W X Y Z : C}
(f : X ⟶ Y)
(g : X ⟶ Z)
(g' : Z ⟶ W)
[category_theory.limits.has_pushout f g]
[category_theory.limits.has_pushout category_theory.limits.pushout.inr g']
[category_theory.limits.has_pushout f (g ≫ g')]
{X' : C}
(f' : category_theory.limits.pushout category_theory.limits.pushout.inr g' ⟶ X') :
@[simp]
theorem
category_theory.limits.inl_inl_pushout_left_pushout_inr_iso_hom
{C : Type u}
[category_theory.category C]
{W X Y Z : C}
(f : X ⟶ Y)
(g : X ⟶ Z)
(g' : Z ⟶ W)
[category_theory.limits.has_pushout f g]
[category_theory.limits.has_pushout category_theory.limits.pushout.inr g']
[category_theory.limits.has_pushout f (g ≫ g')] :
@[simp]
theorem
category_theory.limits.inl_inl_pushout_left_pushout_inr_iso_hom_assoc
{C : Type u}
[category_theory.category C]
{W X Y Z : C}
(f : X ⟶ Y)
(g : X ⟶ Z)
(g' : Z ⟶ W)
[category_theory.limits.has_pushout f g]
[category_theory.limits.has_pushout category_theory.limits.pushout.inr g']
[category_theory.limits.has_pushout f (g ≫ g')]
{X' : C}
(f' : category_theory.limits.pushout f (g ≫ g') ⟶ X') :
@[simp]
theorem
category_theory.limits.inr_inl_pushout_left_pushout_inr_iso_hom
{C : Type u}
[category_theory.category C]
{W X Y Z : C}
(f : X ⟶ Y)
(g : X ⟶ Z)
(g' : Z ⟶ W)
[category_theory.limits.has_pushout f g]
[category_theory.limits.has_pushout category_theory.limits.pushout.inr g']
[category_theory.limits.has_pushout f (g ≫ g')] :
@[simp]
theorem
category_theory.limits.inr_inl_pushout_left_pushout_inr_iso_hom_assoc
{C : Type u}
[category_theory.category C]
{W X Y Z : C}
(f : X ⟶ Y)
(g : X ⟶ Z)
(g' : Z ⟶ W)
[category_theory.limits.has_pushout f g]
[category_theory.limits.has_pushout category_theory.limits.pushout.inr g']
[category_theory.limits.has_pushout f (g ≫ g')]
{X' : C}
(f' : category_theory.limits.pushout f (g ≫ g') ⟶ X') :
noncomputable
def
category_theory.limits.pullback_pullback_left_is_pullback
{C : Type u}
[category_theory.category C]
{X₁ X₂ X₃ Y₁ Y₂ : C}
(f₁ : X₁ ⟶ Y₁)
(f₂ : X₂ ⟶ Y₁)
(f₃ : X₂ ⟶ Y₂)
(f₄ : X₃ ⟶ Y₂)
[category_theory.limits.has_pullback f₁ f₂]
[category_theory.limits.has_pullback f₃ f₄]
[category_theory.limits.has_pullback (category_theory.limits.pullback.snd ≫ f₃) f₄] :
(X₁ ×[Y₁] X₂) ×[Y₂] X₃ is the pullback (X₁ ×[Y₁] X₂) ×[X₂] (X₂ ×[Y₂] X₃).
Equations
- category_theory.limits.pullback_pullback_left_is_pullback f₁ f₂ f₃ f₄ = category_theory.limits.left_square_is_pullback (category_theory.limits.pullback.lift (category_theory.limits.pullback.fst ≫ category_theory.limits.pullback.snd) category_theory.limits.pullback.snd _) category_theory.limits.pullback.snd category_theory.limits.pullback.snd f₃ category_theory.limits.pullback.fst category_theory.limits.pullback.fst f₄ _ category_theory.limits.pullback.condition (category_theory.limits.pullback_is_pullback f₃ f₄) (_.mpr (category_theory.limits.pullback_is_pullback (category_theory.limits.pullback.snd ≫ f₃) f₄))
noncomputable
def
category_theory.limits.pullback_assoc_is_pullback
{C : Type u}
[category_theory.category C]
{X₁ X₂ X₃ Y₁ Y₂ : C}
(f₁ : X₁ ⟶ Y₁)
(f₂ : X₂ ⟶ Y₁)
(f₃ : X₂ ⟶ Y₂)
(f₄ : X₃ ⟶ Y₂)
[category_theory.limits.has_pullback f₁ f₂]
[category_theory.limits.has_pullback f₃ f₄]
[category_theory.limits.has_pullback (category_theory.limits.pullback.snd ≫ f₃) f₄] :
category_theory.limits.is_limit (category_theory.limits.pullback_cone.mk (category_theory.limits.pullback.fst ≫ category_theory.limits.pullback.fst) (category_theory.limits.pullback.lift (category_theory.limits.pullback.fst ≫ category_theory.limits.pullback.snd) category_theory.limits.pullback.snd _) _)
(X₁ ×[Y₁] X₂) ×[Y₂] X₃ is the pullback X₁ ×[Y₁] (X₂ ×[Y₂] X₃).
Equations
- category_theory.limits.pullback_assoc_is_pullback f₁ f₂ f₃ f₄ = category_theory.limits.pullback_cone.flip_is_limit (category_theory.limits.big_square_is_pullback category_theory.limits.pullback.fst category_theory.limits.pullback.fst category_theory.limits.pullback.fst f₂ (category_theory.limits.pullback.lift (category_theory.limits.pullback.fst ≫ category_theory.limits.pullback.snd) category_theory.limits.pullback.snd _) category_theory.limits.pullback.snd f₁ _ _ (category_theory.limits.pullback_cone.flip_is_limit (category_theory.limits.pullback_is_pullback f₁ f₂)) (category_theory.limits.pullback_cone.flip_is_limit (category_theory.limits.pullback_pullback_left_is_pullback f₁ f₂ f₃ f₄)))
theorem
category_theory.limits.has_pullback_assoc
{C : Type u}
[category_theory.category C]
{X₁ X₂ X₃ Y₁ Y₂ : C}
(f₁ : X₁ ⟶ Y₁)
(f₂ : X₂ ⟶ Y₁)
(f₃ : X₂ ⟶ Y₂)
(f₄ : X₃ ⟶ Y₂)
[category_theory.limits.has_pullback f₁ f₂]
[category_theory.limits.has_pullback f₃ f₄]
[category_theory.limits.has_pullback (category_theory.limits.pullback.snd ≫ f₃) f₄] :
noncomputable
def
category_theory.limits.pullback_pullback_right_is_pullback
{C : Type u}
[category_theory.category C]
{X₁ X₂ X₃ Y₁ Y₂ : C}
(f₁ : X₁ ⟶ Y₁)
(f₂ : X₂ ⟶ Y₁)
(f₃ : X₂ ⟶ Y₂)
(f₄ : X₃ ⟶ Y₂)
[category_theory.limits.has_pullback f₁ f₂]
[category_theory.limits.has_pullback f₃ f₄]
[category_theory.limits.has_pullback f₁ (category_theory.limits.pullback.fst ≫ f₂)] :
X₁ ×[Y₁] (X₂ ×[Y₂] X₃) is the pullback (X₁ ×[Y₁] X₂) ×[X₂] (X₂ ×[Y₂] X₃).
Equations
- category_theory.limits.pullback_pullback_right_is_pullback f₁ f₂ f₃ f₄ = category_theory.limits.pullback_cone.flip_is_limit (category_theory.limits.left_square_is_pullback (category_theory.limits.pullback.lift category_theory.limits.pullback.fst (category_theory.limits.pullback.snd ≫ category_theory.limits.pullback.fst) _) category_theory.limits.pullback.fst category_theory.limits.pullback.fst f₂ category_theory.limits.pullback.snd category_theory.limits.pullback.snd f₁ _ _ (category_theory.limits.pullback_cone.flip_is_limit (category_theory.limits.pullback_is_pullback f₁ f₂)) (category_theory.limits.pullback_cone.flip_is_limit (_.mpr (category_theory.limits.pullback_is_pullback f₁ (category_theory.limits.pullback.fst ≫ f₂)))))
noncomputable
def
category_theory.limits.pullback_assoc_symm_is_pullback
{C : Type u}
[category_theory.category C]
{X₁ X₂ X₃ Y₁ Y₂ : C}
(f₁ : X₁ ⟶ Y₁)
(f₂ : X₂ ⟶ Y₁)
(f₃ : X₂ ⟶ Y₂)
(f₄ : X₃ ⟶ Y₂)
[category_theory.limits.has_pullback f₁ f₂]
[category_theory.limits.has_pullback f₃ f₄]
[category_theory.limits.has_pullback f₁ (category_theory.limits.pullback.fst ≫ f₂)] :
category_theory.limits.is_limit (category_theory.limits.pullback_cone.mk (category_theory.limits.pullback.lift category_theory.limits.pullback.fst (category_theory.limits.pullback.snd ≫ category_theory.limits.pullback.fst) _) (category_theory.limits.pullback.snd ≫ category_theory.limits.pullback.snd) _)
X₁ ×[Y₁] (X₂ ×[Y₂] X₃) is the pullback (X₁ ×[Y₁] X₂) ×[Y₂] X₃.
Equations
- category_theory.limits.pullback_assoc_symm_is_pullback f₁ f₂ f₃ f₄ = category_theory.limits.big_square_is_pullback category_theory.limits.pullback.snd category_theory.limits.pullback.snd category_theory.limits.pullback.snd f₃ (category_theory.limits.pullback.lift category_theory.limits.pullback.fst (category_theory.limits.pullback.snd ≫ category_theory.limits.pullback.fst) _) category_theory.limits.pullback.fst f₄ _ category_theory.limits.pullback.condition (category_theory.limits.pullback_is_pullback f₃ f₄) (category_theory.limits.pullback_pullback_right_is_pullback f₁ f₂ f₃ f₄)
theorem
category_theory.limits.has_pullback_assoc_symm
{C : Type u}
[category_theory.category C]
{X₁ X₂ X₃ Y₁ Y₂ : C}
(f₁ : X₁ ⟶ Y₁)
(f₂ : X₂ ⟶ Y₁)
(f₃ : X₂ ⟶ Y₂)
(f₄ : X₃ ⟶ Y₂)
[category_theory.limits.has_pullback f₁ f₂]
[category_theory.limits.has_pullback f₃ f₄]
[category_theory.limits.has_pullback f₁ (category_theory.limits.pullback.fst ≫ f₂)] :
noncomputable
def
category_theory.limits.pullback_assoc
{C : Type u}
[category_theory.category C]
{X₁ X₂ X₃ Y₁ Y₂ : C}
(f₁ : X₁ ⟶ Y₁)
(f₂ : X₂ ⟶ Y₁)
(f₃ : X₂ ⟶ Y₂)
(f₄ : X₃ ⟶ Y₂)
[category_theory.limits.has_pullback f₁ f₂]
[category_theory.limits.has_pullback f₃ f₄]
[category_theory.limits.has_pullback (category_theory.limits.pullback.snd ≫ f₃) f₄]
[category_theory.limits.has_pullback f₁ (category_theory.limits.pullback.fst ≫ f₂)] :
The canonical isomorphism (X₁ ×[Y₁] X₂) ×[Y₂] X₃ ≅ X₁ ×[Y₁] (X₂ ×[Y₂] X₃).
Equations
@[simp]
theorem
category_theory.limits.pullback_assoc_inv_fst_fst_assoc
{C : Type u}
[category_theory.category C]
{X₁ X₂ X₃ Y₁ Y₂ : C}
(f₁ : X₁ ⟶ Y₁)
(f₂ : X₂ ⟶ Y₁)
(f₃ : X₂ ⟶ Y₂)
(f₄ : X₃ ⟶ Y₂)
[category_theory.limits.has_pullback f₁ f₂]
[category_theory.limits.has_pullback f₃ f₄]
[category_theory.limits.has_pullback (category_theory.limits.pullback.snd ≫ f₃) f₄]
[category_theory.limits.has_pullback f₁ (category_theory.limits.pullback.fst ≫ f₂)]
{X' : C}
(f' : X₁ ⟶ X') :
@[simp]
theorem
category_theory.limits.pullback_assoc_inv_fst_fst
{C : Type u}
[category_theory.category C]
{X₁ X₂ X₃ Y₁ Y₂ : C}
(f₁ : X₁ ⟶ Y₁)
(f₂ : X₂ ⟶ Y₁)
(f₃ : X₂ ⟶ Y₂)
(f₄ : X₃ ⟶ Y₂)
[category_theory.limits.has_pullback f₁ f₂]
[category_theory.limits.has_pullback f₃ f₄]
[category_theory.limits.has_pullback (category_theory.limits.pullback.snd ≫ f₃) f₄]
[category_theory.limits.has_pullback f₁ (category_theory.limits.pullback.fst ≫ f₂)] :
@[simp]
theorem
category_theory.limits.pullback_assoc_hom_fst_assoc
{C : Type u}
[category_theory.category C]
{X₁ X₂ X₃ Y₁ Y₂ : C}
(f₁ : X₁ ⟶ Y₁)
(f₂ : X₂ ⟶ Y₁)
(f₃ : X₂ ⟶ Y₂)
(f₄ : X₃ ⟶ Y₂)
[category_theory.limits.has_pullback f₁ f₂]
[category_theory.limits.has_pullback f₃ f₄]
[category_theory.limits.has_pullback (category_theory.limits.pullback.snd ≫ f₃) f₄]
[category_theory.limits.has_pullback f₁ (category_theory.limits.pullback.fst ≫ f₂)]
{X' : C}
(f' : X₁ ⟶ X') :
@[simp]
theorem
category_theory.limits.pullback_assoc_hom_fst
{C : Type u}
[category_theory.category C]
{X₁ X₂ X₃ Y₁ Y₂ : C}
(f₁ : X₁ ⟶ Y₁)
(f₂ : X₂ ⟶ Y₁)
(f₃ : X₂ ⟶ Y₂)
(f₄ : X₃ ⟶ Y₂)
[category_theory.limits.has_pullback f₁ f₂]
[category_theory.limits.has_pullback f₃ f₄]
[category_theory.limits.has_pullback (category_theory.limits.pullback.snd ≫ f₃) f₄]
[category_theory.limits.has_pullback f₁ (category_theory.limits.pullback.fst ≫ f₂)] :
@[simp]
theorem
category_theory.limits.pullback_assoc_hom_snd_fst
{C : Type u}
[category_theory.category C]
{X₁ X₂ X₃ Y₁ Y₂ : C}
(f₁ : X₁ ⟶ Y₁)
(f₂ : X₂ ⟶ Y₁)
(f₃ : X₂ ⟶ Y₂)
(f₄ : X₃ ⟶ Y₂)
[category_theory.limits.has_pullback f₁ f₂]
[category_theory.limits.has_pullback f₃ f₄]
[category_theory.limits.has_pullback (category_theory.limits.pullback.snd ≫ f₃) f₄]
[category_theory.limits.has_pullback f₁ (category_theory.limits.pullback.fst ≫ f₂)] :
@[simp]
theorem
category_theory.limits.pullback_assoc_hom_snd_fst_assoc
{C : Type u}
[category_theory.category C]
{X₁ X₂ X₃ Y₁ Y₂ : C}
(f₁ : X₁ ⟶ Y₁)
(f₂ : X₂ ⟶ Y₁)
(f₃ : X₂ ⟶ Y₂)
(f₄ : X₃ ⟶ Y₂)
[category_theory.limits.has_pullback f₁ f₂]
[category_theory.limits.has_pullback f₃ f₄]
[category_theory.limits.has_pullback (category_theory.limits.pullback.snd ≫ f₃) f₄]
[category_theory.limits.has_pullback f₁ (category_theory.limits.pullback.fst ≫ f₂)]
{X' : C}
(f' : X₂ ⟶ X') :
@[simp]
theorem
category_theory.limits.pullback_assoc_hom_snd_snd
{C : Type u}
[category_theory.category C]
{X₁ X₂ X₃ Y₁ Y₂ : C}
(f₁ : X₁ ⟶ Y₁)
(f₂ : X₂ ⟶ Y₁)
(f₃ : X₂ ⟶ Y₂)
(f₄ : X₃ ⟶ Y₂)
[category_theory.limits.has_pullback f₁ f₂]
[category_theory.limits.has_pullback f₃ f₄]
[category_theory.limits.has_pullback (category_theory.limits.pullback.snd ≫ f₃) f₄]
[category_theory.limits.has_pullback f₁ (category_theory.limits.pullback.fst ≫ f₂)] :
@[simp]
theorem
category_theory.limits.pullback_assoc_hom_snd_snd_assoc
{C : Type u}
[category_theory.category C]
{X₁ X₂ X₃ Y₁ Y₂ : C}
(f₁ : X₁ ⟶ Y₁)
(f₂ : X₂ ⟶ Y₁)
(f₃ : X₂ ⟶ Y₂)
(f₄ : X₃ ⟶ Y₂)
[category_theory.limits.has_pullback f₁ f₂]
[category_theory.limits.has_pullback f₃ f₄]
[category_theory.limits.has_pullback (category_theory.limits.pullback.snd ≫ f₃) f₄]
[category_theory.limits.has_pullback f₁ (category_theory.limits.pullback.fst ≫ f₂)]
{X' : C}
(f' : X₃ ⟶ X') :
@[simp]
theorem
category_theory.limits.pullback_assoc_inv_fst_snd
{C : Type u}
[category_theory.category C]
{X₁ X₂ X₃ Y₁ Y₂ : C}
(f₁ : X₁ ⟶ Y₁)
(f₂ : X₂ ⟶ Y₁)
(f₃ : X₂ ⟶ Y₂)
(f₄ : X₃ ⟶ Y₂)
[category_theory.limits.has_pullback f₁ f₂]
[category_theory.limits.has_pullback f₃ f₄]
[category_theory.limits.has_pullback (category_theory.limits.pullback.snd ≫ f₃) f₄]
[category_theory.limits.has_pullback f₁ (category_theory.limits.pullback.fst ≫ f₂)] :
@[simp]
theorem
category_theory.limits.pullback_assoc_inv_fst_snd_assoc
{C : Type u}
[category_theory.category C]
{X₁ X₂ X₃ Y₁ Y₂ : C}
(f₁ : X₁ ⟶ Y₁)
(f₂ : X₂ ⟶ Y₁)
(f₃ : X₂ ⟶ Y₂)
(f₄ : X₃ ⟶ Y₂)
[category_theory.limits.has_pullback f₁ f₂]
[category_theory.limits.has_pullback f₃ f₄]
[category_theory.limits.has_pullback (category_theory.limits.pullback.snd ≫ f₃) f₄]
[category_theory.limits.has_pullback f₁ (category_theory.limits.pullback.fst ≫ f₂)]
{X' : C}
(f' : X₂ ⟶ X') :
@[simp]
theorem
category_theory.limits.pullback_assoc_inv_snd
{C : Type u}
[category_theory.category C]
{X₁ X₂ X₃ Y₁ Y₂ : C}
(f₁ : X₁ ⟶ Y₁)
(f₂ : X₂ ⟶ Y₁)
(f₃ : X₂ ⟶ Y₂)
(f₄ : X₃ ⟶ Y₂)
[category_theory.limits.has_pullback f₁ f₂]
[category_theory.limits.has_pullback f₃ f₄]
[category_theory.limits.has_pullback (category_theory.limits.pullback.snd ≫ f₃) f₄]
[category_theory.limits.has_pullback f₁ (category_theory.limits.pullback.fst ≫ f₂)] :
@[simp]
theorem
category_theory.limits.pullback_assoc_inv_snd_assoc
{C : Type u}
[category_theory.category C]
{X₁ X₂ X₃ Y₁ Y₂ : C}
(f₁ : X₁ ⟶ Y₁)
(f₂ : X₂ ⟶ Y₁)
(f₃ : X₂ ⟶ Y₂)
(f₄ : X₃ ⟶ Y₂)
[category_theory.limits.has_pullback f₁ f₂]
[category_theory.limits.has_pullback f₃ f₄]
[category_theory.limits.has_pullback (category_theory.limits.pullback.snd ≫ f₃) f₄]
[category_theory.limits.has_pullback f₁ (category_theory.limits.pullback.fst ≫ f₂)]
{X' : C}
(f' : X₃ ⟶ X') :
noncomputable
def
category_theory.limits.pushout_pushout_left_is_pushout
{C : Type u}
[category_theory.category C]
{X₁ X₂ X₃ Z₁ Z₂ : C}
(g₁ : Z₁ ⟶ X₁)
(g₂ : Z₁ ⟶ X₂)
(g₃ : Z₂ ⟶ X₂)
(g₄ : Z₂ ⟶ X₃)
[category_theory.limits.has_pushout g₁ g₂]
[category_theory.limits.has_pushout g₃ g₄]
[category_theory.limits.has_pushout (g₃ ≫ category_theory.limits.pushout.inr) g₄] :
(X₁ ⨿[Z₁] X₂) ⨿[Z₂] X₃ is the pushout (X₁ ⨿[Z₁] X₂) ×[X₂] (X₂ ⨿[Z₂] X₃).
Equations
- category_theory.limits.pushout_pushout_left_is_pushout g₁ g₂ g₃ g₄ = category_theory.limits.pushout_cocone.flip_is_colimit (category_theory.limits.right_square_is_pushout g₃ category_theory.limits.pushout.inr category_theory.limits.pushout.inr (category_theory.limits.pushout.desc (category_theory.limits.pushout.inr ≫ category_theory.limits.pushout.inl) category_theory.limits.pushout.inr _) g₄ category_theory.limits.pushout.inl category_theory.limits.pushout.inl _ _ (category_theory.limits.pushout_cocone.flip_is_colimit (category_theory.limits.pushout_is_pushout g₃ g₄)) (category_theory.limits.pushout_cocone.flip_is_colimit (_.mpr (category_theory.limits.pushout_is_pushout (g₃ ≫ category_theory.limits.pushout.inr) g₄))))
noncomputable
def
category_theory.limits.pushout_assoc_is_pushout
{C : Type u}
[category_theory.category C]
{X₁ X₂ X₃ Z₁ Z₂ : C}
(g₁ : Z₁ ⟶ X₁)
(g₂ : Z₁ ⟶ X₂)
(g₃ : Z₂ ⟶ X₂)
(g₄ : Z₂ ⟶ X₃)
[category_theory.limits.has_pushout g₁ g₂]
[category_theory.limits.has_pushout g₃ g₄]
[category_theory.limits.has_pushout (g₃ ≫ category_theory.limits.pushout.inr) g₄] :
category_theory.limits.is_colimit (category_theory.limits.pushout_cocone.mk (category_theory.limits.pushout.inl ≫ category_theory.limits.pushout.inl) (category_theory.limits.pushout.desc (category_theory.limits.pushout.inr ≫ category_theory.limits.pushout.inl) category_theory.limits.pushout.inr _) _)
(X₁ ⨿[Z₁] X₂) ⨿[Z₂] X₃ is the pushout X₁ ⨿[Z₁] (X₂ ⨿[Z₂] X₃).
Equations
- category_theory.limits.pushout_assoc_is_pushout g₁ g₂ g₃ g₄ = category_theory.limits.big_square_is_pushout g₂ category_theory.limits.pushout.inl category_theory.limits.pushout.inl category_theory.limits.pushout.inl g₁ category_theory.limits.pushout.inr (category_theory.limits.pushout.desc (category_theory.limits.pushout.inr ≫ category_theory.limits.pushout.inl) category_theory.limits.pushout.inr _) category_theory.limits.pushout.condition _ (category_theory.limits.pushout_pushout_left_is_pushout g₁ g₂ g₃ g₄) (category_theory.limits.pushout_is_pushout g₁ g₂)
theorem
category_theory.limits.has_pushout_assoc
{C : Type u}
[category_theory.category C]
{X₁ X₂ X₃ Z₁ Z₂ : C}
(g₁ : Z₁ ⟶ X₁)
(g₂ : Z₁ ⟶ X₂)
(g₃ : Z₂ ⟶ X₂)
(g₄ : Z₂ ⟶ X₃)
[category_theory.limits.has_pushout g₁ g₂]
[category_theory.limits.has_pushout g₃ g₄]
[category_theory.limits.has_pushout (g₃ ≫ category_theory.limits.pushout.inr) g₄] :
noncomputable
def
category_theory.limits.pushout_pushout_right_is_pushout
{C : Type u}
[category_theory.category C]
{X₁ X₂ X₃ Z₁ Z₂ : C}
(g₁ : Z₁ ⟶ X₁)
(g₂ : Z₁ ⟶ X₂)
(g₃ : Z₂ ⟶ X₂)
(g₄ : Z₂ ⟶ X₃)
[category_theory.limits.has_pushout g₁ g₂]
[category_theory.limits.has_pushout g₃ g₄]
[category_theory.limits.has_pushout g₁ (g₂ ≫ category_theory.limits.pushout.inl)] :
X₁ ⨿[Z₁] (X₂ ⨿[Z₂] X₃) is the pushout (X₁ ⨿[Z₁] X₂) ×[X₂] (X₂ ⨿[Z₂] X₃).
Equations
- category_theory.limits.pushout_pushout_right_is_pushout g₁ g₂ g₃ g₄ = category_theory.limits.right_square_is_pushout g₂ category_theory.limits.pushout.inl category_theory.limits.pushout.inl (category_theory.limits.pushout.desc category_theory.limits.pushout.inl (category_theory.limits.pushout.inl ≫ category_theory.limits.pushout.inr) _) g₁ category_theory.limits.pushout.inr category_theory.limits.pushout.inr category_theory.limits.pushout.condition _ (category_theory.limits.pushout_is_pushout g₁ g₂) (_.mpr (category_theory.limits.pushout_is_pushout g₁ (g₂ ≫ category_theory.limits.pushout.inl)))
noncomputable
def
category_theory.limits.pushout_assoc_symm_is_pushout
{C : Type u}
[category_theory.category C]
{X₁ X₂ X₃ Z₁ Z₂ : C}
(g₁ : Z₁ ⟶ X₁)
(g₂ : Z₁ ⟶ X₂)
(g₃ : Z₂ ⟶ X₂)
(g₄ : Z₂ ⟶ X₃)
[category_theory.limits.has_pushout g₁ g₂]
[category_theory.limits.has_pushout g₃ g₄]
[category_theory.limits.has_pushout g₁ (g₂ ≫ category_theory.limits.pushout.inl)] :
category_theory.limits.is_colimit (category_theory.limits.pushout_cocone.mk (category_theory.limits.pushout.desc category_theory.limits.pushout.inl (category_theory.limits.pushout.inl ≫ category_theory.limits.pushout.inr) _) (category_theory.limits.pushout.inr ≫ category_theory.limits.pushout.inr) _)
X₁ ⨿[Z₁] (X₂ ⨿[Z₂] X₃) is the pushout (X₁ ⨿[Z₁] X₂) ⨿[Z₂] X₃.
Equations
- category_theory.limits.pushout_assoc_symm_is_pushout g₁ g₂ g₃ g₄ = category_theory.limits.pushout_cocone.flip_is_colimit (category_theory.limits.big_square_is_pushout g₃ category_theory.limits.pushout.inr category_theory.limits.pushout.inr category_theory.limits.pushout.inr g₄ category_theory.limits.pushout.inl (category_theory.limits.pushout.desc category_theory.limits.pushout.inl (category_theory.limits.pushout.inl ≫ category_theory.limits.pushout.inr) _) _ _ (category_theory.limits.pushout_cocone.flip_is_colimit (category_theory.limits.pushout_pushout_right_is_pushout g₁ g₂ g₃ g₄)) (category_theory.limits.pushout_cocone.flip_is_colimit (category_theory.limits.pushout_is_pushout g₃ g₄)))
theorem
category_theory.limits.has_pushout_assoc_symm
{C : Type u}
[category_theory.category C]
{X₁ X₂ X₃ Z₁ Z₂ : C}
(g₁ : Z₁ ⟶ X₁)
(g₂ : Z₁ ⟶ X₂)
(g₃ : Z₂ ⟶ X₂)
(g₄ : Z₂ ⟶ X₃)
[category_theory.limits.has_pushout g₁ g₂]
[category_theory.limits.has_pushout g₃ g₄]
[category_theory.limits.has_pushout g₁ (g₂ ≫ category_theory.limits.pushout.inl)] :
noncomputable
def
category_theory.limits.pushout_assoc
{C : Type u}
[category_theory.category C]
{X₁ X₂ X₃ Z₁ Z₂ : C}
(g₁ : Z₁ ⟶ X₁)
(g₂ : Z₁ ⟶ X₂)
(g₃ : Z₂ ⟶ X₂)
(g₄ : Z₂ ⟶ X₃)
[category_theory.limits.has_pushout g₁ g₂]
[category_theory.limits.has_pushout g₃ g₄]
[category_theory.limits.has_pushout (g₃ ≫ category_theory.limits.pushout.inr) g₄]
[category_theory.limits.has_pushout g₁ (g₂ ≫ category_theory.limits.pushout.inl)] :
The canonical isomorphism (X₁ ⨿[Z₁] X₂) ⨿[Z₂] X₃ ≅ X₁ ⨿[Z₁] (X₂ ⨿[Z₂] X₃).
Equations
- category_theory.limits.pushout_assoc g₁ g₂ g₃ g₄ = (category_theory.limits.pushout_pushout_left_is_pushout g₁ g₂ g₃ g₄).cocone_point_unique_up_to_iso (category_theory.limits.pushout_pushout_right_is_pushout g₁ g₂ g₃ g₄)
@[simp]
theorem
category_theory.limits.inl_inl_pushout_assoc_hom_assoc
{C : Type u}
[category_theory.category C]
{X₁ X₂ X₃ Z₁ Z₂ : C}
(g₁ : Z₁ ⟶ X₁)
(g₂ : Z₁ ⟶ X₂)
(g₃ : Z₂ ⟶ X₂)
(g₄ : Z₂ ⟶ X₃)
[category_theory.limits.has_pushout g₁ g₂]
[category_theory.limits.has_pushout g₃ g₄]
[category_theory.limits.has_pushout (g₃ ≫ category_theory.limits.pushout.inr) g₄]
[category_theory.limits.has_pushout g₁ (g₂ ≫ category_theory.limits.pushout.inl)]
{X' : C}
(f' : category_theory.limits.pushout g₁ (g₂ ≫ category_theory.limits.pushout.inl) ⟶ X') :
@[simp]
theorem
category_theory.limits.inl_inl_pushout_assoc_hom
{C : Type u}
[category_theory.category C]
{X₁ X₂ X₃ Z₁ Z₂ : C}
(g₁ : Z₁ ⟶ X₁)
(g₂ : Z₁ ⟶ X₂)
(g₃ : Z₂ ⟶ X₂)
(g₄ : Z₂ ⟶ X₃)
[category_theory.limits.has_pushout g₁ g₂]
[category_theory.limits.has_pushout g₃ g₄]
[category_theory.limits.has_pushout (g₃ ≫ category_theory.limits.pushout.inr) g₄]
[category_theory.limits.has_pushout g₁ (g₂ ≫ category_theory.limits.pushout.inl)] :
@[simp]
theorem
category_theory.limits.inr_inl_pushout_assoc_hom
{C : Type u}
[category_theory.category C]
{X₁ X₂ X₃ Z₁ Z₂ : C}
(g₁ : Z₁ ⟶ X₁)
(g₂ : Z₁ ⟶ X₂)
(g₃ : Z₂ ⟶ X₂)
(g₄ : Z₂ ⟶ X₃)
[category_theory.limits.has_pushout g₁ g₂]
[category_theory.limits.has_pushout g₃ g₄]
[category_theory.limits.has_pushout (g₃ ≫ category_theory.limits.pushout.inr) g₄]
[category_theory.limits.has_pushout g₁ (g₂ ≫ category_theory.limits.pushout.inl)] :
@[simp]
theorem
category_theory.limits.inr_inl_pushout_assoc_hom_assoc
{C : Type u}
[category_theory.category C]
{X₁ X₂ X₃ Z₁ Z₂ : C}
(g₁ : Z₁ ⟶ X₁)
(g₂ : Z₁ ⟶ X₂)
(g₃ : Z₂ ⟶ X₂)
(g₄ : Z₂ ⟶ X₃)
[category_theory.limits.has_pushout g₁ g₂]
[category_theory.limits.has_pushout g₃ g₄]
[category_theory.limits.has_pushout (g₃ ≫ category_theory.limits.pushout.inr) g₄]
[category_theory.limits.has_pushout g₁ (g₂ ≫ category_theory.limits.pushout.inl)]
{X' : C}
(f' : category_theory.limits.pushout g₁ (g₂ ≫ category_theory.limits.pushout.inl) ⟶ X') :
@[simp]
theorem
category_theory.limits.inr_inr_pushout_assoc_inv_assoc
{C : Type u}
[category_theory.category C]
{X₁ X₂ X₃ Z₁ Z₂ : C}
(g₁ : Z₁ ⟶ X₁)
(g₂ : Z₁ ⟶ X₂)
(g₃ : Z₂ ⟶ X₂)
(g₄ : Z₂ ⟶ X₃)
[category_theory.limits.has_pushout g₁ g₂]
[category_theory.limits.has_pushout g₃ g₄]
[category_theory.limits.has_pushout (g₃ ≫ category_theory.limits.pushout.inr) g₄]
[category_theory.limits.has_pushout g₁ (g₂ ≫ category_theory.limits.pushout.inl)]
{X' : C}
(f' : category_theory.limits.pushout (g₃ ≫ category_theory.limits.pushout.inr) g₄ ⟶ X') :
@[simp]
theorem
category_theory.limits.inr_inr_pushout_assoc_inv
{C : Type u}
[category_theory.category C]
{X₁ X₂ X₃ Z₁ Z₂ : C}
(g₁ : Z₁ ⟶ X₁)
(g₂ : Z₁ ⟶ X₂)
(g₃ : Z₂ ⟶ X₂)
(g₄ : Z₂ ⟶ X₃)
[category_theory.limits.has_pushout g₁ g₂]
[category_theory.limits.has_pushout g₃ g₄]
[category_theory.limits.has_pushout (g₃ ≫ category_theory.limits.pushout.inr) g₄]
[category_theory.limits.has_pushout g₁ (g₂ ≫ category_theory.limits.pushout.inl)] :
@[simp]
theorem
category_theory.limits.inl_pushout_assoc_inv
{C : Type u}
[category_theory.category C]
{X₁ X₂ X₃ Z₁ Z₂ : C}
(g₁ : Z₁ ⟶ X₁)
(g₂ : Z₁ ⟶ X₂)
(g₃ : Z₂ ⟶ X₂)
(g₄ : Z₂ ⟶ X₃)
[category_theory.limits.has_pushout g₁ g₂]
[category_theory.limits.has_pushout g₃ g₄]
[category_theory.limits.has_pushout (g₃ ≫ category_theory.limits.pushout.inr) g₄]
[category_theory.limits.has_pushout g₁ (g₂ ≫ category_theory.limits.pushout.inl)] :
@[simp]
theorem
category_theory.limits.inl_pushout_assoc_inv_assoc
{C : Type u}
[category_theory.category C]
{X₁ X₂ X₃ Z₁ Z₂ : C}
(g₁ : Z₁ ⟶ X₁)
(g₂ : Z₁ ⟶ X₂)
(g₃ : Z₂ ⟶ X₂)
(g₄ : Z₂ ⟶ X₃)
[category_theory.limits.has_pushout g₁ g₂]
[category_theory.limits.has_pushout g₃ g₄]
[category_theory.limits.has_pushout (g₃ ≫ category_theory.limits.pushout.inr) g₄]
[category_theory.limits.has_pushout g₁ (g₂ ≫ category_theory.limits.pushout.inl)]
{X' : C}
(f' : category_theory.limits.pushout (g₃ ≫ category_theory.limits.pushout.inr) g₄ ⟶ X') :
@[simp]
theorem
category_theory.limits.inl_inr_pushout_assoc_inv_assoc
{C : Type u}
[category_theory.category C]
{X₁ X₂ X₃ Z₁ Z₂ : C}
(g₁ : Z₁ ⟶ X₁)
(g₂ : Z₁ ⟶ X₂)
(g₃ : Z₂ ⟶ X₂)
(g₄ : Z₂ ⟶ X₃)
[category_theory.limits.has_pushout g₁ g₂]
[category_theory.limits.has_pushout g₃ g₄]
[category_theory.limits.has_pushout (g₃ ≫ category_theory.limits.pushout.inr) g₄]
[category_theory.limits.has_pushout g₁ (g₂ ≫ category_theory.limits.pushout.inl)]
{X' : C}
(f' : category_theory.limits.pushout (g₃ ≫ category_theory.limits.pushout.inr) g₄ ⟶ X') :
@[simp]
theorem
category_theory.limits.inl_inr_pushout_assoc_inv
{C : Type u}
[category_theory.category C]
{X₁ X₂ X₃ Z₁ Z₂ : C}
(g₁ : Z₁ ⟶ X₁)
(g₂ : Z₁ ⟶ X₂)
(g₃ : Z₂ ⟶ X₂)
(g₄ : Z₂ ⟶ X₃)
[category_theory.limits.has_pushout g₁ g₂]
[category_theory.limits.has_pushout g₃ g₄]
[category_theory.limits.has_pushout (g₃ ≫ category_theory.limits.pushout.inr) g₄]
[category_theory.limits.has_pushout g₁ (g₂ ≫ category_theory.limits.pushout.inl)] :
@[simp]
theorem
category_theory.limits.inr_pushout_assoc_hom_assoc
{C : Type u}
[category_theory.category C]
{X₁ X₂ X₃ Z₁ Z₂ : C}
(g₁ : Z₁ ⟶ X₁)
(g₂ : Z₁ ⟶ X₂)
(g₃ : Z₂ ⟶ X₂)
(g₄ : Z₂ ⟶ X₃)
[category_theory.limits.has_pushout g₁ g₂]
[category_theory.limits.has_pushout g₃ g₄]
[category_theory.limits.has_pushout (g₃ ≫ category_theory.limits.pushout.inr) g₄]
[category_theory.limits.has_pushout g₁ (g₂ ≫ category_theory.limits.pushout.inl)]
{X' : C}
(f' : category_theory.limits.pushout g₁ (g₂ ≫ category_theory.limits.pushout.inl) ⟶ X') :
@[simp]
theorem
category_theory.limits.inr_pushout_assoc_hom
{C : Type u}
[category_theory.category C]
{X₁ X₂ X₃ Z₁ Z₂ : C}
(g₁ : Z₁ ⟶ X₁)
(g₂ : Z₁ ⟶ X₂)
(g₃ : Z₂ ⟶ X₂)
(g₄ : Z₂ ⟶ X₃)
[category_theory.limits.has_pushout g₁ g₂]
[category_theory.limits.has_pushout g₃ g₄]
[category_theory.limits.has_pushout (g₃ ≫ category_theory.limits.pushout.inr) g₄]
[category_theory.limits.has_pushout g₁ (g₂ ≫ category_theory.limits.pushout.inl)] :
@[reducible]
has_pullbacks represents a choice of pullback for every pair of morphisms
@[reducible]
has_pushouts represents a choice of pushout for every pair of morphisms
theorem
category_theory.limits.has_pullbacks_of_has_limit_cospan
(C : Type u)
[category_theory.category C]
[∀ {X Y Z : C} {f : X ⟶ Z} {g : Y ⟶ Z}, category_theory.limits.has_limit (category_theory.limits.cospan f g)] :
If C has all limits of diagrams cospan f g, then it has all pullbacks
theorem
category_theory.limits.has_pushouts_of_has_colimit_span
(C : Type u)
[category_theory.category C]
[∀ {X Y Z : C} {f : X ⟶ Y} {g : X ⟶ Z}, category_theory.limits.has_colimit (category_theory.limits.span f g)] :
If C has all colimits of diagrams span f g, then it has all pushouts
@[simp]
The duality equivalence walking_spanᵒᵖ ≌ walking_cospan
@[simp]
The duality equivalence walking_cospanᵒᵖ ≌ walking_span
@[simp]
@[simp]
@[protected, instance]
def
category_theory.limits.has_pullbacks_of_has_wide_pullbacks
(C : Type u)
[category_theory.category C]
[category_theory.limits.has_wide_pullbacks C] :
Having wide pullback at any universe level implies having binary pullbacks.
@[simp]
theorem
category_theory.limits.base_change_obj_left
{C : Type u}
[category_theory.category C]
[category_theory.limits.has_pullbacks C]
{X Y : C}
(f : X ⟶ Y)
(g : category_theory.over Y) :
@[simp]
theorem
category_theory.limits.base_change_obj_hom
{C : Type u}
[category_theory.category C]
[category_theory.limits.has_pullbacks C]
{X Y : C}
(f : X ⟶ Y)
(g : category_theory.over Y) :
noncomputable
def
category_theory.limits.base_change
{C : Type u}
[category_theory.category C]
[category_theory.limits.has_pullbacks C]
{X 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
- category_theory.limits.base_change f = {obj := λ (g : category_theory.over Y), category_theory.over.mk category_theory.limits.pullback.snd, map := λ (g₁ g₂ : category_theory.over Y) (i : g₁ ⟶ g₂), category_theory.over.hom_mk (category_theory.limits.pullback.map g₁.hom f g₂.hom f i.left (𝟙 X) (𝟙 ((category_theory.functor.from_punit Y).obj g₁.right)) _ _) _, map_id' := _, map_comp' := _}
@[simp]
theorem
category_theory.limits.base_change_map_left
{C : Type u}
[category_theory.category C]
[category_theory.limits.has_pullbacks C]
{X Y : C}
(f : X ⟶ Y)
(g₁ g₂ : category_theory.over Y)
(i : g₁ ⟶ g₂) :
((category_theory.limits.base_change f).map i).left = category_theory.limits.pullback.map g₁.hom f g₂.hom f i.left (𝟙 X) (𝟙 Y) _ _