Binary (co)products

We define a category WalkingPair, which is the index category for a binary (co)product diagram. A convenience method pair X Y constructs the functor from the walking pair, hitting the given objects.

We define prod X Y and coprod X Y as limits and colimits of such functors.

Typeclasses HasBinaryProducts and HasBinaryCoproducts assert the existence of (co)limits shaped as walking pairs.

We include lemmas for simplifying equations involving projections and coprojections, and define braiding and associating isomorphisms, and the product comparison morphism.

References

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

inductive CategoryTheory.Limits.WalkingPair : Type

The type of objects for the diagram indexing a binary (co)product.

• left : WalkingPair
• right : WalkingPair

instance CategoryTheory.Limits.instDecidableEqWalkingPair : DecidableEq WalkingPair

Equations

• CategoryTheory.Limits.instDecidableEqWalkingPair x✝ y✝ = if h : x✝.toCtorIdx = y✝.toCtorIdx then isTrue ⋯ else isFalse ⋯

instance CategoryTheory.Limits.instInhabitedWalkingPair : Inhabited WalkingPair

Equations

• CategoryTheory.Limits.instInhabitedWalkingPair = { default := CategoryTheory.Limits.WalkingPair.left }

def CategoryTheory.Limits.WalkingPair.swap : WalkingPair ≃ WalkingPair

The equivalence swapping left and right.

Equations

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

@[simp]

theorem CategoryTheory.Limits.WalkingPair.swap_apply_left : swap left = right

@[simp]

theorem CategoryTheory.Limits.WalkingPair.swap_apply_right : swap right = left

@[simp]

theorem CategoryTheory.Limits.WalkingPair.swap_symm_apply_tt : swap.symm left = right

@[simp]

theorem CategoryTheory.Limits.WalkingPair.swap_symm_apply_ff : swap.symm right = left

def CategoryTheory.Limits.WalkingPair.equivBool : WalkingPair ≃ Bool

An equivalence from WalkingPair to Bool, sometimes useful when reindexing limits.

Equations

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

@[simp]

theorem CategoryTheory.Limits.WalkingPair.equivBool_apply_left : equivBool left = true

@[simp]

theorem CategoryTheory.Limits.WalkingPair.equivBool_apply_right : equivBool right = false

@[simp]

theorem CategoryTheory.Limits.WalkingPair.equivBool_symm_apply_true : equivBool.symm true = left

@[simp]

theorem CategoryTheory.Limits.WalkingPair.equivBool_symm_apply_false : equivBool.symm false = right

def CategoryTheory.Limits.pairFunction {C : Type u} (X Y : C) : WalkingPair → C

The function on the walking pair, sending the two points to X and Y.

Equations

• CategoryTheory.Limits.pairFunction X Y j = CategoryTheory.Limits.WalkingPair.casesOn j X Y

@[simp]

theorem CategoryTheory.Limits.pairFunction_left {C : Type u} (X Y : C) : pairFunction X Y WalkingPair.left = X

@[simp]

theorem CategoryTheory.Limits.pairFunction_right {C : Type u} (X Y : C) : pairFunction X Y WalkingPair.right = Y

def CategoryTheory.Limits.pair {C : Type u} [Category.{v, u} C] (X Y : C) : Functor (Discrete WalkingPair) C

The diagram on the walking pair, sending the two points to X and Y.

Equations

• CategoryTheory.Limits.pair X Y = CategoryTheory.Discrete.functor fun (j : CategoryTheory.Limits.WalkingPair) => CategoryTheory.Limits.WalkingPair.casesOn j X Y

@[simp]

theorem CategoryTheory.Limits.pair_obj_left {C : Type u} [Category.{v, u} C] (X Y : C) : (pair X Y).obj { as := WalkingPair.left } = X

@[simp]

theorem CategoryTheory.Limits.pair_obj_right {C : Type u} [Category.{v, u} C] (X Y : C) : (pair X Y).obj { as := WalkingPair.right } = Y

def CategoryTheory.Limits.mapPair {C : Type u} [Category.{v, u} C] {F G : Functor (Discrete WalkingPair) C} (f : F.obj { as := WalkingPair.left } ⟶ G.obj { as := WalkingPair.left }) (g : F.obj { as := WalkingPair.right } ⟶ G.obj { as := WalkingPair.right }) : F ⟶ G

The natural transformation between two functors out of the walking pair, specified by its components.

Equations

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

@[simp]

theorem CategoryTheory.Limits.mapPair_left {C : Type u} [Category.{v, u} C] {F G : Functor (Discrete WalkingPair) C} (f : F.obj { as := WalkingPair.left } ⟶ G.obj { as := WalkingPair.left }) (g : F.obj { as := WalkingPair.right } ⟶ G.obj { as := WalkingPair.right }) : (mapPair f g).app { as := WalkingPair.left } = f

@[simp]

theorem CategoryTheory.Limits.mapPair_right {C : Type u} [Category.{v, u} C] {F G : Functor (Discrete WalkingPair) C} (f : F.obj { as := WalkingPair.left } ⟶ G.obj { as := WalkingPair.left }) (g : F.obj { as := WalkingPair.right } ⟶ G.obj { as := WalkingPair.right }) : (mapPair f g).app { as := WalkingPair.right } = g

def CategoryTheory.Limits.mapPairIso {C : Type u} [Category.{v, u} C] {F G : Functor (Discrete WalkingPair) C} (f : F.obj { as := WalkingPair.left } ≅ G.obj { as := WalkingPair.left }) (g : F.obj { as := WalkingPair.right } ≅ G.obj { as := WalkingPair.right }) : F ≅ G

The natural isomorphism between two functors out of the walking pair, specified by its components.

Equations

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

@[simp]

theorem CategoryTheory.Limits.mapPairIso_inv_app {C : Type u} [Category.{v, u} C] {F G : Functor (Discrete WalkingPair) C} (f : F.obj { as := WalkingPair.left } ≅ G.obj { as := WalkingPair.left }) (g : F.obj { as := WalkingPair.right } ≅ G.obj { as := WalkingPair.right }) (X : Discrete WalkingPair) : (mapPairIso f g).inv.app X = (match X with | { as := WalkingPair.left } => f | { as := WalkingPair.right } => g).inv

@[simp]

theorem CategoryTheory.Limits.mapPairIso_hom_app {C : Type u} [Category.{v, u} C] {F G : Functor (Discrete WalkingPair) C} (f : F.obj { as := WalkingPair.left } ≅ G.obj { as := WalkingPair.left }) (g : F.obj { as := WalkingPair.right } ≅ G.obj { as := WalkingPair.right }) (X : Discrete WalkingPair) : (mapPairIso f g).hom.app X = (match X with | { as := WalkingPair.left } => f | { as := WalkingPair.right } => g).hom

def CategoryTheory.Limits.diagramIsoPair {C : Type u} [Category.{v, u} C] (F : Functor (Discrete WalkingPair) C) : F ≅ pair (F.obj { as := WalkingPair.left }) (F.obj { as := WalkingPair.right })

Every functor out of the walking pair is naturally isomorphic (actually, equal) to a pair

Equations

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

@[simp]

theorem CategoryTheory.Limits.diagramIsoPair_hom_app {C : Type u} [Category.{v, u} C] (F : Functor (Discrete WalkingPair) C) (X : Discrete WalkingPair) : (diagramIsoPair F).hom.app X = (match X with | { as := WalkingPair.left } => Iso.refl (F.obj { as := WalkingPair.left }) | { as := WalkingPair.right } => Iso.refl (F.obj { as := WalkingPair.right })).hom

@[simp]

theorem CategoryTheory.Limits.diagramIsoPair_inv_app {C : Type u} [Category.{v, u} C] (F : Functor (Discrete WalkingPair) C) (X : Discrete WalkingPair) : (diagramIsoPair F).inv.app X = (match X with | { as := WalkingPair.left } => Iso.refl (F.obj { as := WalkingPair.left }) | { as := WalkingPair.right } => Iso.refl (F.obj { as := WalkingPair.right })).inv

def CategoryTheory.Limits.pairComp {C : Type u} [Category.{v, u} C] {D : Type u₁} [Category.{v₁, u₁} D] (X Y : C) (F : Functor C D) : (pair X Y).comp F ≅ pair (F.obj X) (F.obj Y)

The natural isomorphism between pair X Y ⋙ F and pair (F.obj X) (F.obj Y).

Equations

• CategoryTheory.Limits.pairComp X Y F = CategoryTheory.Limits.diagramIsoPair ((CategoryTheory.Limits.pair X Y).comp F)

@[reducible, inline]

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

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

Equations

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

@[reducible, inline]

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

The first projection of a binary fan.

Equations

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

@[reducible, inline]

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

The second projection of a binary fan.

Equations

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

@[simp]

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

@[simp]

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

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

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

Equations

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

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

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

Equations

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

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

@[reducible, inline]

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

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

Equations

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

@[reducible, inline]

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

The first inclusion of a binary cofan.

Equations

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

@[reducible, inline]

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

The second inclusion of a binary cofan.

Equations

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

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

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

Equations

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

@[simp]

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

@[simp]

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

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

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

Equations

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

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

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

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

Equations

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

@[simp]

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

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

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

Equations

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

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

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

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

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

Equations

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

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

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

Equations

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

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

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

Equations

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

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

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

Equations

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

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

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

Equations

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

@[simp]

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

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

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

Equations

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

@[simp]

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

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

Binary products are symmetric.

Equations

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

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

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

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

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

Equations

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

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

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

Equations

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

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

Binary coproducts are symmetric.

Equations

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

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

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

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

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

Equations

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

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

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

Equations

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

@[reducible, inline]

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

An abbreviation for HasLimit (pair X Y).

Equations

• CategoryTheory.Limits.HasBinaryProduct X Y = CategoryTheory.Limits.HasLimit (CategoryTheory.Limits.pair X Y)

@[reducible, inline]

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

An abbreviation for HasColimit (pair X Y).

Equations

• CategoryTheory.Limits.HasBinaryCoproduct X Y = CategoryTheory.Limits.HasColimit (CategoryTheory.Limits.pair X Y)

@[reducible, inline]

noncomputable abbrev CategoryTheory.Limits.prod {C : Type u} [Category.{v, u} C] (X Y : C) [HasBinaryProduct X Y] : C

If we have a product of X and Y, we can access it using prod X Y or X ⨯ Y.

Equations

• (X ⨯ Y) = CategoryTheory.Limits.limit (CategoryTheory.Limits.pair X Y)

@[reducible, inline]

noncomputable abbrev CategoryTheory.Limits.coprod {C : Type u} [Category.{v, u} C] (X Y : C) [HasBinaryCoproduct X Y] : C

If we have a coproduct of X and Y, we can access it using coprod X Y or X ⨿ Y.

Equations

• (X ⨿ Y) = CategoryTheory.Limits.colimit (CategoryTheory.Limits.pair X Y)

def CategoryTheory.Limits.«term_⨯_» : Lean.TrailingParserDescr

Notation for the product

Equations

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

def CategoryTheory.Limits.«term_⨿_» : Lean.TrailingParserDescr

Notation for the coproduct

Equations

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

@[reducible, inline]

noncomputable abbrev CategoryTheory.Limits.prod.fst {C : Type u} [Category.{v, u} C] {X Y : C} [HasBinaryProduct X Y] : X ⨯ Y ⟶ X

The projection map to the first component of the product.

Equations

• CategoryTheory.Limits.prod.fst = CategoryTheory.Limits.limit.π (CategoryTheory.Limits.pair X Y) { as := CategoryTheory.Limits.WalkingPair.left }

@[reducible, inline]

noncomputable abbrev CategoryTheory.Limits.prod.snd {C : Type u} [Category.{v, u} C] {X Y : C} [HasBinaryProduct X Y] : X ⨯ Y ⟶ Y

The projection map to the second component of the product.

Equations

