Bi-Cartesian squares #

BicartesianSq f g h i is the proposition that

  W ---f---> X
  |          |
  g          h
  |          |
  v          v
  Y ---i---> Z

is a pullback square and a pushout square.

We show that the pullback and pushout squares for a biproduct are bi-Cartesian.

source

structure CategoryTheory.BicartesianSq {C : Type u₁} [Category.{v₁, u₁} C] {W X Y Z : C} (f : W ⟶ X) (g : W ⟶ Y) (h : X ⟶ Z) (i : Y ⟶ Z) extends CategoryTheory.IsPullback f g h i, CategoryTheory.IsPushout f g h i :

Prop

A bi-Cartesian square is a commutative square

  W ---f---> X
  |          |
  g          h
  |          |
  v          v
  Y ---i---> Z

that is both a pullback square and a pushout square.

w : CategoryStruct.comp f h = CategoryStruct.comp g i
isLimit' : Nonempty (Limits.IsLimit (Limits.PullbackCone.mk f g ⋯))
isColimit' : Nonempty (Limits.IsColimit (Limits.PushoutCocone.mk h i ⋯))

Instances For

source

theorem CategoryTheory.IsPullback.of_hasBinaryProduct {C : Type u₁} [Category.{v₁, u₁} C] [Limits.HasZeroObject C] [Limits.HasZeroMorphisms C] {X Y : C} [Limits.HasBinaryProduct X Y] :

IsPullback Limits.prod.fst Limits.prod.snd 0 0

source

@[simp]

theorem CategoryTheory.IsPullback.zero_left {C : Type u₁} [Category.{v₁, u₁} C] [Limits.HasZeroObject C] [Limits.HasZeroMorphisms C] (X : C) :

IsPullback 0 0 (CategoryStruct.id X) 0

The square with 0 : 0 ⟶ 0 on the left and 𝟙 X on the right is a pullback square.

source

@[simp]

theorem CategoryTheory.IsPullback.zero_top {C : Type u₁} [Category.{v₁, u₁} C] [Limits.HasZeroObject C] [Limits.HasZeroMorphisms C] (X : C) :

IsPullback 0 0 0 (CategoryStruct.id X)

The square with 0 : 0 ⟶ 0 on the top and 𝟙 X on the bottom is a pullback square.

source

@[simp]

theorem CategoryTheory.IsPullback.zero_right {C : Type u₁} [Category.{v₁, u₁} C] [Limits.HasZeroObject C] [Limits.HasZeroMorphisms C] (X : C) :

IsPullback 0 (CategoryStruct.id X) 0 0

The square with 0 : 0 ⟶ 0 on the right and 𝟙 X on the left is a pullback square.

source

@[simp]

theorem CategoryTheory.IsPullback.zero_bot {C : Type u₁} [Category.{v₁, u₁} C] [Limits.HasZeroObject C] [Limits.HasZeroMorphisms C] (X : C) :

IsPullback (CategoryStruct.id X) 0 0 0

The square with 0 : 0 ⟶ 0 on the bottom and 𝟙 X on the top is a pullback square.

source

theorem CategoryTheory.IsPullback.of_isBilimit {C : Type u₁} [Category.{v₁, u₁} C] [Limits.HasZeroObject C] [Limits.HasZeroMorphisms C] {X Y : C} {b : Limits.BinaryBicone X Y} (h : b.IsBilimit) :

IsPullback b.fst b.snd 0 0

source

@[simp]

theorem CategoryTheory.IsPullback.of_has_biproduct {C : Type u₁} [Category.{v₁, u₁} C] [Limits.HasZeroObject C] [Limits.HasZeroMorphisms C] (X Y : C) [Limits.HasBinaryBiproduct X Y] :

IsPullback Limits.biprod.fst Limits.biprod.snd 0 0

source

theorem CategoryTheory.IsPullback.inl_snd' {C : Type u₁} [Category.{v₁, u₁} C] [Limits.HasZeroObject C] [Limits.HasZeroMorphisms C] {X Y : C} {b : Limits.BinaryBicone X Y} (h : b.IsBilimit) :

