Binary fans and cofans

A binary (co)fan is a (co)cone over a walking-pair diagram. These will be used (in a subsequent file) to define binary products and coproducts.

References

• Stacks: Products of pairs
• Stacks: coproducts of pairs

@[reducible, inline]

abbrev CategoryTheory.Limits.BinaryFan {C : Type u} [Category.{v, u} C] (X Y : C) : Type (max u v)

A binary fan is just a cone on a diagram indexing a product.

Equations

• CategoryTheory.Limits.BinaryFan X Y = CategoryTheory.Limits.Cone (CategoryTheory.Limits.pair X Y)

@[reducible, inline]

abbrev CategoryTheory.Limits.BinaryFan.fst {C : Type u} [Category.{v, u} C] {X Y : C} (s : BinaryFan X Y) : ((Functor.const (Discrete WalkingPair)).obj s.pt).obj { as := WalkingPair.left } ⟶ (pair X Y).obj { as := WalkingPair.left }

The first projection of a binary fan.

Equations

• s.fst = s.π.app { as := CategoryTheory.Limits.WalkingPair.left }

@[reducible, inline]

abbrev CategoryTheory.Limits.BinaryFan.snd {C : Type u} [Category.{v, u} C] {X Y : C} (s : BinaryFan X Y) : ((Functor.const (Discrete WalkingPair)).obj s.pt).obj { as := WalkingPair.right } ⟶ (pair X Y).obj { as := WalkingPair.right }

The second projection of a binary fan.

Equations

• s.snd = s.π.app { as := CategoryTheory.Limits.WalkingPair.right }

theorem CategoryTheory.Limits.BinaryFan.π_app_left {C : Type u} [Category.{v, u} C] {X Y : C} (s : BinaryFan X Y) : s.π.app { as := WalkingPair.left } = s.fst

theorem CategoryTheory.Limits.BinaryFan.π_app_right {C : Type u} [Category.{v, u} C] {X Y : C} (s : BinaryFan X Y) : s.π.app { as := WalkingPair.right } = s.snd

def CategoryTheory.Limits.BinaryFan.ext {C : Type u} [Category.{v, u} C] {A B : C} {c c' : BinaryFan A B} (e : c.pt ≅ c'.pt) (h₁ : c.fst = CategoryStruct.comp e.hom c'.fst) (h₂ : c.snd = CategoryStruct.comp e.hom c'.snd) : c ≅ c'

Constructs an isomorphism of BinaryFans out of an isomorphism of the tips that commutes with the projections.

Equations

• CategoryTheory.Limits.BinaryFan.ext e h₁ h₂ = CategoryTheory.Limits.Cone.ext e ⋯

@[simp]

theorem CategoryTheory.Limits.BinaryFan.ext_hom_hom {C : Type u} [Category.{v, u} C] {A B : C} {c c' : BinaryFan A B} (e : c.pt ≅ c'.pt) (h₁ : c.fst = CategoryStruct.comp e.hom c'.fst) (h₂ : c.snd = CategoryStruct.comp e.hom c'.snd) : (ext e h₁ h₂).hom.hom = e.hom

def CategoryTheory.Limits.BinaryFan.IsLimit.mk {C : Type u} [Category.{v, u} C] {X Y : C} (s : BinaryFan X Y) (lift : {T : C} → (T ⟶ X) → (T ⟶ Y) → (T ⟶ s.pt)) (hl₁ : ∀ {T : C} (f : T ⟶ X) (g : T ⟶ Y), CategoryStruct.comp (lift f g) s.fst = f) (hl₂ : ∀ {T : C} (f : T ⟶ X) (g : T ⟶ Y), CategoryStruct.comp (lift f g) s.snd = g) (uniq : ∀ {T : C} (f : T ⟶ X) (g : T ⟶ Y) (m : T ⟶ s.pt), CategoryStruct.comp m s.fst = f → CategoryStruct.comp m s.snd = g → m = lift f g) : IsLimit s

A convenient way to show that a binary fan is a limit.

Equations

• One or more equations did not get rendered due to their size.

theorem CategoryTheory.Limits.BinaryFan.IsLimit.hom_ext {C : Type u} [Category.{v, u} C] {W X Y : C} {s : BinaryFan X Y} (h : IsLimit s) {f g : W ⟶ s.pt} (h₁ : CategoryStruct.comp f s.fst = CategoryStruct.comp g s.fst) (h₂ : CategoryStruct.comp f s.snd = CategoryStruct.comp g s.snd) : f = g

@[reducible, inline]

abbrev CategoryTheory.Limits.BinaryCofan {C : Type u} [Category.{v, u} C] (X Y : C) : Type (max u v)

A binary cofan is just a cocone on a diagram indexing a coproduct.

Equations

• CategoryTheory.Limits.BinaryCofan X Y = CategoryTheory.Limits.Cocone (CategoryTheory.Limits.pair X Y)

@[reducible, inline]

abbrev CategoryTheory.Limits.BinaryCofan.inl {C : Type u} [Category.{v, u} C] {X Y : C} (s : BinaryCofan X Y) : (pair X Y).obj { as := WalkingPair.left } ⟶ ((Functor.const (Discrete WalkingPair)).obj s.pt).obj { as := WalkingPair.left }

The first inclusion of a binary cofan.

Equations

• s.inl = s.ι.app { as := CategoryTheory.Limits.WalkingPair.left }

@[reducible, inline]

abbrev CategoryTheory.Limits.BinaryCofan.inr {C : Type u} [Category.{v, u} C] {X Y : C} (s : BinaryCofan X Y) : (pair X Y).obj { as := WalkingPair.right } ⟶ ((Functor.const (Discrete WalkingPair)).obj s.pt).obj { as := WalkingPair.right }

The second inclusion of a binary cofan.

Equations

• s.inr = s.ι.app { as := CategoryTheory.Limits.WalkingPair.right }