• CategoryTheory.Limits.prod.snd = CategoryTheory.Limits.limit.π (CategoryTheory.Limits.pair X Y) { as := CategoryTheory.Limits.WalkingPair.right }

@[reducible, inline]

noncomputable abbrev CategoryTheory.Limits.coprod.inl {C : Type u} [Category.{v, u} C] {X Y : C} [HasBinaryCoproduct X Y] : X ⟶ X ⨿ Y

The inclusion map from the first component of the coproduct.

Equations

• CategoryTheory.Limits.coprod.inl = CategoryTheory.Limits.colimit.ι (CategoryTheory.Limits.pair X Y) { as := CategoryTheory.Limits.WalkingPair.left }

@[reducible, inline]

noncomputable abbrev CategoryTheory.Limits.coprod.inr {C : Type u} [Category.{v, u} C] {X Y : C} [HasBinaryCoproduct X Y] : Y ⟶ X ⨿ Y

The inclusion map from the second component of the coproduct.

Equations

• CategoryTheory.Limits.coprod.inr = CategoryTheory.Limits.colimit.ι (CategoryTheory.Limits.pair X Y) { as := CategoryTheory.Limits.WalkingPair.right }

noncomputable def CategoryTheory.Limits.prodIsProd {C : Type u} [Category.{v, u} C] (X Y : C) [HasBinaryProduct X Y] : IsLimit (BinaryFan.mk prod.fst prod.snd)

The binary fan constructed from the projection maps is a limit.

Equations

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

noncomputable def CategoryTheory.Limits.coprodIsCoprod {C : Type u} [Category.{v, u} C] (X Y : C) [HasBinaryCoproduct X Y] : IsColimit (BinaryCofan.mk coprod.inl coprod.inr)

The binary cofan constructed from the coprojection maps is a colimit.

Equations

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

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

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

@[reducible, inline]

noncomputable abbrev CategoryTheory.Limits.prod.lift {C : Type u} [Category.{v, u} C] {W X Y : C} [HasBinaryProduct X Y] (f : W ⟶ X) (g : W ⟶ Y) : W ⟶ X ⨯ Y

If the product of X and Y exists, then every pair of morphisms f : W ⟶ X and g : W ⟶ Y induces a morphism prod.lift f g : W ⟶ X ⨯ Y.

Equations

• CategoryTheory.Limits.prod.lift f g = CategoryTheory.Limits.limit.lift (CategoryTheory.Limits.pair X Y) (CategoryTheory.Limits.BinaryFan.mk f g)

@[reducible, inline]

noncomputable abbrev CategoryTheory.Limits.diag {C : Type u} [Category.{v, u} C] (X : C) [HasBinaryProduct X X] : X ⟶ X ⨯ X

diagonal arrow of the binary product in the category fam I

Equations

• CategoryTheory.Limits.diag X = CategoryTheory.Limits.prod.lift (CategoryTheory.CategoryStruct.id X) (CategoryTheory.CategoryStruct.id X)

@[reducible, inline]

noncomputable abbrev CategoryTheory.Limits.coprod.desc {C : Type u} [Category.{v, u} C] {W X Y : C} [HasBinaryCoproduct X Y] (f : X ⟶ W) (g : Y ⟶ W) : X ⨿ Y ⟶ W

If the coproduct of X and Y exists, then every pair of morphisms f : X ⟶ W and g : Y ⟶ W induces a morphism coprod.desc f g : X ⨿ Y ⟶ W.

Equations

• CategoryTheory.Limits.coprod.desc f g = CategoryTheory.Limits.colimit.desc (CategoryTheory.Limits.pair X Y) (CategoryTheory.Limits.BinaryCofan.mk f g)

@[reducible, inline]

noncomputable abbrev CategoryTheory.Limits.codiag {C : Type u} [Category.{v, u} C] (X : C) [HasBinaryCoproduct X X] : X ⨿ X ⟶ X

codiagonal arrow of the binary coproduct

Equations

• CategoryTheory.Limits.codiag X = CategoryTheory.Limits.coprod.desc (CategoryTheory.CategoryStruct.id X) (CategoryTheory.CategoryStruct.id X)

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

theorem CategoryTheory.Limits.prod.lift_fst_assoc {C : Type u} [Category.{v, u} C] {W X Y : C} [HasBinaryProduct X Y] (f : W ⟶ X) (g : W ⟶ Y) {Z : C} (h : X ⟶ Z) : CategoryStruct.comp (lift f g) (CategoryStruct.comp fst h) = CategoryStruct.comp f h

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

theorem CategoryTheory.Limits.prod.lift_snd_assoc {C : Type u} [Category.{v, u} C] {W X Y : C} [HasBinaryProduct X Y] (f : W ⟶ X) (g : W ⟶ Y) {Z : C} (h : Y ⟶ Z) : CategoryStruct.comp (lift f g) (CategoryStruct.comp snd h) = CategoryStruct.comp g h

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

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

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

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

instance CategoryTheory.Limits.prod.mono_lift_of_mono_left {C : Type u} [Category.{v, u} C] {W X Y : C} [HasBinaryProduct X Y] (f : W ⟶ X) (g : W ⟶ Y) [Mono f] : Mono (lift f g)

instance CategoryTheory.Limits.prod.mono_lift_of_mono_right {C : Type u} [Category.{v, u} C] {W X Y : C} [HasBinaryProduct X Y] (f : W ⟶ X) (g : W ⟶ Y) [Mono g] : Mono (lift f g)

instance CategoryTheory.Limits.coprod.epi_desc_of_epi_left {C : Type u} [Category.{v, u} C] {W X Y : C} [HasBinaryCoproduct X Y] (f : X ⟶ W) (g : Y ⟶ W) [Epi f] : Epi (desc f g)

instance CategoryTheory.Limits.coprod.epi_desc_of_epi_right {C : Type u} [Category.{v, u} C] {W X Y : C} [HasBinaryCoproduct X Y] (f : X ⟶ W) (g : Y ⟶ W) [Epi g] : Epi (desc f g)

noncomputable def CategoryTheory.Limits.prod.lift' {C : Type u} [Category.{v, u} C] {W X Y : C} [HasBinaryProduct X Y] (f : W ⟶ X) (g : W ⟶ Y) : { l : W ⟶ X ⨯ Y // CategoryStruct.comp l fst = f ∧ CategoryStruct.comp l snd = g }

If the product of X and Y exists, then every pair of morphisms f : W ⟶ X and g : W ⟶ Y induces a morphism l : W ⟶ X ⨯ Y satisfying l ≫ Prod.fst = f and l ≫ Prod.snd = g.

Equations

• CategoryTheory.Limits.prod.lift' f g = ⟨CategoryTheory.Limits.prod.lift f g, ⋯⟩

noncomputable def CategoryTheory.Limits.coprod.desc' {C : Type u} [Category.{v, u} C] {W X Y : C} [HasBinaryCoproduct X Y] (f : X ⟶ W) (g : Y ⟶ W) : { l : X ⨿ Y ⟶ W // CategoryStruct.comp inl l = f ∧ CategoryStruct.comp inr l = g }

If the coproduct of X and Y exists, then every pair of morphisms f : X ⟶ W and g : Y ⟶ W induces a morphism l : X ⨿ Y ⟶ W satisfying coprod.inl ≫ l = f and coprod.inr ≫ l = g.

Equations

• CategoryTheory.Limits.coprod.desc' f g = ⟨CategoryTheory.Limits.coprod.desc f g, ⋯⟩

noncomputable def CategoryTheory.Limits.prod.map {C : Type u} [Category.{v, u} C] {W X Y Z : C} [HasBinaryProduct W X] [HasBinaryProduct Y Z] (f : W ⟶ Y) (g : X ⟶ Z) : W ⨯ X ⟶ Y ⨯ Z

If the products W ⨯ X and Y ⨯ Z exist, then every pair of morphisms f : W ⟶ Y and g : X ⟶ Z induces a morphism prod.map f g : W ⨯ X ⟶ Y ⨯ Z.

Equations

• CategoryTheory.Limits.prod.map f g = CategoryTheory.Limits.limMap (CategoryTheory.Limits.mapPair f g)

noncomputable def CategoryTheory.Limits.coprod.map {C : Type u} [Category.{v, u} C] {W X Y Z : C} [HasBinaryCoproduct W X] [HasBinaryCoproduct Y Z] (f : W ⟶ Y) (g : X ⟶ Z) : W ⨿ X ⟶ Y ⨿ Z

If the coproducts W ⨿ X and Y ⨿ Z exist, then every pair of morphisms f : W ⟶ Y and g : W ⟶ Z induces a morphism coprod.map f g : W ⨿ X ⟶ Y ⨿ Z.

Equations

• CategoryTheory.Limits.coprod.map f g = CategoryTheory.Limits.colimMap (CategoryTheory.Limits.mapPair f g)

@[simp]

theorem CategoryTheory.Limits.prod.comp_lift {C : Type u} [Category.{v, u} C] {V W X Y : C} [HasBinaryProduct X Y] (f : V ⟶ W) (g : W ⟶ X) (h : W ⟶ Y) : CategoryStruct.comp f (lift g h) = lift (CategoryStruct.comp f g) (CategoryStruct.comp f h)

theorem CategoryTheory.Limits.prod.comp_lift_assoc {C : Type u} [Category.{v, u} C] {V W X Y : C} [HasBinaryProduct X Y] (f : V ⟶ W) (g : W ⟶ X) (h : W ⟶ Y) {Z : C} (h✝ : X ⨯ Y ⟶ Z) : CategoryStruct.comp f (CategoryStruct.comp (lift g h) h✝) = CategoryStruct.comp (lift (CategoryStruct.comp f g) (CategoryStruct.comp f h)) h✝

theorem CategoryTheory.Limits.prod.comp_diag {C : Type u} [Category.{v, u} C] {X Y : C} [HasBinaryProduct Y Y] (f : X ⟶ Y) : CategoryStruct.comp f (diag Y) = lift f f

@[simp]

theorem CategoryTheory.Limits.prod.map_fst {C : Type u} [Category.{v, u} C] {W X Y Z : C} [HasBinaryProduct W X] [HasBinaryProduct Y Z] (f : W ⟶ Y) (g : X ⟶ Z) : CategoryStruct.comp (map f g) fst = CategoryStruct.comp fst f

@[simp]

theorem CategoryTheory.Limits.prod.map_fst_assoc {C : Type u} [Category.{v, u} C] {W X Y Z : C} [HasBinaryProduct W X] [HasBinaryProduct Y Z] (f : W ⟶ Y) (g : X ⟶ Z) {Z✝ : C} (h : Y ⟶ Z✝) : CategoryStruct.comp (map f g) (CategoryStruct.comp fst h) = CategoryStruct.comp fst (CategoryStruct.comp f h)

@[simp]

theorem CategoryTheory.Limits.prod.map_snd {C : Type u} [Category.{v, u} C] {W X Y Z : C} [HasBinaryProduct W X] [HasBinaryProduct Y Z] (f : W ⟶ Y) (g : X ⟶ Z) : CategoryStruct.comp (map f g) snd = CategoryStruct.comp snd g

@[simp]

theorem CategoryTheory.Limits.prod.map_snd_assoc {C : Type u} [Category.{v, u} C] {W X Y Z : C} [HasBinaryProduct W X] [HasBinaryProduct Y Z] (f : W ⟶ Y) (g : X ⟶ Z) {Z✝ : C} (h : Z ⟶ Z✝) : CategoryStruct.comp (map f g) (CategoryStruct.comp snd h) = CategoryStruct.comp snd (CategoryStruct.comp g h)

@[simp]

theorem CategoryTheory.Limits.prod.map_id_id {C : Type u} [Category.{v, u} C] {X Y : C} [HasBinaryProduct X Y] : map (CategoryStruct.id X) (CategoryStruct.id Y) = CategoryStruct.id (X ⨯ Y)

@[simp]

