Mathlib.CategoryTheory.Limits.Shapes.BinaryBiproducts

CategoryTheory.Limits.BinaryBicone structure

(P Q : C)

Full source

/-- A binary bicone for a pair of objects `P Q : C` consists of the cone point `X`,
maps from `X` to both `P` and `Q`, and maps from both `P` and `Q` to `X`,
so that `inl ≫ fst = 𝟙 P`, `inl ≫ snd = 0`, `inr ≫ fst = 0`, and `inr ≫ snd = 𝟙 Q` -/
structure BinaryBicone (P Q : C) where
  pt : C
  fst : pt ⟶ P
  snd : pt ⟶ Q
  inl : P ⟶ pt
  inr : Q ⟶ pt
  inl_fst : inl ≫ fst = 𝟙 P := by aesop
  inl_snd : inl ≫ snd = 0 := by aesop
  inr_fst : inr ≫ fst = 0 := by aesop
  inr_snd : inr ≫ snd = 𝟙 Q := by aesop

Binary Bicone

Informal description

A binary bicone for a pair of objects $ P $ and $ Q $ in a category $ C $ consists of an object $ X $ (the cone point), morphisms $ \text{fst} : X \to P $ and $ \text{snd} : X \to Q $, and morphisms $ \text{inl} : P \to X $ and $ \text{inr} : Q \to X $, satisfying the following conditions: - $ \text{inl} \circ \text{fst} = \text{id}_P $ - $ \text{inl} \circ \text{snd} = 0 $ - $ \text{inr} \circ \text{fst} = 0 $ - $ \text{inr} \circ \text{snd} = \text{id}_Q $

CategoryTheory.Limits.BinaryBiconeMorphism structure

{P Q : C} (A B : BinaryBicone P Q)

Full source

/-- A binary bicone morphism between two binary bicones for the same diagram is a morphism of the
binary bicone points which commutes with the cone and cocone legs. -/
structure BinaryBiconeMorphism {P Q : C} (A B : BinaryBicone P Q) where
  /-- A morphism between the two vertex objects of the bicones -/
  hom : A.pt ⟶ B.pt
  /-- The triangle consisting of the two natural transformations and `hom` commutes -/
  wfst : hom ≫ B.fst = A.fst := by aesop_cat
  /-- The triangle consisting of the two natural transformations and `hom` commutes -/
  wsnd : hom ≫ B.snd = A.snd := by aesop_cat
  /-- The triangle consisting of the two natural transformations and `hom` commutes -/
  winl : A.inl ≫ hom = B.inl := by aesop_cat
  /-- The triangle consisting of the two natural transformations and `hom` commutes -/
  winr : A.inr ≫ hom = B.inr := by aesop_cat

Binary Bicone Morphism

Informal description

A morphism between two binary bicones $ A $ and $ B $ for the same pair of objects $ P $ and $ Q $ in a category $ C $ consists of a morphism $ f : A.X \to B.X $ between the cone points that commutes with the cone and cocone legs. Specifically, the following diagrams must commute: - $ f \circ A.\text{fst} = B.\text{fst} $ - $ f \circ A.\text{snd} = B.\text{snd} $ - $ A.\text{inl} \circ f = B.\text{inl} $ - $ A.\text{inr} \circ f = B.\text{inr} $

CategoryTheory.Limits.BinaryBicone.category instance

{P Q : C} : Category (BinaryBicone P Q)

Full source

/-- The category of binary bicones on a given diagram. -/
@[simps]
instance BinaryBicone.category {P Q : C} : Category (BinaryBicone P Q) where
  Hom A B := BinaryBiconeMorphism A B
  comp f g := { hom := f.hom ≫ g.hom }
  id B := { hom := 𝟙 B.pt }

-- Porting note: if we do not have `simps` automatically generate the lemma for simplifying
-- the `hom` field of a category, we need to write the `ext` lemma in terms of the categorical
-- morphism, rather than the underlying structure.

Category of Binary Bicones

Informal description

For any pair of objects $P$ and $Q$ in a category $C$, the collection of binary bicones on $P$ and $Q$ forms a category. In this category, the morphisms between two binary bicones are given by morphisms between their cone points that commute with the bicone structure maps.

CategoryTheory.Limits.BinaryBiconeMorphism.ext theorem

{P Q : C} {c c' : BinaryBicone P Q} (f g : c ⟶ c') (w : f.hom = g.hom) : f = g

Full source