def CategoryTheory.Limits.BinaryCofan.ext {C : Type u} [Category.{v, u} C] {A B : C} {c c' : BinaryCofan A B} (e : c.pt ≅ c'.pt) (h₁ : CategoryStruct.comp c.inl e.hom = c'.inl) (h₂ : CategoryStruct.comp c.inr e.hom = c'.inr) : c ≅ c'

Constructs an isomorphism of BinaryCofans out of an isomorphism of the tips that commutes with the injections.

Equations

• CategoryTheory.Limits.BinaryCofan.ext e h₁ h₂ = CategoryTheory.Limits.Cocone.ext e ⋯

@[simp]

theorem CategoryTheory.Limits.BinaryCofan.ext_hom_hom {C : Type u} [Category.{v, u} C] {A B : C} {c c' : BinaryCofan A B} (e : c.pt ≅ c'.pt) (h₁ : CategoryStruct.comp c.inl e.hom = c'.inl) (h₂ : CategoryStruct.comp c.inr e.hom = c'.inr) : (ext e h₁ h₂).hom.hom = e.hom

theorem CategoryTheory.Limits.BinaryCofan.ι_app_left {C : Type u} [Category.{v, u} C] {X Y : C} (s : BinaryCofan X Y) : s.ι.app { as := WalkingPair.left } = s.inl

theorem CategoryTheory.Limits.BinaryCofan.ι_app_right {C : Type u} [Category.{v, u} C] {X Y : C} (s : BinaryCofan X Y) : s.ι.app { as := WalkingPair.right } = s.inr

def CategoryTheory.Limits.BinaryCofan.IsColimit.mk {C : Type u} [Category.{v, u} C] {X Y : C} (s : BinaryCofan X Y) (desc : {T : C} → (X ⟶ T) → (Y ⟶ T) → (s.pt ⟶ T)) (hd₁ : ∀ {T : C} (f : X ⟶ T) (g : Y ⟶ T), CategoryStruct.comp s.inl (desc f g) = f) (hd₂ : ∀ {T : C} (f : X ⟶ T) (g : Y ⟶ T), CategoryStruct.comp s.inr (desc f g) = g) (uniq : ∀ {T : C} (f : X ⟶ T) (g : Y ⟶ T) (m : s.pt ⟶ T), CategoryStruct.comp s.inl m = f → CategoryStruct.comp s.inr m = g → m = desc f g) : IsColimit s

A convenient way to show that a binary cofan is a colimit.

Equations

• One or more equations did not get rendered due to their size.

theorem CategoryTheory.Limits.BinaryCofan.IsColimit.hom_ext {C : Type u} [Category.{v, u} C] {W X Y : C} {s : BinaryCofan X Y} (h : IsColimit s) {f g : s.pt ⟶ W} (h₁ : CategoryStruct.comp s.inl f = CategoryStruct.comp s.inl g) (h₂ : CategoryStruct.comp s.inr f = CategoryStruct.comp s.inr g) : f = g

@[implicit_reducible]

def CategoryTheory.Limits.BinaryFan.mk {C : Type u} [Category.{v, u} C] {X Y P : C} (π₁ : P ⟶ X) (π₂ : P ⟶ Y) : BinaryFan X Y

A binary fan with vertex P consists of the two projections π₁ : P ⟶ X and π₂ : P ⟶ Y.

Equations

• One or more equations did not get rendered due to their size.

@[simp]

theorem CategoryTheory.Limits.BinaryFan.mk_pt {C : Type u} [Category.{v, u} C] {X Y P : C} (π₁ : P ⟶ X) (π₂ : P ⟶ Y) : (mk π₁ π₂).pt = P

@[implicit_reducible]

def CategoryTheory.Limits.BinaryCofan.mk {C : Type u} [Category.{v, u} C] {X Y P : C} (ι₁ : X ⟶ P) (ι₂ : Y ⟶ P) : BinaryCofan X Y

A binary cofan with vertex P consists of the two inclusions ι₁ : X ⟶ P and ι₂ : Y ⟶ P.

Equations

• One or more equations did not get rendered due to their size.

@[simp]

theorem CategoryTheory.Limits.BinaryCofan.mk_pt {C : Type u} [Category.{v, u} C] {X Y P : C} (ι₁ : X ⟶ P) (ι₂ : Y ⟶ P) : (mk ι₁ ι₂).pt = P

@[simp]

theorem CategoryTheory.Limits.BinaryFan.mk_fst {C : Type u} [Category.{v, u} C] {X Y P : C} (π₁ : P ⟶ X) (π₂ : P ⟶ Y) : (mk π₁ π₂).fst = π₁

@[simp]

theorem CategoryTheory.Limits.BinaryFan.mk_snd {C : Type u} [Category.{v, u} C] {X Y P : C} (π₁ : P ⟶ X) (π₂ : P ⟶ Y) : (mk π₁ π₂).snd = π₂

@[simp]

theorem CategoryTheory.Limits.BinaryCofan.mk_inl {C : Type u} [Category.{v, u} C] {X Y P : C} (ι₁ : X ⟶ P) (ι₂ : Y ⟶ P) : (mk ι₁ ι₂).inl = ι₁

@[simp]

theorem CategoryTheory.Limits.BinaryCofan.mk_inr {C : Type u} [Category.{v, u} C] {X Y P : C} (ι₁ : X ⟶ P) (ι₂ : Y ⟶ P) : (mk ι₁ ι₂).inr = ι₂

def CategoryTheory.Limits.isoBinaryFanMk {C : Type u} [Category.{v, u} C] {X Y : C} (c : BinaryFan X Y) : c ≅ BinaryFan.mk c.fst c.snd

Every BinaryFan is isomorphic to an application of BinaryFan.mk.

Equations

• CategoryTheory.Limits.isoBinaryFanMk c = CategoryTheory.Limits.Cone.ext (CategoryTheory.Iso.refl c.pt) ⋯