IsPullback b.inl 0 b.snd 0

source

@[simp]

theorem CategoryTheory.IsPullback.inl_snd {C : Type u₁} [Category.{v₁, u₁} C] [Limits.HasZeroObject C] [Limits.HasZeroMorphisms C] (X Y : C) [Limits.HasBinaryBiproduct X Y] :

IsPullback Limits.biprod.inl 0 Limits.biprod.snd 0

The square

  X --inl--> X ⊞ Y
  |            |
  0           snd
  |            |
  v            v
  0 ---0-----> Y

is a pullback square.

source

theorem CategoryTheory.IsPullback.inr_fst' {C : Type u₁} [Category.{v₁, u₁} C] [Limits.HasZeroObject C] [Limits.HasZeroMorphisms C] {X Y : C} {b : Limits.BinaryBicone X Y} (h : b.IsBilimit) :

IsPullback b.inr 0 b.fst 0

source

@[simp]

theorem CategoryTheory.IsPullback.inr_fst {C : Type u₁} [Category.{v₁, u₁} C] [Limits.HasZeroObject C] [Limits.HasZeroMorphisms C] (X Y : C) [Limits.HasBinaryBiproduct X Y] :

IsPullback Limits.biprod.inr 0 Limits.biprod.fst 0

The square

  Y --inr--> X ⊞ Y
  |            |
  0           fst
  |            |
  v            v
  0 ---0-----> X

is a pullback square.

source

theorem CategoryTheory.IsPullback.of_is_bilimit' {C : Type u₁} [Category.{v₁, u₁} C] [Limits.HasZeroObject C] [Limits.HasZeroMorphisms C] {X Y : C} {b : Limits.BinaryBicone X Y} (h : b.IsBilimit) :

IsPullback 0 0 b.inl b.inr

source

theorem CategoryTheory.IsPullback.of_hasBinaryBiproduct {C : Type u₁} [Category.{v₁, u₁} C] [Limits.HasZeroObject C] [Limits.HasZeroMorphisms C] (X Y : C) [Limits.HasBinaryBiproduct X Y] :

IsPullback 0 0 Limits.biprod.inl Limits.biprod.inr

source

instance CategoryTheory.IsPullback.hasPullback_biprod_fst_biprod_snd {C : Type u₁} [Category.{v₁, u₁} C] [Limits.HasZeroObject C] [Limits.HasZeroMorphisms C] {X Y : C} [Limits.HasBinaryBiproduct X Y] :

Limits.HasPullback Limits.biprod.inl Limits.biprod.inr

source

noncomputable def CategoryTheory.IsPullback.pullbackBiprodInlBiprodInr {C : Type u₁} [Category.{v₁, u₁} C] [Limits.HasZeroObject C] [Limits.HasZeroMorphisms C] {X Y : C} [Limits.HasBinaryBiproduct X Y] :

Limits.pullback Limits.biprod.inl Limits.biprod.inr ≅ 0

The pullback of biprod.inl and biprod.inr is the zero object.

Instances For

source

theorem CategoryTheory.IsPushout.of_hasBinaryCoproduct {C : Type u₁} [Category.{v₁, u₁} C] [Limits.HasZeroObject C] [Limits.HasZeroMorphisms C] {X Y : C} [Limits.HasBinaryCoproduct X Y] :

IsPushout 0 0 Limits.coprod.inl Limits.coprod.inr

source

@[simp]

theorem CategoryTheory.IsPushout.zero_right {C : Type u₁} [Category.{v₁, u₁} C] [Limits.HasZeroObject C] [Limits.HasZeroMorphisms C] (X : C) :

IsPushout 0 (CategoryStruct.id X) 0 0

The square with 0 : 0 ⟶ 0 on the right and 𝟙 X on the left is a pushout square.

source

@[simp]

theorem CategoryTheory.IsPushout.zero_bot {C : Type u₁} [Category.{v₁, u₁} C] [Limits.HasZeroObject C] [Limits.HasZeroMorphisms C] (X : C) :