@[ext]
theorem BinaryBiconeMorphism.ext {P Q : C} {c c' : BinaryBicone P Q}
    (f g : c ⟶ c') (w : f.hom = g.hom) : f = g := by
  cases f
  cases g
  congr

Extensionality of Binary Bicone Morphisms

Informal description

Given two morphisms $f$ and $g$ between binary bicones $c$ and $c'$ for objects $P$ and $Q$ in a category $C$, if the underlying morphisms $f.\text{hom}$ and $g.\text{hom}$ from the cone point of $c$ to the cone point of $c'$ are equal, then $f = g$.

CategoryTheory.Limits.BinaryBicones.functoriality definition

: BinaryBicone P Q ⥤ BinaryBicone (F.obj P) (F.obj Q)

Full source

/-- A functor `F : C ⥤ D` sends binary bicones for `P` and `Q`
to binary bicones for `G.obj P` and `G.obj Q` functorially. -/
@[simps]
def functoriality : BinaryBiconeBinaryBicone P Q ⥤ BinaryBicone (F.obj P) (F.obj Q) where
  obj A :=
    { pt := F.obj A.pt
      fst := F.map A.fst
      snd := F.map A.snd
      inl := F.map A.inl
      inr := F.map A.inr
      inl_fst := by rw [← F.map_comp, A.inl_fst, F.map_id]
      inl_snd := by rw [← F.map_comp, A.inl_snd, F.map_zero]
      inr_fst := by rw [← F.map_comp, A.inr_fst, F.map_zero]
      inr_snd := by rw [← F.map_comp, A.inr_snd, F.map_id] }
  map f :=
    { hom := F.map f.hom
      wfst := by simp [-BinaryBiconeMorphism.wfst, ← f.wfst]
      wsnd := by simp [-BinaryBiconeMorphism.wsnd, ← f.wsnd]
      winl := by simp [-BinaryBiconeMorphism.winl, ← f.winl]
      winr := by simp [-BinaryBiconeMorphism.winr, ← f.winr] }

Functoriality of binary bicones

Informal description

Given a functor $ F : C \to D $ between categories $ C $ and $ D $, the functoriality construction maps a binary bicone for objects $ P $ and $ Q $ in $ C $ to a binary bicone for $ F(P) $ and $ F(Q) $ in $ D $. Specifically, for a binary bicone $ A $ in $ C $ with cone point $ A.pt $, the resulting bicone in $ D $ has: - Cone point $ F(A.pt) $, - Morphisms $ F(A.fst) : F(A.pt) \to F(P) $ and $ F(A.snd) : F(A.pt) \to F(Q) $, - Morphisms $ F(A.inl) : F(P) \to F(A.pt) $ and $ F(A.inr) : F(Q) \to F(A.pt) $. The construction ensures that the bicone conditions are preserved, i.e., the compositions $ F(A.inl) \circ F(A.fst) = \text{id}_{F(P)} $, $ F(A.inl) \circ F(A.snd) = 0 $, $ F(A.inr) \circ F(A.fst) = 0 $, and $ F(A.inr) \circ F(A.snd) = \text{id}_{F(Q)} $ hold in $ D $.

CategoryTheory.Limits.BinaryBicones.functoriality_full instance

[F.Full] [F.Faithful] : (functoriality P Q F).Full

Full source

instance functoriality_full [F.Full] [F.Faithful] : (functoriality P Q F).Full where
  map_surjective t :=
   ⟨{ hom := F.preimage t.hom
      winl := F.map_injective (by simpa using t.winl)
      winr := F.map_injective (by simpa using t.winr)
      wfst := F.map_injective (by simpa using t.wfst)
      wsnd := F.map_injective (by simpa using t.wsnd) }, by aesop_cat⟩

Fullness of Binary Bicone Functoriality for Full and Faithful Functors

Informal description

Given a full and faithful functor $F \colon C \to D$ between categories $C$ and $D$, the functoriality construction that maps binary bicones for objects $P$ and $Q$ in $C$ to binary bicones for $F(P)$ and $F(Q)$ in $D$ is a full functor.

CategoryTheory.Limits.BinaryBicones.functoriality_faithful instance

[F.Faithful] : (functoriality P Q F).Faithful

Full source

instance functoriality_faithful [F.Faithful] : (functoriality P Q F).Faithful where
  map_injective {_X} {_Y} f g h :=
    BinaryBiconeMorphism.ext f g <| F.map_injective <| congr_arg BinaryBiconeMorphism.hom h

Faithfulness of Binary Bicone Functoriality under Faithful Functors

Informal description

Given a faithful functor $ F : C \to D $ between categories $ C $ and $ D $, the induced functor on binary bicones $ \text{functoriality}\, P\, Q\, F : \text{BinaryBicone}\, P\, Q \to \text{BinaryBicone}\, (F\, P)\, (F\, Q) $ is also faithful. This means that for any two morphisms $ f, g $ between binary bicones $ A $ and $ B $ in $ C $, if $ \text{functoriality}\, P\, Q\, F\, f = \text{functoriality}\, P\, Q\, F\, g $, then $ f = g $.

CategoryTheory.Limits.BinaryBicone.toCone definition

(c : BinaryBicone P Q) : Cone (pair P Q)

Full source

/-- Extract the cone from a binary bicone. -/
def toCone (c : BinaryBicone P Q) : Cone (pair P Q) :=
  BinaryFan.mk c.fst c.snd

Cone construction from a binary bicone

Informal description

Given a binary bicone $ c $ for objects $ P $ and $ Q $ in a category $ C $, the function constructs a cone over the functor $ \mathrm{pair}\,P\,Q $, where the cone point is $ c.\mathrm{pt} $ and the projections are given by $ c.\mathrm{fst} $ and $ c.\mathrm{snd} $.

CategoryTheory.Limits.BinaryBicone.toCone_pt theorem

(c : BinaryBicone P Q) : c.toCone.pt = c.pt

Full source

@[simp]
theorem toCone_pt (c : BinaryBicone P Q) : c.toCone.pt = c.pt := rfl

Cone Point of Binary Bicone Equals Bicone Point

Informal description

For any binary bicone $c$ of objects $P$ and $Q$ in a category $\mathcal{C}$, the cone point of the associated cone $c.\mathrm{toCone}$ is equal to the bicone point $c.\mathrm{pt}$.

CategoryTheory.Limits.BinaryBicone.toCone_π_app_left theorem

(c : BinaryBicone P Q) : c.toCone.π.app ⟨WalkingPair.left⟩ = c.fst

Full source

@[simp]
theorem toCone_π_app_left (c : BinaryBicone P Q) : c.toCone.π.app ⟨WalkingPair.left⟩ = c.fst :=
  rfl

Left Projection of Binary Bicone Cone Equals First Projection

Informal description

Given a binary bicone $c$ for objects $P$ and $Q$ in a category $\mathcal{C}$, the left projection morphism of the associated cone, evaluated at the left object of the walking pair, equals the first projection morphism $c.\mathrm{fst}$ of the bicone. That is, $c.\mathrm{toCone}.\pi.\mathrm{app}\,\langle\mathrm{WalkingPair.left}\rangle = c.\mathrm{fst}$.

CategoryTheory.Limits.BinaryBicone.toCone_π_app_right theorem

(c : BinaryBicone P Q) : c.toCone.π.app ⟨WalkingPair.right⟩ = c.snd

Full source

@[simp]
theorem toCone_π_app_right (c : BinaryBicone P Q) : c.toCone.π.app ⟨WalkingPair.right⟩ = c.snd :=
  rfl

Right Projection of Binary Bicone Cone

Informal description

For any binary bicone $c$ of objects $P$ and $Q$ in a category $\mathcal{C}$, the projection morphism of the associated cone $c.\mathrm{toCone}$ at the right object of the walking pair is equal to the second projection morphism $c.\mathrm{snd}$ of the bicone.

CategoryTheory.Limits.BinaryBicone.binary_fan_fst_toCone theorem

(c : BinaryBicone P Q) : BinaryFan.fst c.toCone = c.fst

Full source

@[simp]
theorem binary_fan_fst_toCone (c : BinaryBicone P Q) : BinaryFan.fst c.toCone = c.fst := rfl

Equality of First Projections in Binary Bicone to Cone Construction

Informal description

For any binary bicone $c$ of objects $P$ and $Q$ in a category $\mathcal{C}$, the first projection morphism of the associated binary fan cone is equal to the first projection morphism of the bicone, i.e., $\pi_1(c.\mathrm{toCone}) = c.\mathrm{fst}$.

CategoryTheory.Limits.BinaryBicone.binary_fan_snd_toCone theorem

(c : BinaryBicone P Q) : BinaryFan.snd c.toCone = c.snd

Full source

@[simp]
theorem binary_fan_snd_toCone (c : BinaryBicone P Q) : BinaryFan.snd c.toCone = c.snd := rfl

Equality of Second Projections in Binary Bicone to Cone Construction

Informal description

Given a binary bicone $c$ for objects $P$ and $Q$ in a category $\mathcal{C}$, the second projection morphism of the associated binary fan equals the second projection morphism of the bicone, i.e., $\mathrm{snd}(c.\mathrm{toCone}) = c.\mathrm{snd}$.

CategoryTheory.Limits.BinaryBicone.toCocone definition

(c : BinaryBicone P Q) : Cocone (pair P Q)

Full source

/-- Extract the cocone from a binary bicone. -/
def toCocone (c : BinaryBicone P Q) : Cocone (pair P Q) := BinaryCofan.mk c.inl c.inr

Cocone construction from a binary bicone

Informal description

Given a binary bicone $ c $ for objects $ P $ and $ Q $ in a category $ C $, the function constructs a cocone over the pair $ (P, Q) $ using the injection morphisms $ \text{inl} : P \to c.\text{pt} $ and $ \text{inr} : Q \to c.\text{pt} $ from the bicone. The cocone point is $ c.\text{pt} $, and the cocone morphisms are given by $ \text{inl} $ and $ \text{inr} $.

CategoryTheory.Limits.BinaryBicone.toCocone_pt theorem

(c : BinaryBicone P Q) : c.toCocone.pt = c.pt

Full source

@[simp]
theorem toCocone_pt (c : BinaryBicone P Q) : c.toCocone.pt = c.pt := rfl

Cocone Point Equals Bicone Point in Binary Bicone Construction

Informal description

For any binary bicone $c$ of objects $P$ and $Q$ in a category $\mathcal{C}$, the cocone point of the cocone constructed from $c$ is equal to the bicone point of $c$, i.e., $c.\mathrm{toCocone}.\mathrm{pt} = c.\mathrm{pt}$.

CategoryTheory.Limits.BinaryBicone.toCocone_ι_app_left theorem

(c : BinaryBicone P Q) : c.toCocone.ι.app ⟨WalkingPair.left⟩ = c.inl

Full source

@[simp]
theorem toCocone_ι_app_left (c : BinaryBicone P Q) : c.toCocone.ι.app ⟨WalkingPair.left⟩ = c.inl :=
  rfl

Cocone Inclusion at Left Object Equals Bicone Left Injection

Informal description

For any binary bicone $c$ of objects $P$ and $Q$ in a category $\mathcal{C}$, the cocone inclusion morphism at the left object of the walking pair is equal to the left injection morphism $c.\mathrm{inl}$ of the bicone. That is, $c.\mathrm{toCocone}.\iota.\mathrm{app}\langle\mathrm{WalkingPair.left}\rangle = c.\mathrm{inl}$.

CategoryTheory.Limits.BinaryBicone.toCocone_ι_app_right theorem

(c : BinaryBicone P Q) : c.toCocone.ι.app ⟨WalkingPair.right⟩ = c.inr

Full source

@[simp]
theorem toCocone_ι_app_right (c : BinaryBicone P Q) :
    c.toCocone.ι.app ⟨WalkingPair.right⟩ = c.inr := rfl

Right Cocone Component Equals Right Inclusion in Binary Bicone

Informal description

For any binary bicone $c$ of objects $P$ and $Q$ in a category $\mathcal{C}$, the cocone morphism $\iota$ evaluated at the right object of the walking pair category equals the right inclusion morphism $c.\mathrm{inr}$ of the bicone. That is, $c.\mathrm{toCocone}.\iota(\mathrm{right}) = c.\mathrm{inr}$.

CategoryTheory.Limits.BinaryBicone.binary_cofan_inl_toCocone theorem

(c : BinaryBicone P Q) : BinaryCofan.inl c.toCocone = c.inl

Full source

@[simp]
theorem binary_cofan_inl_toCocone (c : BinaryBicone P Q) : BinaryCofan.inl c.toCocone = c.inl :=
  rfl

Equality of First Coprojection and Bicone Injection in Binary Bicone

Informal description

For any binary bicone $c$ of objects $P$ and $Q$ in a category with zero morphisms, the first coprojection morphism $\iota_X$ of the cocone constructed from $c$ is equal to the injection morphism $\text{inl}$ of the bicone $c$.

CategoryTheory.Limits.BinaryBicone.binary_cofan_inr_toCocone theorem

(c : BinaryBicone P Q) : BinaryCofan.inr c.toCocone = c.inr

Full source

@[simp]
theorem binary_cofan_inr_toCocone (c : BinaryBicone P Q) : BinaryCofan.inr c.toCocone = c.inr :=
  rfl

Right Inclusion Equals Second Coprojection in Binary Bicone Cocone

Informal description

Given a binary bicone $c$ for objects $P$ and $Q$ in a category with zero morphisms, the second coprojection morphism $\iota_Y$ of the associated cocone $c.\mathrm{toCocone}$ is equal to the right inclusion morphism $c.\mathrm{inr}$ of the bicone.

CategoryTheory.Limits.BinaryBicone.instIsSplitMonoInl instance

(c : BinaryBicone P Q) : IsSplitMono c.inl

Full source

instance (c : BinaryBicone P Q) : IsSplitMono c.inl :=
  IsSplitMono.mk'
    { retraction := c.fst
      id := c.inl_fst }

The Inl Morphism in a Binary Bicone is a Split Monomorphism

Informal description

For any binary bicone $c$ of objects $P$ and $Q$ in a category with zero morphisms, the morphism $\text{inl}: P \to c.X$ is a split monomorphism.

CategoryTheory.Limits.BinaryBicone.instIsSplitMonoInr instance

(c : BinaryBicone P Q) : IsSplitMono c.inr

Full source

instance (c : BinaryBicone P Q) : IsSplitMono c.inr :=
  IsSplitMono.mk'
    { retraction := c.snd
      id := c.inr_snd }

The Right Inclusion of a Binary Bicone is a Split Monomorphism

Informal description

For any binary bicone $c$ of objects $P$ and $Q$ in a category with zero morphisms, the morphism $\text{inr}: Q \to c.X$ is a split monomorphism. That is, there exists a retraction morphism $g: c.X \to Q$ such that $g \circ \text{inr} = \text{id}_Q$.

CategoryTheory.Limits.BinaryBicone.instIsSplitEpiFst instance

(c : BinaryBicone P Q) : IsSplitEpi c.fst

Full source

instance (c : BinaryBicone P Q) : IsSplitEpi c.fst :=
  IsSplitEpi.mk'
    { section_ := c.inl
      id := c.inl_fst }

The First Projection of a Binary Bicone is a Split Epimorphism

Informal description

For any binary bicone $c$ of objects $P$ and $Q$ in a category with zero morphisms, the morphism $\text{fst} : X \to P$ is a split epimorphism. That is, there exists a morphism $s : P \to X$ such that $\text{fst} \circ s = \text{id}_P$.

CategoryTheory.Limits.BinaryBicone.instIsSplitEpiSnd instance

(c : BinaryBicone P Q) : IsSplitEpi c.snd

Full source

instance (c : BinaryBicone P Q) : IsSplitEpi c.snd :=
  IsSplitEpi.mk'
    { section_ := c.inr
      id := c.inr_snd }

The Second Projection of a Binary Bicone is a Split Epimorphism

Informal description

For any binary bicone $c$ of objects $P$ and $Q$ in a category with zero morphisms, the morphism $\text{snd} : X \to Q$ is a split epimorphism. That is, there exists a morphism $g : Q \to X$ such that $\text{snd} \circ g = \text{id}_Q$.

CategoryTheory.Limits.BinaryBicone.toBiconeFunctor definition

{X Y : C} : BinaryBicone X Y ⥤ Bicone (pairFunction X Y)

Full source

/-- Convert a `BinaryBicone` into a `Bicone` over a pair. -/
@[simps]
def toBiconeFunctor {X Y : C} : BinaryBiconeBinaryBicone X Y ⥤ Bicone (pairFunction X Y) where
  obj b :=
    { pt := b.pt
      π := fun j => WalkingPair.casesOn j b.fst b.snd
      ι := fun j => WalkingPair.casesOn j b.inl b.inr
      ι_π := fun j j' => by
        rcases j with ⟨⟩ <;> rcases j' with ⟨⟩ <;> simp }
  map f := {
    hom := f.hom
    wπ := fun i => WalkingPair.casesOn i f.wfst f.wsnd
    wι := fun i => WalkingPair.casesOn i f.winl f.winr }

Functor from binary bicones to bicones over pairs

Informal description

The functor that converts a binary bicone for objects $X$ and $Y$ in a category $C$ into a bicone over the pair $(X, Y)$. Specifically: - For a binary bicone $b$, the associated bicone has: - The same cone point $b.pt$ - Projections $\pi_j$ given by $b.fst$ for the left object and $b.snd$ for the right object - Injections $\iota_j$ given by $b.inl$ for the left object and $b.inr$ for the right object - For a morphism $f$ between binary bicones, the associated bicone morphism has the same underlying morphism $f.hom$, and satisfies the required commutativity conditions for both projections and injections.

CategoryTheory.Limits.BinaryBicone.toBicone abbrev

{X Y : C} (b : BinaryBicone X Y) : Bicone (pairFunction X Y)

Full source

/-- A shorthand for `toBiconeFunctor.obj` -/
abbrev toBicone {X Y : C} (b : BinaryBicone X Y) : Bicone (pairFunction X Y) :=
  toBiconeFunctor.obj b

Conversion from Binary Bicone to Bicone over Pair

Informal description

Given a binary bicone $b$ for objects $X$ and $Y$ in a category $C$, the function `BinaryBicone.toBicone` constructs a bicone over the pair $(X, Y)$. Specifically: - The bicone has the same cone point as $b$ - The projections are given by $b.\text{fst}$ (for $X$) and $b.\text{snd}$ (for $Y$) - The injections are given by $b.\text{inl}$ (for $X$) and $b.\text{inr}$ (for $Y$)

CategoryTheory.Limits.BinaryBicone.toBiconeIsLimit definition

{X Y : C} (b : BinaryBicone X Y) : IsLimit b.toBicone.toCone ≃ IsLimit b.toCone

Full source

/-- A binary bicone is a limit cone if and only if the corresponding bicone is a limit cone. -/
def toBiconeIsLimit {X Y : C} (b : BinaryBicone X Y) :
    IsLimitIsLimit b.toBicone.toCone ≃ IsLimit b.toCone :=
  IsLimit.equivIsoLimit <| Cones.ext (Iso.refl _) fun ⟨as⟩ => by cases as <;> simp

Equivalence of limit conditions for binary bicone conversions

Informal description

For any binary bicone $ b $ for objects $ X $ and $ Y $ in a category $ C $, the bicone $ b.\text{toBicone}.\text{toCone} $ is a limit cone if and only if the cone $ b.\text{toCone} $ is a limit cone. This equivalence is established via the identity isomorphism on the cone point.

CategoryTheory.Limits.BinaryBicone.toBiconeIsColimit definition

{X Y : C} (b : BinaryBicone X Y) : IsColimit b.toBicone.toCocone ≃ IsColimit b.toCocone

Full source

/-- A binary bicone is a colimit cocone if and only if the corresponding bicone is a colimit
    cocone. -/
def toBiconeIsColimit {X Y : C} (b : BinaryBicone X Y) :
    IsColimitIsColimit b.toBicone.toCocone ≃ IsColimit b.toCocone :=
  IsColimit.equivIsoColimit <| Cocones.ext (Iso.refl _) fun ⟨as⟩ => by cases as <;> simp

Equivalence of colimit properties for binary bicone cocones

Informal description

Given a binary bicone $ b $ for objects $ X $ and $ Y $ in a category $ C $, there is an equivalence between the property of the cocone constructed from the associated bicone being a colimit cocone and the property of the cocone constructed directly from the binary bicone being a colimit cocone. This equivalence is established via an isomorphism of cocones induced by the identity morphism on the cone point.

CategoryTheory.Limits.Bicone.toBinaryBiconeFunctor definition

{X Y : C} : Bicone (pairFunction X Y) ⥤ BinaryBicone X Y

Full source

/-- Convert a `Bicone` over a function on `WalkingPair` to a BinaryBicone. -/
@[simps]
def toBinaryBiconeFunctor {X Y : C} : BiconeBicone (pairFunction X Y) ⥤ BinaryBicone X Y where
  obj b :=
    { pt := b.pt
      fst := b.π WalkingPair.left
      snd := b.π WalkingPair.right
      inl := b.ι WalkingPair.left
      inr := b.ι WalkingPair.right
      inl_fst := by simp [Bicone.ι_π]
      inr_fst := by simp [Bicone.ι_π]
      inl_snd := by simp [Bicone.ι_π]
      inr_snd := by simp [Bicone.ι_π] }
  map f :=
    { hom := f.hom }

Functor from bicones to binary bicones

Informal description

The functor that converts a bicone over the pair of objects $X$ and $Y$ (indexed by `WalkingPair`) into a binary bicone structure. Specifically: - The object part maps a bicone $b$ to a binary bicone with: - The same cone point $b.pt$ - Projection maps $b.\pi$ for the left and right components - Injection maps $b.\iota$ for the left and right components - The morphism part preserves the homomorphisms between bicones. The conversion preserves the bicone conditions: $ \text{inl} \circ \text{fst} = \text{id}_X $, $ \text{inl} \circ \text{snd} = 0 $, $ \text{inr} \circ \text{fst} = 0 $, and $ \text{inr} \circ \text{snd} = \text{id}_Y $.

CategoryTheory.Limits.Bicone.toBinaryBicone abbrev

{X Y : C} (b : Bicone (pairFunction X Y)) : BinaryBicone X Y

Full source

/-- A shorthand for `toBinaryBiconeFunctor.obj` -/
abbrev toBinaryBicone {X Y : C} (b : Bicone (pairFunction X Y)) : BinaryBicone X Y :=
  toBinaryBiconeFunctor.obj b

Construction of Binary Bicone from Bicone over Pair

Informal description

Given a bicone $b$ over the pair of objects $(X, Y)$ in a category $C$, the construction `toBinaryBicone` produces a binary bicone structure on the same cone point, with projection and injection morphisms satisfying the compatibility conditions: - $\text{inl} \circ \text{fst} = \text{id}_X$ - $\text{inl} \circ \text{snd} = 0$ - $\text{inr} \circ \text{fst} = 0$ - $\text{inr} \circ \text{snd} = \text{id}_Y$

CategoryTheory.Limits.Bicone.toBinaryBiconeIsLimit definition

{X Y : C} (b : Bicone (pairFunction X Y)) : IsLimit b.toBinaryBicone.toCone ≃ IsLimit b.toCone

Full source

/-- A bicone over a pair is a limit cone if and only if the corresponding binary bicone is a limit
    cone. -/
def toBinaryBiconeIsLimit {X Y : C} (b : Bicone (pairFunction X Y)) :
    IsLimitIsLimit b.toBinaryBicone.toCone ≃ IsLimit b.toCone :=
  IsLimit.equivIsoLimit <| Cones.ext (Iso.refl _) fun j => by rcases j with ⟨⟨⟩⟩ <;> simp

Equivalence of limit properties between bicone and binary bicone

Informal description

Given a bicone $b$ over the pair of objects $(X, Y)$ in a category $C$, there is an equivalence between: 1. The property that the cone constructed from the associated binary bicone is a limit cone 2. The property that the original bicone's cone is a limit cone This equivalence is established via the natural isomorphism between the two cones induced by the identity morphism on their common apex.

CategoryTheory.Limits.Bicone.toBinaryBiconeIsColimit definition

{X Y : C} (b : Bicone (pairFunction X Y)) : IsColimit b.toBinaryBicone.toCocone ≃ IsColimit b.toCocone

Full source

/-- A bicone over a pair is a colimit cocone if and only if the corresponding binary bicone is a
    colimit cocone. -/
def toBinaryBiconeIsColimit {X Y : C} (b : Bicone (pairFunction X Y)) :
    IsColimitIsColimit b.toBinaryBicone.toCocone ≃ IsColimit b.toCocone :=
  IsColimit.equivIsoColimit <| Cocones.ext (Iso.refl _) fun j => by rcases j with ⟨⟨⟩⟩ <;> simp

Equivalence of colimit properties between bicone and binary bicone cocones

Informal description

Given a bicone $b$ over the pair of objects $(X, Y)$ in a category $C$ with zero morphisms, the property of the associated binary bicone's cocone being a colimit cocone is equivalent to the property of the original bicone's cocone being a colimit cocone. This equivalence is established via an isomorphism of cocones induced by the identity morphism on the cone point.

CategoryTheory.Limits.BinaryBicone.IsBilimit structure

{P Q : C} (b : BinaryBicone P Q)

Full source

/-- Structure witnessing that a binary bicone is a limit cone and a limit cocone. -/
structure BinaryBicone.IsBilimit {P Q : C} (b : BinaryBicone P Q) where
  isLimit : IsLimit b.toCone
  isColimit : IsColimit b.toCocone

Bilimit Binary Bicone

Informal description

A binary bicone for objects $ P $ and $ Q $ in a category $ C $ is called *bilimit* if it is simultaneously a limit cone and a colimit cocone. This means the bicone satisfies the universal properties of both a product and a coproduct for the pair $ P $ and $ Q $.

CategoryTheory.Limits.BinaryBicone.toBiconeIsBilimit definition

{X Y : C} (b : BinaryBicone X Y) : b.toBicone.IsBilimit ≃ b.IsBilimit

Full source

/-- A binary bicone is a bilimit bicone if and only if the corresponding bicone is a bilimit. -/
def BinaryBicone.toBiconeIsBilimit {X Y : C} (b : BinaryBicone X Y) :
    b.toBicone.IsBilimit ≃ b.IsBilimit where
  toFun h := ⟨b.toBiconeIsLimit h.isLimit, b.toBiconeIsColimit h.isColimit⟩
  invFun h := ⟨b.toBiconeIsLimit.symm h.isLimit, b.toBiconeIsColimit.symm h.isColimit⟩
  left_inv := fun ⟨h, h'⟩ => by dsimp only; simp
  right_inv := fun ⟨h, h'⟩ => by dsimp only; simp

Equivalence of bilimit properties between binary bicone and its associated bicone

Informal description

Given a binary bicone $ b $ for objects $ X $ and $ Y $ in a category $ C $, the bicone $ b.\text{toBicone} $ is a bilimit (i.e., both a limit and a colimit) if and only if the original binary bicone $ b $ is a bilimit. This equivalence is established via the identity isomorphism on the cone point.

CategoryTheory.Limits.Bicone.toBinaryBiconeIsBilimit definition

{X Y : C} (b : Bicone (pairFunction X Y)) : b.toBinaryBicone.IsBilimit ≃ b.IsBilimit

Full source

/-- A bicone over a pair is a bilimit bicone if and only if the corresponding binary bicone is a
    bilimit. -/
def Bicone.toBinaryBiconeIsBilimit {X Y : C} (b : Bicone (pairFunction X Y)) :
    b.toBinaryBicone.IsBilimit ≃ b.IsBilimit where
  toFun h := ⟨b.toBinaryBiconeIsLimit h.isLimit, b.toBinaryBiconeIsColimit h.isColimit⟩
  invFun h := ⟨b.toBinaryBiconeIsLimit.symm h.isLimit, b.toBinaryBiconeIsColimit.symm h.isColimit⟩
  left_inv := fun ⟨h, h'⟩ => by dsimp only; simp
  right_inv := fun ⟨h, h'⟩ => by dsimp only; simp

Equivalence of bilimit properties between bicone and binary bicone

Informal description

Given a bicone $b$ over the pair of objects $(X, Y)$ in a category $C$ with zero morphisms, the property of the associated binary bicone being bilimit (i.e., both a limit cone and a colimit cocone) is equivalent to the original bicone being bilimit. This equivalence is established via natural isomorphisms between the corresponding limit and colimit properties.

CategoryTheory.Limits.BinaryBiproductData structure

(P Q : C)

Full source

/-- A bicone over `P Q : C`, which is both a limit cone and a colimit cocone. -/
structure BinaryBiproductData (P Q : C) where
  bicone : BinaryBicone P Q
  isBilimit : bicone.IsBilimit

Binary Biproduct Data

Informal description

The structure `BinaryBiproductData P Q` represents the data required to define a binary biproduct of objects $ P $ and $ Q $ in a category $ C $. A binary biproduct is both a limit and a colimit, equipped with morphisms that satisfy certain conditions, making it simultaneously a product and a coproduct in a category with zero morphisms.

CategoryTheory.Limits.HasBinaryBiproduct structure

(P Q : C)

Full source

/-- `HasBinaryBiproduct P Q` expresses the mere existence of a bicone which is
simultaneously a limit and a colimit of the diagram `pair P Q`. -/
class HasBinaryBiproduct (P Q : C) : Prop where mk' ::
  exists_binary_biproduct : Nonempty (BinaryBiproductData P Q)

Existence of Binary Biproduct

Informal description

The structure `HasBinaryBiproduct P Q` asserts the existence of a binary biproduct for objects $ P $ and $ Q $ in a category $ C $. A binary biproduct is a bicone that simultaneously serves as both a limit and a colimit of the diagram consisting of $ P $ and $ Q $. This means there exists an object $ X $ with morphisms $ \text{fst} : X \to P $, $ \text{snd} : X \to Q $, $ \text{inl} : P \to X $, and $ \text{inr} : Q \to X $, satisfying the conditions $ \text{inl} \circ \text{fst} = \text{id}_P $, $ \text{inl} \circ \text{snd} = 0 $, $ \text{inr} \circ \text{fst} = 0 $, and $ \text{inr} \circ \text{snd} = \text{id}_Q $, where the bicone is both a limit cone and a colimit cocone.

CategoryTheory.Limits.HasBinaryBiproduct.mk theorem

{P Q : C} (d : BinaryBiproductData P Q) : HasBinaryBiproduct P Q

Full source

theorem HasBinaryBiproduct.mk {P Q : C} (d : BinaryBiproductData P Q) : HasBinaryBiproduct P Q :=
  ⟨Nonempty.intro d⟩

Existence of Binary Biproduct from Biproduct Data

Informal description

Given objects $P$ and $Q$ in a category $C$ with zero morphisms, if there exists a binary biproduct data structure for $P$ and $Q$, then $P$ and $Q$ have a binary biproduct. More precisely, if there exists an object $X$ with morphisms $\text{fst} : X \to P$, $\text{snd} : X \to Q$, $\text{inl} : P \to X$, and $\text{inr} : Q \to X$ satisfying: - $\text{inl} \circ \text{fst} = \text{id}_P$, - $\text{inl} \circ \text{snd} = 0$, - $\text{inr} \circ \text{fst} = 0$, - $\text{inr} \circ \text{snd} = \text{id}_Q$, then $X$ is both a limit and a colimit of the diagram consisting of $P$ and $Q$, i.e., $X$ is a binary biproduct of $P$ and $Q$.

CategoryTheory.Limits.getBinaryBiproductData definition

(P Q : C) [HasBinaryBiproduct P Q] : BinaryBiproductData P Q

Full source

/--
Use the axiom of choice to extract explicit `BinaryBiproductData F` from `HasBinaryBiproduct F`.
-/
def getBinaryBiproductData (P Q : C) [HasBinaryBiproduct P Q] : BinaryBiproductData P Q :=
  Classical.choice HasBinaryBiproduct.exists_binary_biproduct

Extraction of Binary Biproduct Data

Informal description

Given objects $ P $ and $ Q $ in a category $ C $ with zero morphisms, and assuming the existence of a binary biproduct of $ P $ and $ Q $, the function `getBinaryBiproductData` extracts explicit data for the binary biproduct using the axiom of choice. This data includes the biproduct object $ X $ and the morphisms $ \text{fst} : X \to P $, $ \text{snd} : X \to Q $, $ \text{inl} : P \to X $, and $ \text{inr} : Q \to X $, satisfying the conditions $ \text{inl} \circ \text{fst} = \text{id}_P $, $ \text{inl} \circ \text{snd} = 0 $, $ \text{inr} \circ \text{fst} = 0 $, and $ \text{inr} \circ \text{snd} = \text{id}_Q $.

CategoryTheory.Limits.BinaryBiproduct.bicone definition

(P Q : C) [HasBinaryBiproduct P Q] : BinaryBicone P Q

Full source

/-- A bicone for `P Q` which is both a limit cone and a colimit cocone. -/
def BinaryBiproduct.bicone (P Q : C) [HasBinaryBiproduct P Q] : BinaryBicone P Q :=
  (getBinaryBiproductData P Q).bicone

Bicone underlying a binary biproduct

Informal description

Given objects $ P $ and $ Q $ in a category $ C $ with zero morphisms, and assuming the existence of a binary biproduct of $ P $ and $ Q $, the function `BinaryBiproduct.bicone` returns the underlying binary bicone structure. This consists of: - An object $ X $ (the biproduct) - Morphisms $ \text{fst} : X \to P $ and $ \text{snd} : X \to Q $ - Morphisms $ \text{inl} : P \to X $ and $ \text{inr} : Q \to X $ satisfying the conditions: 1. $ \text{inl} \circ \text{fst} = \text{id}_P $ 2. $ \text{inl} \circ \text{snd} = 0 $ 3. $ \text{inr} \circ \text{fst} = 0 $ 4. $ \text{inr} \circ \text{snd} = \text{id}_Q $

CategoryTheory.Limits.BinaryBiproduct.isBilimit definition

(P Q : C) [HasBinaryBiproduct P Q] : (BinaryBiproduct.bicone P Q).IsBilimit

Full source

/-- `BinaryBiproduct.bicone P Q` is a limit bicone. -/
def BinaryBiproduct.isBilimit (P Q : C) [HasBinaryBiproduct P Q] :
    (BinaryBiproduct.bicone P Q).IsBilimit :=
  (getBinaryBiproductData P Q).isBilimit

Bilimit property of binary biproduct bicone

Informal description

Given objects $ P $ and $ Q $ in a category $ C $ with zero morphisms, and assuming the existence of a binary biproduct of $ P $ and $ Q $, the term `BinaryBiproduct.isBilimit` asserts that the underlying bicone structure is bilimit, meaning it is simultaneously a limit cone and a colimit cocone.

CategoryTheory.Limits.BinaryBiproduct.isLimit definition

(P Q : C) [HasBinaryBiproduct P Q] : IsLimit (BinaryBiproduct.bicone P Q).toCone

Full source

/-- `BinaryBiproduct.bicone P Q` is a limit cone. -/
def BinaryBiproduct.isLimit (P Q : C) [HasBinaryBiproduct P Q] :
    IsLimit (BinaryBiproduct.bicone P Q).toCone :=
  (getBinaryBiproductData P Q).isBilimit.isLimit

Limit property of binary biproduct cone

Informal description

Given objects $ P $ and $ Q $ in a category $ C $ with zero morphisms, and assuming the existence of a binary biproduct of $ P $ and $ Q $, the term `BinaryBiproduct.isLimit` asserts that the cone associated to the biproduct bicone is a limit cone. Specifically, the cone formed by the projections $ \text{fst} : X \to P $ and $ \text{snd} : X \to Q $ from the biproduct object $ X $ is a limit of the diagram consisting of $ P $ and $ Q $.

CategoryTheory.Limits.BinaryBiproduct.isColimit definition

(P Q : C) [HasBinaryBiproduct P Q] : IsColimit (BinaryBiproduct.bicone P Q).toCocone

Full source

/-- `BinaryBiproduct.bicone P Q` is a colimit cocone. -/
def BinaryBiproduct.isColimit (P Q : C) [HasBinaryBiproduct P Q] :
    IsColimit (BinaryBiproduct.bicone P Q).toCocone :=
  (getBinaryBiproductData P Q).isBilimit.isColimit

Colimit property of binary biproduct cocone

Informal description

Given objects $ P $ and $ Q $ in a category $ C $ with zero morphisms, and assuming the existence of a binary biproduct of $ P $ and $ Q $, the term `BinaryBiproduct.isColimit` asserts that the cocone constructed from the underlying bicone of the binary biproduct is a colimit cocone. Specifically, the cocone consists of the injection morphisms $ \text{inl} : P \to X $ and $ \text{inr} : Q \to X $, where $ X $ is the biproduct object, and this cocone satisfies the universal property of a colimit.

CategoryTheory.Limits.HasBinaryBiproducts structure

Full source

/-- `HasBinaryBiproducts C` represents the existence of a bicone which is
simultaneously a limit and a colimit of the diagram `pair P Q`, for every `P Q : C`. -/
class HasBinaryBiproducts : Prop where
  has_binary_biproduct : ∀ P Q : C, HasBinaryBiproduct P Q

Existence of binary biproducts in a category

Informal description

A category $ C $ has binary biproducts if for every pair of objects $ P, Q $ in $ C $, there exists a bicone (simultaneously a cone and a cocone) that is both a limit cone and a colimit cocone for the diagram consisting of $ P $ and $ Q $. This means the bicone serves as both a product and a coproduct for $ P $ and $ Q $.

CategoryTheory.Limits.hasBinaryBiproducts_of_finite_biproducts theorem

[HasFiniteBiproducts C] : HasBinaryBiproducts C

Full source

/-- A category with finite biproducts has binary biproducts.

This is not an instance as typically in concrete categories there will be
an alternative construction with nicer definitional properties. -/
theorem hasBinaryBiproducts_of_finite_biproducts [HasFiniteBiproducts C] : HasBinaryBiproducts C :=
  { has_binary_biproduct := fun P Q =>
      HasBinaryBiproduct.mk
        { bicone := (biproduct.bicone (pairFunction P Q)).toBinaryBicone
          isBilimit := (Bicone.toBinaryBiconeIsBilimit _).symm (biproduct.isBilimit _) } }

Finite Biproducts Imply Binary Biproducts

Informal description

If a category $C$ has finite biproducts, then it has binary biproducts. That is, for any pair of objects $P, Q$ in $C$, there exists an object $X$ with morphisms $\text{fst} : X \to P$, $\text{snd} : X \to Q$, $\text{inl} : P \to X$, and $\text{inr} : Q \to X$ such that: - $\text{inl} \circ \text{fst} = \text{id}_P$, - $\text{inl} \circ \text{snd} = 0$, - $\text{inr} \circ \text{fst} = 0$, - $\text{inr} \circ \text{snd} = \text{id}_Q$, and $X$ is both a product and coproduct of $P$ and $Q$.

CategoryTheory.Limits.HasBinaryBiproduct.hasLimit_pair instance

[HasBinaryBiproduct P Q] : HasLimit (pair P Q)

Full source

instance HasBinaryBiproduct.hasLimit_pair [HasBinaryBiproduct P Q] : HasLimit (pair P Q) :=
  HasLimit.mk ⟨_, BinaryBiproduct.isLimit P Q⟩

Existence of Limit for Pair Diagram in Presence of Binary Biproduct

Informal description

For any objects $P$ and $Q$ in a category $C$ that has a binary biproduct, the functor $\mathrm{pair}\,P\,Q \colon \mathrm{Discrete}\,\mathrm{WalkingPair} \to C$ has a limit. This means that the diagram consisting of $P$ and $Q$ admits a limit cone, which is part of the biproduct structure.

CategoryTheory.Limits.HasBinaryBiproduct.hasColimit_pair instance

[HasBinaryBiproduct P Q] : HasColimit (pair P Q)

Full source

instance HasBinaryBiproduct.hasColimit_pair [HasBinaryBiproduct P Q] : HasColimit (pair P Q) :=
  HasColimit.mk ⟨_, BinaryBiproduct.isColimit P Q⟩

Existence of Colimit for Pair Diagram in Presence of Binary Biproduct

Informal description

For any objects $P$ and $Q$ in a category $C$ that has a binary biproduct, the diagram consisting of $P$ and $Q$ admits a colimit. This means that the pair functor $\mathrm{pair}\,P\,Q \colon \mathrm{Discrete}\,\mathrm{WalkingPair} \to C$ has a colimit cocone, which is part of the biproduct structure.

CategoryTheory.Limits.hasBinaryProducts_of_hasBinaryBiproducts instance

[HasBinaryBiproducts C] : HasBinaryProducts C

Full source

instance (priority := 100) hasBinaryProducts_of_hasBinaryBiproducts [HasBinaryBiproducts C] :
    HasBinaryProducts C where
  has_limit F := hasLimit_of_iso (diagramIsoPair F).symm

Binary Biproducts Imply Binary Products

Informal description

In any category $C$ that has binary biproducts, $C$ also has binary products.

CategoryTheory.Limits.hasBinaryCoproducts_of_hasBinaryBiproducts instance

[HasBinaryBiproducts C] : HasBinaryCoproducts C

Full source

instance (priority := 100) hasBinaryCoproducts_of_hasBinaryBiproducts [HasBinaryBiproducts C] :
    HasBinaryCoproducts C where
  has_colimit F := hasColimit_of_iso (diagramIsoPair F)

Binary Biproducts Imply Binary Coproducts

Informal description

Every category with binary biproducts also has binary coproducts. Specifically, if a category $\mathcal{C}$ has biproducts for every pair of objects, then for any two objects $X$ and $Y$ in $\mathcal{C}$, the coproduct $X \sqcup Y$ exists.

CategoryTheory.Limits.biprodIso definition

(X Y : C) [HasBinaryBiproduct X Y] : Limits.prod X Y ≅ Limits.coprod X Y

Full source

/-- The isomorphism between the specified binary product and the specified binary coproduct for
a pair for a binary biproduct. -/
def biprodIso (X Y : C) [HasBinaryBiproduct X Y] : Limits.prodLimits.prod X Y ≅ Limits.coprod X Y :=
  (IsLimit.conePointUniqueUpToIso (limit.isLimit _) (BinaryBiproduct.isLimit X Y)).trans <|
    IsColimit.coconePointUniqueUpToIso (BinaryBiproduct.isColimit X Y) (colimit.isColimit _)

Canonical isomorphism between product and coproduct in a biproduct

Informal description

Given objects $X$ and $Y$ in a category $\mathcal{C}$ with binary biproducts, the isomorphism $\mathrm{biprodIso}\,X\,Y$ is the canonical isomorphism between the product $X \times Y$ and the coproduct $X \sqcup Y$ of $X$ and $Y$. This isomorphism is constructed using the universal properties of the product and coproduct cones associated with the binary biproduct structure.

CategoryTheory.Limits.biprod abbrev

(X Y : C) [HasBinaryBiproduct X Y]

Full source

/-- An arbitrary choice of biproduct of a pair of objects. -/
abbrev biprod (X Y : C) [HasBinaryBiproduct X Y] :=
  (BinaryBiproduct.bicone X Y).pt

Binary Biproduct $X \oplus Y$ in a Category with Zero Morphisms

Informal description

Given objects $X$ and $Y$ in a category $C$ with zero morphisms and binary biproducts, the binary biproduct of $X$ and $Y$ is an object $X \oplus Y$ equipped with morphisms: - $\pi_1: X \oplus Y \to X$ (first projection) - $\pi_2: X \oplus Y \to Y$ (second projection) - $\iota_1: X \to X \oplus Y$ (first inclusion) - $\iota_2: Y \to X \oplus Y$ (second inclusion) satisfying the biproduct identities: 1. $\iota_1 \circ \pi_1 = \text{id}_X$ 2. $\iota_1 \circ \pi_2 = 0$ 3. $\iota_2 \circ \pi_1 = 0$ 4. $\iota_2 \circ \pi_2 = \text{id}_Y$ where $X \oplus Y$ serves simultaneously as both the product and coproduct of $X$ and $Y$.

CategoryTheory.Limits.term_⊞_ definition

: Lean.TrailingParserDescr✝

Full source

@[inherit_doc biprod]
notation:20 X " ⊞ " Y:20 => biprod X Y

Binary biproduct notation

Informal description

The notation `X ⊞ Y` represents the binary biproduct of objects `X` and `Y` in a category, which is both their product and coproduct when they exist. This notation is used when the category has binary biproducts for `X` and `Y`.

CategoryTheory.Limits.biprod.fst abbrev

{X Y : C} [HasBinaryBiproduct X Y] : X ⊞ Y ⟶ X

Full source

/-- The projection onto the first summand of a binary biproduct. -/
abbrev biprod.fst {X Y : C} [HasBinaryBiproduct X Y] : X ⊞ YX ⊞ Y ⟶ X :=
  (BinaryBiproduct.bicone X Y).fst

First Projection Morphism from Binary Biproduct

Informal description

For objects $X$ and $Y$ in a category $C$ with binary biproducts, the first projection morphism $\pi_1: X \oplus Y \to X$ from their biproduct $X \oplus Y$ to $X$ is defined. This morphism satisfies the biproduct identities: 1. $\iota_1 \circ \pi_1 = \text{id}_X$ 2. $\iota_2 \circ \pi_1 = 0$ where $\iota_1: X \to X \oplus Y$ and $\iota_2: Y \to X \oplus Y$ are the inclusion morphisms.

CategoryTheory.Limits.biprod.snd abbrev

{X Y : C} [HasBinaryBiproduct X Y] : X ⊞ Y ⟶ Y

Full source

/-- The projection onto the second summand of a binary biproduct. -/
abbrev biprod.snd {X Y : C} [HasBinaryBiproduct X Y] : X ⊞ YX ⊞ Y ⟶ Y :=
  (BinaryBiproduct.bicone X Y).snd

Second Projection from Binary Biproduct

Informal description

In a category $C$ with zero morphisms and binary biproducts, for any objects $X$ and $Y$, the second projection morphism $\pi_2: X \oplus Y \to Y$ is part of the binary biproduct structure, where $X \oplus Y$ denotes the biproduct of $X$ and $Y$.

CategoryTheory.Limits.biprod.inl abbrev

{X Y : C} [HasBinaryBiproduct X Y] : X ⟶ X ⊞ Y

Full source

/-- The inclusion into the first summand of a binary biproduct. -/
abbrev biprod.inl {X Y : C} [HasBinaryBiproduct X Y] : X ⟶ X ⊞ Y :=
  (BinaryBiproduct.bicone X Y).inl

First inclusion morphism into binary biproduct: $\iota_1: X \to X \oplus Y$

Informal description

For objects $X$ and $Y$ in a category $C$ with binary biproducts, the inclusion morphism $\iota_1: X \to X \oplus Y$ is the first inclusion into the biproduct $X \oplus Y$, satisfying the biproduct identities: 1. $\iota_1 \circ \pi_1 = \text{id}_X$ (where $\pi_1: X \oplus Y \to X$ is the first projection) 2. $\iota_1 \circ \pi_2 = 0$ (where $\pi_2: X \oplus Y \to Y$ is the second projection)

CategoryTheory.Limits.biprod.inr abbrev

{X Y : C} [HasBinaryBiproduct X Y] : Y ⟶ X ⊞ Y

Full source

/-- The inclusion into the second summand of a binary biproduct. -/
abbrev biprod.inr {X Y : C} [HasBinaryBiproduct X Y] : Y ⟶ X ⊞ Y :=
  (BinaryBiproduct.bicone X Y).inr

Inclusion morphism into the second summand of a binary biproduct

Informal description

For objects $X$ and $Y$ in a category $C$ with binary biproducts, the morphism $\text{inr} : Y \to X \oplus Y$ is the inclusion of $Y$ into the binary biproduct $X \oplus Y$.

CategoryTheory.Limits.BinaryBiproduct.bicone_fst theorem

: (BinaryBiproduct.bicone X Y).fst = biprod.fst

Full source

@[simp] theorem BinaryBiproduct.bicone_fst : (BinaryBiproduct.bicone X Y).fst = biprod.fst := rfl

Equality of First Projections in Binary Biproduct Bicone

Informal description

For objects $X$ and $Y$ in a category $C$ with binary biproducts, the first projection morphism $\pi_1$ of the underlying bicone of their biproduct is equal to the first projection morphism $\text{fst}$ of the biproduct itself.

CategoryTheory.Limits.BinaryBiproduct.bicone_snd theorem

: (BinaryBiproduct.bicone X Y).snd = biprod.snd

Full source

@[simp] theorem BinaryBiproduct.bicone_snd : (BinaryBiproduct.bicone X Y).snd = biprod.snd := rfl

Equality of Second Projection Morphisms in Binary Biproduct

Informal description

In a category $C$ with zero morphisms and binary biproducts, for any objects $X$ and $Y$, the second projection morphism $\text{snd}$ of the underlying bicone of the binary biproduct $X \oplus Y$ is equal to the second projection morphism $\text{biprod.snd}$.

CategoryTheory.Limits.BinaryBiproduct.bicone_inl theorem

: (BinaryBiproduct.bicone X Y).inl = biprod.inl

Full source

@[simp] theorem BinaryBiproduct.bicone_inl : (BinaryBiproduct.bicone X Y).inl = biprod.inl := rfl

Equality of inclusion morphisms in binary biproduct bicone

Informal description

For objects $X$ and $Y$ in a category $C$ with binary biproducts, the inclusion morphism $\iota_1$ in the underlying bicone of the binary biproduct $X \oplus Y$ is equal to the canonical inclusion morphism $\text{biprod.inl} : X \to X \oplus Y$.

CategoryTheory.Limits.BinaryBiproduct.bicone_inr theorem

: (BinaryBiproduct.bicone X Y).inr = biprod.inr

Full source

@[simp] theorem BinaryBiproduct.bicone_inr : (BinaryBiproduct.bicone X Y).inr = biprod.inr := rfl

Equality of Inclusion Morphisms in Binary Biproduct Bicone

Informal description

For objects $X$ and $Y$ in a category $C$ with binary biproducts, the inclusion morphism $\text{inr}$ of the underlying bicone of the binary biproduct $X \oplus Y$ is equal to the canonical inclusion morphism $\text{biprod.inr} : Y \to X \oplus Y$.

CategoryTheory.Limits.biprod.inl_fst theorem

{X Y : C} [HasBinaryBiproduct X Y] : (biprod.inl : X ⟶ X ⊞ Y) ≫ (biprod.fst : X ⊞ Y ⟶ X) = 𝟙 X

Full source

@[reassoc]
theorem biprod.inl_fst {X Y : C} [HasBinaryBiproduct X Y] :
    (biprod.inl : X ⟶ X ⊞ Y) ≫ (biprod.fst : X ⊞ Y ⟶ X) = 𝟙 X :=
  (BinaryBiproduct.bicone X Y).inl_fst

First Biproduct Identity: $\iota_1 \circ \pi_1 = \text{id}_X$

Informal description

In a category $C$ with binary biproducts, for any objects $X$ and $Y$, the composition of the first inclusion morphism $\iota_1: X \to X \oplus Y$ with the first projection morphism $\pi_1: X \oplus Y \to X$ equals the identity morphism on $X$, i.e., $\iota_1 \circ \pi_1 = \text{id}_X$.

CategoryTheory.Limits.biprod.inl_snd theorem

{X Y : C} [HasBinaryBiproduct X Y] : (biprod.inl : X ⟶ X ⊞ Y) ≫ (biprod.snd : X ⊞ Y ⟶ Y) = 0

Full source

@[reassoc]
theorem biprod.inl_snd {X Y : C} [HasBinaryBiproduct X Y] :
    (biprod.inl : X ⟶ X ⊞ Y) ≫ (biprod.snd : X ⊞ Y ⟶ Y) = 0 :=
  (BinaryBiproduct.bicone X Y).inl_snd

Biproduct Identity: $\iota_1 \circ \pi_2 = 0$

Informal description

In a category $C$ with zero morphisms and binary biproducts, for any objects $X$ and $Y$, the composition of the first inclusion morphism $\iota_1: X \to X \oplus Y$ and the second projection morphism $\pi_2: X \oplus Y \to Y$ is the zero morphism, i.e., $\iota_1 \circ \pi_2 = 0$.

CategoryTheory.Limits.biprod.inr_fst theorem

{X Y : C} [HasBinaryBiproduct X Y] : (biprod.inr : Y ⟶ X ⊞ Y) ≫ (biprod.fst : X ⊞ Y ⟶ X) = 0

Full source

@[reassoc]
theorem biprod.inr_fst {X Y : C} [HasBinaryBiproduct X Y] :
    (biprod.inr : Y ⟶ X ⊞ Y) ≫ (biprod.fst : X ⊞ Y ⟶ X) = 0 :=
  (BinaryBiproduct.bicone X Y).inr_fst

Composition of Second Inclusion and First Projection Yields Zero Morphism

Informal description

For any objects $X$ and $Y$ in a category $C$ with binary biproducts, the composition of the inclusion morphism $\iota_2: Y \to X \oplus Y$ followed by the first projection morphism $\pi_1: X \oplus Y \to X$ equals the zero morphism, i.e., $\iota_2 \circ \pi_1 = 0$.

CategoryTheory.Limits.biprod.inr_snd theorem

{X Y : C} [HasBinaryBiproduct X Y] : (biprod.inr : Y ⟶ X ⊞ Y) ≫ (biprod.snd : X ⊞ Y ⟶ Y) = 𝟙 Y

Full source

@[reassoc]
theorem biprod.inr_snd {X Y : C} [HasBinaryBiproduct X Y] :
    (biprod.inr : Y ⟶ X ⊞ Y) ≫ (biprod.snd : X ⊞ Y ⟶ Y) = 𝟙 Y :=
  (BinaryBiproduct.bicone X Y).inr_snd

Biproduct Identity: $\iota_2 \circ \pi_2 = \text{id}_Y$

Informal description

In a category $C$ with binary biproducts, for any objects $X$ and $Y$, the composition of the inclusion morphism $\iota_2: Y \to X \oplus Y$ and the second projection $\pi_2: X \oplus Y \to Y$ is equal to the identity morphism on $Y$, i.e., $\iota_2 \circ \pi_2 = \text{id}_Y$.

CategoryTheory.Limits.biprod.lift abbrev

{W X Y : C} [HasBinaryBiproduct X Y] (f : W ⟶ X) (g : W ⟶ Y) : W ⟶ X ⊞ Y

Full source

/-- Given a pair of maps into the summands of a binary biproduct,
we obtain a map into the binary biproduct. -/
abbrev biprod.lift {W X Y : C} [HasBinaryBiproduct X Y] (f : W ⟶ X) (g : W ⟶ Y) : W ⟶ X ⊞ Y :=
  (BinaryBiproduct.isLimit X Y).lift (BinaryFan.mk f g)

Universal property of biproduct: lifting morphisms to $X \oplus Y$

Informal description

Given objects $W, X, Y$ in a category $C$ with binary biproducts, and morphisms $f \colon W \to X$ and $g \colon W \to Y$, there exists a unique morphism $\mathrm{biprod.lift}\,f\,g \colon W \to X \oplus Y$ factoring $f$ and $g$ through the biproduct $X \oplus Y$.

CategoryTheory.Limits.biprod.desc abbrev

{W X Y : C} [HasBinaryBiproduct X Y] (f : X ⟶ W) (g : Y ⟶ W) : X ⊞ Y ⟶ W

Full source

/-- Given a pair of maps out of the summands of a binary biproduct,
we obtain a map out of the binary biproduct. -/
abbrev biprod.desc {W X Y : C} [HasBinaryBiproduct X Y] (f : X ⟶ W) (g : Y ⟶ W) : X ⊞ YX ⊞ Y ⟶ W :=
  (BinaryBiproduct.isColimit X Y).desc (BinaryCofan.mk f g)

Universal Morphism from Biproduct: $X \oplus Y \to W$ via $f$ and $g$

Informal description

Given objects $X$, $Y$, and $W$ in a category $C$ with binary biproducts, and morphisms $f \colon X \to W$ and $g \colon Y \to W$, there exists a unique morphism $\mathrm{biprod.desc}\,f\,g \colon X \oplus Y \to W$ induced by the universal property of the biproduct $X \oplus Y$.

CategoryTheory.Limits.biprod.lift_fst theorem

{W X Y : C} [HasBinaryBiproduct X Y] (f : W ⟶ X) (g : W ⟶ Y) : biprod.lift f g ≫ biprod.fst = f

Full source

@[reassoc (attr := simp)]
theorem biprod.lift_fst {W X Y : C} [HasBinaryBiproduct X Y] (f : W ⟶ X) (g : W ⟶ Y) :
    biprod.liftbiprod.lift f g ≫ biprod.fst = f :=
  (BinaryBiproduct.isLimit X Y).fac _ ⟨WalkingPair.left⟩

First projection of biproduct lifting equals first morphism

Informal description

For any objects $W, X, Y$ in a category $C$ with binary biproducts, and morphisms $f \colon W \to X$ and $g \colon W \to Y$, the composition of the biproduct lifting morphism $\mathrm{lift}(f, g) \colon W \to X \oplus Y$ with the first projection $\pi_1 \colon X \oplus Y \to X$ equals $f$, i.e., $\mathrm{lift}(f, g) \circ \pi_1 = f$.

CategoryTheory.Limits.biprod.lift_snd theorem

{W X Y : C} [HasBinaryBiproduct X Y] (f : W ⟶ X) (g : W ⟶ Y) : biprod.lift f g ≫ biprod.snd = g

Full source

@[reassoc (attr := simp)]
theorem biprod.lift_snd {W X Y : C} [HasBinaryBiproduct X Y] (f : W ⟶ X) (g : W ⟶ Y) :
    biprod.liftbiprod.lift f g ≫ biprod.snd = g :=
  (BinaryBiproduct.isLimit X Y).fac _ ⟨WalkingPair.right⟩

Second projection of biproduct lifting equals second morphism

Informal description

For any objects $W, X, Y$ in a category $C$ with binary biproducts, and morphisms $f \colon W \to X$ and $g \colon W \to Y$, the composition of the biproduct lifting morphism $\mathrm{lift}(f, g) \colon W \to X \oplus Y$ with the second projection $\pi_2 \colon X \oplus Y \to Y$ equals $g$, i.e., $\mathrm{lift}(f, g) \circ \pi_2 = g$.

CategoryTheory.Limits.biprod.inl_desc theorem

{W X Y : C} [HasBinaryBiproduct X Y] (f : X ⟶ W) (g : Y ⟶ W) : biprod.inl ≫ biprod.desc f g = f

Full source

@[reassoc (attr := simp)]
theorem biprod.inl_desc {W X Y : C} [HasBinaryBiproduct X Y] (f : X ⟶ W) (g : Y ⟶ W) :
    biprod.inlbiprod.inl ≫ biprod.desc f g = f :=
  (BinaryBiproduct.isColimit X Y).fac _ ⟨WalkingPair.left⟩

First inclusion property of biproduct universal morphism: $\iota_1 \circ \mathrm{desc}(f,g) = f$

Informal description

In a category with binary biproducts, for any objects $X$, $Y$, and $W$, and morphisms $f \colon X \to W$ and $g \colon Y \to W$, the composition of the first inclusion morphism $\iota_1 \colon X \to X \oplus Y$ with the universal morphism $\mathrm{desc}(f,g) \colon X \oplus Y \to W$ equals $f$, i.e., $\iota_1 \circ \mathrm{desc}(f,g) = f$.

CategoryTheory.Limits.biprod.inr_desc theorem

{W X Y : C} [HasBinaryBiproduct X Y] (f : X ⟶ W) (g : Y ⟶ W) : biprod.inr ≫ biprod.desc f g = g

Full source

@[reassoc (attr := simp)]
theorem biprod.inr_desc {W X Y : C} [HasBinaryBiproduct X Y] (f : X ⟶ W) (g : Y ⟶ W) :
    biprod.inrbiprod.inr ≫ biprod.desc f g = g :=
  (BinaryBiproduct.isColimit X Y).fac _ ⟨WalkingPair.right⟩

Commutativity of second inclusion with biproduct universal morphism: $\iota_2 \circ \mathrm{desc}(f,g) = g$

Informal description

In a category $C$ with binary biproducts, for any objects $W, X, Y$ and morphisms $f \colon X \to W$, $g \colon Y \to W$, the composition of the inclusion morphism $\iota_2 \colon Y \to X \oplus Y$ with the universal morphism $\mathrm{desc}(f, g) \colon X \oplus Y \to W$ equals $g$, i.e., $\iota_2 \circ \mathrm{desc}(f, g) = g$.

CategoryTheory.Limits.biprod.mono_lift_of_mono_left instance

{W X Y : C} [HasBinaryBiproduct X Y] (f : W ⟶ X) (g : W ⟶ Y) [Mono f] : Mono (biprod.lift f g)

Full source

instance biprod.mono_lift_of_mono_left {W X Y : C} [HasBinaryBiproduct X Y] (f : W ⟶ X) (g : W ⟶ Y)
    [Mono f] : Mono (biprod.lift f g) :=
  mono_of_mono_fac <| biprod.lift_fst _ _

Lifted Morphism to Biproduct is Mono When First Factor is Mono

Informal description

In a category with binary biproducts, given morphisms $f \colon W \to X$ and $g \colon W \to Y$ where $f$ is a monomorphism, the lifted morphism $\mathrm{lift}(f, g) \colon W \to X \oplus Y$ is also a monomorphism.

CategoryTheory.Limits.biprod.mono_lift_of_mono_right instance

{W X Y : C} [HasBinaryBiproduct X Y] (f : W ⟶ X) (g : W ⟶ Y) [Mono g] : Mono (biprod.lift f g)

Full source

instance biprod.mono_lift_of_mono_right {W X Y : C} [HasBinaryBiproduct X Y] (f : W ⟶ X) (g : W ⟶ Y)
    [Mono g] : Mono (biprod.lift f g) :=
  mono_of_mono_fac <| biprod.lift_snd _ _

Lifted Morphism to Biproduct is Mono when Right Factor is Mono

Informal description

In a category $C$ with binary biproducts, for any objects $W, X, Y$ and morphisms $f \colon W \to X$, $g \colon W \to Y$, if $g$ is a monomorphism, then the lifted morphism $\mathrm{biprod.lift}\,f\,g \colon W \to X \oplus Y$ is also a monomorphism.

CategoryTheory.Limits.biprod.epi_desc_of_epi_left instance

{W X Y : C} [HasBinaryBiproduct X Y] (f : X ⟶ W) (g : Y ⟶ W) [Epi f] : Epi (biprod.desc f g)

Full source

instance biprod.epi_desc_of_epi_left {W X Y : C} [HasBinaryBiproduct X Y] (f : X ⟶ W) (g : Y ⟶ W)
    [Epi f] : Epi (biprod.desc f g) :=
  epi_of_epi_fac <| biprod.inl_desc _ _

Epimorphism Property of Biproduct Descending Morphism via Left Epimorphism

Informal description

For objects $X$, $Y$, and $W$ in a category $C$ with binary biproducts, given morphisms $f \colon X \to W$ and $g \colon Y \to W$, if $f$ is an epimorphism, then the induced morphism $\mathrm{biprod.desc}\,f\,g \colon X \oplus Y \to W$ is also an epimorphism.

CategoryTheory.Limits.biprod.epi_desc_of_epi_right instance

{W X Y : C} [HasBinaryBiproduct X Y] (f : X ⟶ W) (g : Y ⟶ W) [Epi g] : Epi (biprod.desc f g)

Full source

instance biprod.epi_desc_of_epi_right {W X Y : C} [HasBinaryBiproduct X Y] (f : X ⟶ W) (g : Y ⟶ W)
    [Epi g] : Epi (biprod.desc f g) :=
  epi_of_epi_fac <| biprod.inr_desc _ _

Epimorphism Property of Biproduct Descending Morphism with Right Epimorphism

Informal description

In a category with binary biproducts, given morphisms $f \colon X \to W$ and $g \colon Y \to W$ where $g$ is an epimorphism, the induced morphism $\mathrm{desc}(f, g) \colon X \oplus Y \to W$ is also an epimorphism.

CategoryTheory.Limits.biprod.map abbrev

{W X Y Z : C} [HasBinaryBiproduct W X] [HasBinaryBiproduct Y Z] (f : W ⟶ Y) (g : X ⟶ Z) : W ⊞ X ⟶ Y ⊞ Z

Full source

/-- Given a pair of maps between the summands of a pair of binary biproducts,
we obtain a map between the binary biproducts. -/
abbrev biprod.map {W X Y Z : C} [HasBinaryBiproduct W X] [HasBinaryBiproduct Y Z] (f : W ⟶ Y)
    (g : X ⟶ Z) : W ⊞ XW ⊞ X ⟶ Y ⊞ Z :=
  IsLimit.map (BinaryBiproduct.bicone W X).toCone (BinaryBiproduct.isLimit Y Z)
    (@mapPair _ _ (pair W X) (pair Y Z) f g)

Canonical Morphism Between Biproducts: $f \oplus g: W \oplus X \to Y \oplus Z$

Informal description

Given a category $C$ with binary biproducts, and objects $W, X, Y, Z$ in $C$ such that $W \oplus X$ and $Y \oplus Z$ exist, for any morphisms $f: W \to Y$ and $g: X \to Z$, there exists a canonical morphism $f \oplus g: W \oplus X \to Y \oplus Z$ between the biproducts.

CategoryTheory.Limits.biprod.map' abbrev

{W X Y Z : C} [HasBinaryBiproduct W X] [HasBinaryBiproduct Y Z] (f : W ⟶ Y) (g : X ⟶ Z) : W ⊞ X ⟶ Y ⊞ Z

Full source

/-- An alternative to `biprod.map` constructed via colimits.
This construction only exists in order to show it is equal to `biprod.map`. -/
abbrev biprod.map' {W X Y Z : C} [HasBinaryBiproduct W X] [HasBinaryBiproduct Y Z] (f : W ⟶ Y)
    (g : X ⟶ Z) : W ⊞ XW ⊞ X ⟶ Y ⊞ Z :=
  IsColimit.map (BinaryBiproduct.isColimit W X) (BinaryBiproduct.bicone Y Z).toCocone
    (@mapPair _ _ (pair W X) (pair Y Z) f g)

Biproduct morphism construction via colimits

Informal description

Given objects $W, X, Y, Z$ in a category $C$ with binary biproducts, and morphisms $f: W \to Y$ and $g: X \to Z$, there exists a morphism $W \oplus X \to Y \oplus Z$ between the biproduct objects, where $\oplus$ denotes the biproduct construction.

CategoryTheory.Limits.biprod.hom_ext theorem

 {X Y Z : C} [HasBinaryBiproduct X Y] (f g : Z ⟶ X ⊞ Y) (h₀ : f ≫ biprod.fst = g ≫ biprod.fst)
  (h₁ : f ≫ biprod.snd = g ≫ biprod.snd) : f = g

Full source

@[ext]
theorem biprod.hom_ext {X Y Z : C} [HasBinaryBiproduct X Y] (f g : Z ⟶ X ⊞ Y)
    (h₀ : f ≫ biprod.fst = g ≫ biprod.fst) (h₁ : f ≫ biprod.snd = g ≫ biprod.snd) : f = g :=
  BinaryFan.IsLimit.hom_ext (BinaryBiproduct.isLimit X Y) h₀ h₁

Uniqueness of Morphisms into Biproduct via Commuting Projections

Informal description

Let $X$, $Y$, and $Z$ be objects in a category $C$ with binary biproducts. For any two morphisms $f, g : Z \to X \oplus Y$, if both $f \circ \pi_1 = g \circ \pi_1$ and $f \circ \pi_2 = g \circ \pi_2$ hold (where $\pi_1 : X \oplus Y \to X$ and $\pi_2 : X \oplus Y \to Y$ are the projection morphisms), then $f = g$.

CategoryTheory.Limits.biprod.hom_ext' theorem

 {X Y Z : C} [HasBinaryBiproduct X Y] (f g : X ⊞ Y ⟶ Z) (h₀ : biprod.inl ≫ f = biprod.inl ≫ g)
  (h₁ : biprod.inr ≫ f = biprod.inr ≫ g) : f = g

Full source

@[ext]
theorem biprod.hom_ext' {X Y Z : C} [HasBinaryBiproduct X Y] (f g : X ⊞ YX ⊞ Y ⟶ Z)
    (h₀ : biprod.inlbiprod.inl ≫ f = biprod.inlbiprod.inl ≫ g) (h₁ : biprod.inrbiprod.inr ≫ f = biprod.inrbiprod.inr ≫ g) : f = g :=
  BinaryCofan.IsColimit.hom_ext (BinaryBiproduct.isColimit X Y) h₀ h₁

Uniqueness of Morphisms from Binary Biproduct via Commuting Inclusions

Informal description

Let $X$, $Y$, and $Z$ be objects in a category $C$ with binary biproducts. For any two morphisms $f, g: X \oplus Y \to Z$, if both compositions $f \circ \iota_X = g \circ \iota_X$ and $f \circ \iota_Y = g \circ \iota_Y$ hold (where $\iota_X: X \to X \oplus Y$ and $\iota_Y: Y \to X \oplus Y$ are the inclusion morphisms), then $f = g$.

CategoryTheory.Limits.biprod.isoProd definition

(X Y : C) [HasBinaryBiproduct X Y] : X ⊞ Y ≅ X ⨯ Y

Full source

/-- The canonical isomorphism between the chosen biproduct and the chosen product. -/
def biprod.isoProd (X Y : C) [HasBinaryBiproduct X Y] : X ⊞ YX ⊞ Y ≅ X ⨯ Y :=
  IsLimit.conePointUniqueUpToIso (BinaryBiproduct.isLimit X Y) (limit.isLimit _)

Isomorphism between biproduct and product $X \oplus Y \cong X \times Y$

Informal description

The canonical isomorphism between the binary biproduct $X \oplus Y$ and the binary product $X \times Y$ in a category with binary biproducts. This isomorphism exists because the biproduct simultaneously serves as both the product and coproduct of $X$ and $Y$ in such categories.

CategoryTheory.Limits.biprod.isoProd_hom theorem

{X Y : C} [HasBinaryBiproduct X Y] : (biprod.isoProd X Y).hom = prod.lift biprod.fst biprod.snd

Full source

@[simp]
theorem biprod.isoProd_hom {X Y : C} [HasBinaryBiproduct X Y] :
    (biprod.isoProd X Y).hom = prod.lift biprod.fst biprod.snd := by
      ext <;> simp [biprod.isoProd]

Homomorphism of Biproduct-Product Isomorphism as Lift of Projections

Informal description

For objects $X$ and $Y$ in a category $C$ with binary biproducts, the homomorphism component of the canonical isomorphism $X \oplus Y \cong X \times Y$ is equal to the morphism $\mathrm{prod.lift}\, \pi_1\, \pi_2$, where $\pi_1: X \oplus Y \to X$ and $\pi_2: X \oplus Y \to Y$ are the projection morphisms from the biproduct.

CategoryTheory.Limits.biprod.isoProd_inv theorem

{X Y : C} [HasBinaryBiproduct X Y] : (biprod.isoProd X Y).inv = biprod.lift prod.fst prod.snd

Full source

@[simp]
theorem biprod.isoProd_inv {X Y : C} [HasBinaryBiproduct X Y] :
    (biprod.isoProd X Y).inv = biprod.lift prod.fst prod.snd := by
  ext <;> simp [Iso.inv_comp_eq]

Inverse of Biproduct-Product Isomorphism via Lifting Projections

Informal description

For objects $X$ and $Y$ in a category $\mathcal{C}$ with binary biproducts, the inverse of the canonical isomorphism $X \oplus Y \cong X \times Y$ is equal to the morphism $\mathrm{biprod.lift}\, \pi_1\, \pi_2$, where $\pi_1: X \times Y \to X$ and $\pi_2: X \times Y \to Y$ are the projection morphisms from the product.

CategoryTheory.Limits.biprod.isoCoprod definition

(X Y : C) [HasBinaryBiproduct X Y] : X ⊞ Y ≅ X ⨿ Y

Full source

/-- The canonical isomorphism between the chosen biproduct and the chosen coproduct. -/
def biprod.isoCoprod (X Y : C) [HasBinaryBiproduct X Y] : X ⊞ YX ⊞ Y ≅ X ⨿ Y :=
  IsColimit.coconePointUniqueUpToIso (BinaryBiproduct.isColimit X Y) (colimit.isColimit _)

Isomorphism between biproduct and coproduct

Informal description

Given objects $X$ and $Y$ in a category $C$ with binary biproducts, there exists a canonical isomorphism between the biproduct $X \oplus Y$ and the coproduct $X \sqcup Y$. This isomorphism is induced by the universal properties of the biproduct (as both a limit and colimit) and the coproduct (as a colimit).

CategoryTheory.Limits.biprod.isoCoprod_inv theorem

{X Y : C} [HasBinaryBiproduct X Y] : (biprod.isoCoprod X Y).inv = coprod.desc biprod.inl biprod.inr

Full source

@[simp]
theorem biprod.isoCoprod_inv {X Y : C} [HasBinaryBiproduct X Y] :
    (biprod.isoCoprod X Y).inv = coprod.desc biprod.inl biprod.inr := by
  ext <;> simp [biprod.isoCoprod]

Inverse of Biproduct-Coproduct Isomorphism via Coproduct Universal Property

Informal description

For objects $X$ and $Y$ in a category $C$ with binary biproducts, the inverse of the canonical isomorphism $X \oplus Y \cong X \sqcup Y$ between the biproduct and coproduct is equal to the morphism induced by the universal property of the coproduct, applied to the inclusion maps $\iota_1: X \to X \oplus Y$ and $\iota_2: Y \to X \oplus Y$.

CategoryTheory.Limits.biprod_isoCoprod_hom theorem

{X Y : C} [HasBinaryBiproduct X Y] : (biprod.isoCoprod X Y).hom = biprod.desc coprod.inl coprod.inr

Full source

@[simp]
theorem biprod_isoCoprod_hom {X Y : C} [HasBinaryBiproduct X Y] :
    (biprod.isoCoprod X Y).hom = biprod.desc coprod.inl coprod.inr := by
  ext <;> simp [← Iso.eq_comp_inv]

Forward isomorphism of biproduct-coproduct equivalence via coproduct inclusions

Informal description

For objects $X$ and $Y$ in a category $C$ with binary biproducts, the forward direction of the canonical isomorphism $X \oplus Y \cong X \sqcup Y$ between the biproduct and coproduct is equal to the universal morphism $\mathrm{desc}(\iota_1, \iota_2) \colon X \oplus Y \to X \sqcup Y$ induced by the coproduct inclusions $\iota_1 \colon X \to X \sqcup Y$ and $\iota_2 \colon Y \to X \sqcup Y$.

CategoryTheory.Limits.biprod.map_eq_map' theorem

 {W X Y Z : C} [HasBinaryBiproduct W X] [HasBinaryBiproduct Y Z] (f : W ⟶ Y) (g : X ⟶ Z) :
  biprod.map f g = biprod.map' f g

Full source

theorem biprod.map_eq_map' {W X Y Z : C} [HasBinaryBiproduct W X] [HasBinaryBiproduct Y Z]
    (f : W ⟶ Y) (g : X ⟶ Z) : biprod.map f g = biprod.map' f g := by
  ext
  · simp only [mapPair_left, IsColimit.ι_map, IsLimit.map_π, biprod.inl_fst_assoc,
      Category.assoc, ← BinaryBicone.toCone_π_app_left, ← BinaryBiproduct.bicone_fst, ←
      BinaryBicone.toCocone_ι_app_left, ← BinaryBiproduct.bicone_inl]
    dsimp; simp
  · simp only [mapPair_left, IsColimit.ι_map, IsLimit.map_π, zero_comp, biprod.inl_snd_assoc,
      Category.assoc, ← BinaryBicone.toCone_π_app_right, ← BinaryBiproduct.bicone_snd, ←
      BinaryBicone.toCocone_ι_app_left, ← BinaryBiproduct.bicone_inl]
    simp
  · simp only [mapPair_right, biprod.inr_fst_assoc, IsColimit.ι_map, IsLimit.map_π, zero_comp,
      Category.assoc, ← BinaryBicone.toCone_π_app_left, ← BinaryBiproduct.bicone_fst, ←
      BinaryBicone.toCocone_ι_app_right, ← BinaryBiproduct.bicone_inr]
    simp
  · simp only [mapPair_right, IsColimit.ι_map, IsLimit.map_π, biprod.inr_snd_assoc,
      Category.assoc, ← BinaryBicone.toCone_π_app_right, ← BinaryBiproduct.bicone_snd, ←
      BinaryBicone.toCocone_ι_app_right, ← BinaryBiproduct.bicone_inr]
    simp

Equality of Biproduct Morphisms Constructed via Limits and Colimits: $f \oplus g = f \oplus' g$

Informal description

Let $C$ be a category with binary biproducts, and let $W, X, Y, Z$ be objects in $C$ such that biproducts $W \oplus X$ and $Y \oplus Z$ exist. For any morphisms $f: W \to Y$ and $g: X \to Z$, the canonical morphism $f \oplus g: W \oplus X \to Y \oplus Z$ constructed via the limit property equals the morphism constructed via the colimit property.

CategoryTheory.Limits.biprod.inl_mono instance

{X Y : C} [HasBinaryBiproduct X Y] : IsSplitMono (biprod.inl : X ⟶ X ⊞ Y)

Full source

instance biprod.inl_mono {X Y : C} [HasBinaryBiproduct X Y] :
    IsSplitMono (biprod.inl : X ⟶ X ⊞ Y) :=
  IsSplitMono.mk' { retraction := biprod.fst }

The First Inclusion into a Biproduct is a Split Monomorphism

Informal description

For any objects $X$ and $Y$ in a category $C$ with binary biproducts, the inclusion morphism $\iota_1: X \to X \oplus Y$ is a split monomorphism. This means there exists a retraction morphism $r: X \oplus Y \to X$ such that $r \circ \iota_1 = \text{id}_X$.

CategoryTheory.Limits.biprod.inr_mono instance

{X Y : C} [HasBinaryBiproduct X Y] : IsSplitMono (biprod.inr : Y ⟶ X ⊞ Y)

Full source

instance biprod.inr_mono {X Y : C} [HasBinaryBiproduct X Y] :
    IsSplitMono (biprod.inr : Y ⟶ X ⊞ Y) :=
  IsSplitMono.mk' { retraction := biprod.snd }

The Second Inclusion in a Biproduct is a Split Monomorphism

Informal description

In a category $C$ with binary biproducts, the inclusion morphism $\text{inr} : Y \to X \oplus Y$ into the second summand of the biproduct $X \oplus Y$ is a split monomorphism. This means there exists a retraction morphism $r : X \oplus Y \to Y$ such that $r \circ \text{inr} = \text{id}_Y$.

CategoryTheory.Limits.biprod.fst_epi instance

{X Y : C} [HasBinaryBiproduct X Y] : IsSplitEpi (biprod.fst : X ⊞ Y ⟶ X)

Full source

instance biprod.fst_epi {X Y : C} [HasBinaryBiproduct X Y] : IsSplitEpi (biprod.fst : X ⊞ YX ⊞ Y ⟶ X) :=
  IsSplitEpi.mk' { section_ := biprod.inl }

First Projection from Biproduct is a Split Epimorphism

Informal description

For any objects $X$ and $Y$ in a category $C$ with binary biproducts, the first projection morphism $\pi_1: X \oplus Y \to X$ is a split epimorphism. That is, there exists a morphism $s: X \to X \oplus Y$ such that $\pi_1 \circ s = \text{id}_X$.

CategoryTheory.Limits.biprod.snd_epi instance

{X Y : C} [HasBinaryBiproduct X Y] : IsSplitEpi (biprod.snd : X ⊞ Y ⟶ Y)

Full source

instance biprod.snd_epi {X Y : C} [HasBinaryBiproduct X Y] : IsSplitEpi (biprod.snd : X ⊞ YX ⊞ Y ⟶ Y) :=
  IsSplitEpi.mk' { section_ := biprod.inr }

Second Projection from Binary Biproduct is a Split Epimorphism

Informal description

For any objects $X$ and $Y$ in a category $C$ with binary biproducts, the second projection morphism $\pi_2: X \oplus Y \to Y$ is a split epimorphism. This means there exists a morphism $s: Y \to X \oplus Y$ such that $\pi_2 \circ s = \text{id}_Y$.

CategoryTheory.Limits.biprod.map_fst theorem

 {W X Y Z : C} [HasBinaryBiproduct W X] [HasBinaryBiproduct Y Z] (f : W ⟶ Y) (g : X ⟶ Z) :
  biprod.map f g ≫ biprod.fst = biprod.fst ≫ f

Full source

@[reassoc (attr := simp)]
theorem biprod.map_fst {W X Y Z : C} [HasBinaryBiproduct W X] [HasBinaryBiproduct Y Z] (f : W ⟶ Y)
    (g : X ⟶ Z) : biprod.mapbiprod.map f g ≫ biprod.fst = biprod.fstbiprod.fst ≫ f :=
  IsLimit.map_π _ _ _ (⟨WalkingPair.left⟩ : Discrete WalkingPair)

Commutativity of biproduct map with first projection: $(f \oplus g) \circ \pi_1 = \pi_1 \circ f$

Informal description

Let $C$ be a category with binary biproducts, and let $W, X, Y, Z$ be objects in $C$ such that the biproducts $W \oplus X$ and $Y \oplus Z$ exist. For any morphisms $f: W \to Y$ and $g: X \to Z$, the following diagram commutes: \[ (f \oplus g) \circ \pi_1 = \pi_1 \circ f \] where $\pi_1: W \oplus X \to W$ and $\pi_1: Y \oplus Z \to Y$ are the first projection morphisms from the respective biproducts, and $f \oplus g: W \oplus X \to Y \oplus Z$ is the canonical morphism induced by $f$ and $g$.

CategoryTheory.Limits.biprod.map_snd theorem

 {W X Y Z : C} [HasBinaryBiproduct W X] [HasBinaryBiproduct Y Z] (f : W ⟶ Y) (g : X ⟶ Z) :
  biprod.map f g ≫ biprod.snd = biprod.snd ≫ g

Full source

@[reassoc (attr := simp)]
theorem biprod.map_snd {W X Y Z : C} [HasBinaryBiproduct W X] [HasBinaryBiproduct Y Z] (f : W ⟶ Y)
    (g : X ⟶ Z) : biprod.mapbiprod.map f g ≫ biprod.snd = biprod.sndbiprod.snd ≫ g :=
  IsLimit.map_π _ _ _ (⟨WalkingPair.right⟩ : Discrete WalkingPair)

Commutativity of Biproduct Map with Second Projection: $(f \oplus g) \circ \pi_2 = \pi_2 \circ g$

Informal description

In a category $C$ with binary biproducts, for any objects $W, X, Y, Z$ and morphisms $f: W \to Y$, $g: X \to Z$, the following diagram commutes: \[ (f \oplus g) \circ \pi_2 = \pi_2 \circ g \] where $\pi_2: X \oplus Y \to Y$ is the second projection from the biproduct and $f \oplus g: W \oplus X \to Y \oplus Z$ is the canonical morphism between biproducts induced by $f$ and $g$.

CategoryTheory.Limits.biprod.inl_map theorem

 {W X Y Z : C} [HasBinaryBiproduct W X] [HasBinaryBiproduct Y Z] (f : W ⟶ Y) (g : X ⟶ Z) :
  biprod.inl ≫ biprod.map f g = f ≫ biprod.inl

Full source

@[reassoc (attr := simp)]
theorem biprod.inl_map {W X Y Z : C} [HasBinaryBiproduct W X] [HasBinaryBiproduct Y Z] (f : W ⟶ Y)
    (g : X ⟶ Z) : biprod.inlbiprod.inl ≫ biprod.map f g = f ≫ biprod.inl := by
  rw [biprod.map_eq_map']
  exact IsColimit.ι_map (BinaryBiproduct.isColimit W X) _ _ ⟨WalkingPair.left⟩

Naturality of first inclusion with respect to biproduct morphisms: $\iota_1 \circ (f \oplus g) = f \circ \iota_1$

Informal description

Let $C$ be a category with binary biproducts, and let $W, X, Y, Z$ be objects in $C$ such that the biproducts $W \oplus X$ and $Y \oplus Z$ exist. For any morphisms $f: W \to Y$ and $g: X \to Z$, the following diagram commutes: \[ \iota_1 \circ (f \oplus g) = f \circ \iota_1 \] where $\iota_1: W \to W \oplus X$ is the first inclusion morphism into the biproduct, and $f \oplus g: W \oplus X \to Y \oplus Z$ is the canonical morphism between biproducts induced by $f$ and $g$.

CategoryTheory.Limits.biprod.inr_map theorem

 {W X Y Z : C} [HasBinaryBiproduct W X] [HasBinaryBiproduct Y Z] (f : W ⟶ Y) (g : X ⟶ Z) :
  biprod.inr ≫ biprod.map f g = g ≫ biprod.inr

Full source

@[reassoc (attr := simp)]
theorem biprod.inr_map {W X Y Z : C} [HasBinaryBiproduct W X] [HasBinaryBiproduct Y Z] (f : W ⟶ Y)
    (g : X ⟶ Z) : biprod.inrbiprod.inr ≫ biprod.map f g = g ≫ biprod.inr := by
  rw [biprod.map_eq_map']
  exact IsColimit.ι_map (BinaryBiproduct.isColimit W X) _ _ ⟨WalkingPair.right⟩

Naturality of second inclusion with respect to biproduct morphisms: $\iota_2 \circ (f \oplus g) = g \circ \iota_2$

Informal description

In a category $C$ with binary biproducts, for any objects $W, X, Y, Z$ and morphisms $f: W \to Y$, $g: X \to Z$, the following diagram commutes: \[ \iota_2 \circ (f \oplus g) = g \circ \iota_2 \] where $\iota_2: X \to X \oplus Y$ is the inclusion of the second summand into the biproduct, and $f \oplus g: W \oplus X \to Y \oplus Z$ is the canonical morphism between biproducts induced by $f$ and $g$.

CategoryTheory.Limits.biprod.mapIso definition

{W X Y Z : C} [HasBinaryBiproduct W X] [HasBinaryBiproduct Y Z] (f : W ≅ Y) (g : X ≅ Z) : W ⊞ X ≅ Y ⊞ Z

Full source

/-- Given a pair of isomorphisms between the summands of a pair of binary biproducts,
we obtain an isomorphism between the binary biproducts. -/
@[simps]
def biprod.mapIso {W X Y Z : C} [HasBinaryBiproduct W X] [HasBinaryBiproduct Y Z] (f : W ≅ Y)
    (g : X ≅ Z) : W ⊞ XW ⊞ X ≅ Y ⊞ Z where
  hom := biprod.map f.hom g.hom
  inv := biprod.map f.inv g.inv

Isomorphism between biproducts induced by isomorphisms of summands

Informal description

Given a category $ C $ with binary biproducts, and objects $ W, X, Y, Z $ in $ C $ such that $ W \oplus X $ and $ Y \oplus Z $ exist, for any isomorphisms $ f: W \cong Y $ and $ g: X \cong Z $, there exists an isomorphism $ W \oplus X \cong Y \oplus Z $ between the biproducts, where the forward morphism is the canonical map $ f \oplus g $ and the inverse morphism is the canonical map $ f^{-1} \oplus g^{-1} $.

CategoryTheory.Limits.biprod.conePointUniqueUpToIso_hom theorem

 (X Y : C) [HasBinaryBiproduct X Y] {b : BinaryBicone X Y} (hb : b.IsBilimit) :
  (hb.isLimit.conePointUniqueUpToIso (BinaryBiproduct.isLimit _ _)).hom = biprod.lift b.fst b.snd

Full source

/-- Auxiliary lemma for `biprod.uniqueUpToIso`. -/
theorem biprod.conePointUniqueUpToIso_hom (X Y : C) [HasBinaryBiproduct X Y] {b : BinaryBicone X Y}
    (hb : b.IsBilimit) :
    (hb.isLimit.conePointUniqueUpToIso (BinaryBiproduct.isLimit _ _)).hom =
      biprod.lift b.fst b.snd := rfl

Isomorphism component between bilimit bicone and biproduct equals lifting morphism

Informal description

Let $X$ and $Y$ be objects in a category $\mathcal{C}$ with binary biproducts, and let $b$ be a binary bicone for $X$ and $Y$ that is a bilimit. Then the homomorphism component of the isomorphism between the apex of $b$ and the biproduct $X \oplus Y$, induced by their universal properties as limits, is equal to the morphism $\mathrm{biprod.lift}\,b.\mathrm{fst}\,b.\mathrm{snd}$.

CategoryTheory.Limits.biprod.conePointUniqueUpToIso_inv theorem

 (X Y : C) [HasBinaryBiproduct X Y] {b : BinaryBicone X Y} (hb : b.IsBilimit) :
  (hb.isLimit.conePointUniqueUpToIso (BinaryBiproduct.isLimit _ _)).inv = biprod.desc b.inl b.inr

Full source

/-- Auxiliary lemma for `biprod.uniqueUpToIso`. -/
theorem biprod.conePointUniqueUpToIso_inv (X Y : C) [HasBinaryBiproduct X Y] {b : BinaryBicone X Y}
    (hb : b.IsBilimit) :
    (hb.isLimit.conePointUniqueUpToIso (BinaryBiproduct.isLimit _ _)).inv =
      biprod.desc b.inl b.inr := by
  refine biprod.hom_ext' _ _ (hb.isLimit.hom_ext fun j => ?_) (hb.isLimit.hom_ext fun j => ?_)
  all_goals
    simp only [Category.assoc, IsLimit.conePointUniqueUpToIso_inv_comp]
    rcases j with ⟨⟨⟩⟩
  all_goals simp

Inverse isomorphism component between bilimit bicone and biproduct equals descending morphism

Informal description

Let $X$ and $Y$ be objects in a category $\mathcal{C}$ with binary biproducts, and let $b$ be a binary bicone for $X$ and $Y$ that is a bilimit. Then the inverse component of the isomorphism between the apex of $b$ and the biproduct $X \oplus Y$, induced by their universal properties as limits, is equal to the morphism $\mathrm{biprod.desc}\,b.\mathrm{inl}\,b.\mathrm{inr}$.

CategoryTheory.Limits.biprod.uniqueUpToIso definition

(X Y : C) [HasBinaryBiproduct X Y] {b : BinaryBicone X Y} (hb : b.IsBilimit) : b.pt ≅ X ⊞ Y

Full source

/-- Binary biproducts are unique up to isomorphism. This already follows because bilimits are
    limits, but in the case of biproducts we can give an isomorphism with particularly nice
    definitional properties, namely that `biprod.lift b.fst b.snd` and `biprod.desc b.inl b.inr`
    are inverses of each other. -/
@[simps]
def biprod.uniqueUpToIso (X Y : C) [HasBinaryBiproduct X Y] {b : BinaryBicone X Y}
    (hb : b.IsBilimit) : b.pt ≅ X ⊞ Y where
  hom := biprod.lift b.fst b.snd
  inv := biprod.desc b.inl b.inr
  hom_inv_id := by
    rw [← biprod.conePointUniqueUpToIso_hom X Y hb, ←
      biprod.conePointUniqueUpToIso_inv X Y hb, Iso.hom_inv_id]
  inv_hom_id := by
    rw [← biprod.conePointUniqueUpToIso_hom X Y hb, ←
      biprod.conePointUniqueUpToIso_inv X Y hb, Iso.inv_hom_id]

Canonical isomorphism between bilimit bicone and biproduct

Informal description

Given objects $X$ and $Y$ in a category $C$ with binary biproducts, and a binary bicone $b$ for $X$ and $Y$ that is bilimit (i.e., simultaneously a limit and colimit), there exists a canonical isomorphism $b.pt \cong X \oplus Y$ between the bicone's point and the biproduct of $X$ and $Y$. This isomorphism is given by: - The forward map: $\mathrm{biprod.lift}\,b.\mathrm{fst}\,b.\mathrm{snd} : b.pt \to X \oplus Y$ (combining the projections) - The inverse map: $\mathrm{biprod.desc}\,b.\mathrm{inl}\,b.\mathrm{inr} : X \oplus Y \to b.pt$ (combining the inclusions)

CategoryTheory.Limits.biprod.isIso_inl_iff_id_eq_fst_comp_inl theorem

(X Y : C) [HasBinaryBiproduct X Y] : IsIso (biprod.inl : X ⟶ X ⊞ Y) ↔ 𝟙 (X ⊞ Y) = biprod.fst ≫ biprod.inl

Full source

theorem biprod.isIso_inl_iff_id_eq_fst_comp_inl (X Y : C) [HasBinaryBiproduct X Y] :
    IsIsoIsIso (biprod.inl : X ⟶ X ⊞ Y) ↔ 𝟙 (X ⊞ Y) = biprod.fst ≫ biprod.inl := by
  constructor
  · intro h
    have := (cancel_epi (inv biprod.inl : X ⊞ YX ⊞ Y ⟶ X)).2 <| @biprod.inl_fst _ _ _ X Y _
    rw [IsIso.inv_hom_id_assoc, Category.comp_id] at this
    rw [this, IsIso.inv_hom_id]
  · intro h
    exact ⟨⟨biprod.fst, biprod.inl_fst, h.symm⟩⟩

Isomorphism Criterion for Biproduct Inclusion: $\iota_1$ is iso iff $\text{id} = \pi_1 \circ \iota_1$

Informal description

Let $X$ and $Y$ be objects in a category $C$ with binary biproducts. The inclusion morphism $\iota_1 \colon X \to X \oplus Y$ is an isomorphism if and only if the identity morphism on $X \oplus Y$ equals the composition of the first projection $\pi_1 \colon X \oplus Y \to X$ followed by $\iota_1$, i.e., $\text{id}_{X \oplus Y} = \pi_1 \circ \iota_1$.

CategoryTheory.Limits.biprod.map_epi instance

 {W X Y Z : C} (f : W ⟶ Y) (g : X ⟶ Z) [Epi f] [Epi g] [HasBinaryBiproduct W X] [HasBinaryBiproduct Y Z] :
  Epi (biprod.map f g)

Full source

instance biprod.map_epi {W X Y Z : C} (f : W ⟶ Y) (g : X ⟶ Z) [Epi f]
    [Epi g] [HasBinaryBiproduct W X] [HasBinaryBiproduct Y Z] : Epi (biprod.map f g) := by
  rw [show biprod.map f g =
    (biprod.isoCoprod _ _).hom ≫ coprod.map f g ≫ (biprod.isoCoprod _ _).inv by aesop]
  infer_instance

Biproduct of Epimorphisms is Epimorphic

Informal description

For objects $W, X, Y, Z$ in a category $C$ with binary biproducts, if $f: W \to Y$ and $g: X \to Z$ are epimorphisms, then the induced morphism $f \oplus g: W \oplus X \to Y \oplus Z$ is also an epimorphism.

CategoryTheory.Limits.prod.map_epi instance

 {W X Y Z : C} (f : W ⟶ Y) (g : X ⟶ Z) [Epi f] [Epi g] [HasBinaryBiproduct W X] [HasBinaryBiproduct Y Z] :
  Epi (prod.map f g)

Full source

instance prod.map_epi {W X Y Z : C} (f : W ⟶ Y) (g : X ⟶ Z) [Epi f]
    [Epi g] [HasBinaryBiproduct W X] [HasBinaryBiproduct Y Z] : Epi (prod.map f g) := by
  rw [show prod.map f g = (biprod.isoProd _ _).inv ≫ biprod.map f g ≫
    (biprod.isoProd _ _).hom by simp]
  infer_instance

Product of Epimorphisms is Epimorphic

Informal description

For objects $W, X, Y, Z$ in a category $\mathcal{C}$ with binary biproducts, if $f \colon W \to Y$ and $g \colon X \to Z$ are epimorphisms, then the induced morphism $f \times g \colon W \times X \to Y \times Z$ is also an epimorphism.

CategoryTheory.Limits.biprod.map_mono instance

 {W X Y Z : C} (f : W ⟶ Y) (g : X ⟶ Z) [Mono f] [Mono g] [HasBinaryBiproduct W X] [HasBinaryBiproduct Y Z] :
  Mono (biprod.map f g)

Full source

instance biprod.map_mono {W X Y Z : C} (f : W ⟶ Y) (g : X ⟶ Z) [Mono f]
    [Mono g] [HasBinaryBiproduct W X] [HasBinaryBiproduct Y Z] : Mono (biprod.map f g) := by
  rw [show biprod.map f g = (biprod.isoProd _ _).hom ≫ prod.map f g ≫
    (biprod.isoProd _ _).inv by aesop]
  infer_instance

Biproduct Map Preserves Monomorphisms

Informal description

Let $\mathcal{C}$ be a category with binary biproducts. For any objects $W, X, Y, Z$ in $\mathcal{C}$ and monomorphisms $f \colon W \to Y$ and $g \colon X \to Z$, the induced morphism $f \oplus g \colon W \oplus X \to Y \oplus Z$ is also a monomorphism.

CategoryTheory.Limits.coprod.map_mono instance

 {W X Y Z : C} (f : W ⟶ Y) (g : X ⟶ Z) [Mono f] [Mono g] [HasBinaryBiproduct W X] [HasBinaryBiproduct Y Z] :
  Mono (coprod.map f g)

Full source

instance coprod.map_mono {W X Y Z : C} (f : W ⟶ Y) (g : X ⟶ Z) [Mono f]
    [Mono g] [HasBinaryBiproduct W X] [HasBinaryBiproduct Y Z] : Mono (coprod.map f g) := by
  rw [show coprod.map f g = (biprod.isoCoprod _ _).inv ≫ biprod.map f g ≫
    (biprod.isoCoprod _ _).hom by simp]
  infer_instance

Coproduct Map Preserves Monomorphisms

Informal description

In a category with binary biproducts, for any objects $W, X, Y, Z$ and monomorphisms $f \colon W \to Y$ and $g \colon X \to Z$, the coproduct map $f \sqcup g \colon W \sqcup X \to Y \sqcup Z$ is also a monomorphism.

CategoryTheory.Limits.BinaryBicone.fstKernelFork definition

: KernelFork c.fst

Full source

/-- A kernel fork for the kernel of `BinaryBicone.fst`. It consists of the morphism
`BinaryBicone.inr`. -/
def BinaryBicone.fstKernelFork : KernelFork c.fst :=
  KernelFork.ofι c.inr c.inr_fst

Kernel fork for the first projection of a binary bicone

Informal description

Given a binary bicone for objects $ P $ and $ Q $ in a category $ C $ with zero morphisms, the kernel fork for the morphism $ \text{fst} : X \to P $ is constructed using the morphism $ \text{inr} : Q \to X $, which satisfies $ \text{inr} \circ \text{fst} = 0 $.

CategoryTheory.Limits.BinaryBicone.fstKernelFork_ι theorem

: (BinaryBicone.fstKernelFork c).ι = c.inr

Full source

@[simp]
theorem BinaryBicone.fstKernelFork_ι : (BinaryBicone.fstKernelFork c).ι = c.inr := rfl

Kernel Fork Inclusion for First Projection Equals Right Inclusion in Binary Bicone

Informal description

For a binary bicone $c$ in a category with zero morphisms, the inclusion morphism $\iota$ of the kernel fork for the first projection $\text{fst} : X \to P$ is equal to the right inclusion morphism $\text{inr} : Q \to X$ of the bicone.

CategoryTheory.Limits.BinaryBicone.sndKernelFork definition

: KernelFork c.snd

Full source

/-- A kernel fork for the kernel of `BinaryBicone.snd`. It consists of the morphism
`BinaryBicone.inl`. -/
def BinaryBicone.sndKernelFork : KernelFork c.snd :=
  KernelFork.ofι c.inl c.inl_snd

Kernel fork for the second projection of a binary bicone

Informal description

Given a binary bicone `c` for objects `P` and `Q` in a category with zero morphisms, the kernel fork for the morphism `c.snd : X → Q` is constructed using the morphism `c.inl : P → X`, which satisfies the kernel condition `c.inl ≫ c.snd = 0`. This kernel fork consists of the object `P` and the morphism `c.inl`, demonstrating that `c.inl` is a kernel of `c.snd`.

CategoryTheory.Limits.BinaryBicone.sndKernelFork_ι theorem

: (BinaryBicone.sndKernelFork c).ι = c.inl

Full source

@[simp]
theorem BinaryBicone.sndKernelFork_ι : (BinaryBicone.sndKernelFork c).ι = c.inl := rfl

Kernel Fork Inclusion for Second Projection Equals First Inclusion in Binary Bicone

Informal description

For a binary bicone $c$ in a category with zero morphisms, the inclusion morphism $\iota$ of the kernel fork for the second projection $c.\text{snd}$ is equal to the first inclusion morphism $c.\text{inl}$ of the bicone.

CategoryTheory.Limits.BinaryBicone.inlCokernelCofork definition

: CokernelCofork c.inl

Full source

/-- A cokernel cofork for the cokernel of `BinaryBicone.inl`. It consists of the morphism
`BinaryBicone.snd`. -/
def BinaryBicone.inlCokernelCofork : CokernelCofork c.inl :=
  CokernelCofork.ofπ c.snd c.inl_snd

Cokernel cofork for the first inclusion of a binary bicone

Informal description

Given a binary bicone `c` for objects `P` and `Q` in a category with zero morphisms, the cokernel cofork for the morphism `c.inl : P ⟶ c.X` is constructed using the morphism `c.snd : c.X ⟶ Q`, satisfying the condition `c.inl ≫ c.snd = 0`.

CategoryTheory.Limits.BinaryBicone.inlCokernelCofork_π theorem

: (BinaryBicone.inlCokernelCofork c).π = c.snd

Full source

@[simp]
theorem BinaryBicone.inlCokernelCofork_π : (BinaryBicone.inlCokernelCofork c).π = c.snd := rfl

Cokernel cofork projection equals second projection in binary bicone

Informal description

For a binary bicone $c$ in a category with zero morphisms, the projection morphism $\pi$ of the cokernel cofork associated to the inclusion $c.\text{inl}$ is equal to the second projection $c.\text{snd}$ of the bicone.

CategoryTheory.Limits.BinaryBicone.inrCokernelCofork definition

: CokernelCofork c.inr

Full source

/-- A cokernel cofork for the cokernel of `BinaryBicone.inr`. It consists of the morphism
`BinaryBicone.fst`. -/
def BinaryBicone.inrCokernelCofork : CokernelCofork c.inr :=
  CokernelCofork.ofπ c.fst c.inr_fst

Cokernel cofork for the second inclusion of a binary bicone

Informal description

Given a binary bicone $ c $ for objects $ P $ and $ Q $ in a category with zero morphisms, the cokernel cofork for the morphism $ \text{inr} : Q \to X $ is constructed using the morphism $ \text{fst} : X \to P $, satisfying the condition $ \text{inr} \circ \text{fst} = 0 $.

CategoryTheory.Limits.BinaryBicone.inrCokernelCofork_π theorem

: (BinaryBicone.inrCokernelCofork c).π = c.fst

Full source

@[simp]
theorem BinaryBicone.inrCokernelCofork_π : (BinaryBicone.inrCokernelCofork c).π = c.fst := rfl

Cokernel Cofork Projection Equals First Projection in Binary Bicone

Informal description

For a binary bicone $c$ in a category with zero morphisms, the projection morphism $\pi$ of the cokernel cofork associated to the second inclusion $c.\text{inr}$ is equal to the first projection $c.\text{fst}$ of the bicone.

CategoryTheory.Limits.BinaryBicone.isLimitFstKernelFork definition

(i : IsLimit c.toCone) : IsLimit c.fstKernelFork

Full source

/-- The fork defined in `BinaryBicone.fstKernelFork` is indeed a kernel. -/
def BinaryBicone.isLimitFstKernelFork (i : IsLimit c.toCone) : IsLimit c.fstKernelFork :=
  Fork.IsLimit.mk' _ fun s =>
    ⟨s.ι ≫ c.snd, by apply BinaryFan.IsLimit.hom_ext i <;> simp, fun hm => by simp [← hm]⟩

Limit property of the kernel fork for the first projection in a binary bicone

Informal description

Given a binary bicone $ c $ for objects $ P $ and $ Q $ in a category with zero morphisms, if the cone associated to $ c $ is a limit cone, then the kernel fork for the first projection $ \text{fst} : X \to P $ is also a limit cone. Specifically, for any other fork $ s $ on $ \text{fst} $, there exists a unique morphism $ l : s.\text{pt} \to X $ such that $ l \circ \text{inr} = s.\iota $, where $ \text{inr} : Q \to X $ is the inclusion morphism of the bicone.

CategoryTheory.Limits.BinaryBicone.isLimitSndKernelFork definition

(i : IsLimit c.toCone) : IsLimit c.sndKernelFork

Full source

/-- The fork defined in `BinaryBicone.sndKernelFork` is indeed a kernel. -/
def BinaryBicone.isLimitSndKernelFork (i : IsLimit c.toCone) : IsLimit c.sndKernelFork :=
  Fork.IsLimit.mk' _ fun s =>
    ⟨s.ι ≫ c.fst, by apply BinaryFan.IsLimit.hom_ext i <;> simp, fun hm => by simp [← hm]⟩

Limit property of the kernel fork for the second projection in a binary bicone

Informal description

Given a binary bicone $ c $ for objects $ P $ and $ Q $ in a category with zero morphisms, if the cone associated to $ c $ is a limit cone, then the kernel fork for the second projection $ \text{snd} : X \to Q $ is also a limit cone. Specifically, for any other fork $ s $ on $ \text{snd} $, there exists a unique morphism $ l : s.\text{pt} \to X $ such that $ l \circ \text{inl} = s.\iota $, where $ \text{inl} : P \to X $ is the inclusion morphism of the bicone.

CategoryTheory.Limits.BinaryBicone.isColimitInlCokernelCofork definition

(i : IsColimit c.toCocone) : IsColimit c.inlCokernelCofork

Full source

/-- The cofork defined in `BinaryBicone.inlCokernelCofork` is indeed a cokernel. -/
def BinaryBicone.isColimitInlCokernelCofork (i : IsColimit c.toCocone) :
    IsColimit c.inlCokernelCofork :=
  Cofork.IsColimit.mk' _ fun s =>
    ⟨c.inr ≫ s.π, by apply BinaryCofan.IsColimit.hom_ext i <;> simp, fun hm => by simp [← hm]⟩

Colimit property of the cokernel cofork for the first inclusion in a binary bicone

Informal description

Given a binary bicone $ c $ for objects $ P $ and $ Q $ in a category with zero morphisms, if the cocone associated to $ c $ is a colimit cocone, then the cokernel cofork for the inclusion morphism $ \text{inl} : P \to c.X $ is also a colimit cofork. Specifically, for any other cofork $ s $ on $ \text{inl} $, there exists a unique morphism $ l : c.X \to s.\text{pt} $ such that $ \text{inr} \circ l = s.\pi $, where $ \text{inr} : Q \to c.X $ is the inclusion morphism of the bicone.

CategoryTheory.Limits.BinaryBicone.isColimitInrCokernelCofork definition

(i : IsColimit c.toCocone) : IsColimit c.inrCokernelCofork

Full source

/-- The cofork defined in `BinaryBicone.inrCokernelCofork` is indeed a cokernel. -/
def BinaryBicone.isColimitInrCokernelCofork (i : IsColimit c.toCocone) :
    IsColimit c.inrCokernelCofork :=
  Cofork.IsColimit.mk' _ fun s =>
    ⟨c.inl ≫ s.π, by apply BinaryCofan.IsColimit.hom_ext i <;> simp, fun hm => by simp [← hm]⟩

Colimit property of the cokernel cofork for the second inclusion in a binary bicone

Informal description

Given a binary bicone $ c $ for objects $ P $ and $ Q $ in a category with zero morphisms, if the cocone $ c.\text{toCocone} $ is a colimit cocone, then the cokernel cofork $ c.\text{inrCokernelCofork} $ for the morphism $ \text{inr} : Q \to c.\text{pt} $ is also a colimit cocone. Specifically, the universal property is satisfied: for any other cofork $ s $, there exists a unique morphism $ c.\text{inl} \circ s.\pi $ that makes the appropriate diagram commute.

CategoryTheory.Limits.biprod.fstKernelFork definition

: KernelFork (biprod.fst : X ⊞ Y ⟶ X)

Full source

/-- A kernel fork for the kernel of `biprod.fst`. It consists of the
morphism `biprod.inr`. -/
def biprod.fstKernelFork : KernelFork (biprod.fst : X ⊞ YX ⊞ Y ⟶ X) :=
  BinaryBicone.fstKernelFork _

Kernel fork for the first projection of a binary biproduct

Informal description

The kernel fork for the first projection morphism $\pi_1: X \oplus Y \to X$ from the binary biproduct $X \oplus Y$ is constructed using the inclusion morphism $\iota_2: Y \to X \oplus Y$, which satisfies $\iota_2 \circ \pi_1 = 0$.

CategoryTheory.Limits.biprod.fstKernelFork_ι theorem

: Fork.ι (biprod.fstKernelFork X Y) = (biprod.inr : Y ⟶ X ⊞ Y)

Full source

@[simp]
theorem biprod.fstKernelFork_ι : Fork.ι (biprod.fstKernelFork X Y) = (biprod.inr : Y ⟶ X ⊞ Y) :=
  rfl

Inclusion Morphism of Kernel Fork for First Projection Equals Second Inclusion

Informal description

For objects $X$ and $Y$ in a category $C$ with binary biproducts, the inclusion morphism $\iota$ of the kernel fork for the first projection $\pi_1: X \oplus Y \to X$ is equal to the second inclusion morphism $\text{inr}: Y \to X \oplus Y$.

CategoryTheory.Limits.biprod.isKernelFstKernelFork definition

: IsLimit (biprod.fstKernelFork X Y)

Full source

/-- The fork `biprod.fstKernelFork` is indeed a limit. -/
def biprod.isKernelFstKernelFork : IsLimit (biprod.fstKernelFork X Y) :=
  BinaryBicone.isLimitFstKernelFork (BinaryBiproduct.isLimit _ _)

Limit property of the kernel fork for the first projection of a binary biproduct

Informal description

The kernel fork for the first projection morphism $\pi_1: X \oplus Y \to X$ from the binary biproduct $X \oplus Y$ is a limit cone. This means that given any other fork $s$ on $\pi_1$, there exists a unique morphism $l: s.\text{pt} \to X \oplus Y$ such that $l \circ \iota_2 = s.\iota$, where $\iota_2: Y \to X \oplus Y$ is the second inclusion morphism of the biproduct.

CategoryTheory.Limits.biprod.sndKernelFork definition

: KernelFork (biprod.snd : X ⊞ Y ⟶ Y)

Full source

/-- A kernel fork for the kernel of `biprod.snd`. It consists of the
morphism `biprod.inl`. -/
def biprod.sndKernelFork : KernelFork (biprod.snd : X ⊞ YX ⊞ Y ⟶ Y) :=
  BinaryBicone.sndKernelFork _

Kernel fork for the second projection of a binary biproduct

Informal description

Given objects $ X $ and $ Y $ in a category $ C $ with zero morphisms and binary biproducts, the kernel fork for the second projection morphism $ \pi_2: X \oplus Y \to Y $ is constructed using the first inclusion morphism $ \iota_1: X \to X \oplus Y $, which satisfies $ \iota_1 \circ \pi_2 = 0 $.

CategoryTheory.Limits.biprod.sndKernelFork_ι theorem

: Fork.ι (biprod.sndKernelFork X Y) = (biprod.inl : X ⟶ X ⊞ Y)

Full source

@[simp]
theorem biprod.sndKernelFork_ι : Fork.ι (biprod.sndKernelFork X Y) = (biprod.inl : X ⟶ X ⊞ Y) :=
  rfl

Kernel Fork Inclusion Equals First Biproduct Inclusion

Informal description

In a category with zero morphisms and binary biproducts, for any objects $X$ and $Y$, the inclusion morphism of the kernel fork for the second projection $\pi_2: X \oplus Y \to Y$ is equal to the first inclusion morphism $\iota_1: X \to X \oplus Y$.

CategoryTheory.Limits.biprod.isKernelSndKernelFork definition

: IsLimit (biprod.sndKernelFork X Y)

Full source

/-- The fork `biprod.sndKernelFork` is indeed a limit. -/
def biprod.isKernelSndKernelFork : IsLimit (biprod.sndKernelFork X Y) :=
  BinaryBicone.isLimitSndKernelFork (BinaryBiproduct.isLimit _ _)

Limit property of the kernel fork for the second projection in a binary biproduct

Informal description

The kernel fork for the second projection $\pi_2: X \oplus Y \to Y$ in a binary biproduct is a limit cone. This means that given any other fork $s$ on $\pi_2$, there exists a unique morphism $l: s.\text{pt} \to X \oplus Y$ such that $l \circ \iota_1 = s.\iota$, where $\iota_1: X \to X \oplus Y$ is the first inclusion morphism of the biproduct.

CategoryTheory.Limits.biprod.inlCokernelCofork definition

: CokernelCofork (biprod.inl : X ⟶ X ⊞ Y)

Full source

/-- A cokernel cofork for the cokernel of `biprod.inl`. It consists of the
morphism `biprod.snd`. -/
def biprod.inlCokernelCofork : CokernelCofork (biprod.inl : X ⟶ X ⊞ Y) :=
  BinaryBicone.inlCokernelCofork _

Cokernel cofork for first biproduct inclusion

Informal description

The cokernel cofork for the first inclusion morphism $\iota_1: X \to X \oplus Y$ in a binary biproduct is given by the second projection $\pi_2: X \oplus Y \to Y$, satisfying $\iota_1 \circ \pi_2 = 0$.

CategoryTheory.Limits.biprod.inlCokernelCofork_π theorem

: Cofork.π (biprod.inlCokernelCofork X Y) = biprod.snd

Full source

@[simp]
theorem biprod.inlCokernelCofork_π : Cofork.π (biprod.inlCokernelCofork X Y) = biprod.snd :=
  rfl

Projection of Cokernel Cofork for First Biproduct Inclusion Equals Second Projection

Informal description

In a category with binary biproducts, the projection morphism $\pi$ of the cokernel cofork for the first inclusion $\iota_1: X \to X \oplus Y$ is equal to the second projection $\pi_2: X \oplus Y \to Y$.

CategoryTheory.Limits.biprod.isCokernelInlCokernelFork definition

: IsColimit (biprod.inlCokernelCofork X Y)

Full source

/-- The cofork `biprod.inlCokernelFork` is indeed a colimit. -/
def biprod.isCokernelInlCokernelFork : IsColimit (biprod.inlCokernelCofork X Y) :=
  BinaryBicone.isColimitInlCokernelCofork (BinaryBiproduct.isColimit _ _)

Cokernel property of the first biproduct inclusion

Informal description

The cokernel cofork for the first inclusion morphism $\iota_1: X \to X \oplus Y$ in a binary biproduct is a colimit cofork. This means that the cofork formed by the second projection $\pi_2: X \oplus Y \to Y$ (which satisfies $\iota_1 \circ \pi_2 = 0$) has the universal property of a cokernel for $\iota_1$.

CategoryTheory.Limits.biprod.inrCokernelCofork definition

: CokernelCofork (biprod.inr : Y ⟶ X ⊞ Y)

Full source

/-- A cokernel cofork for the cokernel of `biprod.inr`. It consists of the
morphism `biprod.fst`. -/
def biprod.inrCokernelCofork : CokernelCofork (biprod.inr : Y ⟶ X ⊞ Y) :=
  BinaryBicone.inrCokernelCofork _

Cokernel cofork for the second inclusion in a binary biproduct

Informal description

Given objects $X$ and $Y$ in a category $C$ with binary biproducts, the cokernel cofork for the inclusion morphism $\text{inr} : Y \to X \oplus Y$ is constructed using the projection morphism $\text{fst} : X \oplus Y \to X$, satisfying $\text{inr} \circ \text{fst} = 0$.

CategoryTheory.Limits.biprod.inrCokernelCofork_π theorem

: Cofork.π (biprod.inrCokernelCofork X Y) = biprod.fst

Full source

@[simp]
theorem biprod.inrCokernelCofork_π : Cofork.π (biprod.inrCokernelCofork X Y) = biprod.fst :=
  rfl

Projection of Cokernel Cofork for Second Inclusion in Binary Biproduct Equals First Projection

Informal description

For objects $X$ and $Y$ in a category $C$ with binary biproducts, the projection morphism $\pi$ of the cokernel cofork for the inclusion $\text{inr}: Y \to X \oplus Y$ is equal to the first projection $\text{fst}: X \oplus Y \to X$.

CategoryTheory.Limits.biprod.isCokernelInrCokernelFork definition

: IsColimit (biprod.inrCokernelCofork X Y)

Full source

/-- The cofork `biprod.inrCokernelFork` is indeed a colimit. -/
def biprod.isCokernelInrCokernelFork : IsColimit (biprod.inrCokernelCofork X Y) :=
  BinaryBicone.isColimitInrCokernelCofork (BinaryBiproduct.isColimit _ _)

Cokernel cofork for the second inclusion in a binary biproduct is a colimit

Informal description

The cokernel cofork for the inclusion morphism $\text{inr} : Y \to X \oplus Y$ in a binary biproduct is a colimit cocone. This means that the cofork satisfies the universal property of a cokernel for $\text{inr}$, where the projection morphism $\text{fst} : X \oplus Y \to X$ serves as the cofork morphism.

CategoryTheory.Limits.instHasKernelFst instance

: HasKernel (biprod.fst : X ⊞ Y ⟶ X)

Full source

instance : HasKernel (biprod.fst : X ⊞ YX ⊞ Y ⟶ X) :=
  HasLimit.mk ⟨_, biprod.isKernelFstKernelFork X Y⟩

Existence of Kernel for First Projection in Binary Biproduct

Informal description

For any objects $X$ and $Y$ in a category with binary biproducts, the first projection morphism $\pi_1: X \oplus Y \to X$ has a kernel.

CategoryTheory.Limits.kernelBiprodFstIso definition

: kernel (biprod.fst : X ⊞ Y ⟶ X) ≅ Y

Full source

/-- The kernel of `biprod.fst : X ⊞ Y ⟶ X` is `Y`. -/
@[simps!]
def kernelBiprodFstIso : kernelkernel (biprod.fst : X ⊞ Y ⟶ X) ≅ Y :=
  limit.isoLimitCone ⟨_, biprod.isKernelFstKernelFork X Y⟩

Isomorphism between kernel of first projection and second summand in a binary biproduct

Informal description

The kernel of the first projection morphism $\pi_1: X \oplus Y \to X$ from the binary biproduct $X \oplus Y$ is isomorphic to $Y$. More precisely, there exists an isomorphism between the kernel object $\text{ker}(\pi_1)$ and $Y$ in the category. This isomorphism arises from the universal property of the kernel, where the inclusion morphism $\iota_2: Y \to X \oplus Y$ serves as the kernel morphism, satisfying $\iota_2 \circ \pi_1 = 0$.

CategoryTheory.Limits.instHasKernelSnd instance

: HasKernel (biprod.snd : X ⊞ Y ⟶ Y)

Full source

instance : HasKernel (biprod.snd : X ⊞ YX ⊞ Y ⟶ Y) :=
  HasLimit.mk ⟨_, biprod.isKernelSndKernelFork X Y⟩

Existence of Kernel for the Second Projection in a Binary Biproduct

Informal description

For any objects $X$ and $Y$ in a category $\mathcal{C}$ with zero morphisms and binary biproducts, the second projection morphism $\pi_2: X \oplus Y \to Y$ has a kernel.

CategoryTheory.Limits.kernelBiprodSndIso definition

: kernel (biprod.snd : X ⊞ Y ⟶ Y) ≅ X

Full source

/-- The kernel of `biprod.snd : X ⊞ Y ⟶ Y` is `X`. -/
@[simps!]
def kernelBiprodSndIso : kernelkernel (biprod.snd : X ⊞ Y ⟶ Y) ≅ X :=
  limit.isoLimitCone ⟨_, biprod.isKernelSndKernelFork X Y⟩

Isomorphism between kernel of second projection and first biproduct factor

Informal description

The kernel of the second projection morphism $\pi_2: X \oplus Y \to Y$ in a binary biproduct is isomorphic to $X$. This isomorphism arises from the fact that the kernel fork for $\pi_2$ is a limit cone, where the first inclusion morphism $\iota_1: X \to X \oplus Y$ serves as the kernel morphism.

CategoryTheory.Limits.instHasCokernelInl instance

: HasCokernel (biprod.inl : X ⟶ X ⊞ Y)

Full source

instance : HasCokernel (biprod.inl : X ⟶ X ⊞ Y) :=
  HasColimit.mk ⟨_, biprod.isCokernelInlCokernelFork X Y⟩

Existence of Cokernel for First Biproduct Inclusion

Informal description

For any objects $X$ and $Y$ in a category with binary biproducts, the first inclusion morphism $\iota_1: X \to X \oplus Y$ has a cokernel.

CategoryTheory.Limits.cokernelBiprodInlIso definition

: cokernel (biprod.inl : X ⟶ X ⊞ Y) ≅ Y

Full source

/-- The cokernel of `biprod.inl : X ⟶ X ⊞ Y` is `Y`. -/
@[simps!]
def cokernelBiprodInlIso : cokernelcokernel (biprod.inl : X ⟶ X ⊞ Y) ≅ Y :=
  colimit.isoColimitCocone ⟨_, biprod.isCokernelInlCokernelFork X Y⟩

Isomorphism between cokernel of first biproduct inclusion and second object

Informal description

The cokernel of the first inclusion morphism $\iota_1: X \to X \oplus Y$ in a binary biproduct is isomorphic to $Y$.

CategoryTheory.Limits.instHasCokernelInr instance

: HasCokernel (biprod.inr : Y ⟶ X ⊞ Y)

Full source

instance : HasCokernel (biprod.inr : Y ⟶ X ⊞ Y) :=
  HasColimit.mk ⟨_, biprod.isCokernelInrCokernelFork X Y⟩

Existence of Cokernel for the Second Inclusion in a Binary Biproduct

Informal description

For any objects $X$ and $Y$ in a category with binary biproducts, the inclusion morphism $\text{inr} : Y \to X \oplus Y$ has a cokernel.

CategoryTheory.Limits.cokernelBiprodInrIso definition

: cokernel (biprod.inr : Y ⟶ X ⊞ Y) ≅ X

Full source

/-- The cokernel of `biprod.inr : Y ⟶ X ⊞ Y` is `X`. -/
@[simps!]
def cokernelBiprodInrIso : cokernelcokernel (biprod.inr : Y ⟶ X ⊞ Y) ≅ X :=
  colimit.isoColimitCocone ⟨_, biprod.isCokernelInrCokernelFork X Y⟩

Isomorphism between cokernel of second biproduct inclusion and first object

Informal description

The cokernel of the inclusion morphism $\text{inr} : Y \to X \oplus Y$ in a binary biproduct is isomorphic to $X$.

CategoryTheory.Limits.isoBiprodZero definition

{X Y : C} [HasBinaryBiproduct X Y] (hY : IsZero Y) : X ≅ X ⊞ Y

Full source

/-- If `Y` is a zero object, `X ≅ X ⊞ Y` for any `X`. -/
@[simps!]
def isoBiprodZero {X Y : C} [HasBinaryBiproduct X Y] (hY : IsZero Y) : X ≅ X ⊞ Y where
  hom := biprod.inl
  inv := biprod.fst
  inv_hom_id := by
    apply CategoryTheory.Limits.biprod.hom_ext <;>
      simp only [Category.assoc, biprod.inl_fst, Category.comp_id, Category.id_comp, biprod.inl_snd,
        comp_zero]
    apply hY.eq_of_tgt

Isomorphism $X \cong X \oplus Y$ when $Y$ is zero

Informal description

Given objects $X$ and $Y$ in a category $C$ with binary biproducts, if $Y$ is a zero object, then there is an isomorphism $X \cong X \oplus Y$ where: - The forward morphism is the first inclusion $\iota_1: X \to X \oplus Y$ - The inverse morphism is the first projection $\pi_1: X \oplus Y \to X$ This isomorphism satisfies $\pi_1 \circ \iota_1 = \text{id}_X$ and $\iota_1 \circ \pi_1 = \text{id}_{X \oplus Y}$ (modulo the zero morphisms involving $Y$).

CategoryTheory.Limits.isoZeroBiprod definition

{X Y : C} [HasBinaryBiproduct X Y] (hY : IsZero X) : Y ≅ X ⊞ Y

Full source

/-- If `X` is a zero object, `Y ≅ X ⊞ Y` for any `Y`. -/
@[simps]
def isoZeroBiprod {X Y : C} [HasBinaryBiproduct X Y] (hY : IsZero X) : Y ≅ X ⊞ Y where
  hom := biprod.inr
  inv := biprod.snd
  inv_hom_id := by
    apply CategoryTheory.Limits.biprod.hom_ext <;>
      simp only [Category.assoc, biprod.inr_snd, Category.comp_id, Category.id_comp, biprod.inr_fst,
        comp_zero]
    apply hY.eq_of_tgt

Isomorphism between an object and its biproduct with a zero object

Informal description

Given objects $X$ and $Y$ in a category $C$ with binary biproducts, if $X$ is a zero object, then $Y$ is isomorphic to the biproduct $X \oplus Y$. The isomorphism consists of: - The inclusion morphism $\text{inr} : Y \to X \oplus Y$ as the forward map - The second projection $\pi_2 : X \oplus Y \to Y$ as the inverse map

CategoryTheory.Limits.biprod_isZero_iff theorem

(A B : C) [HasBinaryBiproduct A B] : IsZero (biprod A B) ↔ IsZero A ∧ IsZero B

Full source

@[simp]
lemma biprod_isZero_iff (A B : C) [HasBinaryBiproduct A B] :
    IsZeroIsZero (biprod A B) ↔ IsZero A ∧ IsZero B := by
  constructor
  · intro h
    simp only [IsZero.iff_id_eq_zero] at h ⊢
    simp only [show 𝟙 A = biprod.inlbiprod.inl ≫ 𝟙 (A ⊞ B) ≫ biprod.fst by simp,
      show 𝟙 B = biprod.inrbiprod.inr ≫ 𝟙 (A ⊞ B) ≫ biprod.snd by simp, h, zero_comp, comp_zero,
      and_self]
  · rintro ⟨hA, hB⟩
    rw [IsZero.iff_id_eq_zero]
    apply biprod.hom_ext
    · apply hA.eq_of_tgt
    · apply hB.eq_of_tgt

Biproduct is Zero if and Only if Both Components Are Zero

Informal description

Let $A$ and $B$ be objects in a category $C$ with binary biproducts. The biproduct $A \oplus B$ is a zero object if and only if both $A$ and $B$ are zero objects.

CategoryTheory.Limits.biprod.braiding definition

(P Q : C) : P ⊞ Q ≅ Q ⊞ P

Full source

/-- The braiding isomorphism which swaps a binary biproduct. -/
@[simps]
def biprod.braiding (P Q : C) : P ⊞ QP ⊞ Q ≅ Q ⊞ P where
  hom := biprod.lift biprod.snd biprod.fst
  inv := biprod.lift biprod.snd biprod.fst

Biproduct braiding isomorphism $P \oplus Q \cong Q \oplus P$

Informal description

The braiding isomorphism $\sigma_{P,Q} \colon P \oplus Q \to Q \oplus P$ between the binary biproducts of objects $P$ and $Q$ in a category $C$ with zero morphisms and binary biproducts. The isomorphism is given by: - The forward map $\sigma_{P,Q}$ is the unique morphism induced by the universal property of $P \oplus Q$ using the second projection $\pi_2 \colon P \oplus Q \to Q$ and first projection $\pi_1 \colon P \oplus Q \to P$. - The inverse map $\sigma_{Q,P}^{-1}$ is similarly defined as the unique morphism induced by the universal property of $Q \oplus P$ using the second projection $\pi_2 \colon Q \oplus P \to P$ and first projection $\pi_1 \colon Q \oplus P \to Q$. This isomorphism swaps the components of the biproduct, satisfying $\sigma_{Q,P} \circ \sigma_{P,Q} = \text{id}_{P \oplus Q}$ and $\sigma_{P,Q} \circ \sigma_{Q,P} = \text{id}_{Q \oplus P}$.

CategoryTheory.Limits.biprod.braiding' definition

(P Q : C) : P ⊞ Q ≅ Q ⊞ P

Full source

/-- An alternative formula for the braiding isomorphism which swaps a binary biproduct,
using the fact that the biproduct is a coproduct. -/
@[simps]
def biprod.braiding' (P Q : C) : P ⊞ QP ⊞ Q ≅ Q ⊞ P where
  hom := biprod.desc biprod.inr biprod.inl
  inv := biprod.desc biprod.inr biprod.inl

Biproduct braiding isomorphism (alternative definition)

Informal description

The isomorphism $\text{biprod.braiding}'$ between the binary biproducts $P \oplus Q$ and $Q \oplus P$ in a category with zero morphisms is defined by the morphisms: - $\text{hom} := \text{biprod.desc}\, \text{biprod.inr}\, \text{biprod.inl}$ (swapping the inclusions) - $\text{inv} := \text{biprod.desc}\, \text{biprod.inr}\, \text{biprod.inl}$ (same as hom, since the operation is self-inverse) This isomorphism swaps the two summands of the biproduct using the universal property of biproducts.

CategoryTheory.Limits.biprod.braiding'_eq_braiding theorem

{P Q : C} : biprod.braiding' P Q = biprod.braiding P Q

Full source

theorem biprod.braiding'_eq_braiding {P Q : C} : biprod.braiding' P Q = biprod.braiding P Q := by
  aesop_cat

Equality of Biproduct Braiding Isomorphisms: $\text{biprod.braiding}' = \text{biprod.braiding}$

Informal description

For any objects $P$ and $Q$ in a category $C$ with zero morphisms and binary biproducts, the two braiding isomorphisms $\text{biprod.braiding}'$ and $\text{biprod.braiding}$ between $P \oplus Q$ and $Q \oplus P$ are equal.

CategoryTheory.Limits.biprod.braid_natural theorem

 {W X Y Z : C} (f : X ⟶ Y) (g : Z ⟶ W) :
  biprod.map f g ≫ (biprod.braiding _ _).hom = (biprod.braiding _ _).hom ≫ biprod.map g f

Full source

/-- The braiding isomorphism can be passed through a map by swapping the order. -/
@[reassoc]
theorem biprod.braid_natural {W X Y Z : C} (f : X ⟶ Y) (g : Z ⟶ W) :
    biprod.mapbiprod.map f g ≫ (biprod.braiding _ _).hom = (biprod.braiding _ _).hom ≫ biprod.map g f := by
  aesop_cat

Naturality of Biproduct Braiding: $(f \oplus g) \circ \sigma = \sigma \circ (g \oplus f)$

Informal description

Let $C$ be a category with binary biproducts, and let $W, X, Y, Z$ be objects in $C$. For any morphisms $f \colon X \to Y$ and $g \colon Z \to W$, the following diagram commutes: \[ (f \oplus g) \circ \sigma_{Y,W} = \sigma_{X,Z} \circ (g \oplus f) \] where $\sigma_{A,B} \colon A \oplus B \to B \oplus A$ denotes the braiding isomorphism between the biproducts of $A$ and $B$, and $f \oplus g \colon X \oplus Z \to Y \oplus W$ is the canonical morphism induced by $f$ and $g$.

CategoryTheory.Limits.biprod.braiding_map_braiding theorem

 {W X Y Z : C} (f : W ⟶ Y) (g : X ⟶ Z) :
  (biprod.braiding X W).hom ≫ biprod.map f g ≫ (biprod.braiding Y Z).hom = biprod.map g f

Full source

@[reassoc]
theorem biprod.braiding_map_braiding {W X Y Z : C} (f : W ⟶ Y) (g : X ⟶ Z) :
    (biprod.braiding X W).hom ≫ biprod.map f g ≫ (biprod.braiding Y Z).hom = biprod.map g f := by
  aesop_cat

Naturality of Biproduct Braiding: $\sigma \circ (f \oplus g) \circ \sigma = g \oplus f$

Informal description

For any objects $W, X, Y, Z$ in a category $C$ with binary biproducts, and morphisms $f: W \to Y$ and $g: X \to Z$, the following diagram commutes: \[ \sigma_{X,W} \circ (f \oplus g) \circ \sigma_{Y,Z} = g \oplus f \] where $\sigma_{A,B}: A \oplus B \to B \oplus A$ denotes the braiding isomorphism that swaps the components of the biproduct, and $f \oplus g: W \oplus X \to Y \oplus Z$ is the canonical morphism between biproducts induced by $f$ and $g$.

CategoryTheory.Limits.biprod.symmetry' theorem

(P Q : C) : biprod.lift biprod.snd biprod.fst ≫ biprod.lift biprod.snd biprod.fst = 𝟙 (P ⊞ Q)

Full source

@[reassoc (attr := simp)]
theorem biprod.symmetry' (P Q : C) :
    biprod.liftbiprod.lift biprod.snd biprod.fst ≫ biprod.lift biprod.snd biprod.fst = 𝟙 (P ⊞ Q) := by
  aesop_cat

Identity via Double Swap of Binary Biproduct Components

Informal description

For any objects $P$ and $Q$ in a category $C$ with binary biproducts, the composition of the morphism $\mathrm{lift}(\pi_2, \pi_1) \colon P \oplus Q \to Q \oplus P$ with itself equals the identity morphism on $P \oplus Q$, i.e., \[ \mathrm{lift}(\pi_2, \pi_1) \circ \mathrm{lift}(\pi_2, \pi_1) = \mathrm{id}_{P \oplus Q} \] where $\pi_1 \colon P \oplus Q \to P$ and $\pi_2 \colon P \oplus Q \to Q$ are the projection morphisms.

CategoryTheory.Limits.biprod.symmetry theorem

(P Q : C) : (biprod.braiding P Q).hom ≫ (biprod.braiding Q P).hom = 𝟙 _

Full source

/-- The braiding isomorphism is symmetric. -/
@[reassoc]
theorem biprod.symmetry (P Q : C) :
    (biprod.braiding P Q).hom ≫ (biprod.braiding Q P).hom = 𝟙 _ := by simp

Braiding isomorphism for binary biproducts is involutive

Informal description

For any objects $P$ and $Q$ in a category $C$ with binary biproducts, the composition of the braiding isomorphism $\sigma_{P,Q} \colon P \oplus Q \to Q \oplus P$ with its inverse $\sigma_{Q,P} \colon Q \oplus P \to P \oplus Q$ equals the identity morphism on $P \oplus Q$, i.e., \[ \sigma_{P,Q} \circ \sigma_{Q,P} = \text{id}_{P \oplus Q}. \]

CategoryTheory.Limits.biprod.associator definition

(P Q R : C) : (P ⊞ Q) ⊞ R ≅ P ⊞ (Q ⊞ R)

Full source

/-- The associator isomorphism which associates a binary biproduct. -/
@[simps]
def biprod.associator (P Q R : C) : (P ⊞ Q) ⊞ R(P ⊞ Q) ⊞ R ≅ P ⊞ (Q ⊞ R) where
  hom := biprod.lift (biprod.fst ≫ biprod.fst) (biprod.lift (biprod.fst ≫ biprod.snd) biprod.snd)
  inv := biprod.lift (biprod.lift biprod.fst (biprod.snd ≫ biprod.fst)) (biprod.snd ≫ biprod.snd)

Associator isomorphism for binary biproducts

Informal description

The associator isomorphism for binary biproducts in a category with zero morphisms is a natural isomorphism between $(P \oplus Q) \oplus R$ and $P \oplus (Q \oplus R)$. Explicitly, it consists of: - A morphism $\text{hom} \colon (P \oplus Q) \oplus R \to P \oplus (Q \oplus R)$ defined by: \[ \text{hom} = \pi_1 \circ \pi_1 + (\pi_2 \circ \pi_1) \oplus \pi_2 \] - An inverse morphism $\text{inv} \colon P \oplus (Q \oplus R) \to (P \oplus Q) \oplus R$ defined by: \[ \text{inv} = (\pi_1 \oplus (\pi_1 \circ \pi_2)) + \pi_2 \circ \pi_2 \] where $\pi_1$ and $\pi_2$ are the projection morphisms from the respective biproducts, and $+$ denotes the universal morphism from the biproduct property.

CategoryTheory.Limits.biprod.associator_natural theorem

 {U V W X Y Z : C} (f : U ⟶ X) (g : V ⟶ Y) (h : W ⟶ Z) :
  biprod.map (biprod.map f g) h ≫ (biprod.associator _ _ _).hom =
    (biprod.associator _ _ _).hom ≫ biprod.map f (biprod.map g h)

Full source

/-- The associator isomorphism can be passed through a map by swapping the order. -/
@[reassoc]
theorem biprod.associator_natural {U V W X Y Z : C} (f : U ⟶ X) (g : V ⟶ Y) (h : W ⟶ Z) :
    biprod.mapbiprod.map (biprod.map f g) h ≫ (biprod.associator _ _ _).hom
      = (biprod.associator _ _ _).hom ≫ biprod.map f (biprod.map g h) := by
  aesop_cat

Naturality of the Biproduct Associator Isomorphism

Informal description

For any objects $U, V, W, X, Y, Z$ in a category $C$ with binary biproducts, and any morphisms $f: U \to X$, $g: V \to Y$, $h: W \to Z$, the following diagram commutes: \[ (f \oplus g) \oplus h \circ \alpha_{X,Y,Z} = \alpha_{U,V,W} \circ f \oplus (g \oplus h) \] where $\alpha_{P,Q,R}: (P \oplus Q) \oplus R \cong P \oplus (Q \oplus R)$ is the associator isomorphism for biproducts, and $\oplus$ denotes the biproduct operation.

CategoryTheory.Limits.biprod.associator_inv_natural theorem

 {U V W X Y Z : C} (f : U ⟶ X) (g : V ⟶ Y) (h : W ⟶ Z) :
  biprod.map f (biprod.map g h) ≫ (biprod.associator _ _ _).inv =
    (biprod.associator _ _ _).inv ≫ biprod.map (biprod.map f g) h

Full source

/-- The associator isomorphism can be passed through a map by swapping the order. -/
@[reassoc]
theorem biprod.associator_inv_natural {U V W X Y Z : C} (f : U ⟶ X) (g : V ⟶ Y) (h : W ⟶ Z) :
    biprod.mapbiprod.map f (biprod.map g h) ≫ (biprod.associator _ _ _).inv
      = (biprod.associator _ _ _).inv ≫ biprod.map (biprod.map f g) h := by
  aesop_cat

Naturality of the Associator Inverse for Binary Biproducts

Informal description

For any objects $U, V, W, X, Y, Z$ in a category $C$ with binary biproducts, and any morphisms $f \colon U \to X$, $g \colon V \to Y$, $h \colon W \to Z$, the following diagram commutes: \[ (f \oplus (g \oplus h)) \circ \alpha^{-1} = \alpha^{-1} \circ ((f \oplus g) \oplus h) \] where $\alpha \colon (P \oplus Q) \oplus R \cong P \oplus (Q \oplus R)$ is the associator isomorphism for binary biproducts, and $\alpha^{-1}$ denotes its inverse.

CategoryTheory.Indecomposable definition

(X : C) : Prop

Full source

/-- An object is indecomposable if it cannot be written as the biproduct of two nonzero objects. -/
def Indecomposable (X : C) : Prop :=
  ¬IsZero X¬IsZero X ∧ ∀ Y Z, (X ≅ Y ⊞ Z) → IsZero Y ∨ IsZero Z

Indecomposable object in a category

Informal description

An object $X$ in a category $\mathcal{C}$ is called *indecomposable* if it is not a zero object and cannot be expressed as the biproduct $Y \oplus Z$ of two objects $Y$ and $Z$ unless at least one of $Y$ or $Z$ is a zero object.

CategoryTheory.isIso_left_of_isIso_biprod_map theorem

{W X Y Z : C} (f : W ⟶ Y) (g : X ⟶ Z) [IsIso (biprod.map f g)] : IsIso f

Full source

/-- If
```
(f 0)
(0 g)
```
is invertible, then `f` is invertible.
-/
theorem isIso_left_of_isIso_biprod_map {W X Y Z : C} (f : W ⟶ Y) (g : X ⟶ Z)
    [IsIso (biprod.map f g)] : IsIso f :=
  ⟨⟨biprod.inl ≫ inv (biprod.map f g) ≫ biprod.fst,
      ⟨by
        have t := congrArg (fun p : W ⊞ X ⟶ W ⊞ X => biprod.inl ≫ p ≫ biprod.fst)
          (IsIso.hom_inv_id (biprod.map f g))
        simp only [Category.id_comp, Category.assoc, biprod.inl_map_assoc] at t
        simp [t], by
        have t := congrArg (fun p : Y ⊞ Z ⟶ Y ⊞ Z => biprod.inl ≫ p ≫ biprod.fst)
          (IsIso.inv_hom_id (biprod.map f g))
        simp only [Category.id_comp, Category.assoc, biprod.map_fst] at t
        simp only [Category.assoc]
        simp [t]⟩⟩⟩

Invertibility of Left Component in Biproduct Map: $f \oplus g$ invertible implies $f$ invertible

Informal description

Let $C$ be a category with binary biproducts, and let $W, X, Y, Z$ be objects in $C$. Given morphisms $f: W \to Y$ and $g: X \to Z$, if the canonical morphism $f \oplus g: W \oplus X \to Y \oplus Z$ is an isomorphism, then $f$ is an isomorphism.

CategoryTheory.isIso_right_of_isIso_biprod_map theorem

{W X Y Z : C} (f : W ⟶ Y) (g : X ⟶ Z) [IsIso (biprod.map f g)] : IsIso g

Full source

/-- If
```
(f 0)
(0 g)
```
is invertible, then `g` is invertible.
-/
theorem isIso_right_of_isIso_biprod_map {W X Y Z : C} (f : W ⟶ Y) (g : X ⟶ Z)
    [IsIso (biprod.map f g)] : IsIso g :=
  letI : IsIso (biprod.map g f) := by
    rw [← biprod.braiding_map_braiding]
    infer_instance
  isIso_left_of_isIso_biprod_map g f

Invertibility of Right Component in Biproduct Map: $f \oplus g$ invertible implies $g$ invertible

Informal description

Let $\mathcal{C}$ be a category with binary biproducts, and let $W, X, Y, Z$ be objects in $\mathcal{C}$. Given morphisms $f \colon W \to Y$ and $g \colon X \to Z$, if the canonical morphism $f \oplus g \colon W \oplus X \to Y \oplus Z$ is an isomorphism, then $g$ is an isomorphism.