def CategoryTheory.Limits.isoBinaryCofanMk {C : Type u} [Category.{v, u} C] {X Y : C} (c : BinaryCofan X Y) : c ≅ BinaryCofan.mk c.inl c.inr

Every BinaryFan is isomorphic to an application of BinaryFan.mk.

Equations

• CategoryTheory.Limits.isoBinaryCofanMk c = CategoryTheory.Limits.Cocone.ext (CategoryTheory.Iso.refl c.pt) ⋯

def CategoryTheory.Limits.BinaryFan.isLimitMk {C : Type u} [Category.{v, u} C] {X Y W : C} {fst : W ⟶ X} {snd : W ⟶ Y} (lift : (s : BinaryFan X Y) → s.pt ⟶ W) (fac_left : ∀ (s : BinaryFan X Y), CategoryStruct.comp (lift s) fst = s.fst) (fac_right : ∀ (s : BinaryFan X Y), CategoryStruct.comp (lift s) snd = s.snd) (uniq : ∀ (s : BinaryFan X Y) (m : s.pt ⟶ W), CategoryStruct.comp m fst = s.fst → CategoryStruct.comp m snd = s.snd → m = lift s) : IsLimit (mk fst snd)

This is a more convenient formulation to show that a BinaryFan constructed using BinaryFan.mk is a limit cone.

Equations

• CategoryTheory.Limits.BinaryFan.isLimitMk lift fac_left fac_right uniq = { lift := lift, fac := ⋯, uniq := ⋯ }

def CategoryTheory.Limits.BinaryCofan.isColimitMk {C : Type u} [Category.{v, u} C] {X Y W : C} {inl : X ⟶ W} {inr : Y ⟶ W} (desc : (s : BinaryCofan X Y) → W ⟶ s.pt) (fac_left : ∀ (s : BinaryCofan X Y), CategoryStruct.comp inl (desc s) = s.inl) (fac_right : ∀ (s : BinaryCofan X Y), CategoryStruct.comp inr (desc s) = s.inr) (uniq : ∀ (s : BinaryCofan X Y) (m : W ⟶ s.pt), CategoryStruct.comp inl m = s.inl → CategoryStruct.comp inr m = s.inr → m = desc s) : IsColimit (mk inl inr)

This is a more convenient formulation to show that a BinaryCofan constructed using BinaryCofan.mk is a colimit cocone.

Equations

• CategoryTheory.Limits.BinaryCofan.isColimitMk desc fac_left fac_right uniq = { desc := desc, fac := ⋯, uniq := ⋯ }

def CategoryTheory.Limits.BinaryFan.IsLimit.lift {C : Type u} [Category.{v, u} C] {X Y W : C} {s : BinaryFan X Y} (h : IsLimit s) (f : W ⟶ X) (g : W ⟶ Y) : W ⟶ s.pt

If s is a limit binary fan over X and Y, then every pair of morphisms f : W ⟶ X and g : W ⟶ Y induces a morphism l : W ⟶ s.pt satisfying l ≫ s.fst = f and l ≫ s.snd = g.

Equations

• CategoryTheory.Limits.BinaryFan.IsLimit.lift h f g = h.lift (CategoryTheory.Limits.BinaryFan.mk f g)

@[simp]

theorem CategoryTheory.Limits.BinaryFan.IsLimit.lift_fst {C : Type u} [Category.{v, u} C] {X Y W : C} {s : BinaryFan X Y} (h : IsLimit s) (f : W ⟶ X) (g : W ⟶ Y) : CategoryStruct.comp (lift h f g) s.fst = f

@[simp]

theorem CategoryTheory.Limits.BinaryFan.IsLimit.lift_fst_assoc {C : Type u} [Category.{v, u} C] {X Y W : C} {s : BinaryFan X Y} (h : IsLimit s) (f : W ⟶ X) (g : W ⟶ Y) {Z : C} (h✝ : (pair X Y).obj { as := WalkingPair.left } ⟶ Z) : CategoryStruct.comp (lift h f g) (CategoryStruct.comp s.fst h✝) = CategoryStruct.comp f h✝

@[simp]

theorem CategoryTheory.Limits.BinaryFan.IsLimit.lift_snd {C : Type u} [Category.{v, u} C] {X Y W : C} {s : BinaryFan X Y} (h : IsLimit s) (f : W ⟶ X) (g : W ⟶ Y) : CategoryStruct.comp (lift h f g) s.snd = g

@[simp]

theorem CategoryTheory.Limits.BinaryFan.IsLimit.lift_snd_assoc {C : Type u} [Category.{v, u} C] {X Y W : C} {s : BinaryFan X Y} (h : IsLimit s) (f : W ⟶ X) (g : W ⟶ Y) {Z : C} (h✝ : (pair X Y).obj { as := WalkingPair.right } ⟶ Z) : CategoryStruct.comp (lift h f g) (CategoryStruct.comp s.snd h✝) = CategoryStruct.comp g h✝

def CategoryTheory.Limits.BinaryFan.IsLimit.lift' {C : Type u} [Category.{v, u} C] {W X Y : C} {s : BinaryFan X Y} (h : IsLimit s) (f : W ⟶ X) (g : W ⟶ Y) : { l : W ⟶ s.pt // CategoryStruct.comp l s.fst = f ∧ CategoryStruct.comp l s.snd = g }

If s is a limit binary fan over X and Y, then every pair of morphisms f : W ⟶ X and g : W ⟶ Y induces a morphism l : W ⟶ s.pt satisfying l ≫ s.fst = f and l ≫ s.snd = g.

Equations

• CategoryTheory.Limits.BinaryFan.IsLimit.lift' h f g = ⟨h.lift (CategoryTheory.Limits.BinaryFan.mk f g), ⋯⟩

@[simp]