IsPushout (CategoryStruct.id X) 0 0 0

The square with 0 : 0 ⟶ 0 on the bottom and 𝟙 X on the top is a pushout square.

source

@[simp]

theorem CategoryTheory.IsPushout.zero_left {C : Type u₁} [Category.{v₁, u₁} C] [Limits.HasZeroObject C] [Limits.HasZeroMorphisms C] (X : C) :

IsPushout 0 0 (CategoryStruct.id X) 0

The square with 0 : 0 ⟶ 0 on the right left 𝟙 X on the right is a pushout square.

source

@[simp]

theorem CategoryTheory.IsPushout.zero_top {C : Type u₁} [Category.{v₁, u₁} C] [Limits.HasZeroObject C] [Limits.HasZeroMorphisms C] (X : C) :

IsPushout 0 0 0 (CategoryStruct.id X)

The square with 0 : 0 ⟶ 0 on the top and 𝟙 X on the bottom is a pushout square.

source

theorem CategoryTheory.IsPushout.of_isBilimit {C : Type u₁} [Category.{v₁, u₁} C] [Limits.HasZeroObject C] [Limits.HasZeroMorphisms C] {X Y : C} {b : Limits.BinaryBicone X Y} (h : b.IsBilimit) :

IsPushout 0 0 b.inl b.inr

source

@[simp]

theorem CategoryTheory.IsPushout.of_has_biproduct {C : Type u₁} [Category.{v₁, u₁} C] [Limits.HasZeroObject C] [Limits.HasZeroMorphisms C] (X Y : C) [Limits.HasBinaryBiproduct X Y] :

IsPushout 0 0 Limits.biprod.inl Limits.biprod.inr

source

theorem CategoryTheory.IsPushout.inl_snd' {C : Type u₁} [Category.{v₁, u₁} C] [Limits.HasZeroObject C] [Limits.HasZeroMorphisms C] {X Y : C} {b : Limits.BinaryBicone X Y} (h : b.IsBilimit) :

IsPushout b.inl 0 b.snd 0

source

theorem CategoryTheory.IsPushout.inl_snd {C : Type u₁} [Category.{v₁, u₁} C] [Limits.HasZeroObject C] [Limits.HasZeroMorphisms C] (X Y : C) [Limits.HasBinaryBiproduct X Y] :

IsPushout Limits.biprod.inl 0 Limits.biprod.snd 0

The square

  X --inl--> X ⊞ Y
  |            |
  0           snd
  |            |
  v            v
  0 ---0-----> Y

is a pushout square.

source

theorem CategoryTheory.IsPushout.inr_fst' {C : Type u₁} [Category.{v₁, u₁} C] [Limits.HasZeroObject C] [Limits.HasZeroMorphisms C] {X Y : C} {b : Limits.BinaryBicone X Y} (h : b.IsBilimit) :

IsPushout b.inr 0 b.fst 0

source

theorem CategoryTheory.IsPushout.inr_fst {C : Type u₁} [Category.{v₁, u₁} C] [Limits.HasZeroObject C] [Limits.HasZeroMorphisms C] (X Y : C) [Limits.HasBinaryBiproduct X Y] :

IsPushout Limits.biprod.inr 0 Limits.biprod.fst 0

The square

  Y --inr--> X ⊞ Y
  |            |
  0           fst
  |            |
  v            v
  0 ---0-----> X

is a pushout square.

source

theorem CategoryTheory.IsPushout.of_is_bilimit' {C : Type u₁} [Category.{v₁, u₁} C] [Limits.HasZeroObject C] [Limits.HasZeroMorphisms C] {X Y : C} {b : Limits.BinaryBicone X Y} (h : b.IsBilimit) :

IsPushout b.fst b.snd 0 0

source

theorem CategoryTheory.IsPushout.of_hasBinaryBiproduct {C : Type u₁} [Category.{v₁, u₁} C] [Limits.HasZeroObject C] [Limits.HasZeroMorphisms C] (X Y : C) [Limits.HasBinaryBiproduct X Y] :