theorem CategoryTheory.Limits.prod.lift_fst_snd {C : Type u} [Category.{v, u} C] {X Y : C} [HasBinaryProduct X Y] : lift fst snd = CategoryStruct.id (X ⨯ Y)

@[simp]

theorem CategoryTheory.Limits.prod.lift_map {C : Type u} [Category.{v, u} C] {V W X Y Z : C} [HasBinaryProduct W X] [HasBinaryProduct Y Z] (f : V ⟶ W) (g : V ⟶ X) (h : W ⟶ Y) (k : X ⟶ Z) : CategoryStruct.comp (lift f g) (map h k) = lift (CategoryStruct.comp f h) (CategoryStruct.comp g k)

@[simp]

theorem CategoryTheory.Limits.prod.lift_map_assoc {C : Type u} [Category.{v, u} C] {V W X Y Z : C} [HasBinaryProduct W X] [HasBinaryProduct Y Z] (f : V ⟶ W) (g : V ⟶ X) (h : W ⟶ Y) (k : X ⟶ Z) {Z✝ : C} (h✝ : Y ⨯ Z ⟶ Z✝) : CategoryStruct.comp (lift f g) (CategoryStruct.comp (map h k) h✝) = CategoryStruct.comp (lift (CategoryStruct.comp f h) (CategoryStruct.comp g k)) h✝

@[simp]

theorem CategoryTheory.Limits.prod.lift_fst_comp_snd_comp {C : Type u} [Category.{v, u} C] {W X Y Z : C} [HasBinaryProduct W Y] [HasBinaryProduct X Z] (g : W ⟶ X) (g' : Y ⟶ Z) : lift (CategoryStruct.comp fst g) (CategoryStruct.comp snd g') = map g g'

@[simp]

theorem CategoryTheory.Limits.prod.map_map {C : Type u} [Category.{v, u} C] {A₁ A₂ A₃ B₁ B₂ B₃ : C} [HasBinaryProduct A₁ B₁] [HasBinaryProduct A₂ B₂] [HasBinaryProduct A₃ B₃] (f : A₁ ⟶ A₂) (g : B₁ ⟶ B₂) (h : A₂ ⟶ A₃) (k : B₂ ⟶ B₃) : CategoryStruct.comp (map f g) (map h k) = map (CategoryStruct.comp f h) (CategoryStruct.comp g k)

@[simp]

theorem CategoryTheory.Limits.prod.map_map_assoc {C : Type u} [Category.{v, u} C] {A₁ A₂ A₃ B₁ B₂ B₃ : C} [HasBinaryProduct A₁ B₁] [HasBinaryProduct A₂ B₂] [HasBinaryProduct A₃ B₃] (f : A₁ ⟶ A₂) (g : B₁ ⟶ B₂) (h : A₂ ⟶ A₃) (k : B₂ ⟶ B₃) {Z : C} (h✝ : A₃ ⨯ B₃ ⟶ Z) : CategoryStruct.comp (map f g) (CategoryStruct.comp (map h k) h✝) = CategoryStruct.comp (map (CategoryStruct.comp f h) (CategoryStruct.comp g k)) h✝

theorem CategoryTheory.Limits.prod.map_swap {C : Type u} [Category.{v, u} C] {A B X Y : C} (f : A ⟶ B) (g : X ⟶ Y) [HasLimitsOfShape (Discrete WalkingPair) C] : CategoryStruct.comp (map (CategoryStruct.id X) f) (map g (CategoryStruct.id B)) = CategoryStruct.comp (map g (CategoryStruct.id A)) (map (CategoryStruct.id Y) f)

theorem CategoryTheory.Limits.prod.map_swap_assoc {C : Type u} [Category.{v, u} C] {A B X Y : C} (f : A ⟶ B) (g : X ⟶ Y) [HasLimitsOfShape (Discrete WalkingPair) C] {Z : C} (h : Y ⨯ B ⟶ Z) : CategoryStruct.comp (map (CategoryStruct.id X) f) (CategoryStruct.comp (map g (CategoryStruct.id B)) h) = CategoryStruct.comp (map g (CategoryStruct.id A)) (CategoryStruct.comp (map (CategoryStruct.id Y) f) h)

theorem CategoryTheory.Limits.prod.map_comp_id {C : Type u} [Category.{v, u} C] {X Y Z W : C} (f : X ⟶ Y) (g : Y ⟶ Z) [HasBinaryProduct X W] [HasBinaryProduct Z W] [HasBinaryProduct Y W] : map (CategoryStruct.comp f g) (CategoryStruct.id W) = CategoryStruct.comp (map f (CategoryStruct.id W)) (map g (CategoryStruct.id W))

theorem CategoryTheory.Limits.prod.map_comp_id_assoc {C : Type u} [Category.{v, u} C] {X Y Z W : C} (f : X ⟶ Y) (g : Y ⟶ Z) [HasBinaryProduct X W] [HasBinaryProduct Z W] [HasBinaryProduct Y W] {Z✝ : C} (h : Z ⨯ W ⟶ Z✝) : CategoryStruct.comp (map (CategoryStruct.comp f g) (CategoryStruct.id W)) h = CategoryStruct.comp (map f (CategoryStruct.id W)) (CategoryStruct.comp (map g (CategoryStruct.id W)) h)

theorem CategoryTheory.Limits.prod.map_id_comp {C : Type u} [Category.{v, u} C] {X Y Z W : C} (f : X ⟶ Y) (g : Y ⟶ Z) [HasBinaryProduct W X] [HasBinaryProduct W Y] [HasBinaryProduct W Z] : map (CategoryStruct.id W) (CategoryStruct.comp f g) = CategoryStruct.comp (map (CategoryStruct.id W) f) (map (CategoryStruct.id W) g)

theorem CategoryTheory.Limits.prod.map_id_comp_assoc {C : Type u} [Category.{v, u} C] {X Y Z W : C} (f : X ⟶ Y) (g : Y ⟶ Z) [HasBinaryProduct W X] [HasBinaryProduct W Y] [HasBinaryProduct W Z] {Z✝ : C} (h : W ⨯ Z ⟶ Z✝) : CategoryStruct.comp (map (CategoryStruct.id W) (CategoryStruct.comp f g)) h = CategoryStruct.comp (map (CategoryStruct.id W) f) (CategoryStruct.comp (map (CategoryStruct.id W) g) h)

def CategoryTheory.Limits.prod.mapIso {C : Type u} [Category.{v, u} C] {W X Y Z : C} [HasBinaryProduct W X] [HasBinaryProduct Y Z] (f : W ≅ Y) (g : X ≅ Z) : W ⨯ X ≅ Y ⨯ Z

If the products W ⨯ X and Y ⨯ Z exist, then every pair of isomorphisms f : W ≅ Y and g : X ≅ Z induces an isomorphism prod.mapIso f g : W ⨯ X ≅ Y ⨯ Z.

Equations

• CategoryTheory.Limits.prod.mapIso f g = { hom := CategoryTheory.Limits.prod.map f.hom g.hom, inv := CategoryTheory.Limits.prod.map f.inv g.inv, hom_inv_id := ⋯, inv_hom_id := ⋯ }

@[simp]

theorem CategoryTheory.Limits.prod.mapIso_inv {C : Type u} [Category.{v, u} C] {W X Y Z : C} [HasBinaryProduct W X] [HasBinaryProduct Y Z] (f : W ≅ Y) (g : X ≅ Z) : (mapIso f g).inv = map f.inv g.inv

@[simp]

theorem CategoryTheory.Limits.prod.mapIso_hom {C : Type u} [Category.{v, u} C] {W X Y Z : C} [HasBinaryProduct W X] [HasBinaryProduct Y Z] (f : W ≅ Y) (g : X ≅ Z) : (mapIso f g).hom = map f.hom g.hom

instance CategoryTheory.Limits.isIso_prod {C : Type u} [Category.{v, u} C] {W X Y Z : C} [HasBinaryProduct W X] [HasBinaryProduct Y Z] (f : W ⟶ Y) (g : X ⟶ Z) [IsIso f] [IsIso g] : IsIso (prod.map f g)

instance CategoryTheory.Limits.prod.map_mono {C : Type u_1} [Category.{u_2, u_1} C] {W X Y Z : C} (f : W ⟶ Y) (g : X ⟶ Z) [Mono f] [Mono g] [HasBinaryProduct W X] [HasBinaryProduct Y Z] : Mono (map f g)

theorem CategoryTheory.Limits.prod.diag_map {C : Type u} [Category.{v, u} C] {X Y : C} (f : X ⟶ Y) [HasBinaryProduct X X] [HasBinaryProduct Y Y] : CategoryStruct.comp (diag X) (map f f) = CategoryStruct.comp f (diag Y)

theorem CategoryTheory.Limits.prod.diag_map_assoc {C : Type u} [Category.{v, u} C] {X Y : C} (f : X ⟶ Y) [HasBinaryProduct X X] [HasBinaryProduct Y Y] {Z : C} (h : Y ⨯ Y ⟶ Z) : CategoryStruct.comp (diag X) (CategoryStruct.comp (map f f) h) = CategoryStruct.comp f (CategoryStruct.comp (diag Y) h)

theorem CategoryTheory.Limits.prod.diag_map_fst_snd {C : Type u} [Category.{v, u} C] {X Y : C} [HasBinaryProduct X Y] [HasBinaryProduct (X ⨯ Y) (X ⨯ Y)] : CategoryStruct.comp (diag (X ⨯ Y)) (map fst snd) = CategoryStruct.id (X ⨯ Y)

theorem CategoryTheory.Limits.prod.diag_map_fst_snd_assoc {C : Type u} [Category.{v, u} C] {X Y : C} [HasBinaryProduct X Y] [HasBinaryProduct (X ⨯ Y) (X ⨯ Y)] {Z : C} (h : X ⨯ Y ⟶ Z) : CategoryStruct.comp (diag (X ⨯ Y)) (CategoryStruct.comp (map fst snd) h) = h