theorem CategoryTheory.Limits.BinaryFan.IsLimit.lift'_coe {C : Type u} [Category.{v, u} C] {W X Y : C} {s : BinaryFan X Y} (h : IsLimit s) (f : W ⟶ X) (g : W ⟶ Y) : ↑(lift' h f g) = h.lift (BinaryFan.mk f g)

def CategoryTheory.Limits.BinaryCofan.IsColimit.desc {C : Type u} [Category.{v, u} C] {X Y W : C} {s : BinaryCofan X Y} (h : IsColimit s) (f : X ⟶ W) (g : Y ⟶ W) : s.pt ⟶ W

If s is a colimit binary cofan over X and Y, then every pair of morphisms f : X ⟶ W and g : Y ⟶ W induces a morphism l : s.pt ⟶ W satisfying s.inl ≫ l = f and s.inr ≫ l = g.

Equations

• CategoryTheory.Limits.BinaryCofan.IsColimit.desc h f g = h.desc (CategoryTheory.Limits.BinaryCofan.mk f g)

@[simp]

theorem CategoryTheory.Limits.BinaryCofan.IsColimit.inl_desc {C : Type u} [Category.{v, u} C] {X Y W : C} {s : BinaryCofan X Y} (h : IsColimit s) (f : X ⟶ W) (g : Y ⟶ W) : CategoryStruct.comp s.inl (desc h f g) = f

@[simp]

theorem CategoryTheory.Limits.BinaryCofan.IsColimit.inl_desc_assoc {C : Type u} [Category.{v, u} C] {X Y W : C} {s : BinaryCofan X Y} (h : IsColimit s) (f : X ⟶ W) (g : Y ⟶ W) {Z : C} (h✝ : W ⟶ Z) : CategoryStruct.comp s.inl (CategoryStruct.comp (desc h f g) h✝) = CategoryStruct.comp f h✝

@[simp]

theorem CategoryTheory.Limits.BinaryCofan.IsColimit.inr_desc {C : Type u} [Category.{v, u} C] {X Y W : C} {s : BinaryCofan X Y} (h : IsColimit s) (f : X ⟶ W) (g : Y ⟶ W) : CategoryStruct.comp s.inr (desc h f g) = g

@[simp]

theorem CategoryTheory.Limits.BinaryCofan.IsColimit.inr_desc_assoc {C : Type u} [Category.{v, u} C] {X Y W : C} {s : BinaryCofan X Y} (h : IsColimit s) (f : X ⟶ W) (g : Y ⟶ W) {Z : C} (h✝ : W ⟶ Z) : CategoryStruct.comp s.inr (CategoryStruct.comp (desc h f g) h✝) = CategoryStruct.comp g h✝

def CategoryTheory.Limits.BinaryCofan.IsColimit.desc' {C : Type u} [Category.{v, u} C] {W X Y : C} {s : BinaryCofan X Y} (h : IsColimit s) (f : X ⟶ W) (g : Y ⟶ W) : { l : s.pt ⟶ W // CategoryStruct.comp s.inl l = f ∧ CategoryStruct.comp s.inr l = g }

If s is a colimit binary cofan over X and Y, then every pair of morphisms f : X ⟶ W and g : Y ⟶ W induces a morphism l : s.pt ⟶ W satisfying s.inl ≫ l = f and s.inr ≫ l = g.

Equations

• CategoryTheory.Limits.BinaryCofan.IsColimit.desc' h f g = ⟨h.desc (CategoryTheory.Limits.BinaryCofan.mk f g), ⋯⟩

@[simp]

theorem CategoryTheory.Limits.BinaryCofan.IsColimit.desc'_coe {C : Type u} [Category.{v, u} C] {W X Y : C} {s : BinaryCofan X Y} (h : IsColimit s) (f : X ⟶ W) (g : Y ⟶ W) : ↑(desc' h f g) = h.desc (BinaryCofan.mk f g)

def CategoryTheory.Limits.BinaryFan.isLimitFlip {C : Type u} [Category.{v, u} C] {X Y : C} {c : BinaryFan X Y} (hc : IsLimit c) : IsLimit (mk c.snd c.fst)

Binary products are symmetric.

Equations

• One or more equations did not get rendered due to their size.

theorem CategoryTheory.Limits.BinaryFan.isLimit_iff_isIso_fst {C : Type u} [Category.{v, u} C] {X Y : C} (h : IsTerminal Y) (c : BinaryFan X Y) : Nonempty (IsLimit c) ↔ IsIso c.fst

theorem CategoryTheory.Limits.BinaryFan.isLimit_iff_isIso_snd {C : Type u} [Category.{v, u} C] {X Y : C} (h : IsTerminal X) (c : BinaryFan X Y) : Nonempty (IsLimit c) ↔ IsIso c.snd

noncomputable def CategoryTheory.Limits.BinaryFan.isLimitCompLeftIso {C : Type u} [Category.{v, u} C] {X Y X' : C} (c : BinaryFan X Y) (f : X ⟶ X') [IsIso f] (h : IsLimit c) : IsLimit (mk (CategoryStruct.comp c.fst f) c.snd)

If X' ≅ X, then X × Y also is the product of X' and Y.

Equations

• One or more equations did not get rendered due to their size.

noncomputable def CategoryTheory.Limits.BinaryFan.isLimitCompRightIso {C : Type u} [Category.{v, u} C] {X Y Y' : C} (c : BinaryFan X Y) (f : Y ⟶ Y') [IsIso f] (h : IsLimit c) : IsLimit (mk c.fst (CategoryStruct.comp c.snd f))

If Y' ≅ Y, then X x Y also is the product of X and Y'.

Equations

• One or more equations did not get rendered due to their size.

def CategoryTheory.Limits.BinaryCofan.isColimitFlip {C : Type u} [Category.{v, u} C] {X Y : C} {c : BinaryCofan X Y} (hc : IsColimit c) : IsColimit (mk c.inr c.inl)

