Pullbacks #
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 #
The type of objects for the diagram indexing a pullback, defined as a special case of
wide_pullback_shape.
The left point of the walking cospan.
The right point of the walking cospan.
The central point of the walking cospan.
The type of objects for the diagram indexing a pushout, defined as a special case of
wide_pushout_shape.
The left point of the walking span.
The right point of the walking span.
The central point of the walking span.
The type of arrows for the diagram indexing a pullback.
The left arrow of the walking cospan.
The right arrow of the walking cospan.
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]
The type of arrows for the diagram indexing a pushout.
The left arrow of the walking span.
The right arrow of the walking span.
The identity arrows of the walking span.
@[protected, instance]
The functor between two walking_cospans in different universes.
Equations
- category_theory.limits.walking_cospan_functor = {obj := λ (ᾰ : category_theory.limits.walking_cospan), option.cases_on ᾰ category_theory.limits.walking_cospan.one (λ (ᾰ : category_theory.limits.walking_pair), ᾰ.cases_on category_theory.limits.walking_cospan.left category_theory.limits.walking_cospan.right), map := λ (X Y : category_theory.limits.walking_cospan) (ᾰ : X ⟶ Y), category_theory.limits.wide_pullback_shape.hom.cases_on ᾰ (λ (ᾰ_1 : category_theory.limits.wide_pullback_shape category_theory.limits.walking_pair) (H_1 : X = ᾰ_1), eq.rec (λ (H_2 : Y = X), eq.rec (λ (ᾰ : X ⟶ X) (H_3 : ᾰ == category_theory.limits.wide_pullback_shape.hom.id X), eq.rec (category_theory.limits.walking_cospan.hom.id (option.cases_on X category_theory.limits.walking_cospan.one (λ (ᾰ : category_theory.limits.walking_pair), ᾰ.cases_on category_theory.limits.walking_cospan.left category_theory.limits.walking_cospan.right))) _) _ ᾰ) H_1) (λ (ᾰ_1 : category_theory.limits.walking_pair) (H_1 : X = some ᾰ_1), eq.rec (λ (ᾰ : some ᾰ_1 ⟶ Y) (H_2 : Y = none), eq.rec (λ (ᾰ : some ᾰ_1 ⟶ none) (H_3 : ᾰ == category_theory.limits.wide_pullback_shape.hom.term ᾰ_1), eq.rec (ᾰ_1.cases_on category_theory.limits.walking_cospan.hom.inl category_theory.limits.walking_cospan.hom.inr) _) _ ᾰ) _ ᾰ) _ _ _, map_id' := category_theory.limits.walking_cospan_functor._proof_6, map_comp' := category_theory.limits.walking_cospan_functor._proof_7}
The equivalence between two walking_cospans in different universes.
Equations
- category_theory.limits.walking_cospan_equiv = {functor := category_theory.limits.walking_cospan_functor, inverse := category_theory.limits.walking_cospan_functor, unit_iso := category_theory.nat_iso.of_components (λ (x : category_theory.limits.walking_cospan), category_theory.eq_to_iso _) category_theory.limits.walking_cospan_equiv._proof_2, counit_iso := category_theory.nat_iso.of_components (λ (x : category_theory.limits.walking_cospan), category_theory.eq_to_iso _) category_theory.limits.walking_cospan_equiv._proof_4, functor_unit_iso_comp' := category_theory.limits.walking_cospan_equiv._proof_5}
The functor between two walking_spans in different universes.
Equations
- category_theory.limits.walking_span_functor = {obj := λ (ᾰ : category_theory.limits.walking_span), option.cases_on ᾰ category_theory.limits.walking_span.zero (λ (ᾰ : category_theory.limits.walking_pair), ᾰ.cases_on category_theory.limits.walking_span.left category_theory.limits.walking_span.right), map := λ (X Y : category_theory.limits.walking_span) (ᾰ : X ⟶ Y), category_theory.limits.wide_pushout_shape.hom.cases_on ᾰ (λ (ᾰ_1 : category_theory.limits.wide_pushout_shape category_theory.limits.walking_pair) (H_1 : X = ᾰ_1), eq.rec (λ (H_2 : Y = X), eq.rec (λ (ᾰ : X ⟶ X) (H_3 : ᾰ == category_theory.limits.wide_pushout_shape.hom.id X), eq.rec (category_theory.limits.walking_span.hom.id (option.cases_on X category_theory.limits.walking_span.zero (λ (ᾰ : category_theory.limits.walking_pair), ᾰ.cases_on category_theory.limits.walking_span.left category_theory.limits.walking_span.right))) _) _ ᾰ) H_1) (λ (ᾰ_1 : category_theory.limits.walking_pair) (H_1 : X = none), eq.rec (λ (ᾰ : none ⟶ Y) (H_2 : Y = some ᾰ_1), eq.rec (λ (ᾰ : none ⟶ some ᾰ_1) (H_3 : ᾰ == category_theory.limits.wide_pushout_shape.hom.init ᾰ_1), eq.rec (ᾰ_1.cases_on category_theory.limits.walking_span.hom.fst category_theory.limits.walking_span.hom.snd) _) _ ᾰ) _ ᾰ) _ _ _, map_id' := category_theory.limits.walking_span_functor._proof_6, map_comp' := category_theory.limits.walking_span_functor._proof_7}
The equivalence between two walking_spans in different universes.
Equations
- category_theory.limits.walking_span_equiv = {functor := category_theory.limits.walking_span_functor, inverse := category_theory.limits.walking_span_functor, unit_iso := category_theory.nat_iso.of_components (λ (x : category_theory.limits.walking_span), category_theory.eq_to_iso _) category_theory.limits.walking_span_equiv._proof_2, counit_iso := category_theory.nat_iso.of_components (λ (x : category_theory.limits.walking_span), category_theory.eq_to_iso _) category_theory.limits.walking_span_equiv._proof_4, functor_unit_iso_comp' := category_theory.limits.walking_span_equiv._proof_5}
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)
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)
@[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.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.
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.
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.
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.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, _⟩)))
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.
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.
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.
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_assoc
{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)
{X' : C}
(f' : t.X ⟶ X') :
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.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) :
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.
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.
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.
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.
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.
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.
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.
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.
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.
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.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') :
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
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
@[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₂)
@[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) _ _
noncomputable
def
category_theory.limits.pullback_comparison
{C : Type u}
[category_theory.category C]
{X Y Z : C}
{D : Type u₂}
[category_theory.category D]
(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
@[simp]
theorem
category_theory.limits.pullback_comparison_comp_fst
{C : Type u}
[category_theory.category C]
{X Y Z : C}
{D : Type u₂}
[category_theory.category D]
(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]
{X Y Z : C}
{D : Type u₂}
[category_theory.category D]
(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]
{X Y Z : C}
{D : Type u₂}
[category_theory.category D]
(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]
{X Y Z : C}
{D : Type u₂}
[category_theory.category D]
(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]
{X Y Z : C}
{D : Type u₂}
[category_theory.category D]
(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]
{X Y Z : C}
{D : Type u₂}
[category_theory.category D]
(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]
{X Y Z : C}
{D : Type u₂}
[category_theory.category D]
(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
@[simp]
theorem
category_theory.limits.inl_comp_pushout_comparison
{C : Type u}
[category_theory.category C]
{X Y Z : C}
{D : Type u₂}
[category_theory.category D]
(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]
{X Y Z : C}
{D : Type u₂}
[category_theory.category D]
(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]
{X Y Z : C}
{D : Type u₂}
[category_theory.category D]
(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]
{X Y Z : C}
{D : Type u₂}
[category_theory.category D]
(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]
{X Y Z : C}
{D : Type u₂}
[category_theory.category D]
(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]
{X Y Z : C}
{D : Type u₂}
[category_theory.category D]
(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)] :
has_pullbacks represents a choice of pullback for every pair of morphisms
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