structure
CategoryTheory.WeakPullback
{C : Type u_1}
[Category.{u_2, u_1} C]
{P X Y Z : C}
(fst : P ⟶ X)
(snd : P ⟶ Y)
(f : X ⟶ Z)
(g : Y ⟶ Z)
extends CategoryTheory.CommSq fst snd f g :
Type (max u_1 u_2)
- lift {W : C} (a : W ⟶ X) (b : W ⟶ Y) (h : CategoryStruct.comp a f = CategoryStruct.comp b g) : W ⟶ P
- lift_fst' {W : C} (a : W ⟶ X) (b : W ⟶ Y) (h : CategoryStruct.comp a f = CategoryStruct.comp b g) : CategoryStruct.comp (self.lift a b h) fst = a
- lift_snd' {W : C} (a : W ⟶ X) (b : W ⟶ Y) (h : CategoryStruct.comp a f = CategoryStruct.comp b g) : CategoryStruct.comp (self.lift a b h) snd = b
Instances For
@[simp]
theorem
CategoryTheory.WeakPullback.lift_fst
{C : Type u_1}
[Category.{u_2, u_1} C]
{P X Y Z : C}
{fst : P ⟶ X}
{snd : P ⟶ Y}
{f : X ⟶ Z}
{g : Y ⟶ Z}
(wp : WeakPullback fst snd f g)
{W : C}
(a : W ⟶ X)
(b : W ⟶ Y)
(h : CategoryStruct.comp a f = CategoryStruct.comp b g)
:
@[simp]
theorem
CategoryTheory.WeakPullback.lift_snd
{C : Type u_1}
[Category.{u_2, u_1} C]
{P X Y Z : C}
{fst : P ⟶ X}
{snd : P ⟶ Y}
{f : X ⟶ Z}
{g : Y ⟶ Z}
(wp : WeakPullback fst snd f g)
{W : C}
(a : W ⟶ X)
(b : W ⟶ Y)
(h : CategoryStruct.comp a f = CategoryStruct.comp b g)
:
def
CategoryTheory.WeakPullback.coherentLift
{C : Type u_1}
[Category.{u_2, u_1} C]
{P X Y Z : C}
{fst : P ⟶ X}
{snd : P ⟶ Y}
{f : X ⟶ Z}
{g : Y ⟶ Z}
(wp : WeakPullback fst snd f g)
{W : C}
(a : W ⟶ X)
(b : W ⟶ Y)
(h : CategoryStruct.comp a f = CategoryStruct.comp b g)
[Limits.HasPullbacks C]
:
Equations
- One or more equations did not get rendered due to their size.
Instances For
@[simp]
theorem
CategoryTheory.WeakPullback.coherentLift_fst
{C : Type u_1}
[Category.{u_2, u_1} C]
{P X Y Z : C}
{fst : P ⟶ X}
{snd : P ⟶ Y}
{f : X ⟶ Z}
{g : Y ⟶ Z}
(wp : WeakPullback fst snd f g)
{W : C}
(a : W ⟶ X)
(b : W ⟶ Y)
(h : CategoryStruct.comp a f = CategoryStruct.comp b g)
[Limits.HasPullbacks C]
:
@[simp]
theorem
CategoryTheory.WeakPullback.coherentLift_snd
{C : Type u_1}
[Category.{u_2, u_1} C]
{P X Y Z : C}
{fst : P ⟶ X}
{snd : P ⟶ Y}
{f : X ⟶ Z}
{g : Y ⟶ Z}
(wp : WeakPullback fst snd f g)
{W : C}
(a : W ⟶ X)
(b : W ⟶ Y)
(h : CategoryStruct.comp a f = CategoryStruct.comp b g)
[Limits.HasPullbacks C]
:
theorem
CategoryTheory.WeakPullback.coherentLift_comp_left
{C : Type u_1}
[Category.{u_2, u_1} C]
{P X Y Z : C}
{fst : P ⟶ X}
{snd : P ⟶ Y}
{f : X ⟶ Z}
{g : Y ⟶ Z}
(wp : WeakPullback fst snd f g)
{W : C}
(a : W ⟶ X)
(b : W ⟶ Y)
(h : CategoryStruct.comp a f = CategoryStruct.comp b g)
[Limits.HasPullbacks C]
{W' : C}
(σ : W' ⟶ W)
:
CategoryStruct.comp σ (wp.coherentLift a b h) = wp.coherentLift (CategoryStruct.comp σ a) (CategoryStruct.comp σ b) ⋯