Binary coproducts are symmetric.

Equations

• One or more equations did not get rendered due to their size.

theorem CategoryTheory.Limits.BinaryCofan.isColimit_iff_isIso_inl {C : Type u} [Category.{v, u} C] {X Y : C} (h : IsInitial Y) (c : BinaryCofan X Y) : Nonempty (IsColimit c) ↔ IsIso c.inl

theorem CategoryTheory.Limits.BinaryCofan.isColimit_iff_isIso_inr {C : Type u} [Category.{v, u} C] {X Y : C} (h : IsInitial X) (c : BinaryCofan X Y) : Nonempty (IsColimit c) ↔ IsIso c.inr

noncomputable def CategoryTheory.Limits.BinaryCofan.isColimitCompLeftIso {C : Type u} [Category.{v, u} C] {X Y X' : C} (c : BinaryCofan X Y) (f : X' ⟶ X) [IsIso f] (h : IsColimit c) : IsColimit (mk (CategoryStruct.comp f c.inl) c.inr)

If X' ≅ X, then X ⨿ Y also is the coproduct of X' and Y.

Equations

• One or more equations did not get rendered due to their size.

noncomputable def CategoryTheory.Limits.BinaryCofan.isColimitCompRightIso {C : Type u} [Category.{v, u} C] {X Y Y' : C} (c : BinaryCofan X Y) (f : Y' ⟶ Y) [IsIso f] (h : IsColimit c) : IsColimit (mk c.inl (CategoryStruct.comp f c.inr))

If Y' ≅ Y, then X ⨿ Y also is the coproduct of X and Y'.

Equations

• One or more equations did not get rendered due to their size.

@[reducible, inline]

abbrev CategoryTheory.Limits.BinaryFan.map {C : Type u} [Category.{v, u} C] {D : Type u_1} [Category.{v_1, u_1} D] (F : Functor C D) {X Y : C} (s : BinaryFan X Y) : BinaryFan (F.obj X) (F.obj Y)

The image of a binary fan by a functor.

Equations

• CategoryTheory.Limits.BinaryFan.map F s = CategoryTheory.Limits.BinaryFan.mk (F.map s.fst) (F.map s.snd)

@[simp]

theorem CategoryTheory.Limits.BinaryFan.map_fst {C : Type u} [Category.{v, u} C] {D : Type u_1} [Category.{v_1, u_1} D] {F : Functor C D} {X Y : C} (s : BinaryFan X Y) : (map F s).fst = F.map s.fst

@[simp]

theorem CategoryTheory.Limits.BinaryFan.map_snd {C : Type u} [Category.{v, u} C] {D : Type u_1} [Category.{v_1, u_1} D] {F : Functor C D} {X Y : C} (s : BinaryFan X Y) : (map F s).snd = F.map s.snd

@[reducible, inline]

abbrev CategoryTheory.Limits.BinaryCofan.map {C : Type u} [Category.{v, u} C] {D : Type u_1} [Category.{v_1, u_1} D] (F : Functor C D) {X Y : C} (s : BinaryCofan X Y) : BinaryCofan (F.obj X) (F.obj Y)

The image of a binary cofan by a functor.

Equations

• CategoryTheory.Limits.BinaryCofan.map F s = CategoryTheory.Limits.BinaryCofan.mk (F.map s.inl) (F.map s.inr)

@[simp]

theorem CategoryTheory.Limits.BinaryCofan.map_inl {C : Type u} [Category.{v, u} C] {D : Type u_1} [Category.{v_1, u_1} D] {F : Functor C D} {X Y : C} (s : BinaryCofan X Y) : (map F s).inl = F.map s.inl

@[simp]

theorem CategoryTheory.Limits.BinaryCofan.map_inr {C : Type u} [Category.{v, u} C] {D : Type u_1} [Category.{v_1, u_1} D] {F : Functor C D} {X Y : C} (s : BinaryCofan X Y) : (map F s).inr = F.map s.inr

def CategoryTheory.Limits.BinaryFan.isLimitMapConeEquiv {C : Type u} [Category.{v, u} C] {D : Type u_1} [Category.{v_1, u_1} D] {F : Functor C D} {X Y : C} {s : BinaryFan X Y} : IsLimit (F.mapCone s) ≃ IsLimit (map F s)

F.mapCone s being limiting is the same as the induced binary fan being limiting.

Equations

• One or more equations did not get rendered due to their size.

def CategoryTheory.Limits.BinaryCofan.isColimitMapConeEquiv {C : Type u} [Category.{v, u} C] {D : Type u_1} [Category.{v_1, u_1} D] {F : Functor C D} {X Y : C} {s : BinaryCofan X Y} : IsColimit (F.mapCocone s) ≃ IsColimit (map F s)

F.mapCocone s being colimiting is the same as the induced binary cofan being colimiting.

Equations

• One or more equations did not get rendered due to their size.

@[reducible, inline]

abbrev CategoryTheory.Limits.BinaryFan.op {C : Type u} [Category.{v, u} C] {X Y : C} (c : BinaryFan X Y) : BinaryCofan (Opposite.op X) (Opposite.op Y)

A binary fan gives a binary cofan in the opposite category.

Equations

• c.op = CategoryTheory.Limits.BinaryCofan.mk c.fst.op c.snd.op

@[reducible, inline]

abbrev CategoryTheory.Limits.BinaryCofan.op {C : Type u} [Category.{v, u} C] {X Y : C} (c : BinaryCofan X Y) : BinaryFan (Opposite.op X) (Opposite.op Y)

A binary cofan gives a binary fan in the opposite category.

Equations

• c.op = CategoryTheory.Limits.BinaryFan.mk c.inl.op c.inr.op

@[reducible, inline]

abbrev CategoryTheory.Limits.BinaryFan.unop {C : Type u} [Category.{v, u} C] {X Y : C} (c : BinaryFan (Opposite.op X) (Opposite.op Y)) : BinaryCofan X Y