IsPushout Limits.biprod.fst Limits.biprod.snd 0 0

source

instance CategoryTheory.IsPushout.hasPushout_biprod_fst_biprod_snd {C : Type u₁} [Category.{v₁, u₁} C] [Limits.HasZeroObject C] [Limits.HasZeroMorphisms C] {X Y : C} [Limits.HasBinaryBiproduct X Y] :

Limits.HasPushout Limits.biprod.fst Limits.biprod.snd

source

noncomputable def CategoryTheory.IsPushout.pushoutBiprodFstBiprodSnd {C : Type u₁} [Category.{v₁, u₁} C] [Limits.HasZeroObject C] [Limits.HasZeroMorphisms C] {X Y : C} [Limits.HasBinaryBiproduct X Y] :

Limits.pushout Limits.biprod.fst Limits.biprod.snd ≅ 0

The pushout of biprod.fst and biprod.snd is the zero object.

Instances For

source

theorem CategoryTheory.BicartesianSq.of_isPullback_isPushout {C : Type u₁} [Category.{v₁, u₁} C] {W X Y Z : C} {f : W ⟶ X} {g : W ⟶ Y} {h : X ⟶ Z} {i : Y ⟶ Z} (p₁ : IsPullback f g h i) (p₂ : IsPushout f g h i) :

BicartesianSq f g h i

source

theorem CategoryTheory.BicartesianSq.flip {C : Type u₁} [Category.{v₁, u₁} C] {W X Y Z : C} {f : W ⟶ X} {g : W ⟶ Y} {h : X ⟶ Z} {i : Y ⟶ Z} (p : BicartesianSq f g h i) :

BicartesianSq g f i h

source

theorem CategoryTheory.BicartesianSq.of_is_biproduct₁ {C : Type u₁} [Category.{v₁, u₁} C] [Limits.HasZeroObject C] [Limits.HasZeroMorphisms C] {X Y : C} {b : Limits.BinaryBicone X Y} (h : b.IsBilimit) :

BicartesianSq b.fst b.snd 0 0

 X ⊞ Y --fst--> X
   |            |
  snd           0
   |            |
   v            v
   Y -----0---> 0

is a bi-Cartesian square.

source

theorem CategoryTheory.BicartesianSq.of_is_biproduct₂ {C : Type u₁} [Category.{v₁, u₁} C] [Limits.HasZeroObject C] [Limits.HasZeroMorphisms C] {X Y : C} {b : Limits.BinaryBicone X Y} (h : b.IsBilimit) :

BicartesianSq 0 0 b.inl b.inr

   0 -----0---> X
   |            |
   0           inl
   |            |
   v            v
   Y --inr--> X ⊞ Y

is a bi-Cartesian square.

source

@[simp]

theorem CategoryTheory.BicartesianSq.of_has_biproduct₁ {C : Type u₁} [Category.{v₁, u₁} C] [Limits.HasZeroObject C] [Limits.HasZeroMorphisms C] {X Y : C} [Limits.HasBinaryBiproduct X Y] :

BicartesianSq Limits.biprod.fst Limits.biprod.snd 0 0

 X ⊞ Y --fst--> X
   |            |
  snd           0
   |            |
   v            v
   Y -----0---> 0

is a bi-Cartesian square.

source

@[simp]

theorem CategoryTheory.BicartesianSq.of_has_biproduct₂ {C : Type u₁} [Category.{v₁, u₁} C] [Limits.HasZeroObject C] [Limits.HasZeroMorphisms C] {X Y : C} [Limits.HasBinaryBiproduct X Y] :

BicartesianSq 0 0 Limits.biprod.inl Limits.biprod.inr

   0 -----0---> X
   |            |
   0           inl
   |            |
   v            v
   Y --inr--> X ⊞ Y

is a bi-Cartesian square.

Documentation

Mathlib.CategoryTheory.Limits.Shapes.Pullback.IsPullback.BicartesianSq

Bi-Cartesian squares #