theorem CategoryTheory.Limits.prod.diag_map_fst_snd_comp {C : Type u} [Category.{v, u} C] [HasLimitsOfShape (Discrete WalkingPair) C] {X X' Y Y' : C} (g : X ⟶ Y) (g' : X' ⟶ Y') : CategoryStruct.comp (diag (X ⨯ X')) (map (CategoryStruct.comp fst g) (CategoryStruct.comp snd g')) = map g g'

theorem CategoryTheory.Limits.prod.diag_map_fst_snd_comp_assoc {C : Type u} [Category.{v, u} C] [HasLimitsOfShape (Discrete WalkingPair) C] {X X' Y Y' : C} (g : X ⟶ Y) (g' : X' ⟶ Y') {Z : C} (h : Y ⨯ Y' ⟶ Z) : CategoryStruct.comp (diag (X ⨯ X')) (CategoryStruct.comp (map (CategoryStruct.comp fst g) (CategoryStruct.comp snd g')) h) = CategoryStruct.comp (map g g') h

instance CategoryTheory.Limits.instIsSplitMonoDiag {C : Type u} [Category.{v, u} C] {X : C} [HasBinaryProduct X X] : IsSplitMono (diag X)

@[simp]

theorem CategoryTheory.Limits.coprod.desc_comp {C : Type u} [Category.{v, u} C] {V W X Y : C} [HasBinaryCoproduct X Y] (f : V ⟶ W) (g : X ⟶ V) (h : Y ⟶ V) : CategoryStruct.comp (desc g h) f = desc (CategoryStruct.comp g f) (CategoryStruct.comp h f)

theorem CategoryTheory.Limits.coprod.desc_comp_assoc {C : Type u} [Category.{v, u} C] {V W X Y : C} [HasBinaryCoproduct X Y] (f : V ⟶ W) (g : X ⟶ V) (h : Y ⟶ V) {Z : C} (h✝ : W ⟶ Z) : CategoryStruct.comp (desc g h) (CategoryStruct.comp f h✝) = CategoryStruct.comp (desc (CategoryStruct.comp g f) (CategoryStruct.comp h f)) h✝

theorem CategoryTheory.Limits.coprod.diag_comp {C : Type u} [Category.{v, u} C] {X Y : C} [HasBinaryCoproduct X X] (f : X ⟶ Y) : CategoryStruct.comp (codiag X) f = desc f f

@[simp]

theorem CategoryTheory.Limits.coprod.inl_map {C : Type u} [Category.{v, u} C] {W X Y Z : C} [HasBinaryCoproduct W X] [HasBinaryCoproduct Y Z] (f : W ⟶ Y) (g : X ⟶ Z) : CategoryStruct.comp inl (map f g) = CategoryStruct.comp f inl

@[simp]

theorem CategoryTheory.Limits.coprod.inl_map_assoc {C : Type u} [Category.{v, u} C] {W X Y Z : C} [HasBinaryCoproduct W X] [HasBinaryCoproduct Y Z] (f : W ⟶ Y) (g : X ⟶ Z) {Z✝ : C} (h : Y ⨿ Z ⟶ Z✝) : CategoryStruct.comp inl (CategoryStruct.comp (map f g) h) = CategoryStruct.comp f (CategoryStruct.comp inl h)

@[simp]

theorem CategoryTheory.Limits.coprod.inr_map {C : Type u} [Category.{v, u} C] {W X Y Z : C} [HasBinaryCoproduct W X] [HasBinaryCoproduct Y Z] (f : W ⟶ Y) (g : X ⟶ Z) : CategoryStruct.comp inr (map f g) = CategoryStruct.comp g inr

@[simp]

theorem CategoryTheory.Limits.coprod.inr_map_assoc {C : Type u} [Category.{v, u} C] {W X Y Z : C} [HasBinaryCoproduct W X] [HasBinaryCoproduct Y Z] (f : W ⟶ Y) (g : X ⟶ Z) {Z✝ : C} (h : Y ⨿ Z ⟶ Z✝) : CategoryStruct.comp inr (CategoryStruct.comp (map f g) h) = CategoryStruct.comp g (CategoryStruct.comp inr h)

@[simp]

theorem CategoryTheory.Limits.coprod.map_id_id {C : Type u} [Category.{v, u} C] {X Y : C} [HasBinaryCoproduct X Y] : map (CategoryStruct.id X) (CategoryStruct.id Y) = CategoryStruct.id (X ⨿ Y)

@[simp]

theorem CategoryTheory.Limits.coprod.desc_inl_inr {C : Type u} [Category.{v, u} C] {X Y : C} [HasBinaryCoproduct X Y] : desc inl inr = CategoryStruct.id (X ⨿ Y)

@[simp]

theorem CategoryTheory.Limits.coprod.map_desc {C : Type u} [Category.{v, u} C] {S T U V W : C} [HasBinaryCoproduct U W] [HasBinaryCoproduct T V] (f : U ⟶ S) (g : W ⟶ S) (h : T ⟶ U) (k : V ⟶ W) : CategoryStruct.comp (map h k) (desc f g) = desc (CategoryStruct.comp h f) (CategoryStruct.comp k g)

theorem CategoryTheory.Limits.coprod.map_desc_assoc {C : Type u} [Category.{v, u} C] {S T U V W : C} [HasBinaryCoproduct U W] [HasBinaryCoproduct T V] (f : U ⟶ S) (g : W ⟶ S) (h : T ⟶ U) (k : V ⟶ W) {Z : C} (h✝ : S ⟶ Z) : CategoryStruct.comp (map h k) (CategoryStruct.comp (desc f g) h✝) = CategoryStruct.comp (desc (CategoryStruct.comp h f) (CategoryStruct.comp k g)) h✝

@[simp]

theorem CategoryTheory.Limits.coprod.desc_comp_inl_comp_inr {C : Type u} [Category.{v, u} C] {W X Y Z : C} [HasBinaryCoproduct W Y] [HasBinaryCoproduct X Z] (g : W ⟶ X) (g' : Y ⟶ Z) : desc (CategoryStruct.comp g inl) (CategoryStruct.comp g' inr) = map g g'

@[simp]

theorem CategoryTheory.Limits.coprod.map_map {C : Type u} [Category.{v, u} C] {A₁ A₂ A₃ B₁ B₂ B₃ : C} [HasBinaryCoproduct A₁ B₁] [HasBinaryCoproduct A₂ B₂] [HasBinaryCoproduct A₃ B₃] (f : A₁ ⟶ A₂) (g : B₁ ⟶ B₂) (h : A₂ ⟶ A₃) (k : B₂ ⟶ B₃) : CategoryStruct.comp (map f g) (map h k) = map (CategoryStruct.comp f h) (CategoryStruct.comp g k)

@[simp]

theorem CategoryTheory.Limits.coprod.map_map_assoc {C : Type u} [Category.{v, u} C] {A₁ A₂ A₃ B₁ B₂ B₃ : C} [HasBinaryCoproduct A₁ B₁] [HasBinaryCoproduct A₂ B₂] [HasBinaryCoproduct A₃ B₃] (f : A₁ ⟶ A₂) (g : B₁ ⟶ B₂) (h : A₂ ⟶ A₃) (k : B₂ ⟶ B₃) {Z : C} (h✝ : A₃ ⨿ B₃ ⟶ Z) : CategoryStruct.comp (map f g) (CategoryStruct.comp (map h k) h✝) = CategoryStruct.comp (map (CategoryStruct.comp f h) (CategoryStruct.comp g k)) h✝

theorem CategoryTheory.Limits.coprod.map_swap {C : Type u} [Category.{v, u} C] {A B X Y : C} (f : A ⟶ B) (g : X ⟶ Y) [HasColimitsOfShape (Discrete WalkingPair) C] : CategoryStruct.comp (map (CategoryStruct.id X) f) (map g (CategoryStruct.id B)) = CategoryStruct.comp (map g (CategoryStruct.id A)) (map (CategoryStruct.id Y) f)

theorem CategoryTheory.Limits.coprod.map_swap_assoc {C : Type u} [Category.{v, u} C] {A B X Y : C} (f : A ⟶ B) (g : X ⟶ Y) [HasColimitsOfShape (Discrete WalkingPair) C] {Z : C} (h : Y ⨿ B ⟶ Z) : CategoryStruct.comp (map (CategoryStruct.id X) f) (CategoryStruct.comp (map g (CategoryStruct.id B)) h) = CategoryStruct.comp (map g (CategoryStruct.id A)) (CategoryStruct.comp (map (CategoryStruct.id Y) f) h)

theorem CategoryTheory.Limits.coprod.map_comp_id {C : Type u} [Category.{v, u} C] {X Y Z W : C} (f : X ⟶ Y) (g : Y ⟶ Z) [HasBinaryCoproduct Z W] [HasBinaryCoproduct Y W] [HasBinaryCoproduct X W] : map (CategoryStruct.comp f g) (CategoryStruct.id W) = CategoryStruct.comp (map f (CategoryStruct.id W)) (map g (CategoryStruct.id W))

theorem CategoryTheory.Limits.coprod.map_comp_id_assoc {C : Type u} [Category.{v, u} C] {X Y Z W : C} (f : X ⟶ Y) (g : Y ⟶ Z) [HasBinaryCoproduct Z W] [HasBinaryCoproduct Y W] [HasBinaryCoproduct X W] {Z✝ : C} (h : Z ⨿ W ⟶ Z✝) : CategoryStruct.comp (map (CategoryStruct.comp f g) (CategoryStruct.id W)) h = CategoryStruct.comp (map f (CategoryStruct.id W)) (CategoryStruct.comp (map g (CategoryStruct.id W)) h)

theorem CategoryTheory.Limits.coprod.map_id_comp {C : Type u} [Category.{v, u} C] {X Y Z W : C} (f : X ⟶ Y) (g : Y ⟶ Z) [HasBinaryCoproduct W X] [HasBinaryCoproduct W Y] [HasBinaryCoproduct W Z] : map (CategoryStruct.id W) (CategoryStruct.comp f g) = CategoryStruct.comp (map (CategoryStruct.id W) f) (map (CategoryStruct.id W) g)

theorem CategoryTheory.Limits.coprod.map_id_comp_assoc {C : Type u} [Category.{v, u} C] {X Y Z W : C} (f : X ⟶ Y) (g : Y ⟶ Z) [HasBinaryCoproduct W X] [HasBinaryCoproduct W Y] [HasBinaryCoproduct W Z] {Z✝ : C} (h : W ⨿ Z ⟶ Z✝) : CategoryStruct.comp (map (CategoryStruct.id W) (CategoryStruct.comp f g)) h = CategoryStruct.comp (map (CategoryStruct.id W) f) (CategoryStruct.comp (map (CategoryStruct.id W) g) h)

def CategoryTheory.Limits.coprod.mapIso {C : Type u} [Category.{v, u} C] {W X Y Z : C} [HasBinaryCoproduct W X] [HasBinaryCoproduct Y Z] (f : W ≅ Y) (g : X ≅ Z) : W ⨿ X ≅ Y ⨿ Z

If the coproducts W ⨿ X and Y ⨿ Z exist, then every pair of isomorphisms f : W ≅ Y and g : W ≅ Z induces an isomorphism coprod.mapIso f g : W ⨿ X ≅ Y ⨿ Z.

Equations

• CategoryTheory.Limits.coprod.mapIso f g = { hom := CategoryTheory.Limits.coprod.map f.hom g.hom, inv := CategoryTheory.Limits.coprod.map f.inv g.inv, hom_inv_id := ⋯, inv_hom_id := ⋯ }

@[simp]

theorem CategoryTheory.Limits.coprod.mapIso_inv {C : Type u} [Category.{v, u} C] {W X Y Z : C} [HasBinaryCoproduct W X] [HasBinaryCoproduct Y Z] (f : W ≅ Y) (g : X ≅ Z) : (mapIso f g).inv = map f.inv g.inv

@[simp]

theorem CategoryTheory.Limits.coprod.mapIso_hom {C : Type u} [Category.{v, u} C] {W X Y Z : C} [HasBinaryCoproduct W X] [HasBinaryCoproduct Y Z] (f : W ≅ Y) (g : X ≅ Z) : (mapIso f g).hom = map f.hom g.hom

instance CategoryTheory.Limits.isIso_coprod {C : Type u} [Category.{v, u} C] {W X Y Z : C} [HasBinaryCoproduct W X] [HasBinaryCoproduct Y Z] (f : W ⟶ Y) (g : X ⟶ Z) [IsIso f] [IsIso g] : IsIso (coprod.map f g)

instance CategoryTheory.Limits.coprod.map_epi {C : Type u_1} [Category.{u_2, u_1} C] {W X Y Z : C} (f : W ⟶ Y) (g : X ⟶ Z) [Epi f] [Epi g] [HasBinaryCoproduct W X] [HasBinaryCoproduct Y Z] : Epi (map f g)

theorem CategoryTheory.Limits.coprod.map_codiag {C : Type u} [Category.{v, u} C] {X Y : C} (f : X ⟶ Y) [HasBinaryCoproduct X X] [HasBinaryCoproduct Y Y] : CategoryStruct.comp (map f f) (codiag Y) = CategoryStruct.comp (codiag X) f

theorem CategoryTheory.Limits.coprod.map_codiag_assoc {C : Type u} [Category.{v, u} C] {X Y : C} (f : X ⟶ Y) [HasBinaryCoproduct X X] [HasBinaryCoproduct Y Y] {Z : C} (h : Y ⟶ Z) : CategoryStruct.comp (map f f) (CategoryStruct.comp (codiag Y) h) = CategoryStruct.comp (codiag X) (CategoryStruct.comp f h)

theorem CategoryTheory.Limits.coprod.map_inl_inr_codiag {C : Type u} [Category.{v, u} C] {X Y : C} [HasBinaryCoproduct X Y] [HasBinaryCoproduct (X ⨿ Y) (X ⨿ Y)] : CategoryStruct.comp (map inl inr) (codiag (X ⨿ Y)) = CategoryStruct.id (X ⨿ Y)

theorem CategoryTheory.Limits.coprod.map_inl_inr_codiag_assoc {C : Type u} [Category.{v, u} C] {X Y : C} [HasBinaryCoproduct X Y] [HasBinaryCoproduct (X ⨿ Y) (X ⨿ Y)] {Z : C} (h : X ⨿ Y ⟶ Z) : CategoryStruct.comp (map inl inr) (CategoryStruct.comp (codiag (X ⨿ Y)) h) = h

theorem CategoryTheory.Limits.coprod.map_comp_inl_inr_codiag {C : Type u} [Category.{v, u} C] [HasColimitsOfShape (Discrete WalkingPair) C] {X X' Y Y' : C} (g : X ⟶ Y) (g' : X' ⟶ Y') : CategoryStruct.comp (map (CategoryStruct.comp g inl) (CategoryStruct.comp g' inr)) (codiag (Y ⨿ Y')) = map g g'

theorem CategoryTheory.Limits.coprod.map_comp_inl_inr_codiag_assoc {C : Type u} [Category.{v, u} C] [HasColimitsOfShape (Discrete WalkingPair) C] {X X' Y Y' : C} (g : X ⟶ Y) (g' : X' ⟶ Y') {Z : C} (h : Y ⨿ Y' ⟶ Z) : CategoryStruct.comp (map (CategoryStruct.comp g inl) (CategoryStruct.comp g' inr)) (CategoryStruct.comp (codiag (Y ⨿ Y')) h) = CategoryStruct.comp (map g g') h

@[reducible, inline]

abbrev CategoryTheory.Limits.HasBinaryProducts (C : Type u) [Category.{v, u} C] : Prop

HasBinaryProducts represents a choice of product for every pair of objects.

Stacks Tag 001T

Equations

• CategoryTheory.Limits.HasBinaryProducts C = CategoryTheory.Limits.HasLimitsOfShape (CategoryTheory.Discrete CategoryTheory.Limits.WalkingPair) C

@[reducible, inline]

abbrev CategoryTheory.Limits.HasBinaryCoproducts (C : Type u) [Category.{v, u} C] : Prop

HasBinaryCoproducts represents a choice of coproduct for every pair of objects.

Stacks Tag 04AP

Equations

• CategoryTheory.Limits.HasBinaryCoproducts C = CategoryTheory.Limits.HasColimitsOfShape (CategoryTheory.Discrete CategoryTheory.Limits.WalkingPair) C

theorem CategoryTheory.Limits.hasBinaryProducts_of_hasLimit_pair (C : Type u) [Category.{v, u} C] [∀ {X Y : C}, HasLimit (pair X Y)] : HasBinaryProducts C

If C has all limits of diagrams pair X Y, then it has all binary products

theorem CategoryTheory.Limits.hasBinaryCoproducts_of_hasColimit_pair (C : Type u) [Category.{v, u} C] [∀ {X Y : C}, HasColimit (pair X Y)] : HasBinaryCoproducts C

If C has all colimits of diagrams pair X Y, then it has all binary coproducts

def CategoryTheory.Limits.prod.braiding {C : Type u} [Category.{v, u} C] (P Q : C) [HasBinaryProduct P Q] [HasBinaryProduct Q P] : P ⨯ Q ≅ Q ⨯ P

The braiding isomorphism which swaps a binary product.

Equations

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

@[simp]

theorem CategoryTheory.Limits.prod.braiding_hom {C : Type u} [Category.{v, u} C] (P Q : C) [HasBinaryProduct P Q] [HasBinaryProduct Q P] : (braiding P Q).hom = lift snd fst

@[simp]

theorem CategoryTheory.Limits.prod.braiding_inv {C : Type u} [Category.{v, u} C] (P Q : C) [HasBinaryProduct P Q] [HasBinaryProduct Q P] : (braiding P Q).inv = lift snd fst

theorem CategoryTheory.Limits.braid_natural {C : Type u} [Category.{v, u} C] [HasBinaryProducts C] {W X Y Z : C} (f : X ⟶ Y) (g : Z ⟶ W) : CategoryStruct.comp (prod.map f g) (prod.braiding Y W).hom = CategoryStruct.comp (prod.braiding X Z).hom (prod.map g f)

The braiding isomorphism can be passed through a map by swapping the order.

theorem CategoryTheory.Limits.braid_natural_assoc {C : Type u} [Category.{v, u} C] [HasBinaryProducts C] {W X Y Z : C} (f : X ⟶ Y) (g : Z ⟶ W) {Z✝ : C} (h : W ⨯ Y ⟶ Z✝) : CategoryStruct.comp (prod.map f g) (CategoryStruct.comp (prod.braiding Y W).hom h) = CategoryStruct.comp (prod.braiding X Z).hom (CategoryStruct.comp (prod.map g f) h)

theorem CategoryTheory.Limits.prod.symmetry' {C : Type u} [Category.{v, u} C] (P Q : C) [HasBinaryProduct P Q] [HasBinaryProduct Q P] : CategoryStruct.comp (lift snd fst) (lift snd fst) = CategoryStruct.id (P ⨯ Q)

theorem CategoryTheory.Limits.prod.symmetry'_assoc {C : Type u} [Category.{v, u} C] (P Q : C) [HasBinaryProduct P Q] [HasBinaryProduct Q P] {Z : C} (h : P ⨯ Q ⟶ Z) : CategoryStruct.comp (lift snd fst) (CategoryStruct.comp (lift snd fst) h) = h

theorem CategoryTheory.Limits.prod.symmetry {C : Type u} [Category.{v, u} C] (P Q : C) [HasBinaryProduct P Q] [HasBinaryProduct Q P] : CategoryStruct.comp (braiding P Q).hom (braiding Q P).hom = CategoryStruct.id (P ⨯ Q)

The braiding isomorphism is symmetric.

theorem CategoryTheory.Limits.prod.symmetry_assoc {C : Type u} [Category.{v, u} C] (P Q : C) [HasBinaryProduct P Q] [HasBinaryProduct Q P] {Z : C} (h : P ⨯ Q ⟶ Z) : CategoryStruct.comp (braiding P Q).hom (CategoryStruct.comp (braiding Q P).hom h) = h

def CategoryTheory.Limits.prod.associator {C : Type u} [Category.{v, u} C] [HasBinaryProducts C] (P Q R : C) : (P ⨯ Q) ⨯ R ≅ P ⨯ Q ⨯ R

The associator isomorphism for binary products.

Equations

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

@[simp]

theorem CategoryTheory.Limits.prod.associator_hom {C : Type u} [Category.{v, u} C] [HasBinaryProducts C] (P Q R : C) : (associator P Q R).hom = lift (CategoryStruct.comp fst fst) (lift (CategoryStruct.comp fst snd) snd)

@[simp]

theorem CategoryTheory.Limits.prod.associator_inv {C : Type u} [Category.{v, u} C] [HasBinaryProducts C] (P Q R : C) : (associator P Q R).inv = lift (lift fst (CategoryStruct.comp snd fst)) (CategoryStruct.comp snd snd)

theorem CategoryTheory.Limits.prod.pentagon {C : Type u} [Category.{v, u} C] [HasBinaryProducts C] (W X Y Z : C) : CategoryStruct.comp (map (associator W X Y).hom (CategoryStruct.id Z)) (CategoryStruct.comp (associator W (X ⨯ Y) Z).hom (map (CategoryStruct.id W) (associator X Y Z).hom)) = CategoryStruct.comp (associator (W ⨯ X) Y Z).hom (associator W X (Y ⨯ Z)).hom

theorem CategoryTheory.Limits.prod.pentagon_assoc {C : Type u} [Category.{v, u} C] [HasBinaryProducts C] (W X Y Z : C) {Z✝ : C} (h : W ⨯ X ⨯ Y ⨯ Z ⟶ Z✝) : CategoryStruct.comp (map (associator W X Y).hom (CategoryStruct.id Z)) (CategoryStruct.comp (associator W (X ⨯ Y) Z).hom (CategoryStruct.comp (map (CategoryStruct.id W) (associator X Y Z).hom) h)) = CategoryStruct.comp (associator (W ⨯ X) Y Z).hom (CategoryStruct.comp (associator W X (Y ⨯ Z)).hom h)

theorem CategoryTheory.Limits.prod.associator_naturality {C : Type u} [Category.{v, u} C] [HasBinaryProducts C] {X₁ X₂ X₃ Y₁ Y₂ Y₃ : C} (f₁ : X₁ ⟶ Y₁) (f₂ : X₂ ⟶ Y₂) (f₃ : X₃ ⟶ Y₃) : CategoryStruct.comp (map (map f₁ f₂) f₃) (associator Y₁ Y₂ Y₃).hom = CategoryStruct.comp (associator X₁ X₂ X₃).hom (map f₁ (map f₂ f₃))

theorem CategoryTheory.Limits.prod.associator_naturality_assoc {C : Type u} [Category.{v, u} C] [HasBinaryProducts C] {X₁ X₂ X₃ Y₁ Y₂ Y₃ : C} (f₁ : X₁ ⟶ Y₁) (f₂ : X₂ ⟶ Y₂) (f₃ : X₃ ⟶ Y₃) {Z : C} (h : Y₁ ⨯ Y₂ ⨯ Y₃ ⟶ Z) : CategoryStruct.comp (map (map f₁ f₂) f₃) (CategoryStruct.comp (associator Y₁ Y₂ Y₃).hom h) = CategoryStruct.comp (associator X₁ X₂ X₃).hom (CategoryStruct.comp (map f₁ (map f₂ f₃)) h)

def CategoryTheory.Limits.prod.leftUnitor {C : Type u} [Category.{v, u} C] [HasTerminal C] (P : C) [HasBinaryProduct (⊤_ C) P] : (⊤_ C) ⨯ P ≅ P

The left unitor isomorphism for binary products with the terminal object.

Equations

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

@[simp]

theorem CategoryTheory.Limits.prod.leftUnitor_hom {C : Type u} [Category.{v, u} C] [HasTerminal C] (P : C) [HasBinaryProduct (⊤_ C) P] : (leftUnitor P).hom = snd

@[simp]

theorem CategoryTheory.Limits.prod.leftUnitor_inv {C : Type u} [Category.{v, u} C] [HasTerminal C] (P : C) [HasBinaryProduct (⊤_ C) P] : (leftUnitor P).inv = lift (terminal.from P) (CategoryStruct.id P)

def CategoryTheory.Limits.prod.rightUnitor {C : Type u} [Category.{v, u} C] [HasTerminal C] (P : C) [HasBinaryProduct P (⊤_ C)] : P ⨯ ⊤_ C ≅ P

The right unitor isomorphism for binary products with the terminal object.

Equations

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

@[simp]

theorem CategoryTheory.Limits.prod.rightUnitor_inv {C : Type u} [Category.{v, u} C] [HasTerminal C] (P : C) [HasBinaryProduct P (⊤_ C)] : (rightUnitor P).inv = lift (CategoryStruct.id P) (terminal.from P)

@[simp]

theorem CategoryTheory.Limits.prod.rightUnitor_hom {C : Type u} [Category.{v, u} C] [HasTerminal C] (P : C) [HasBinaryProduct P (⊤_ C)] : (rightUnitor P).hom = fst

theorem CategoryTheory.Limits.prod.leftUnitor_hom_naturality {C : Type u} [Category.{v, u} C] {X Y : C} [HasTerminal C] [HasBinaryProducts C] (f : X ⟶ Y) : CategoryStruct.comp (map (CategoryStruct.id (⊤_ C)) f) (leftUnitor Y).hom = CategoryStruct.comp (leftUnitor X).hom f

theorem CategoryTheory.Limits.prod.leftUnitor_hom_naturality_assoc {C : Type u} [Category.{v, u} C] {X Y : C} [HasTerminal C] [HasBinaryProducts C] (f : X ⟶ Y) {Z : C} (h : Y ⟶ Z) : CategoryStruct.comp (map (CategoryStruct.id (⊤_ C)) f) (CategoryStruct.comp (leftUnitor Y).hom h) = CategoryStruct.comp (leftUnitor X).hom (CategoryStruct.comp f h)

theorem CategoryTheory.Limits.prod.leftUnitor_inv_naturality {C : Type u} [Category.{v, u} C] {X Y : C} [HasTerminal C] [HasBinaryProducts C] (f : X ⟶ Y) : CategoryStruct.comp (leftUnitor X).inv (map (CategoryStruct.id (⊤_ C)) f) = CategoryStruct.comp f (leftUnitor Y).inv

theorem CategoryTheory.Limits.prod.leftUnitor_inv_naturality_assoc {C : Type u} [Category.{v, u} C] {X Y : C} [HasTerminal C] [HasBinaryProducts C] (f : X ⟶ Y) {Z : C} (h : (⊤_ C) ⨯ Y ⟶ Z) : CategoryStruct.comp (leftUnitor X).inv (CategoryStruct.comp (map (CategoryStruct.id (⊤_ C)) f) h) = CategoryStruct.comp f (CategoryStruct.comp (leftUnitor Y).inv h)

theorem CategoryTheory.Limits.prod.rightUnitor_hom_naturality {C : Type u} [Category.{v, u} C] {X Y : C} [HasTerminal C] [HasBinaryProducts C] (f : X ⟶ Y) : CategoryStruct.comp (map f (CategoryStruct.id (⊤_ C))) (rightUnitor Y).hom = CategoryStruct.comp (rightUnitor X).hom f

theorem CategoryTheory.Limits.prod.rightUnitor_hom_naturality_assoc {C : Type u} [Category.{v, u} C] {X Y : C} [HasTerminal C] [HasBinaryProducts C] (f : X ⟶ Y) {Z : C} (h : Y ⟶ Z) : CategoryStruct.comp (map f (CategoryStruct.id (⊤_ C))) (CategoryStruct.comp (rightUnitor Y).hom h) = CategoryStruct.comp (rightUnitor X).hom (CategoryStruct.comp f h)

theorem CategoryTheory.Limits.prod_rightUnitor_inv_naturality {C : Type u} [Category.{v, u} C] {X Y : C} [HasTerminal C] [HasBinaryProducts C] (f : X ⟶ Y) : CategoryStruct.comp (prod.rightUnitor X).inv (prod.map f (CategoryStruct.id (⊤_ C))) = CategoryStruct.comp f (prod.rightUnitor Y).inv

theorem CategoryTheory.Limits.prod_rightUnitor_inv_naturality_assoc {C : Type u} [Category.{v, u} C] {X Y : C} [HasTerminal C] [HasBinaryProducts C] (f : X ⟶ Y) {Z : C} (h : Y ⨯ ⊤_ C ⟶ Z) : CategoryStruct.comp (prod.rightUnitor X).inv (CategoryStruct.comp (prod.map f (CategoryStruct.id (⊤_ C))) h) = CategoryStruct.comp f (CategoryStruct.comp (prod.rightUnitor Y).inv h)

theorem CategoryTheory.Limits.prod.triangle {C : Type u} [Category.{v, u} C] [HasTerminal C] [HasBinaryProducts C] (X Y : C) : CategoryStruct.comp (associator X (⊤_ C) Y).hom (map (CategoryStruct.id X) (leftUnitor Y).hom) = map (rightUnitor X).hom (CategoryStruct.id Y)

def CategoryTheory.Limits.coprod.braiding {C : Type u} [Category.{v, u} C] [HasBinaryCoproducts C] (P Q : C) : P ⨿ Q ≅ Q ⨿ P

The braiding isomorphism which swaps a binary coproduct.

Equations

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

@[simp]

theorem CategoryTheory.Limits.coprod.braiding_inv {C : Type u} [Category.{v, u} C] [HasBinaryCoproducts C] (P Q : C) : (braiding P Q).inv = desc inr inl

@[simp]

theorem CategoryTheory.Limits.coprod.braiding_hom {C : Type u} [Category.{v, u} C] [HasBinaryCoproducts C] (P Q : C) : (braiding P Q).hom = desc inr inl

theorem CategoryTheory.Limits.coprod.symmetry' {C : Type u} [Category.{v, u} C] [HasBinaryCoproducts C] (P Q : C) : CategoryStruct.comp (desc inr inl) (desc inr inl) = CategoryStruct.id (P ⨿ Q)

theorem CategoryTheory.Limits.coprod.symmetry'_assoc {C : Type u} [Category.{v, u} C] [HasBinaryCoproducts C] (P Q : C) {Z : C} (h : P ⨿ Q ⟶ Z) : CategoryStruct.comp (desc inr inl) (CategoryStruct.comp (desc inr inl) h) = h

theorem CategoryTheory.Limits.coprod.symmetry {C : Type u} [Category.{v, u} C] [HasBinaryCoproducts C] (P Q : C) : CategoryStruct.comp (braiding P Q).hom (braiding Q P).hom = CategoryStruct.id (P ⨿ Q)

The braiding isomorphism is symmetric.

def CategoryTheory.Limits.coprod.associator {C : Type u} [Category.{v, u} C] [HasBinaryCoproducts C] (P Q R : C) : (P ⨿ Q) ⨿ R ≅ P ⨿ Q ⨿ R

The associator isomorphism for binary coproducts.

Equations

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

@[simp]

theorem CategoryTheory.Limits.coprod.associator_inv {C : Type u} [Category.{v, u} C] [HasBinaryCoproducts C] (P Q R : C) : (associator P Q R).inv = desc (CategoryStruct.comp inl inl) (desc (CategoryStruct.comp inr inl) inr)

@[simp]

theorem CategoryTheory.Limits.coprod.associator_hom {C : Type u} [Category.{v, u} C] [HasBinaryCoproducts C] (P Q R : C) : (associator P Q R).hom = desc (desc inl (CategoryStruct.comp inl inr)) (CategoryStruct.comp inr inr)

theorem CategoryTheory.Limits.coprod.pentagon {C : Type u} [Category.{v, u} C] [HasBinaryCoproducts C] (W X Y Z : C) : CategoryStruct.comp (map (associator W X Y).hom (CategoryStruct.id Z)) (CategoryStruct.comp (associator W (X ⨿ Y) Z).hom (map (CategoryStruct.id W) (associator X Y Z).hom)) = CategoryStruct.comp (associator (W ⨿ X) Y Z).hom (associator W X (Y ⨿ Z)).hom

theorem CategoryTheory.Limits.coprod.associator_naturality {C : Type u} [Category.{v, u} C] [HasBinaryCoproducts C] {X₁ X₂ X₃ Y₁ Y₂ Y₃ : C} (f₁ : X₁ ⟶ Y₁) (f₂ : X₂ ⟶ Y₂) (f₃ : X₃ ⟶ Y₃) : CategoryStruct.comp (map (map f₁ f₂) f₃) (associator Y₁ Y₂ Y₃).hom = CategoryStruct.comp (associator X₁ X₂ X₃).hom (map f₁ (map f₂ f₃))

def CategoryTheory.Limits.coprod.leftUnitor {C : Type u} [Category.{v, u} C] [HasBinaryCoproducts C] [HasInitial C] (P : C) : (⊥_ C) ⨿ P ≅ P

The left unitor isomorphism for binary coproducts with the initial object.

Equations

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

@[simp]

theorem CategoryTheory.Limits.coprod.leftUnitor_inv {C : Type u} [Category.{v, u} C] [HasBinaryCoproducts C] [HasInitial C] (P : C) : (leftUnitor P).inv = inr

@[simp]

theorem CategoryTheory.Limits.coprod.leftUnitor_hom {C : Type u} [Category.{v, u} C] [HasBinaryCoproducts C] [HasInitial C] (P : C) : (leftUnitor P).hom = desc (initial.to P) (CategoryStruct.id P)

def CategoryTheory.Limits.coprod.rightUnitor {C : Type u} [Category.{v, u} C] [HasBinaryCoproducts C] [HasInitial C] (P : C) : P ⨿ ⊥_ C ≅ P

The right unitor isomorphism for binary coproducts with the initial object.

Equations

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

@[simp]

theorem CategoryTheory.Limits.coprod.rightUnitor_inv {C : Type u} [Category.{v, u} C] [HasBinaryCoproducts C] [HasInitial C] (P : C) : (rightUnitor P).inv = inl

@[simp]

theorem CategoryTheory.Limits.coprod.rightUnitor_hom {C : Type u} [Category.{v, u} C] [HasBinaryCoproducts C] [HasInitial C] (P : C) : (rightUnitor P).hom = desc (CategoryStruct.id P) (initial.to P)

theorem CategoryTheory.Limits.coprod.triangle {C : Type u} [Category.{v, u} C] [HasBinaryCoproducts C] [HasInitial C] (X Y : C) : CategoryStruct.comp (associator X (⊥_ C) Y).hom (map (CategoryStruct.id X) (leftUnitor Y).hom) = map (rightUnitor X).hom (CategoryStruct.id Y)

def CategoryTheory.Limits.prod.functor {C : Type u} [Category.{v, u} C] [HasBinaryProducts C] : Functor C (Functor C C)

The binary product functor.

Equations

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

@[simp]

theorem CategoryTheory.Limits.prod.functor_obj_obj {C : Type u} [Category.{v, u} C] [HasBinaryProducts C] (X Y : C) : (functor.obj X).obj Y = (X ⨯ Y)

@[simp]

theorem CategoryTheory.Limits.prod.functor_map_app {C : Type u} [Category.{v, u} C] [HasBinaryProducts C] {X✝ Y✝ : C} (f : X✝ ⟶ Y✝) (T : C) : (functor.map f).app T = map f (CategoryStruct.id T)

@[simp]

theorem CategoryTheory.Limits.prod.functor_obj_map {C : Type u} [Category.{v, u} C] [HasBinaryProducts C] (X : C) {x✝ x✝¹ : C} (g : x✝ ⟶ x✝¹) : (functor.obj X).map g = map (CategoryStruct.id X) g

def CategoryTheory.Limits.prod.functorLeftComp {C : Type u} [Category.{v, u} C] [HasBinaryProducts C] (X Y : C) : functor.obj (X ⨯ Y) ≅ (functor.obj Y).comp (functor.obj X)

The product functor can be decomposed.

Equations

• CategoryTheory.Limits.prod.functorLeftComp X Y = CategoryTheory.NatIso.ofComponents (CategoryTheory.Limits.prod.associator X Y) ⋯

def CategoryTheory.Limits.coprod.functor {C : Type u} [Category.{v, u} C] [HasBinaryCoproducts C] : Functor C (Functor C C)

The binary coproduct functor.

Equations

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

@[simp]

theorem CategoryTheory.Limits.coprod.functor_map_app {C : Type u} [Category.{v, u} C] [HasBinaryCoproducts C] {X✝ Y✝ : C} (f : X✝ ⟶ Y✝) (T : C) : (functor.map f).app T = map f (CategoryStruct.id T)

@[simp]

theorem CategoryTheory.Limits.coprod.functor_obj_map {C : Type u} [Category.{v, u} C] [HasBinaryCoproducts C] (X : C) {x✝ x✝¹ : C} (g : x✝ ⟶ x✝¹) : (functor.obj X).map g = map (CategoryStruct.id X) g

@[simp]

theorem CategoryTheory.Limits.coprod.functor_obj_obj {C : Type u} [Category.{v, u} C] [HasBinaryCoproducts C] (X Y : C) : (functor.obj X).obj Y = (X ⨿ Y)

def CategoryTheory.Limits.coprod.functorLeftComp {C : Type u} [Category.{v, u} C] [HasBinaryCoproducts C] (X Y : C) : functor.obj (X ⨿ Y) ≅ (functor.obj Y).comp (functor.obj X)

The coproduct functor can be decomposed.

Equations

• CategoryTheory.Limits.coprod.functorLeftComp X Y = CategoryTheory.NatIso.ofComponents (CategoryTheory.Limits.coprod.associator X Y) ⋯

def CategoryTheory.Limits.prodComparison {C : Type u} [Category.{v, u} C] {D : Type u₂} [Category.{w, u₂} D] (F : Functor C D) (A B : C) [HasBinaryProduct A B] [HasBinaryProduct (F.obj A) (F.obj B)] : F.obj (A ⨯ B) ⟶ F.obj A ⨯ F.obj B

The product comparison morphism.

In CategoryTheory/Limits/Preserves we show this is always an iso iff F preserves binary products.

Equations

• CategoryTheory.Limits.prodComparison F A B = CategoryTheory.Limits.prod.lift (F.map CategoryTheory.Limits.prod.fst) (F.map CategoryTheory.Limits.prod.snd)

@[simp]

theorem CategoryTheory.Limits.prodComparison_fst {C : Type u} [Category.{v, u} C] {D : Type u₂} [Category.{w, u₂} D] (F : Functor C D) (A B : C) [HasBinaryProduct A B] [HasBinaryProduct (F.obj A) (F.obj B)] : CategoryStruct.comp (prodComparison F A B) prod.fst = F.map prod.fst

@[simp]

theorem CategoryTheory.Limits.prodComparison_fst_assoc {C : Type u} [Category.{v, u} C] {D : Type u₂} [Category.{w, u₂} D] (F : Functor C D) (A B : C) [HasBinaryProduct A B] [HasBinaryProduct (F.obj A) (F.obj B)] {Z : D} (h : F.obj A ⟶ Z) : CategoryStruct.comp (prodComparison F A B) (CategoryStruct.comp prod.fst h) = CategoryStruct.comp (F.map prod.fst) h

@[simp]

theorem CategoryTheory.Limits.prodComparison_snd {C : Type u} [Category.{v, u} C] {D : Type u₂} [Category.{w, u₂} D] (F : Functor C D) (A B : C) [HasBinaryProduct A B] [HasBinaryProduct (F.obj A) (F.obj B)] : CategoryStruct.comp (prodComparison F A B) prod.snd = F.map prod.snd

@[simp]

theorem CategoryTheory.Limits.prodComparison_snd_assoc {C : Type u} [Category.{v, u} C] {D : Type u₂} [Category.{w, u₂} D] (F : Functor C D) (A B : C) [HasBinaryProduct A B] [HasBinaryProduct (F.obj A) (F.obj B)] {Z : D} (h : F.obj B ⟶ Z) : CategoryStruct.comp (prodComparison F A B) (CategoryStruct.comp prod.snd h) = CategoryStruct.comp (F.map prod.snd) h

theorem CategoryTheory.Limits.prodComparison_natural {C : Type u} [Category.{v, u} C] {D : Type u₂} [Category.{w, u₂} D] (F : Functor C D) {A A' B B' : C} [HasBinaryProduct A B] [HasBinaryProduct A' B'] [HasBinaryProduct (F.obj A) (F.obj B)] [HasBinaryProduct (F.obj A') (F.obj B')] (f : A ⟶ A') (g : B ⟶ B') : CategoryStruct.comp (F.map (prod.map f g)) (prodComparison F A' B') = CategoryStruct.comp (prodComparison F A B) (prod.map (F.map f) (F.map g))

Naturality of the prodComparison morphism in both arguments.

theorem CategoryTheory.Limits.prodComparison_natural_assoc {C : Type u} [Category.{v, u} C] {D : Type u₂} [Category.{w, u₂} D] (F : Functor C D) {A A' B B' : C} [HasBinaryProduct A B] [HasBinaryProduct A' B'] [HasBinaryProduct (F.obj A) (F.obj B)] [HasBinaryProduct (F.obj A') (F.obj B')] (f : A ⟶ A') (g : B ⟶ B') {Z : D} (h : F.obj A' ⨯ F.obj B' ⟶ Z) : CategoryStruct.comp (F.map (prod.map f g)) (CategoryStruct.comp (prodComparison F A' B') h) = CategoryStruct.comp (prodComparison F A B) (CategoryStruct.comp (prod.map (F.map f) (F.map g)) h)

def CategoryTheory.Limits.prodComparisonNatTrans {C : Type u} [Category.{v, u} C] {D : Type u₂} [Category.{w, u₂} D] [HasBinaryProducts C] [HasBinaryProducts D] (F : Functor C D) (A : C) : (prod.functor.obj A).comp F ⟶ F.comp (prod.functor.obj (F.obj A))

The product comparison morphism from F(A ⨯ -) to FA ⨯ F-, whose components are given by prodComparison.

Equations

• CategoryTheory.Limits.prodComparisonNatTrans F A = { app := fun (B : C) => CategoryTheory.Limits.prodComparison F A B, naturality := ⋯ }

@[simp]

theorem CategoryTheory.Limits.prodComparisonNatTrans_app {C : Type u} [Category.{v, u} C] {D : Type u₂} [Category.{w, u₂} D] [HasBinaryProducts C] [HasBinaryProducts D] (F : Functor C D) (A B : C) : (prodComparisonNatTrans F A).app B = prodComparison F A B

theorem CategoryTheory.Limits.inv_prodComparison_map_fst {C : Type u} [Category.{v, u} C] {D : Type u₂} [Category.{w, u₂} D] (F : Functor C D) {A B : C} [HasBinaryProduct A B] [HasBinaryProduct (F.obj A) (F.obj B)] [IsIso (prodComparison F A B)] : CategoryStruct.comp (inv (prodComparison F A B)) (F.map prod.fst) = prod.fst

theorem CategoryTheory.Limits.inv_prodComparison_map_fst_assoc {C : Type u} [Category.{v, u} C] {D : Type u₂} [Category.{w, u₂} D] (F : Functor C D) {A B : C} [HasBinaryProduct A B] [HasBinaryProduct (F.obj A) (F.obj B)] [IsIso (prodComparison F A B)] {Z : D} (h : F.obj A ⟶ Z) : CategoryStruct.comp (inv (prodComparison F A B)) (CategoryStruct.comp (F.map prod.fst) h) = CategoryStruct.comp prod.fst h

theorem CategoryTheory.Limits.inv_prodComparison_map_snd {C : Type u} [Category.{v, u} C] {D : Type u₂} [Category.{w, u₂} D] (F : Functor C D) {A B : C} [HasBinaryProduct A B] [HasBinaryProduct (F.obj A) (F.obj B)] [IsIso (prodComparison F A B)] : CategoryStruct.comp (inv (prodComparison F A B)) (F.map prod.snd) = prod.snd

theorem CategoryTheory.Limits.inv_prodComparison_map_snd_assoc {C : Type u} [Category.{v, u} C] {D : Type u₂} [Category.{w, u₂} D] (F : Functor C D) {A B : C} [HasBinaryProduct A B] [HasBinaryProduct (F.obj A) (F.obj B)] [IsIso (prodComparison F A B)] {Z : D} (h : F.obj B ⟶ Z) : CategoryStruct.comp (inv (prodComparison F A B)) (CategoryStruct.comp (F.map prod.snd) h) = CategoryStruct.comp prod.snd h

theorem CategoryTheory.Limits.prodComparison_inv_natural {C : Type u} [Category.{v, u} C] {D : Type u₂} [Category.{w, u₂} D] (F : Functor C D) {A A' B B' : C} [HasBinaryProduct A B] [HasBinaryProduct A' B'] [HasBinaryProduct (F.obj A) (F.obj B)] [HasBinaryProduct (F.obj A') (F.obj B')] (f : A ⟶ A') (g : B ⟶ B') [IsIso (prodComparison F A B)] [IsIso (prodComparison F A' B')] : CategoryStruct.comp (inv (prodComparison F A B)) (F.map (prod.map f g)) = CategoryStruct.comp (prod.map (F.map f) (F.map g)) (inv (prodComparison F A' B'))

If the product comparison morphism is an iso, its inverse is natural.

theorem CategoryTheory.Limits.prodComparison_inv_natural_assoc {C : Type u} [Category.{v, u} C] {D : Type u₂} [Category.{w, u₂} D] (F : Functor C D) {A A' B B' : C} [HasBinaryProduct A B] [HasBinaryProduct A' B'] [HasBinaryProduct (F.obj A) (F.obj B)] [HasBinaryProduct (F.obj A') (F.obj B')] (f : A ⟶ A') (g : B ⟶ B') [IsIso (prodComparison F A B)] [IsIso (prodComparison F A' B')] {Z : D} (h : F.obj (A' ⨯ B') ⟶ Z) : CategoryStruct.comp (inv (prodComparison F A B)) (CategoryStruct.comp (F.map (prod.map f g)) h) = CategoryStruct.comp (prod.map (F.map f) (F.map g)) (CategoryStruct.comp (inv (prodComparison F A' B')) h)

def CategoryTheory.Limits.prodComparisonNatIso {C : Type u} [Category.{v, u} C] {D : Type u₂} [Category.{w, u₂} D] (F : Functor C D) [HasBinaryProducts C] [HasBinaryProducts D] (A : C) [∀ (B : C), IsIso (prodComparison F A B)] : (prod.functor.obj A).comp F ≅ F.comp (prod.functor.obj (F.obj A))

The natural isomorphism F(A ⨯ -) ≅ FA ⨯ F-, provided each prodComparison F A B is an isomorphism (as B changes).

Equations

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

@[simp]

theorem CategoryTheory.Limits.prodComparisonNatIso_inv {C : Type u} [Category.{v, u} C] {D : Type u₂} [Category.{w, u₂} D] (F : Functor C D) [HasBinaryProducts C] [HasBinaryProducts D] (A : C) [∀ (B : C), IsIso (prodComparison F A B)] : (prodComparisonNatIso F A).inv = (asIso { app := fun (B : C) => prodComparison F A B, naturality := ⋯ }).inv

@[simp]

theorem CategoryTheory.Limits.prodComparisonNatIso_hom {C : Type u} [Category.{v, u} C] {D : Type u₂} [Category.{w, u₂} D] (F : Functor C D) [HasBinaryProducts C] [HasBinaryProducts D] (A : C) [∀ (B : C), IsIso (prodComparison F A B)] : (prodComparisonNatIso F A).hom = prodComparisonNatTrans F A

theorem CategoryTheory.Limits.prodComparison_comp {C : Type u} [Category.{v, u} C] {D : Type u₂} [Category.{w, u₂} D] {E : Type u₃} [Category.{w', u₃} E] (F : Functor C D) (G : Functor D E) {A B : C} [HasBinaryProduct A B] [HasBinaryProduct (F.obj A) (F.obj B)] [HasBinaryProduct (G.obj (F.obj A)) (G.obj (F.obj B))] [HasBinaryProduct ((F.comp G).obj A) ((F.comp G).obj B)] : prodComparison (F.comp G) A B = CategoryStruct.comp (G.map (prodComparison F A B)) (prodComparison G (F.obj A) (F.obj B))

def CategoryTheory.Limits.coprodComparison {C : Type u} [Category.{v, u} C] {D : Type u₂} [Category.{w, u₂} D] (F : Functor C D) (A B : C) [HasBinaryCoproduct A B] [HasBinaryCoproduct (F.obj A) (F.obj B)] : F.obj A ⨿ F.obj B ⟶ F.obj (A ⨿ B)

The coproduct comparison morphism.

In CategoryTheory/Limits/Preserves we show this is always an iso iff F preserves binary coproducts.

Equations

• CategoryTheory.Limits.coprodComparison F A B = CategoryTheory.Limits.coprod.desc (F.map CategoryTheory.Limits.coprod.inl) (F.map CategoryTheory.Limits.coprod.inr)

@[simp]

theorem CategoryTheory.Limits.coprodComparison_inl {C : Type u} [Category.{v, u} C] {D : Type u₂} [Category.{w, u₂} D] (F : Functor C D) {A B : C} [HasBinaryCoproduct A B] [HasBinaryCoproduct (F.obj A) (F.obj B)] : CategoryStruct.comp coprod.inl (coprodComparison F A B) = F.map coprod.inl

@[simp]

theorem CategoryTheory.Limits.coprodComparison_inl_assoc {C : Type u} [Category.{v, u} C] {D : Type u₂} [Category.{w, u₂} D] (F : Functor C D) {A B : C} [HasBinaryCoproduct A B] [HasBinaryCoproduct (F.obj A) (F.obj B)] {Z : D} (h : F.obj (A ⨿ B) ⟶ Z) : CategoryStruct.comp coprod.inl (CategoryStruct.comp (coprodComparison F A B) h) = CategoryStruct.comp (F.map coprod.inl) h

@[simp]

theorem CategoryTheory.Limits.coprodComparison_inr {C : Type u} [Category.{v, u} C] {D : Type u₂} [Category.{w, u₂} D] (F : Functor C D) {A B : C} [HasBinaryCoproduct A B] [HasBinaryCoproduct (F.obj A) (F.obj B)] : CategoryStruct.comp coprod.inr (coprodComparison F A B) = F.map coprod.inr

@[simp]

theorem CategoryTheory.Limits.coprodComparison_inr_assoc {C : Type u} [Category.{v, u} C] {D : Type u₂} [Category.{w, u₂} D] (F : Functor C D) {A B : C} [HasBinaryCoproduct A B] [HasBinaryCoproduct (F.obj A) (F.obj B)] {Z : D} (h : F.obj (A ⨿ B) ⟶ Z) : CategoryStruct.comp coprod.inr (CategoryStruct.comp (coprodComparison F A B) h) = CategoryStruct.comp (F.map coprod.inr) h

theorem CategoryTheory.Limits.coprodComparison_natural {C : Type u} [Category.{v, u} C] {D : Type u₂} [Category.{w, u₂} D] (F : Functor C D) {A A' B B' : C} [HasBinaryCoproduct A B] [HasBinaryCoproduct A' B'] [HasBinaryCoproduct (F.obj A) (F.obj B)] [HasBinaryCoproduct (F.obj A') (F.obj B')] (f : A ⟶ A') (g : B ⟶ B') : CategoryStruct.comp (coprodComparison F A B) (F.map (coprod.map f g)) = CategoryStruct.comp (coprod.map (F.map f) (F.map g)) (coprodComparison F A' B')

Naturality of the coprod_comparison morphism in both arguments.

theorem CategoryTheory.Limits.coprodComparison_natural_assoc {C : Type u} [Category.{v, u} C] {D : Type u₂} [Category.{w, u₂} D] (F : Functor C D) {A A' B B' : C} [HasBinaryCoproduct A B] [HasBinaryCoproduct A' B'] [HasBinaryCoproduct (F.obj A) (F.obj B)] [HasBinaryCoproduct (F.obj A') (F.obj B')] (f : A ⟶ A') (g : B ⟶ B') {Z : D} (h : F.obj (A' ⨿ B') ⟶ Z) : CategoryStruct.comp (coprodComparison F A B) (CategoryStruct.comp (F.map (coprod.map f g)) h) = CategoryStruct.comp (coprod.map (F.map f) (F.map g)) (CategoryStruct.comp (coprodComparison F A' B') h)

def CategoryTheory.Limits.coprodComparisonNatTrans {C : Type u} [Category.{v, u} C] {D : Type u₂} [Category.{w, u₂} D] [HasBinaryCoproducts C] [HasBinaryCoproducts D] (F : Functor C D) (A : C) : F.comp (coprod.functor.obj (F.obj A)) ⟶ (coprod.functor.obj A).comp F

The coproduct comparison morphism from FA ⨿ F- to F(A ⨿ -), whose components are given by coprodComparison.

Equations

• CategoryTheory.Limits.coprodComparisonNatTrans F A = { app := fun (B : C) => CategoryTheory.Limits.coprodComparison F A B, naturality := ⋯ }

@[simp]

theorem CategoryTheory.Limits.coprodComparisonNatTrans_app {C : Type u} [Category.{v, u} C] {D : Type u₂} [Category.{w, u₂} D] [HasBinaryCoproducts C] [HasBinaryCoproducts D] (F : Functor C D) (A B : C) : (coprodComparisonNatTrans F A).app B = coprodComparison F A B

theorem CategoryTheory.Limits.map_inl_inv_coprodComparison {C : Type u} [Category.{v, u} C] {D : Type u₂} [Category.{w, u₂} D] (F : Functor C D) {A B : C} [HasBinaryCoproduct A B] [HasBinaryCoproduct (F.obj A) (F.obj B)] [IsIso (coprodComparison F A B)] : CategoryStruct.comp (F.map coprod.inl) (inv (coprodComparison F A B)) = coprod.inl

theorem CategoryTheory.Limits.map_inl_inv_coprodComparison_assoc {C : Type u} [Category.{v, u} C] {D : Type u₂} [Category.{w, u₂} D] (F : Functor C D) {A B : C} [HasBinaryCoproduct A B] [HasBinaryCoproduct (F.obj A) (F.obj B)] [IsIso (coprodComparison F A B)] {Z : D} (h : F.obj A ⨿ F.obj B ⟶ Z) : CategoryStruct.comp (F.map coprod.inl) (CategoryStruct.comp (inv (coprodComparison F A B)) h) = CategoryStruct.comp coprod.inl h

theorem CategoryTheory.Limits.map_inr_inv_coprodComparison {C : Type u} [Category.{v, u} C] {D : Type u₂} [Category.{w, u₂} D] (F : Functor C D) {A B : C} [HasBinaryCoproduct A B] [HasBinaryCoproduct (F.obj A) (F.obj B)] [IsIso (coprodComparison F A B)] : CategoryStruct.comp (F.map coprod.inr) (inv (coprodComparison F A B)) = coprod.inr

theorem CategoryTheory.Limits.map_inr_inv_coprodComparison_assoc {C : Type u} [Category.{v, u} C] {D : Type u₂} [Category.{w, u₂} D] (F : Functor C D) {A B : C} [HasBinaryCoproduct A B] [HasBinaryCoproduct (F.obj A) (F.obj B)] [IsIso (coprodComparison F A B)] {Z : D} (h : F.obj A ⨿ F.obj B ⟶ Z) : CategoryStruct.comp (F.map coprod.inr) (CategoryStruct.comp (inv (coprodComparison F A B)) h) = CategoryStruct.comp coprod.inr h

theorem CategoryTheory.Limits.coprodComparison_inv_natural {C : Type u} [Category.{v, u} C] {D : Type u₂} [Category.{w, u₂} D] (F : Functor C D) {A A' B B' : C} [HasBinaryCoproduct A B] [HasBinaryCoproduct A' B'] [HasBinaryCoproduct (F.obj A) (F.obj B)] [HasBinaryCoproduct (F.obj A') (F.obj B')] (f : A ⟶ A') (g : B ⟶ B') [IsIso (coprodComparison F A B)] [IsIso (coprodComparison F A' B')] : CategoryStruct.comp (inv (coprodComparison F A B)) (coprod.map (F.map f) (F.map g)) = CategoryStruct.comp (F.map (coprod.map f g)) (inv (coprodComparison F A' B'))

If the coproduct comparison morphism is an iso, its inverse is natural.

theorem CategoryTheory.Limits.coprodComparison_inv_natural_assoc {C : Type u} [Category.{v, u} C] {D : Type u₂} [Category.{w, u₂} D] (F : Functor C D) {A A' B B' : C} [HasBinaryCoproduct A B] [HasBinaryCoproduct A' B'] [HasBinaryCoproduct (F.obj A) (F.obj B)] [HasBinaryCoproduct (F.obj A') (F.obj B')] (f : A ⟶ A') (g : B ⟶ B') [IsIso (coprodComparison F A B)] [IsIso (coprodComparison F A' B')] {Z : D} (h : F.obj A' ⨿ F.obj B' ⟶ Z) : CategoryStruct.comp (inv (coprodComparison F A B)) (CategoryStruct.comp (coprod.map (F.map f) (F.map g)) h) = CategoryStruct.comp (F.map (coprod.map f g)) (CategoryStruct.comp (inv (coprodComparison F A' B')) h)

def CategoryTheory.Limits.coprodComparisonNatIso {C : Type u} [Category.{v, u} C] {D : Type u₂} [Category.{w, u₂} D] (F : Functor C D) [HasBinaryCoproducts C] [HasBinaryCoproducts D] (A : C) [∀ (B : C), IsIso (coprodComparison F A B)] : F.comp (coprod.functor.obj (F.obj A)) ≅ (coprod.functor.obj A).comp F

The natural isomorphism FA ⨿ F- ≅ F(A ⨿ -), provided each coprodComparison F A B is an isomorphism (as B changes).

Equations

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

@[simp]

theorem CategoryTheory.Limits.coprodComparisonNatIso_inv {C : Type u} [Category.{v, u} C] {D : Type u₂} [Category.{w, u₂} D] (F : Functor C D) [HasBinaryCoproducts C] [HasBinaryCoproducts D] (A : C) [∀ (B : C), IsIso (coprodComparison F A B)] : (coprodComparisonNatIso F A).inv = (asIso { app := fun (B : C) => coprodComparison F A B, naturality := ⋯ }).inv

@[simp]

theorem CategoryTheory.Limits.coprodComparisonNatIso_hom {C : Type u} [Category.{v, u} C] {D : Type u₂} [Category.{w, u₂} D] (F : Functor C D) [HasBinaryCoproducts C] [HasBinaryCoproducts D] (A : C) [∀ (B : C), IsIso (coprodComparison F A B)] : (coprodComparisonNatIso F A).hom = coprodComparisonNatTrans F A

noncomputable def CategoryTheory.Over.coprodObj {C : Type u} [Category.{v, u} C] [Limits.HasBinaryCoproducts C] {A : C} : Over A → Functor (Over A) (Over A)

Auxiliary definition for Over.coprod.

Equations

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

@[simp]

theorem CategoryTheory.Over.coprodObj_obj {C : Type u} [Category.{v, u} C] [Limits.HasBinaryCoproducts C] {A : C} (a✝ g : Over A) : a✝.coprodObj.obj g = mk (Limits.coprod.desc a✝.hom g.hom)

@[simp]

theorem CategoryTheory.Over.coprodObj_map {C : Type u} [Category.{v, u} C] [Limits.HasBinaryCoproducts C] {A : C} (a✝ : Over A) {X✝ Y✝ : Over A} (k : X✝ ⟶ Y✝) : a✝.coprodObj.map k = homMk (Limits.coprod.map (CategoryStruct.id ((Functor.id C).obj a✝.left)) k.left) ⋯

noncomputable def CategoryTheory.Over.coprod {C : Type u} [Category.{v, u} C] [Limits.HasBinaryCoproducts C] {A : C} : Functor (Over A) (Functor (Over A) (Over A))

A category with binary coproducts has a functorial sup operation on over categories.

Equations

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

@[simp]

theorem CategoryTheory.Over.coprod_map_app {C : Type u} [Category.{v, u} C] [Limits.HasBinaryCoproducts C] {A : C} {X✝ Y✝ : Over A} (k : X✝ ⟶ Y✝) (g : Over A) : (coprod.map k).app g = homMk (Limits.coprod.map k.left (CategoryStruct.id ((Functor.id C).obj g.left))) ⋯

@[simp]

theorem CategoryTheory.Over.coprod_obj {C : Type u} [Category.{v, u} C] [Limits.HasBinaryCoproducts C] {A : C} (f : Over A) : coprod.obj f = f.coprodObj