A binary fan in the opposite category gives a binary cofan.

Equations

• c.unop = CategoryTheory.Limits.BinaryCofan.mk c.fst.unop c.snd.unop

@[reducible, inline]

abbrev CategoryTheory.Limits.BinaryCofan.unop {C : Type u} [Category.{v, u} C] {X Y : C} (c : BinaryCofan (Opposite.op X) (Opposite.op Y)) : BinaryFan X Y

A binary cofan in the opposite category gives a binary fan.

Equations

• c.unop = CategoryTheory.Limits.BinaryFan.mk c.inl.unop c.inr.unop

@[simp]

theorem CategoryTheory.Limits.BinaryFan.op_mk {C : Type u} [Category.{v, u} C] {X Y P : C} (π₁ : P ⟶ X) (π₂ : P ⟶ Y) : (mk π₁ π₂).op = BinaryCofan.mk π₁.op π₂.op

@[simp]

theorem CategoryTheory.Limits.BinaryFan.unop_mk {C : Type u} [Category.{v, u} C] {X Y P : C} (π₁ : Opposite.op P ⟶ Opposite.op X) (π₂ : Opposite.op P ⟶ Opposite.op Y) : (mk π₁ π₂).unop = BinaryCofan.mk π₁.unop π₂.unop

@[simp]

theorem CategoryTheory.Limits.BinaryCofan.op_mk {C : Type u} [Category.{v, u} C] {X Y P : C} (ι₁ : X ⟶ P) (ι₂ : Y ⟶ P) : (mk ι₁ ι₂).op = BinaryFan.mk ι₁.op ι₂.op

@[simp]

theorem CategoryTheory.Limits.BinaryCofan.unop_mk {C : Type u} [Category.{v, u} C] {X Y P : C} (ι₁ : Opposite.op X ⟶ Opposite.op P) (ι₂ : Opposite.op Y ⟶ Opposite.op P) : (mk ι₁ ι₂).unop = BinaryFan.mk ι₁.unop ι₂.unop

def CategoryTheory.Limits.BinaryFan.IsLimit.op {C : Type u} [Category.{v, u} C] {X Y : C} {c : BinaryFan X Y} (hc : IsLimit c) : IsColimit c.op

If a BinaryFan is a limit, then its opposite is a colimit.

Equations

• One or more equations did not get rendered due to their size.

def CategoryTheory.Limits.BinaryCofan.IsColimit.op {C : Type u} [Category.{v, u} C] {X Y : C} {c : BinaryCofan X Y} (hc : IsColimit c) : IsLimit c.op

If a BinaryCofan is a colimit, then its opposite is a limit.

Equations

• One or more equations did not get rendered due to their size.

def CategoryTheory.Limits.BinaryFan.IsLimit.unop {C : Type u} [Category.{v, u} C] {X Y : C} {c : BinaryFan (Opposite.op X) (Opposite.op Y)} (hc : IsLimit c) : IsColimit c.unop

If a BinaryFan in the opposite category is a limit, then its unop is a colimit.

Equations

• CategoryTheory.Limits.BinaryFan.IsLimit.unop hc = CategoryTheory.Limits.BinaryCofan.isColimitMk (fun (s : CategoryTheory.Limits.BinaryCofan X Y) => (hc.lift s.op).unop) ⋯ ⋯ ⋯

def CategoryTheory.Limits.BinaryCofan.IsColimit.unop {C : Type u} [Category.{v, u} C] {X Y : C} {c : BinaryCofan (Opposite.op X) (Opposite.op Y)} (hc : IsColimit c) : IsLimit c.unop

If a BinaryCofan in the opposite category is a colimit, then its unop is a limit.

Equations

• CategoryTheory.Limits.BinaryCofan.IsColimit.unop hc = CategoryTheory.Limits.BinaryFan.isLimitMk (fun (s : CategoryTheory.Limits.BinaryFan X Y) => (hc.desc s.op).unop) ⋯ ⋯ ⋯

def CategoryTheory.Limits.BinaryFan.swap {C : Type u} [Category.{v, u} C] {X Y : C} (s : BinaryFan X Y) : BinaryFan Y X

Swap the two sides of a BinaryFan.

Equations

• s.swap = CategoryTheory.Limits.BinaryFan.mk s.snd s.fst

@[simp]

theorem CategoryTheory.Limits.BinaryFan.swap_fst {C : Type u} [Category.{v, u} C] {X Y : C} (s : BinaryFan X Y) : s.swap.fst = s.snd

@[simp]

theorem CategoryTheory.Limits.BinaryFan.swap_snd {C : Type u} [Category.{v, u} C] {X Y : C} (s : BinaryFan X Y) : s.swap.snd = s.fst

def CategoryTheory.Limits.IsLimit.binaryFanSwap {C : Type u} [Category.{v, u} C] {X Y : C} {s : BinaryFan X Y} (I : IsLimit s) : IsLimit s.swap

If a binary fan s over X Y is a limit cone, then s.swap is a limit cone over Y X.

Equations

• I.binaryFanSwap = { lift := fun (t : CategoryTheory.Limits.Cone (CategoryTheory.Limits.pair Y X)) => I.lift (CategoryTheory.Limits.BinaryFan.swap t), fac := ⋯, uniq := ⋯ }

@[simp]

theorem CategoryTheory.Limits.IsLimit.binaryFanSwap_lift {C : Type u} [Category.{v, u} C] {X Y : C} {s : BinaryFan X Y} (I : IsLimit s) (t : Cone (pair Y X)) : I.binaryFanSwap.lift t = I.lift (BinaryFan.swap t)

def CategoryTheory.Limits.BinaryFan.braiding {C : Type u} [Category.{v, u} C] {X Y : C} {s : BinaryFan X Y} {t : BinaryFan Y X} (P : IsLimit s) (Q : IsLimit t) : s.pt ≅ t.pt

