Pullback and pushout squares #

We provide another API for pullbacks and pushouts.

IsPullback fst snd f g is the proposition that

  P --fst--> X
  |          |
 snd         f
  |          |
  v          v
  Y ---g---> Z

is a pullback square.

(And similarly for IsPushout.)

We provide the glue to go back and forth to the usual IsLimit API for pullbacks, and prove IsPullback (pullback.fst f g) (pullback.snd f g) f g for the usual pullback f g provided by the HasLimit API.

source

structure CategoryTheory.IsPullback {C : Type u₁} [Category.{v₁, u₁} 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 :

Prop

The proposition that a square

  P --fst--> X
  |          |
 snd         f
  |          |
  v          v
  Y ---g---> Z

is a pullback square. (Also known as a fibered product or Cartesian square.)

w : CategoryStruct.comp fst f = CategoryStruct.comp snd g
isLimit' : Nonempty (Limits.IsLimit (Limits.PullbackCone.mk fst snd ⋯))
the pullback cone is a limit

Instances For

source

structure CategoryTheory.IsPushout {C : Type u₁} [Category.{v₁, u₁} C] {Z X Y P : C} (f : Z ⟶ X) (g : Z ⟶ Y) (inl : X ⟶ P) (inr : Y ⟶ P) extends CategoryTheory.CommSq f g inl inr :

Prop

The proposition that a square

  Z ---f---> X
  |          |
  g         inl
  |          |
  v          v
  Y --inr--> P

is a pushout square. (Also known as a fiber coproduct or co-Cartesian square.)

w : CategoryStruct.comp f inl = CategoryStruct.comp g inr
isColimit' : Nonempty (Limits.IsColimit (Limits.PushoutCocone.mk inl inr ⋯))
the pushout cocone is a colimit

Instances For

source

def CategoryTheory.IsPullback.cone {C : Type u₁} [Category.{v₁, u₁} C] {P X Y Z : C} {fst : P ⟶ X} {snd : P ⟶ Y} {f : X ⟶ Z} {g : Y ⟶ Z} (h : IsPullback fst snd f g) :

Limits.PullbackCone f g

The (limiting) PullbackCone f g implicit in the statement that we have an IsPullback fst snd f g.

Equations

h.cone = ⋯.cone

Instances For

source

@[simp]

theorem CategoryTheory.IsPullback.cone_fst {C : Type u₁} [Category.{v₁, u₁} C] {P X Y Z : C} {fst : P ⟶ X} {snd : P ⟶ Y} {f : X ⟶ Z} {g : Y ⟶ Z} (h : IsPullback fst snd f g) :

h.cone.fst = fst

source

@[simp]

theorem CategoryTheory.IsPullback.cone_snd {C : Type u₁} [Category.{v₁, u₁} C] {P X Y Z : C} {fst : P ⟶ X} {snd : P ⟶ Y} {f : X ⟶ Z} {g : Y ⟶ Z} (h : IsPullback fst snd f g) :

h.cone.snd = snd

source

noncomputable def CategoryTheory.IsPullback.isLimit {C : Type u₁} [Category.{v₁, u₁} C] {P X Y Z : C} {fst : P ⟶ X} {snd : P ⟶ Y} {f : X ⟶ Z} {g : Y ⟶ Z} (h : IsPullback fst snd f g) :

Limits.IsLimit h.cone

The cone obtained from IsPullback fst snd f g is a limit cone.

Equations

h.isLimit = ⋯.some

Instances For

source

noncomputable def CategoryTheory.IsPullback.lift {C : Type u₁} [Category.{v₁, u₁} C] {P X Y Z : C} {fst : P ⟶ X} {snd : P ⟶ Y} {f : X ⟶ Z} {g : Y ⟶ Z} (hP : IsPullback fst snd f g) {W : C} (h : W ⟶ X) (k : W ⟶ Y) (w : CategoryStruct.comp h f = CategoryStruct.comp k g) :

W ⟶ P

API for PullbackCone.IsLimit.lift for IsPullback

Equations

hP.lift h k w = CategoryTheory.Limits.PullbackCone.IsLimit.lift hP.isLimit h k w

Instances For

source

@[simp]

theorem CategoryTheory.IsPullback.lift_fst {C : Type u₁} [Category.{v₁, u₁} C] {P X Y Z : C} {fst : P ⟶ X} {snd : P ⟶ Y} {f : X ⟶ Z} {g : Y ⟶ Z} (hP : IsPullback fst snd f g) {W : C} (h : W ⟶ X) (k : W ⟶ Y) (w : CategoryStruct.comp h f = CategoryStruct.comp k g) :

CategoryStruct.comp (hP.lift h k w) fst = h

source

@[simp]

theorem CategoryTheory.IsPullback.lift_fst_assoc {C : Type u₁} [Category.{v₁, u₁} C] {P X Y Z : C} {fst : P ⟶ X} {snd : P ⟶ Y} {f : X ⟶ Z} {g : Y ⟶ Z} (hP : IsPullback fst snd f g) {W : C} (h : W ⟶ X) (k : W ⟶ Y) (w : CategoryStruct.comp h f = CategoryStruct.comp k g) {Z✝ : C} (h✝ : X ⟶ Z✝) :

CategoryStruct.comp (hP.lift h k w) (CategoryStruct.comp fst h✝) = CategoryStruct.comp h h✝

source

@[simp]

theorem CategoryTheory.IsPullback.lift_snd {C : Type u₁} [Category.{v₁, u₁} C] {P X Y Z : C} {fst : P ⟶ X} {snd : P ⟶ Y} {f : X ⟶ Z} {g : Y ⟶ Z} (hP : IsPullback fst snd f g) {W : C} (h : W ⟶ X) (k : W ⟶ Y) (w : CategoryStruct.comp h f = CategoryStruct.comp k g) :

CategoryStruct.comp (hP.lift h k w) snd = k

source

@[simp]

theorem CategoryTheory.IsPullback.lift_snd_assoc {C : Type u₁} [Category.{v₁, u₁} C] {P X Y Z : C} {fst : P ⟶ X} {snd : P ⟶ Y} {f : X ⟶ Z} {g : Y ⟶ Z} (hP : IsPullback fst snd f g) {W : C} (h : W ⟶ X) (k : W ⟶ Y) (w : CategoryStruct.comp h f = CategoryStruct.comp k g) {Z✝ : C} (h✝ : Y ⟶ Z✝) :

CategoryStruct.comp (hP.lift h k w) (CategoryStruct.comp snd h✝) = CategoryStruct.comp k h✝

source

theorem CategoryTheory.IsPullback.exists_lift {C : Type u₁} [Category.{v₁, u₁} C] {P X Y Z : C} {fst : P ⟶ X} {snd : P ⟶ Y} {f : X ⟶ Z} {g : Y ⟶ Z} (hP : IsPullback fst snd f g) {W : C} (h : W ⟶ X) (k : W ⟶ Y) (w : CategoryStruct.comp h f = CategoryStruct.comp k g) :

∃ (l : W ⟶ P), CategoryStruct.comp l fst = h ∧ CategoryStruct.comp l snd = k

source

theorem CategoryTheory.IsPullback.hom_ext {C : Type u₁} [Category.{v₁, u₁} C] {P X Y Z : C} {fst : P ⟶ X} {snd : P ⟶ Y} {f : X ⟶ Z} {g : Y ⟶ Z} (hP : IsPullback fst snd f g) {W : C} {k l : W ⟶ P} (h₀ : CategoryStruct.comp k fst = CategoryStruct.comp l fst) (h₁ : CategoryStruct.comp k snd = CategoryStruct.comp l snd) :

k = l

source

theorem CategoryTheory.IsPullback.of_isLimit {C : Type u₁} [Category.{v₁, u₁} C] {X Y Z : C} {f : X ⟶ Z} {g : Y ⟶ Z} {c : Limits.PullbackCone f g} (h : Limits.IsLimit c) :

IsPullback c.fst c.snd f g

If c is a limiting pullback cone, then we have an IsPullback c.fst c.snd f g.

source

theorem CategoryTheory.IsPullback.of_isLimit' {C : Type u₁} [Category.{v₁, u₁} C] {P X Y Z : C} {fst : P ⟶ X} {snd : P ⟶ Y} {f : X ⟶ Z} {g : Y ⟶ Z} (w : CommSq fst snd f g) (h : Limits.IsLimit w.cone) :

IsPullback fst snd f g

A variant of of_isLimit that is more useful with apply.

source

theorem CategoryTheory.IsPullback.of_isLimit_cone {C : Type u₁} [Category.{v₁, u₁} C] {D : Functor Limits.WalkingCospan C} {c : Limits.Cone D} (hc : Limits.IsLimit c) :

IsPullback (c.π.app Limits.WalkingCospan.left) (c.π.app Limits.WalkingCospan.right) (D.map Limits.WalkingCospan.Hom.inl) (D.map Limits.WalkingCospan.Hom.inr)

Variant of of_isLimit for an arbitrary cone on a diagram WalkingCospan ⥤ C.

source

theorem CategoryTheory.IsPullback.hasPullback {C : Type u₁} [Category.{v₁, u₁} C] {P X Y Z : C} {fst : P ⟶ X} {snd : P ⟶ Y} {f : X ⟶ Z} {g : Y ⟶ Z} (h : IsPullback fst snd f g) :

Limits.HasPullback f g

source

theorem CategoryTheory.IsPullback.of_hasPullback {C : Type u₁} [Category.{v₁, u₁} C] {X Y Z : C} (f : X ⟶ Z) (g : Y ⟶ Z) [Limits.HasPullback f g] :

IsPullback (Limits.pullback.fst f g) (Limits.pullback.snd f g) f g

The pullback provided by HasPullback f g fits into an IsPullback.

source

noncomputable def CategoryTheory.IsPullback.isoIsPullback {C : Type u₁} [Category.{v₁, u₁} C] {P : C} (X Y : C) {Z : C} {fst : P ⟶ X} {snd : P ⟶ Y} {f : X ⟶ Z} {g : Y ⟶ Z} {P' : C} {fst' : P' ⟶ X} {snd' : P' ⟶ Y} (h : IsPullback fst snd f g) (h' : IsPullback fst' snd' f g) :

P ≅ P'

Any object at the top left of a pullback square is isomorphic to the object at the top left of any other pullback square with the same cospan.

Equations

CategoryTheory.IsPullback.isoIsPullback X Y h h' = h.isLimit.conePointUniqueUpToIso h'.isLimit

Instances For

source

@[simp]

theorem CategoryTheory.IsPullback.isoIsPullback_hom_fst {C : Type u₁} [Category.{v₁, u₁} C] {P : C} (X Y : C) {Z : C} {fst : P ⟶ X} {snd : P ⟶ Y} {f : X ⟶ Z} {g : Y ⟶ Z} {P' : C} {fst' : P' ⟶ X} {snd' : P' ⟶ Y} (h : IsPullback fst snd f g) (h' : IsPullback fst' snd' f g) :

CategoryStruct.comp (isoIsPullback X Y h h').hom fst' = fst

source

@[simp]

theorem CategoryTheory.IsPullback.isoIsPullback_hom_fst_assoc {C : Type u₁} [Category.{v₁, u₁} C] {P : C} (X Y : C) {Z : C} {fst : P ⟶ X} {snd : P ⟶ Y} {f : X ⟶ Z} {g : Y ⟶ Z} {P' : C} {fst' : P' ⟶ X} {snd' : P' ⟶ Y} (h : IsPullback fst snd f g) (h' : IsPullback fst' snd' f g) {Z✝ : C} (h✝ : X ⟶ Z✝) :

CategoryStruct.comp (isoIsPullback X Y h h').hom (CategoryStruct.comp fst' h✝) = CategoryStruct.comp fst h✝

source

@[simp]

theorem CategoryTheory.IsPullback.isoIsPullback_hom_snd {C : Type u₁} [Category.{v₁, u₁} C] {P : C} (X Y : C) {Z : C} {fst : P ⟶ X} {snd : P ⟶ Y} {f : X ⟶ Z} {g : Y ⟶ Z} {P' : C} {fst' : P' ⟶ X} {snd' : P' ⟶ Y} (h : IsPullback fst snd f g) (h' : IsPullback fst' snd' f g) :

CategoryStruct.comp (isoIsPullback X Y h h').hom snd' = snd

source

@[simp]

theorem CategoryTheory.IsPullback.isoIsPullback_hom_snd_assoc {C : Type u₁} [Category.{v₁, u₁} C] {P : C} (X Y : C) {Z : C} {fst : P ⟶ X} {snd : P ⟶ Y} {f : X ⟶ Z} {g : Y ⟶ Z} {P' : C} {fst' : P' ⟶ X} {snd' : P' ⟶ Y} (h : IsPullback fst snd f g) (h' : IsPullback fst' snd' f g) {Z✝ : C} (h✝ : Y ⟶ Z✝) :

CategoryStruct.comp (isoIsPullback X Y h h').hom (CategoryStruct.comp snd' h✝) = CategoryStruct.comp snd h✝

source

@[simp]

theorem CategoryTheory.IsPullback.isoIsPullback_inv_fst {C : Type u₁} [Category.{v₁, u₁} C] {P : C} (X Y : C) {Z : C} {fst : P ⟶ X} {snd : P ⟶ Y} {f : X ⟶ Z} {g : Y ⟶ Z} {P' : C} {fst' : P' ⟶ X} {snd' : P' ⟶ Y} (h : IsPullback fst snd f g) (h' : IsPullback fst' snd' f g) :

CategoryStruct.comp (isoIsPullback X Y h h').inv fst = fst'

source

@[simp]

theorem CategoryTheory.IsPullback.isoIsPullback_inv_fst_assoc {C : Type u₁} [Category.{v₁, u₁} C] {P : C} (X Y : C) {Z : C} {fst : P ⟶ X} {snd : P ⟶ Y} {f : X ⟶ Z} {g : Y ⟶ Z} {P' : C} {fst' : P' ⟶ X} {snd' : P' ⟶ Y} (h : IsPullback fst snd f g) (h' : IsPullback fst' snd' f g) {Z✝ : C} (h✝ : X ⟶ Z✝) :

CategoryStruct.comp (isoIsPullback X Y h h').inv (CategoryStruct.comp fst h✝) = CategoryStruct.comp fst' h✝

source

@[simp]

theorem CategoryTheory.IsPullback.isoIsPullback_inv_snd {C : Type u₁} [Category.{v₁, u₁} C] {P : C} (X Y : C) {Z : C} {fst : P ⟶ X} {snd : P ⟶ Y} {f : X ⟶ Z} {g : Y ⟶ Z} {P' : C} {fst' : P' ⟶ X} {snd' : P' ⟶ Y} (h : IsPullback fst snd f g) (h' : IsPullback fst' snd' f g) :

CategoryStruct.comp (isoIsPullback X Y h h').inv snd = snd'

source

@[simp]

theorem CategoryTheory.IsPullback.isoIsPullback_inv_snd_assoc {C : Type u₁} [Category.{v₁, u₁} C] {P : C} (X Y : C) {Z : C} {fst : P ⟶ X} {snd : P ⟶ Y} {f : X ⟶ Z} {g : Y ⟶ Z} {P' : C} {fst' : P' ⟶ X} {snd' : P' ⟶ Y} (h : IsPullback fst snd f g) (h' : IsPullback fst' snd' f g) {Z✝ : C} (h✝ : Y ⟶ Z✝) :

CategoryStruct.comp (isoIsPullback X Y h h').inv (CategoryStruct.comp snd h✝) = CategoryStruct.comp snd' h✝

source

noncomputable def CategoryTheory.IsPullback.isoPullback {C : Type u₁} [Category.{v₁, u₁} C] {P X Y Z : C} {fst : P ⟶ X} {snd : P ⟶ Y} {f : X ⟶ Z} {g : Y ⟶ Z} (h : IsPullback fst snd f g) [Limits.HasPullback f g] :

P ≅ Limits.pullback f g

Any object at the top left of a pullback square is isomorphic to the pullback provided by the HasLimit API.

Equations

h.isoPullback = (CategoryTheory.Limits.limit.isoLimitCone { cone := h.cone, isLimit := h.isLimit }).symm

Instances For

source

@[simp]

theorem CategoryTheory.IsPullback.isoPullback_hom_fst {C : Type u₁} [Category.{v₁, u₁} C] {P X Y Z : C} {fst : P ⟶ X} {snd : P ⟶ Y} {f : X ⟶ Z} {g : Y ⟶ Z} (h : IsPullback fst snd f g) [Limits.HasPullback f g] :

CategoryStruct.comp h.isoPullback.hom (Limits.pullback.fst f g) = fst

source

@[simp]

theorem CategoryTheory.IsPullback.isoPullback_hom_fst_assoc {C : Type u₁} [Category.{v₁, u₁} C] {P X Y Z : C} {fst : P ⟶ X} {snd : P ⟶ Y} {f : X ⟶ Z} {g : Y ⟶ Z} (h : IsPullback fst snd f g) [Limits.HasPullback f g] {Z✝ : C} (h✝ : X ⟶ Z✝) :

CategoryStruct.comp h.isoPullback.hom (CategoryStruct.comp (Limits.pullback.fst f g) h✝) = CategoryStruct.comp fst h✝

source

@[simp]

theorem CategoryTheory.IsPullback.isoPullback_hom_snd {C : Type u₁} [Category.{v₁, u₁} C] {P X Y Z : C} {fst : P ⟶ X} {snd : P ⟶ Y} {f : X ⟶ Z} {g : Y ⟶ Z} (h : IsPullback fst snd f g) [Limits.HasPullback f g] :

CategoryStruct.comp h.isoPullback.hom (Limits.pullback.snd f g) = snd

source

@[simp]

theorem CategoryTheory.IsPullback.isoPullback_hom_snd_assoc {C : Type u₁} [Category.{v₁, u₁} C] {P X Y Z : C} {fst : P ⟶ X} {snd : P ⟶ Y} {f : X ⟶ Z} {g : Y ⟶ Z} (h : IsPullback fst snd f g) [Limits.HasPullback f g] {Z✝ : C} (h✝ : Y ⟶ Z✝) :

CategoryStruct.comp h.isoPullback.hom (CategoryStruct.comp (Limits.pullback.snd f g) h✝) = CategoryStruct.comp snd h✝

source

@[simp]

theorem CategoryTheory.IsPullback.isoPullback_inv_fst {C : Type u₁} [Category.{v₁, u₁} C] {P X Y Z : C} {fst : P ⟶ X} {snd : P ⟶ Y} {f : X ⟶ Z} {g : Y ⟶ Z} (h : IsPullback fst snd f g) [Limits.HasPullback f g] :

CategoryStruct.comp h.isoPullback.inv fst = Limits.pullback.fst f g

source

@[simp]

theorem CategoryTheory.IsPullback.isoPullback_inv_fst_assoc {C : Type u₁} [Category.{v₁, u₁} C] {P X Y Z : C} {fst : P ⟶ X} {snd : P ⟶ Y} {f : X ⟶ Z} {g : Y ⟶ Z} (h : IsPullback fst snd f g) [Limits.HasPullback f g] {Z✝ : C} (h✝ : X ⟶ Z✝) :

CategoryStruct.comp h.isoPullback.inv (CategoryStruct.comp fst h✝) = CategoryStruct.comp (Limits.pullback.fst f g) h✝

source

@[simp]

theorem CategoryTheory.IsPullback.isoPullback_inv_snd {C : Type u₁} [Category.{v₁, u₁} C] {P X Y Z : C} {fst : P ⟶ X} {snd : P ⟶ Y} {f : X ⟶ Z} {g : Y ⟶ Z} (h : IsPullback fst snd f g) [Limits.HasPullback f g] :

CategoryStruct.comp h.isoPullback.inv snd = Limits.pullback.snd f g

source

@[simp]

theorem CategoryTheory.IsPullback.isoPullback_inv_snd_assoc {C : Type u₁} [Category.{v₁, u₁} C] {P X Y Z : C} {fst : P ⟶ X} {snd : P ⟶ Y} {f : X ⟶ Z} {g : Y ⟶ Z} (h : IsPullback fst snd f g) [Limits.HasPullback f g] {Z✝ : C} (h✝ : Y ⟶ Z✝) :

CategoryStruct.comp h.isoPullback.inv (CategoryStruct.comp snd h✝) = CategoryStruct.comp (Limits.pullback.snd f g) h✝

source

def CategoryTheory.IsPushout.cocone {C : Type u₁} [Category.{v₁, u₁} C] {Z X Y P : C} {f : Z ⟶ X} {g : Z ⟶ Y} {inl : X ⟶ P} {inr : Y ⟶ P} (h : IsPushout f g inl inr) :

Limits.PushoutCocone f g

The (colimiting) PushoutCocone f g implicit in the statement that we have an IsPushout f g inl inr.

Equations

h.cocone = ⋯.cocone

Instances For

source

@[simp]

theorem CategoryTheory.IsPushout.cocone_inl {C : Type u₁} [Category.{v₁, u₁} C] {Z X Y P : C} {f : Z ⟶ X} {g : Z ⟶ Y} {inl : X ⟶ P} {inr : Y ⟶ P} (h : IsPushout f g inl inr) :

h.cocone.inl = inl

source

@[simp]

theorem CategoryTheory.IsPushout.cocone_inr {C : Type u₁} [Category.{v₁, u₁} C] {Z X Y P : C} {f : Z ⟶ X} {g : Z ⟶ Y} {inl : X ⟶ P} {inr : Y ⟶ P} (h : IsPushout f g inl inr) :

h.cocone.inr = inr

source

noncomputable def CategoryTheory.IsPushout.isColimit {C : Type u₁} [Category.{v₁, u₁} C] {Z X Y P : C} {f : Z ⟶ X} {g : Z ⟶ Y} {inl : X ⟶ P} {inr : Y ⟶ P} (h : IsPushout f g inl inr) :

Limits.IsColimit h.cocone

The cocone obtained from IsPushout f g inl inr is a colimit cocone.

Equations

h.isColimit = ⋯.some

Instances For

source

noncomputable def CategoryTheory.IsPushout.desc {C : Type u₁} [Category.{v₁, u₁} C] {Z X Y P : C} {f : Z ⟶ X} {g : Z ⟶ Y} {inl : X ⟶ P} {inr : Y ⟶ P} (hP : IsPushout f g inl inr) {W : C} (h : X ⟶ W) (k : Y ⟶ W) (w : CategoryStruct.comp f h = CategoryStruct.comp g k) :

P ⟶ W

API for PushoutCocone.IsColimit.lift for IsPushout

Equations

hP.desc h k w = CategoryTheory.Limits.PushoutCocone.IsColimit.desc hP.isColimit h k w

Instances For

source

@[simp]

theorem CategoryTheory.IsPushout.inl_desc {C : Type u₁} [Category.{v₁, u₁} C] {Z X Y P : C} {f : Z ⟶ X} {g : Z ⟶ Y} {inl : X ⟶ P} {inr : Y ⟶ P} (hP : IsPushout f g inl inr) {W : C} (h : X ⟶ W) (k : Y ⟶ W) (w : CategoryStruct.comp f h = CategoryStruct.comp g k) :

CategoryStruct.comp inl (hP.desc h k w) = h

source

@[simp]

theorem CategoryTheory.IsPushout.inl_desc_assoc {C : Type u₁} [Category.{v₁, u₁} C] {Z X Y P : C} {f : Z ⟶ X} {g : Z ⟶ Y} {inl : X ⟶ P} {inr : Y ⟶ P} (hP : IsPushout f g inl inr) {W : C} (h : X ⟶ W) (k : Y ⟶ W) (w : CategoryStruct.comp f h = CategoryStruct.comp g k) {Z✝ : C} (h✝ : W ⟶ Z✝) :

CategoryStruct.comp inl (CategoryStruct.comp (hP.desc h k w) h✝) = CategoryStruct.comp h h✝

source

@[simp]

theorem CategoryTheory.IsPushout.inr_desc {C : Type u₁} [Category.{v₁, u₁} C] {Z X Y P : C} {f : Z ⟶ X} {g : Z ⟶ Y} {inl : X ⟶ P} {inr : Y ⟶ P} (hP : IsPushout f g inl inr) {W : C} (h : X ⟶ W) (k : Y ⟶ W) (w : CategoryStruct.comp f h = CategoryStruct.comp g k) :

CategoryStruct.comp inr (hP.desc h k w) = k

source

@[simp]

theorem CategoryTheory.IsPushout.inr_desc_assoc {C : Type u₁} [Category.{v₁, u₁} C] {Z X Y P : C} {f : Z ⟶ X} {g : Z ⟶ Y} {inl : X ⟶ P} {inr : Y ⟶ P} (hP : IsPushout f g inl inr) {W : C} (h : X ⟶ W) (k : Y ⟶ W) (w : CategoryStruct.comp f h = CategoryStruct.comp g k) {Z✝ : C} (h✝ : W ⟶ Z✝) :

CategoryStruct.comp inr (CategoryStruct.comp (hP.desc h k w) h✝) = CategoryStruct.comp k h✝

source

theorem CategoryTheory.IsPushout.exists_desc {C : Type u₁} [Category.{v₁, u₁} C] {Z X Y P : C} {f : Z ⟶ X} {g : Z ⟶ Y} {inl : X ⟶ P} {inr : Y ⟶ P} (hP : IsPushout f g inl inr) {W : C} (h : X ⟶ W) (k : Y ⟶ W) (w : CategoryStruct.comp f h = CategoryStruct.comp g k) :

∃ (d : P ⟶ W), CategoryStruct.comp inl d = h ∧ CategoryStruct.comp inr d = k

source

theorem CategoryTheory.IsPushout.hom_ext {C : Type u₁} [Category.{v₁, u₁} C] {Z X Y P : C} {f : Z ⟶ X} {g : Z ⟶ Y} {inl : X ⟶ P} {inr : Y ⟶ P} (hP : IsPushout f g inl inr) {W : C} {k l : P ⟶ W} (h₀ : CategoryStruct.comp inl k = CategoryStruct.comp inl l) (h₁ : CategoryStruct.comp inr k = CategoryStruct.comp inr l) :

k = l

source

theorem CategoryTheory.IsPushout.of_isColimit {C : Type u₁} [Category.{v₁, u₁} C] {Z X Y : C} {f : Z ⟶ X} {g : Z ⟶ Y} {c : Limits.PushoutCocone f g} (h : Limits.IsColimit c) :

IsPushout f g c.inl c.inr

If c is a colimiting pushout cocone, then we have an IsPushout f g c.inl c.inr.

source

theorem CategoryTheory.IsPushout.of_isColimit' {C : Type u₁} [Category.{v₁, u₁} C] {Z X Y P : C} {f : Z ⟶ X} {g : Z ⟶ Y} {inl : X ⟶ P} {inr : Y ⟶ P} (w : CommSq f g inl inr) (h : Limits.IsColimit w.cocone) :

IsPushout f g inl inr

A variant of of_isColimit that is more useful with apply.

source

theorem CategoryTheory.IsPushout.of_isColimit_cocone {C : Type u₁} [Category.{v₁, u₁} C] {D : Functor Limits.WalkingSpan C} {c : Limits.Cocone D} (hc : Limits.IsColimit c) :

IsPushout (D.map Limits.WalkingSpan.Hom.fst) (D.map Limits.WalkingSpan.Hom.snd) (c.ι.app Limits.WalkingSpan.left) (c.ι.app Limits.WalkingSpan.right)

Variant of of_isColimit for an arbitrary cocone on a diagram WalkingSpan ⥤ C.

source

theorem CategoryTheory.IsPushout.hasPushout {C : Type u₁} [Category.{v₁, u₁} C] {Z X Y P : C} {f : Z ⟶ X} {g : Z ⟶ Y} {inl : X ⟶ P} {inr : Y ⟶ P} (h : IsPushout f g inl inr) :

Limits.HasPushout f g

source

theorem CategoryTheory.IsPushout.of_hasPushout {C : Type u₁} [Category.{v₁, u₁} C] {Z X Y : C} (f : Z ⟶ X) (g : Z ⟶ Y) [Limits.HasPushout f g] :

IsPushout f g (Limits.pushout.inl f g) (Limits.pushout.inr f g)

The pushout provided by HasPushout f g fits into an IsPushout.

source

noncomputable def CategoryTheory.IsPushout.isoIsPushout {C : Type u₁} [Category.{v₁, u₁} C] {Z : C} (X Y : C) {P : C} {f : Z ⟶ X} {g : Z ⟶ Y} {inl : X ⟶ P} {inr : Y ⟶ P} {P' : C} {inl' : X ⟶ P'} {inr' : Y ⟶ P'} (h : IsPushout f g inl inr) (h' : IsPushout f g inl' inr') :

P ≅ P'

Any object at the bottom right of a pushout square is isomorphic to the object at the bottom right of any other pushout square with the same span.

Equations

CategoryTheory.IsPushout.isoIsPushout X Y h h' = h.isColimit.coconePointUniqueUpToIso h'.isColimit

Instances For

source

@[simp]

theorem CategoryTheory.IsPushout.inl_isoIsPushout_hom {C : Type u₁} [Category.{v₁, u₁} C] {Z : C} (X Y : C) {P : C} {f : Z ⟶ X} {g : Z ⟶ Y} {inl : X ⟶ P} {inr : Y ⟶ P} {P' : C} {inl' : X ⟶ P'} {inr' : Y ⟶ P'} (h : IsPushout f g inl inr) (h' : IsPushout f g inl' inr') :

CategoryStruct.comp inl (isoIsPushout X Y h h').hom = inl'

source

@[simp]

theorem CategoryTheory.IsPushout.inl_isoIsPushout_hom_assoc {C : Type u₁} [Category.{v₁, u₁} C] {Z : C} (X Y : C) {P : C} {f : Z ⟶ X} {g : Z ⟶ Y} {inl : X ⟶ P} {inr : Y ⟶ P} {P' : C} {inl' : X ⟶ P'} {inr' : Y ⟶ P'} (h : IsPushout f g inl inr) (h' : IsPushout f g inl' inr') {Z✝ : C} (h✝ : P' ⟶ Z✝) :

CategoryStruct.comp inl (CategoryStruct.comp (isoIsPushout X Y h h').hom h✝) = CategoryStruct.comp inl' h✝

source

@[simp]

theorem CategoryTheory.IsPushout.inr_isoIsPushout_hom {C : Type u₁} [Category.{v₁, u₁} C] {Z : C} (X Y : C) {P : C} {f : Z ⟶ X} {g : Z ⟶ Y} {inl : X ⟶ P} {inr : Y ⟶ P} {P' : C} {inl' : X ⟶ P'} {inr' : Y ⟶ P'} (h : IsPushout f g inl inr) (h' : IsPushout f g inl' inr') :

CategoryStruct.comp inr (isoIsPushout X Y h h').hom = inr'

source

@[simp]

theorem CategoryTheory.IsPushout.inr_isoIsPushout_hom_assoc {C : Type u₁} [Category.{v₁, u₁} C] {Z : C} (X Y : C) {P : C} {f : Z ⟶ X} {g : Z ⟶ Y} {inl : X ⟶ P} {inr : Y ⟶ P} {P' : C} {inl' : X ⟶ P'} {inr' : Y ⟶ P'} (h : IsPushout f g inl inr) (h' : IsPushout f g inl' inr') {Z✝ : C} (h✝ : P' ⟶ Z✝) :

CategoryStruct.comp inr (CategoryStruct.comp (isoIsPushout X Y h h').hom h✝) = CategoryStruct.comp inr' h✝

source

@[simp]

theorem CategoryTheory.IsPushout.inl_isoIsPushout_inv {C : Type u₁} [Category.{v₁, u₁} C] {Z : C} (X Y : C) {P : C} {f : Z ⟶ X} {g : Z ⟶ Y} {inl : X ⟶ P} {inr : Y ⟶ P} {P' : C} {inl' : X ⟶ P'} {inr' : Y ⟶ P'} (h : IsPushout f g inl inr) (h' : IsPushout f g inl' inr') :

CategoryStruct.comp inl' (isoIsPushout X Y h h').inv = inl

source

@[simp]

theorem CategoryTheory.IsPushout.inl_isoIsPushout_inv_assoc {C : Type u₁} [Category.{v₁, u₁} C] {Z : C} (X Y : C) {P : C} {f : Z ⟶ X} {g : Z ⟶ Y} {inl : X ⟶ P} {inr : Y ⟶ P} {P' : C} {inl' : X ⟶ P'} {inr' : Y ⟶ P'} (h : IsPushout f g inl inr) (h' : IsPushout f g inl' inr') {Z✝ : C} (h✝ : P ⟶ Z✝) :

CategoryStruct.comp inl' (CategoryStruct.comp (isoIsPushout X Y h h').inv h✝) = CategoryStruct.comp inl h✝

source

@[simp]

theorem CategoryTheory.IsPushout.inr_isoIsPushout_inv {C : Type u₁} [Category.{v₁, u₁} C] {Z : C} (X Y : C) {P : C} {f : Z ⟶ X} {g : Z ⟶ Y} {inl : X ⟶ P} {inr : Y ⟶ P} {P' : C} {inl' : X ⟶ P'} {inr' : Y ⟶ P'} (h : IsPushout f g inl inr) (h' : IsPushout f g inl' inr') :

CategoryStruct.comp inr' (isoIsPushout X Y h h').inv = inr

source

@[simp]

theorem CategoryTheory.IsPushout.inr_isoIsPushout_inv_assoc {C : Type u₁} [Category.{v₁, u₁} C] {Z : C} (X Y : C) {P : C} {f : Z ⟶ X} {g : Z ⟶ Y} {inl : X ⟶ P} {inr : Y ⟶ P} {P' : C} {inl' : X ⟶ P'} {inr' : Y ⟶ P'} (h : IsPushout f g inl inr) (h' : IsPushout f g inl' inr') {Z✝ : C} (h✝ : P ⟶ Z✝) :

CategoryStruct.comp inr' (CategoryStruct.comp (isoIsPushout X Y h h').inv h✝) = CategoryStruct.comp inr h✝

source

noncomputable def CategoryTheory.IsPushout.isoPushout {C : Type u₁} [Category.{v₁, u₁} C] {Z X Y P : C} {f : Z ⟶ X} {g : Z ⟶ Y} {inl : X ⟶ P} {inr : Y ⟶ P} (h : IsPushout f g inl inr) [Limits.HasPushout f g] :

P ≅ Limits.pushout f g

Any object at the top left of a pullback square is isomorphic to the pullback provided by the HasLimit API.

Equations

h.isoPushout = (CategoryTheory.Limits.colimit.isoColimitCocone { cocone := h.cocone, isColimit := h.isColimit }).symm

Instances For

source

@[simp]

theorem CategoryTheory.IsPushout.inl_isoPushout_inv {C : Type u₁} [Category.{v₁, u₁} C] {Z X Y P : C} {f : Z ⟶ X} {g : Z ⟶ Y} {inl : X ⟶ P} {inr : Y ⟶ P} (h : IsPushout f g inl inr) [Limits.HasPushout f g] :

CategoryStruct.comp (Limits.pushout.inl f g) h.isoPushout.inv = inl

source

@[simp]

theorem CategoryTheory.IsPushout.inl_isoPushout_inv_assoc {C : Type u₁} [Category.{v₁, u₁} C] {Z X Y P : C} {f : Z ⟶ X} {g : Z ⟶ Y} {inl : X ⟶ P} {inr : Y ⟶ P} (h : IsPushout f g inl inr) [Limits.HasPushout f g] {Z✝ : C} (h✝ : P ⟶ Z✝) :

CategoryStruct.comp (Limits.pushout.inl f g) (CategoryStruct.comp h.isoPushout.inv h✝) = CategoryStruct.comp inl h✝

source

@[simp]

theorem CategoryTheory.IsPushout.inr_isoPushout_inv {C : Type u₁} [Category.{v₁, u₁} C] {Z X Y P : C} {f : Z ⟶ X} {g : Z ⟶ Y} {inl : X ⟶ P} {inr : Y ⟶ P} (h : IsPushout f g inl inr) [Limits.HasPushout f g] :

CategoryStruct.comp (Limits.pushout.inr f g) h.isoPushout.inv = inr

source

@[simp]

theorem CategoryTheory.IsPushout.inr_isoPushout_inv_assoc {C : Type u₁} [Category.{v₁, u₁} C] {Z X Y P : C} {f : Z ⟶ X} {g : Z ⟶ Y} {inl : X ⟶ P} {inr : Y ⟶ P} (h : IsPushout f g inl inr) [Limits.HasPushout f g] {Z✝ : C} (h✝ : P ⟶ Z✝) :

CategoryStruct.comp (Limits.pushout.inr f g) (CategoryStruct.comp h.isoPushout.inv h✝) = CategoryStruct.comp inr h✝

source

@[simp]

theorem CategoryTheory.IsPushout.inl_isoPushout_hom {C : Type u₁} [Category.{v₁, u₁} C] {Z X Y P : C} {f : Z ⟶ X} {g : Z ⟶ Y} {inl : X ⟶ P} {inr : Y ⟶ P} (h : IsPushout f g inl inr) [Limits.HasPushout f g] :

CategoryStruct.comp inl h.isoPushout.hom = Limits.pushout.inl f g

source

@[simp]

theorem CategoryTheory.IsPushout.inl_isoPushout_hom_assoc {C : Type u₁} [Category.{v₁, u₁} C] {Z X Y P : C} {f : Z ⟶ X} {g : Z ⟶ Y} {inl : X ⟶ P} {inr : Y ⟶ P} (h : IsPushout f g inl inr) [Limits.HasPushout f g] {Z✝ : C} (h✝ : Limits.pushout f g ⟶ Z✝) :

CategoryStruct.comp inl (CategoryStruct.comp h.isoPushout.hom h✝) = CategoryStruct.comp (Limits.pushout.inl f g) h✝

source

@[simp]

theorem CategoryTheory.IsPushout.inr_isoPushout_hom {C : Type u₁} [Category.{v₁, u₁} C] {Z X Y P : C} {f : Z ⟶ X} {g : Z ⟶ Y} {inl : X ⟶ P} {inr : Y ⟶ P} (h : IsPushout f g inl inr) [Limits.HasPushout f g] :

CategoryStruct.comp inr h.isoPushout.hom = Limits.pushout.inr f g

source

@[simp]

theorem CategoryTheory.IsPushout.inr_isoPushout_hom_assoc {C : Type u₁} [Category.{v₁, u₁} C] {Z X Y P : C} {f : Z ⟶ X} {g : Z ⟶ Y} {inl : X ⟶ P} {inr : Y ⟶ P} (h : IsPushout f g inl inr) [Limits.HasPushout f g] {Z✝ : C} (h✝ : Limits.pushout f g ⟶ Z✝) :

CategoryStruct.comp inr (CategoryStruct.comp h.isoPushout.hom h✝) = CategoryStruct.comp (Limits.pushout.inr f g) h✝

source

theorem CategoryTheory.IsPullback.flip {C : Type u₁} [Category.{v₁, u₁} C] {P X Y Z : C} {fst : P ⟶ X} {snd : P ⟶ Y} {f : X ⟶ Z} {g : Y ⟶ Z} (h : IsPullback fst snd f g) :

IsPullback snd fst g f

source

theorem CategoryTheory.IsPullback.flip_iff {C : Type u₁} [Category.{v₁, u₁} C] {P X Y Z : C} {fst : P ⟶ X} {snd : P ⟶ Y} {f : X ⟶ Z} {g : Y ⟶ Z} :

IsPullback fst snd f g ↔ IsPullback snd fst g f

source

theorem CategoryTheory.IsPullback.op {C : Type u₁} [Category.{v₁, u₁} C] {P X Y Z : C} {fst : P ⟶ X} {snd : P ⟶ Y} {f : X ⟶ Z} {g : Y ⟶ Z} (h : IsPullback fst snd f g) :

IsPushout g.op f.op snd.op fst.op

source

theorem CategoryTheory.IsPullback.unop {C : Type u₁} [Category.{v₁, u₁} C] {P X Y Z : Cᵒᵖ} {fst : P ⟶ X} {snd : P ⟶ Y} {f : X ⟶ Z} {g : Y ⟶ Z} (h : IsPullback fst snd f g) :

IsPushout g.unop f.unop snd.unop fst.unop

source

theorem CategoryTheory.IsPushout.flip {C : Type u₁} [Category.{v₁, u₁} C] {Z X Y P : C} {f : Z ⟶ X} {g : Z ⟶ Y} {inl : X ⟶ P} {inr : Y ⟶ P} (h : IsPushout f g inl inr) :

IsPushout g f inr inl

source

theorem CategoryTheory.IsPushout.flip_iff {C : Type u₁} [Category.{v₁, u₁} C] {Z X Y P : C} {f : Z ⟶ X} {g : Z ⟶ Y} {inl : X ⟶ P} {inr : Y ⟶ P} :

IsPushout f g inl inr ↔ IsPushout g f inr inl

source

theorem CategoryTheory.IsPushout.op {C : Type u₁} [Category.{v₁, u₁} C] {Z X Y P : C} {f : Z ⟶ X} {g : Z ⟶ Y} {inl : X ⟶ P} {inr : Y ⟶ P} (h : IsPushout f g inl inr) :

IsPullback inr.op inl.op g.op f.op

source

theorem CategoryTheory.IsPushout.unop {C : Type u₁} [Category.{v₁, u₁} C] {Z X Y P : Cᵒᵖ} {f : Z ⟶ X} {g : Z ⟶ Y} {inl : X ⟶ P} {inr : Y ⟶ P} (h : IsPushout f g inl inr) :

IsPullback inr.unop inl.unop g.unop f.unop

Documentation

Mathlib.CategoryTheory.Limits.Shapes.Pullback.IsPullback.Defs

Pullback and pushout squares #