Given a limit cone over X and Y, and another limit cone over Y and X, we can construct an isomorphism between the cone points. Relative to some fixed choice of limits cones for every pair, these isomorphisms constitute a braiding.

Equations

• CategoryTheory.Limits.BinaryFan.braiding P Q = P.conePointUniqueUpToIso Q.binaryFanSwap

@[simp]

theorem CategoryTheory.Limits.BinaryFan.braiding_hom_fst {C : Type u} [Category.{v, u} C] {X Y : C} {s : BinaryFan X Y} (P : IsLimit s) {t : BinaryFan Y X} (Q : IsLimit t) : CategoryStruct.comp (braiding P Q).hom t.fst = s.snd

@[simp]

theorem CategoryTheory.Limits.BinaryFan.braiding_hom_fst_assoc {C : Type u} [Category.{v, u} C] {X Y : C} {s : BinaryFan X Y} (P : IsLimit s) {t : BinaryFan Y X} (Q : IsLimit t) {Z : C} (h : (pair Y X).obj { as := WalkingPair.left } ⟶ Z) : CategoryStruct.comp (braiding P Q).hom (CategoryStruct.comp t.fst h) = CategoryStruct.comp s.snd h

@[simp]

theorem CategoryTheory.Limits.BinaryFan.braiding_hom_snd {C : Type u} [Category.{v, u} C] {X Y : C} {s : BinaryFan X Y} (P : IsLimit s) {t : BinaryFan Y X} (Q : IsLimit t) : CategoryStruct.comp (braiding P Q).hom t.snd = s.fst

@[simp]

theorem CategoryTheory.Limits.BinaryFan.braiding_hom_snd_assoc {C : Type u} [Category.{v, u} C] {X Y : C} {s : BinaryFan X Y} (P : IsLimit s) {t : BinaryFan Y X} (Q : IsLimit t) {Z : C} (h : (pair Y X).obj { as := WalkingPair.right } ⟶ Z) : CategoryStruct.comp (braiding P Q).hom (CategoryStruct.comp t.snd h) = CategoryStruct.comp s.fst h

@[simp]

theorem CategoryTheory.Limits.BinaryFan.braiding_inv_fst {C : Type u} [Category.{v, u} C] {X Y : C} {s : BinaryFan X Y} (P : IsLimit s) {t : BinaryFan Y X} (Q : IsLimit t) : CategoryStruct.comp (braiding P Q).inv s.fst = t.snd

@[simp]

theorem CategoryTheory.Limits.BinaryFan.braiding_inv_fst_assoc {C : Type u} [Category.{v, u} C] {X Y : C} {s : BinaryFan X Y} (P : IsLimit s) {t : BinaryFan Y X} (Q : IsLimit t) {Z : C} (h : (pair X Y).obj { as := WalkingPair.left } ⟶ Z) : CategoryStruct.comp (braiding P Q).inv (CategoryStruct.comp s.fst h) = CategoryStruct.comp t.snd h

@[simp]

theorem CategoryTheory.Limits.BinaryFan.braiding_inv_snd {C : Type u} [Category.{v, u} C] {X Y : C} {s : BinaryFan X Y} (P : IsLimit s) {t : BinaryFan Y X} (Q : IsLimit t) : CategoryStruct.comp (braiding P Q).inv s.snd = t.fst

@[simp]

theorem CategoryTheory.Limits.BinaryFan.braiding_inv_snd_assoc {C : Type u} [Category.{v, u} C] {X Y : C} {s : BinaryFan X Y} (P : IsLimit s) {t : BinaryFan Y X} (Q : IsLimit t) {Z : C} (h : (pair X Y).obj { as := WalkingPair.right } ⟶ Z) : CategoryStruct.comp (braiding P Q).inv (CategoryStruct.comp s.snd h) = CategoryStruct.comp t.fst h

def CategoryTheory.Limits.BinaryFan.assoc {C : Type u} [Category.{v, u} C] {X Y Z : C} {sXY : BinaryFan X Y} {sYZ : BinaryFan Y Z} (Q : IsLimit sYZ) (s : BinaryFan sXY.pt Z) : BinaryFan X sYZ.pt

Given binary fans sXY over X Y, and sYZ over Y Z, and s over sXY.X Z, if sYZ is a limit cone we can construct a binary fan over X sYZ.X.

This is an ingredient of building the associator for a Cartesian category.

Equations

• One or more equations did not get rendered due to their size.

@[simp]

theorem CategoryTheory.Limits.BinaryFan.assoc_fst {C : Type u} [Category.{v, u} C] {X Y Z : C} {sXY : BinaryFan X Y} {sYZ : BinaryFan Y Z} (Q : IsLimit sYZ) (s : BinaryFan sXY.pt Z) : (assoc Q s).fst = CategoryStruct.comp s.fst sXY.fst

@[simp]

theorem CategoryTheory.Limits.BinaryFan.assoc_snd {C : Type u} [Category.{v, u} C] {X Y Z : C} {sXY : BinaryFan X Y} {sYZ : BinaryFan Y Z} (Q : IsLimit sYZ) (s : BinaryFan sXY.pt Z) : (assoc Q s).snd = Q.lift (mk (CategoryStruct.comp s.fst sXY.snd) s.snd)

def CategoryTheory.Limits.BinaryFan.assocInv {C : Type u} [Category.{v, u} C] {X Y Z : C} {sXY : BinaryFan X Y} {sYZ : BinaryFan Y Z} (P : IsLimit sXY) (s : BinaryFan X sYZ.pt) : BinaryFan sXY.pt Z

Given binary fans sXY over X Y, and sYZ over Y Z, and s over X sYZ.X, if sYZ is a limit cone we can construct a binary fan over sXY.X Z.

This is an ingredient of building the associator for a Cartesian category.

Equations

• One or more equations did not get rendered due to their size.

@[simp]

theorem CategoryTheory.Limits.BinaryFan.assocInv_fst {C : Type u} [Category.{v, u} C] {X Y Z : C} {sXY : BinaryFan X Y} {sYZ : BinaryFan Y Z} (P : IsLimit sXY) (s : BinaryFan X sYZ.pt) : (assocInv P s).fst = IsLimit.lift P s.fst (CategoryStruct.comp s.snd sYZ.fst)

@[simp]

theorem CategoryTheory.Limits.BinaryFan.assocInv_snd {C : Type u} [Category.{v, u} C] {X Y Z : C} {sXY : BinaryFan X Y} {sYZ : BinaryFan Y Z} (P : IsLimit sXY) (s : BinaryFan X sYZ.pt) : (assocInv P s).snd = CategoryStruct.comp s.snd sYZ.snd

def CategoryTheory.Limits.IsLimit.assoc {C : Type u} [Category.{v, u} C] {X Y Z : C} {sXY : BinaryFan X Y} {sYZ : BinaryFan Y Z} (P : IsLimit sXY) (Q : IsLimit sYZ) {s : BinaryFan sXY.pt Z} (R : IsLimit s) : IsLimit (BinaryFan.assoc Q s)

If all the binary fans involved a limit cones, BinaryFan.assoc produces another limit cone.

Equations

• P.assoc Q R = { lift := fun (t : CategoryTheory.Limits.Cone (CategoryTheory.Limits.pair X sYZ.pt)) => R.lift (CategoryTheory.Limits.BinaryFan.assocInv P t), fac := ⋯, uniq := ⋯ }

@[simp]

theorem CategoryTheory.Limits.IsLimit.assoc_lift {C : Type u} [Category.{v, u} C] {X Y Z : C} {sXY : BinaryFan X Y} {sYZ : BinaryFan Y Z} (P : IsLimit sXY) (Q : IsLimit sYZ) {s : BinaryFan sXY.pt Z} (R : IsLimit s) (t : Cone (pair X sYZ.pt)) : (P.assoc Q R).lift t = R.lift (BinaryFan.assocInv P t)

@[reducible, inline]

abbrev CategoryTheory.Limits.BinaryFan.associator {C : Type u} [Category.{v, u} C] {X Y Z : C} {sXY : BinaryFan X Y} {sYZ : BinaryFan Y Z} (P : IsLimit sXY) (Q : IsLimit sYZ) {s : BinaryFan sXY.pt Z} (R : IsLimit s) {t : BinaryFan X sYZ.pt} (S : IsLimit t) : s.pt ≅ t.pt

Given two pairs of limit cones corresponding to the parenthesisations of X × Y × Z, we obtain an isomorphism between the cone points.

Equations

• CategoryTheory.Limits.BinaryFan.associator P Q R S = (P.assoc Q R).conePointUniqueUpToIso S

@[reducible, inline]

abbrev CategoryTheory.Limits.BinaryFan.associatorOfLimitCone {C : Type u} [Category.{v, u} C] (L : (X Y : C) → LimitCone (pair X Y)) (X Y Z : C) : (L (L X Y).cone.pt Z).cone.pt ≅ (L X (L Y Z).cone.pt).cone.pt

Given a fixed family of limit data for every pair X Y, we obtain an associator.

Equations

• One or more equations did not get rendered due to their size.

def CategoryTheory.Limits.BinaryFan.leftUnitor {C : Type u} [Category.{v, u} C] {X : C} {s : Cone (Functor.empty C)} (P : IsLimit s) {t : BinaryFan s.pt X} (Q : IsLimit t) : t.pt ≅ X

Construct a left unitor from specified limit cones.

Equations

• One or more equations did not get rendered due to their size.

@[simp]

theorem CategoryTheory.Limits.BinaryFan.leftUnitor_inv {C : Type u} [Category.{v, u} C] {X : C} {s : Cone (Functor.empty C)} (P : IsLimit s) {t : BinaryFan s.pt X} (Q : IsLimit t) : (leftUnitor P Q).inv = Q.lift (mk (P.lift { pt := X, π := { app := fun (x : Discrete PEmpty.{1}) => x.as.elim, naturality := ⋯ } }) (CategoryStruct.id { pt := X, π := { app := fun (x : Discrete PEmpty.{1}) => x.as.elim, naturality := ⋯ } }.pt))

@[simp]

theorem CategoryTheory.Limits.BinaryFan.leftUnitor_hom {C : Type u} [Category.{v, u} C] {X : C} {s : Cone (Functor.empty C)} (P : IsLimit s) {t : BinaryFan s.pt X} (Q : IsLimit t) : (leftUnitor P Q).hom = t.snd

def CategoryTheory.Limits.BinaryFan.rightUnitor {C : Type u} [Category.{v, u} C] {X : C} {s : Cone (Functor.empty C)} (P : IsLimit s) {t : BinaryFan X s.pt} (Q : IsLimit t) : t.pt ≅ X

Construct a right unitor from specified limit cones.

Equations

• One or more equations did not get rendered due to their size.

@[simp]

theorem CategoryTheory.Limits.BinaryFan.rightUnitor_hom {C : Type u} [Category.{v, u} C] {X : C} {s : Cone (Functor.empty C)} (P : IsLimit s) {t : BinaryFan X s.pt} (Q : IsLimit t) : (rightUnitor P Q).hom = t.fst

@[simp]

theorem CategoryTheory.Limits.BinaryFan.rightUnitor_inv {C : Type u} [Category.{v, u} C] {X : C} {s : Cone (Functor.empty C)} (P : IsLimit s) {t : BinaryFan X s.pt} (Q : IsLimit t) : (rightUnitor P Q).inv = Q.lift (mk (CategoryStruct.id X) (P.lift { pt := X, π := { app := fun (x : Discrete PEmpty.{1}) => x.as.elim, naturality := ⋯ } }))