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: CategoryTheory.Limits.WalkingPair
• right: CategoryTheory.Limits.WalkingPair

instance CategoryTheory.Limits.instDecidableEqWalkingPair : DecidableEq CategoryTheory.Limits.WalkingPair

Equations

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

instance CategoryTheory.Limits.instInhabitedWalkingPair : Inhabited CategoryTheory.Limits.WalkingPair

Equations

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

def CategoryTheory.Limits.WalkingPair.swap : CategoryTheory.Limits.WalkingPair ≃ CategoryTheory.Limits.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 : CategoryTheory.Limits.WalkingPair.swap CategoryTheory.Limits.WalkingPair.left = CategoryTheory.Limits.WalkingPair.right

@[simp]

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

@[simp]

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

@[simp]

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

def CategoryTheory.Limits.WalkingPair.equivBool : CategoryTheory.Limits.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 : CategoryTheory.Limits.WalkingPair.equivBool CategoryTheory.Limits.WalkingPair.left = true

@[simp]

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

@[simp]

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

@[simp]

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

def CategoryTheory.Limits.pairFunction {C : Type u} (X Y : C) : CategoryTheory.Limits.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) : CategoryTheory.Limits.pairFunction X Y CategoryTheory.Limits.WalkingPair.left = X

@[simp]

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

def CategoryTheory.Limits.pair {C : Type u} [CategoryTheory.Category.{v, u} C] (X Y : C) : CategoryTheory.Functor (CategoryTheory.Discrete CategoryTheory.Limits.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} [CategoryTheory.Category.{v, u} C] (X Y : C) : (CategoryTheory.Limits.pair X Y).obj { as := CategoryTheory.Limits.WalkingPair.left } = X

@[simp]

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

def CategoryTheory.Limits.mapPair {C : Type u} [CategoryTheory.Category.{v, u} C] {F G : CategoryTheory.Functor (CategoryTheory.Discrete CategoryTheory.Limits.WalkingPair) C} (f : F.obj { as := CategoryTheory.Limits.WalkingPair.left } ⟶ G.obj { as := CategoryTheory.Limits.WalkingPair.left }) (g : F.obj { as := CategoryTheory.Limits.WalkingPair.right } ⟶ G.obj { as := CategoryTheory.Limits.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} [CategoryTheory.Category.{v, u} C] {F G : CategoryTheory.Functor (CategoryTheory.Discrete CategoryTheory.Limits.WalkingPair) C} (f : F.obj { as := CategoryTheory.Limits.WalkingPair.left } ⟶ G.obj { as := CategoryTheory.Limits.WalkingPair.left }) (g : F.obj { as := CategoryTheory.Limits.WalkingPair.right } ⟶ G.obj { as := CategoryTheory.Limits.WalkingPair.right }) : (CategoryTheory.Limits.mapPair f g).app { as := CategoryTheory.Limits.WalkingPair.left } = f

@[simp]

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

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

@[simp]

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

def CategoryTheory.Limits.diagramIsoPair {C : Type u} [CategoryTheory.Category.{v, u} C] (F : CategoryTheory.Functor (CategoryTheory.Discrete CategoryTheory.Limits.WalkingPair) C) : F ≅ CategoryTheory.Limits.pair (F.obj { as := CategoryTheory.Limits.WalkingPair.left }) (F.obj { as := CategoryTheory.Limits.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} [CategoryTheory.Category.{v, u} C] (F : CategoryTheory.Functor (CategoryTheory.Discrete CategoryTheory.Limits.WalkingPair) C) (X : CategoryTheory.Discrete CategoryTheory.Limits.WalkingPair) : (CategoryTheory.Limits.diagramIsoPair F).hom.app X = (match X with | { as := CategoryTheory.Limits.WalkingPair.left } => CategoryTheory.Iso.refl (F.obj { as := CategoryTheory.Limits.WalkingPair.left }) | { as := CategoryTheory.Limits.WalkingPair.right } => CategoryTheory.Iso.refl (F.obj { as := CategoryTheory.Limits.WalkingPair.right })).hom

@[simp]

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

def CategoryTheory.Limits.pairComp {C : Type u} [CategoryTheory.Category.{v, u} C] {D : Type u₁} [CategoryTheory.Category.{v₁, u₁} D] (X Y : C) (F : CategoryTheory.Functor C D) : (CategoryTheory.Limits.pair X Y).comp F ≅ CategoryTheory.Limits.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} [CategoryTheory.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} [CategoryTheory.Category.{v, u} C] {X Y : C} (s : CategoryTheory.Limits.BinaryFan X Y) : ((CategoryTheory.Functor.const (CategoryTheory.Discrete CategoryTheory.Limits.WalkingPair)).obj s.pt).obj { as := CategoryTheory.Limits.WalkingPair.left } ⟶ (CategoryTheory.Limits.pair X Y).obj { as := CategoryTheory.Limits.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} [CategoryTheory.Category.{v, u} C] {X Y : C} (s : CategoryTheory.Limits.BinaryFan X Y) : ((CategoryTheory.Functor.const (CategoryTheory.Discrete CategoryTheory.Limits.WalkingPair)).obj s.pt).obj { as := CategoryTheory.Limits.WalkingPair.right } ⟶ (CategoryTheory.Limits.pair X Y).obj { as := CategoryTheory.Limits.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} [CategoryTheory.Category.{v, u} C] {X Y : C} (s : CategoryTheory.Limits.BinaryFan X Y) : s.π.app { as := CategoryTheory.Limits.WalkingPair.left } = s.fst

@[simp]

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

def CategoryTheory.Limits.BinaryFan.ext {C : Type u} [CategoryTheory.Category.{v, u} C] {A B : C} {c c' : CategoryTheory.Limits.BinaryFan A B} (e : c.pt ≅ c'.pt) (h₁ : c.fst = CategoryTheory.CategoryStruct.comp e.hom c'.fst) (h₂ : c.snd = CategoryTheory.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} [CategoryTheory.Category.{v, u} C] {X Y : C} (s : CategoryTheory.Limits.BinaryFan X Y) (lift : {T : C} → (T ⟶ X) → (T ⟶ Y) → (T ⟶ s.pt)) (hl₁ : ∀ {T : C} (f : T ⟶ X) (g : T ⟶ Y), CategoryTheory.CategoryStruct.comp (lift f g) s.fst = f) (hl₂ : ∀ {T : C} (f : T ⟶ X) (g : T ⟶ Y), CategoryTheory.CategoryStruct.comp (lift f g) s.snd = g) (uniq : ∀ {T : C} (f : T ⟶ X) (g : T ⟶ Y) (m : T ⟶ s.pt), CategoryTheory.CategoryStruct.comp m s.fst = f → CategoryTheory.CategoryStruct.comp m s.snd = g → m = lift f g) : CategoryTheory.Limits.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} [CategoryTheory.Category.{v, u} C] {W X Y : C} {s : CategoryTheory.Limits.BinaryFan X Y} (h : CategoryTheory.Limits.IsLimit s) {f g : W ⟶ s.pt} (h₁ : CategoryTheory.CategoryStruct.comp f s.fst = CategoryTheory.CategoryStruct.comp g s.fst) (h₂ : CategoryTheory.CategoryStruct.comp f s.snd = CategoryTheory.CategoryStruct.comp g s.snd) : f = g

@[reducible, inline]

abbrev CategoryTheory.Limits.BinaryCofan {C : Type u} [CategoryTheory.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} [CategoryTheory.Category.{v, u} C] {X Y : C} (s : CategoryTheory.Limits.BinaryCofan X Y) : (CategoryTheory.Limits.pair X Y).obj { as := CategoryTheory.Limits.WalkingPair.left } ⟶ ((CategoryTheory.Functor.const (CategoryTheory.Discrete CategoryTheory.Limits.WalkingPair)).obj s.pt).obj { as := CategoryTheory.Limits.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} [CategoryTheory.Category.{v, u} C] {X Y : C} (s : CategoryTheory.Limits.BinaryCofan X Y) : (CategoryTheory.Limits.pair X Y).obj { as := CategoryTheory.Limits.WalkingPair.right } ⟶ ((CategoryTheory.Functor.const (CategoryTheory.Discrete CategoryTheory.Limits.WalkingPair)).obj s.pt).obj { as := CategoryTheory.Limits.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} [CategoryTheory.Category.{v, u} C] {A B : C} {c c' : CategoryTheory.Limits.BinaryCofan A B} (e : c.pt ≅ c'.pt) (h₁ : CategoryTheory.CategoryStruct.comp c.inl e.hom = c'.inl) (h₂ : CategoryTheory.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} [CategoryTheory.Category.{v, u} C] {X Y : C} (s : CategoryTheory.Limits.BinaryCofan X Y) : s.ι.app { as := CategoryTheory.Limits.WalkingPair.left } = s.inl

@[simp]

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

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

def CategoryTheory.Limits.BinaryFan.mk {C : Type u} [CategoryTheory.Category.{v, u} C] {X Y P : C} (π₁ : P ⟶ X) (π₂ : P ⟶ Y) : CategoryTheory.Limits.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} [CategoryTheory.Category.{v, u} C] {X Y P : C} (π₁ : P ⟶ X) (π₂ : P ⟶ Y) : (CategoryTheory.Limits.BinaryFan.mk π₁ π₂).pt = P

def CategoryTheory.Limits.BinaryCofan.mk {C : Type u} [CategoryTheory.Category.{v, u} C] {X Y P : C} (ι₁ : X ⟶ P) (ι₂ : Y ⟶ P) : CategoryTheory.Limits.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} [CategoryTheory.Category.{v, u} C] {X Y P : C} (ι₁ : X ⟶ P) (ι₂ : Y ⟶ P) : (CategoryTheory.Limits.BinaryCofan.mk ι₁ ι₂).pt = P

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

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

def CategoryTheory.Limits.isoBinaryFanMk {C : Type u} [CategoryTheory.Category.{v, u} C] {X Y : C} (c : CategoryTheory.Limits.BinaryFan X Y) : c ≅ CategoryTheory.Limits.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} [CategoryTheory.Category.{v, u} C] {X Y : C} (c : CategoryTheory.Limits.BinaryCofan X Y) : c ≅ CategoryTheory.Limits.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} [CategoryTheory.Category.{v, u} C] {X Y W : C} {fst : W ⟶ X} {snd : W ⟶ Y} (lift : (s : CategoryTheory.Limits.BinaryFan X Y) → s.pt ⟶ W) (fac_left : ∀ (s : CategoryTheory.Limits.BinaryFan X Y), CategoryTheory.CategoryStruct.comp (lift s) fst = s.fst) (fac_right : ∀ (s : CategoryTheory.Limits.BinaryFan X Y), CategoryTheory.CategoryStruct.comp (lift s) snd = s.snd) (uniq : ∀ (s : CategoryTheory.Limits.BinaryFan X Y) (m : s.pt ⟶ W), CategoryTheory.CategoryStruct.comp m fst = s.fst → CategoryTheory.CategoryStruct.comp m snd = s.snd → m = lift s) : CategoryTheory.Limits.IsLimit (CategoryTheory.Limits.BinaryFan.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} [CategoryTheory.Category.{v, u} C] {X Y W : C} {inl : X ⟶ W} {inr : Y ⟶ W} (desc : (s : CategoryTheory.Limits.BinaryCofan X Y) → W ⟶ s.pt) (fac_left : ∀ (s : CategoryTheory.Limits.BinaryCofan X Y), CategoryTheory.CategoryStruct.comp inl (desc s) = s.inl) (fac_right : ∀ (s : CategoryTheory.Limits.BinaryCofan X Y), CategoryTheory.CategoryStruct.comp inr (desc s) = s.inr) (uniq : ∀ (s : CategoryTheory.Limits.BinaryCofan X Y) (m : W ⟶ s.pt), CategoryTheory.CategoryStruct.comp inl m = s.inl → CategoryTheory.CategoryStruct.comp inr m = s.inr → m = desc s) : CategoryTheory.Limits.IsColimit (CategoryTheory.Limits.BinaryCofan.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} [CategoryTheory.Category.{v, u} C] {W X Y : C} {s : CategoryTheory.Limits.BinaryFan X Y} (h : CategoryTheory.Limits.IsLimit s) (f : W ⟶ X) (g : W ⟶ Y) : { l : W ⟶ s.pt // CategoryTheory.CategoryStruct.comp l s.fst = f ∧ CategoryTheory.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} [CategoryTheory.Category.{v, u} C] {W X Y : C} {s : CategoryTheory.Limits.BinaryFan X Y} (h : CategoryTheory.Limits.IsLimit s) (f : W ⟶ X) (g : W ⟶ Y) : ↑(CategoryTheory.Limits.BinaryFan.IsLimit.lift' h f g) = h.lift (CategoryTheory.Limits.BinaryFan.mk f g)

def CategoryTheory.Limits.BinaryCofan.IsColimit.desc' {C : Type u} [CategoryTheory.Category.{v, u} C] {W X Y : C} {s : CategoryTheory.Limits.BinaryCofan X Y} (h : CategoryTheory.Limits.IsColimit s) (f : X ⟶ W) (g : Y ⟶ W) : { l : s.pt ⟶ W // CategoryTheory.CategoryStruct.comp s.inl l = f ∧ CategoryTheory.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} [CategoryTheory.Category.{v, u} C] {W X Y : C} {s : CategoryTheory.Limits.BinaryCofan X Y} (h : CategoryTheory.Limits.IsColimit s) (f : X ⟶ W) (g : Y ⟶ W) : ↑(CategoryTheory.Limits.BinaryCofan.IsColimit.desc' h f g) = h.desc (CategoryTheory.Limits.BinaryCofan.mk f g)

def CategoryTheory.Limits.BinaryFan.isLimitFlip {C : Type u} [CategoryTheory.Category.{v, u} C] {X Y : C} {c : CategoryTheory.Limits.BinaryFan X Y} (hc : CategoryTheory.Limits.IsLimit c) : CategoryTheory.Limits.IsLimit (CategoryTheory.Limits.BinaryFan.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} [CategoryTheory.Category.{v, u} C] {X Y : C} (h : CategoryTheory.Limits.IsTerminal Y) (c : CategoryTheory.Limits.BinaryFan X Y) : Nonempty (CategoryTheory.Limits.IsLimit c) ↔ CategoryTheory.IsIso c.fst

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

noncomputable def CategoryTheory.Limits.BinaryFan.isLimitCompLeftIso {C : Type u} [CategoryTheory.Category.{v, u} C] {X Y X' : C} (c : CategoryTheory.Limits.BinaryFan X Y) (f : X ⟶ X') [CategoryTheory.IsIso f] (h : CategoryTheory.Limits.IsLimit c) : CategoryTheory.Limits.IsLimit (CategoryTheory.Limits.BinaryFan.mk (CategoryTheory.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} [CategoryTheory.Category.{v, u} C] {X Y Y' : C} (c : CategoryTheory.Limits.BinaryFan X Y) (f : Y ⟶ Y') [CategoryTheory.IsIso f] (h : CategoryTheory.Limits.IsLimit c) : CategoryTheory.Limits.IsLimit (CategoryTheory.Limits.BinaryFan.mk c.fst (CategoryTheory.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} [CategoryTheory.Category.{v, u} C] {X Y : C} {c : CategoryTheory.Limits.BinaryCofan X Y} (hc : CategoryTheory.Limits.IsColimit c) : CategoryTheory.Limits.IsColimit (CategoryTheory.Limits.BinaryCofan.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} [CategoryTheory.Category.{v, u} C] {X Y : C} (h : CategoryTheory.Limits.IsInitial Y) (c : CategoryTheory.Limits.BinaryCofan X Y) : Nonempty (CategoryTheory.Limits.IsColimit c) ↔ CategoryTheory.IsIso c.inl

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

noncomputable def CategoryTheory.Limits.BinaryCofan.isColimitCompLeftIso {C : Type u} [CategoryTheory.Category.{v, u} C] {X Y X' : C} (c : CategoryTheory.Limits.BinaryCofan X Y) (f : X' ⟶ X) [CategoryTheory.IsIso f] (h : CategoryTheory.Limits.IsColimit c) : CategoryTheory.Limits.IsColimit (CategoryTheory.Limits.BinaryCofan.mk (CategoryTheory.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} [CategoryTheory.Category.{v, u} C] {X Y Y' : C} (c : CategoryTheory.Limits.BinaryCofan X Y) (f : Y' ⟶ Y) [CategoryTheory.IsIso f] (h : CategoryTheory.Limits.IsColimit c) : CategoryTheory.Limits.IsColimit (CategoryTheory.Limits.BinaryCofan.mk c.inl (CategoryTheory.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} [CategoryTheory.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} [CategoryTheory.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} [CategoryTheory.Category.{v, u} C] (X Y : C) [CategoryTheory.Limits.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} [CategoryTheory.Category.{v, u} C] (X Y : C) [CategoryTheory.Limits.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} [CategoryTheory.Category.{v, u} C] {X Y : C} [CategoryTheory.Limits.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} [CategoryTheory.Category.{v, u} C] {X Y : C} [CategoryTheory.Limits.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} [CategoryTheory.Category.{v, u} C] {X Y : C} [CategoryTheory.Limits.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} [CategoryTheory.Category.{v, u} C] {X Y : C} [CategoryTheory.Limits.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} [CategoryTheory.Category.{v, u} C] (X Y : C) [CategoryTheory.Limits.HasBinaryProduct X Y] : CategoryTheory.Limits.IsLimit (CategoryTheory.Limits.BinaryFan.mk CategoryTheory.Limits.prod.fst CategoryTheory.Limits.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} [CategoryTheory.Category.{v, u} C] (X Y : C) [CategoryTheory.Limits.HasBinaryCoproduct X Y] : CategoryTheory.Limits.IsColimit (CategoryTheory.Limits.BinaryCofan.mk CategoryTheory.Limits.coprod.inl CategoryTheory.Limits.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} [CategoryTheory.Category.{v, u} C] {W X Y : C} [CategoryTheory.Limits.HasBinaryProduct X Y] {f g : W ⟶ X ⨯ Y} (h₁ : CategoryTheory.CategoryStruct.comp f CategoryTheory.Limits.prod.fst = CategoryTheory.CategoryStruct.comp g CategoryTheory.Limits.prod.fst) (h₂ : CategoryTheory.CategoryStruct.comp f CategoryTheory.Limits.prod.snd = CategoryTheory.CategoryStruct.comp g CategoryTheory.Limits.prod.snd) : f = g

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

@[reducible, inline]

noncomputable abbrev CategoryTheory.Limits.prod.lift {C : Type u} [CategoryTheory.Category.{v, u} C] {W X Y : C} [CategoryTheory.Limits.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} [CategoryTheory.Category.{v, u} C] (X : C) [CategoryTheory.Limits.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} [CategoryTheory.Category.{v, u} C] {W X Y : C} [CategoryTheory.Limits.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} [CategoryTheory.Category.{v, u} C] (X : C) [CategoryTheory.Limits.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} [CategoryTheory.Category.{v, u} C] {W X Y : C} [CategoryTheory.Limits.HasBinaryProduct X Y] (f : W ⟶ X) (g : W ⟶ Y) : CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.prod.lift f g) CategoryTheory.Limits.prod.fst = f

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

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

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

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

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

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

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

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

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

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

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

noncomputable def CategoryTheory.Limits.prod.lift' {C : Type u} [CategoryTheory.Category.{v, u} C] {W X Y : C} [CategoryTheory.Limits.HasBinaryProduct X Y] (f : W ⟶ X) (g : W ⟶ Y) : { l : W ⟶ X ⨯ Y // CategoryTheory.CategoryStruct.comp l CategoryTheory.Limits.prod.fst = f ∧ CategoryTheory.CategoryStruct.comp l CategoryTheory.Limits.prod.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} [CategoryTheory.Category.{v, u} C] {W X Y : C} [CategoryTheory.Limits.HasBinaryCoproduct X Y] (f : X ⟶ W) (g : Y ⟶ W) : { l : X ⨿ Y ⟶ W // CategoryTheory.CategoryStruct.comp CategoryTheory.Limits.coprod.inl l = f ∧ CategoryTheory.CategoryStruct.comp CategoryTheory.Limits.coprod.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} [CategoryTheory.Category.{v, u} C] {W X Y Z : C} [CategoryTheory.Limits.HasBinaryProduct W X] [CategoryTheory.Limits.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} [CategoryTheory.Category.{v, u} C] {W X Y Z : C} [CategoryTheory.Limits.HasBinaryCoproduct W X] [CategoryTheory.Limits.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} [CategoryTheory.Category.{v, u} C] {V W X Y : C} [CategoryTheory.Limits.HasBinaryProduct X Y] (f : V ⟶ W) (g : W ⟶ X) (h : W ⟶ Y) : CategoryTheory.CategoryStruct.comp f (CategoryTheory.Limits.prod.lift g h) = CategoryTheory.Limits.prod.lift (CategoryTheory.CategoryStruct.comp f g) (CategoryTheory.CategoryStruct.comp f h)

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

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

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

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

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

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

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

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

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

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

def CategoryTheory.Limits.prod.mapIso {C : Type u} [CategoryTheory.Category.{v, u} C] {W X Y Z : C} [CategoryTheory.Limits.HasBinaryProduct W X] [CategoryTheory.Limits.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} [CategoryTheory.Category.{v, u} C] {W X Y Z : C} [CategoryTheory.Limits.HasBinaryProduct W X] [CategoryTheory.Limits.HasBinaryProduct Y Z] (f : W ≅ Y) (g : X ≅ Z) : (CategoryTheory.Limits.prod.mapIso f g).inv = CategoryTheory.Limits.prod.map f.inv g.inv

@[simp]

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

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

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

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

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

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

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

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

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

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

@[simp]

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

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

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

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

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

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

@[simp]

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

@[simp]

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

@[simp]

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

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

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

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

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

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

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

def CategoryTheory.Limits.coprod.mapIso {C : Type u} [CategoryTheory.Category.{v, u} C] {W X Y Z : C} [CategoryTheory.Limits.HasBinaryCoproduct W X] [CategoryTheory.Limits.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} [CategoryTheory.Category.{v, u} C] {W X Y Z : C} [CategoryTheory.Limits.HasBinaryCoproduct W X] [CategoryTheory.Limits.HasBinaryCoproduct Y Z] (f : W ≅ Y) (g : X ≅ Z) : (CategoryTheory.Limits.coprod.mapIso f g).inv = CategoryTheory.Limits.coprod.map f.inv g.inv

@[simp]

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

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

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

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

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

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

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

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

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

@[reducible, inline]

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

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

See https://stacks.math.columbia.edu/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) [CategoryTheory.Category.{v, u} C] : Prop

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

See https://stacks.math.columbia.edu/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) [CategoryTheory.Category.{v, u} C] [∀ {X Y : C}, CategoryTheory.Limits.HasLimit (CategoryTheory.Limits.pair X Y)] : CategoryTheory.Limits.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) [CategoryTheory.Category.{v, u} C] [∀ {X Y : C}, CategoryTheory.Limits.HasColimit (CategoryTheory.Limits.pair X Y)] : CategoryTheory.Limits.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} [CategoryTheory.Category.{v, u} C] (P Q : C) [CategoryTheory.Limits.HasBinaryProduct P Q] [CategoryTheory.Limits.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} [CategoryTheory.Category.{v, u} C] (P Q : C) [CategoryTheory.Limits.HasBinaryProduct P Q] [CategoryTheory.Limits.HasBinaryProduct Q P] : (CategoryTheory.Limits.prod.braiding P Q).hom = CategoryTheory.Limits.prod.lift CategoryTheory.Limits.prod.snd CategoryTheory.Limits.prod.fst

@[simp]

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

theorem CategoryTheory.Limits.braid_natural {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasBinaryProducts C] {W X Y Z : C} (f : X ⟶ Y) (g : Z ⟶ W) : CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.prod.map f g) (CategoryTheory.Limits.prod.braiding Y W).hom = CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.prod.braiding X Z).hom (CategoryTheory.Limits.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} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasBinaryProducts C] {W X Y Z : C} (f : X ⟶ Y) (g : Z ⟶ W) {Z✝ : C} (h : W ⨯ Y ⟶ Z✝) : CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.prod.map f g) (CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.prod.braiding Y W).hom h) = CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.prod.braiding X Z).hom (CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.prod.map g f) h)

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

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

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

The braiding isomorphism is symmetric.

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

def CategoryTheory.Limits.prod.associator {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.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} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasBinaryProducts C] (P Q R : C) : (CategoryTheory.Limits.prod.associator P Q R).hom = CategoryTheory.Limits.prod.lift (CategoryTheory.CategoryStruct.comp CategoryTheory.Limits.prod.fst CategoryTheory.Limits.prod.fst) (CategoryTheory.Limits.prod.lift (CategoryTheory.CategoryStruct.comp CategoryTheory.Limits.prod.fst CategoryTheory.Limits.prod.snd) CategoryTheory.Limits.prod.snd)

@[simp]

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

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

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

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

theorem CategoryTheory.Limits.prod.associator_naturality_assoc {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.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) : CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.prod.map (CategoryTheory.Limits.prod.map f₁ f₂) f₃) (CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.prod.associator Y₁ Y₂ Y₃).hom h) = CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.prod.associator X₁ X₂ X₃).hom (CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.prod.map f₁ (CategoryTheory.Limits.prod.map f₂ f₃)) h)

def CategoryTheory.Limits.prod.leftUnitor {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasTerminal C] (P : C) [CategoryTheory.Limits.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} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasTerminal C] (P : C) [CategoryTheory.Limits.HasBinaryProduct (⊤_ C) P] : (CategoryTheory.Limits.prod.leftUnitor P).hom = CategoryTheory.Limits.prod.snd

@[simp]

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

def CategoryTheory.Limits.prod.rightUnitor {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasTerminal C] (P : C) [CategoryTheory.Limits.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} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasTerminal C] (P : C) [CategoryTheory.Limits.HasBinaryProduct P (⊤_ C)] : (CategoryTheory.Limits.prod.rightUnitor P).inv = CategoryTheory.Limits.prod.lift (CategoryTheory.CategoryStruct.id P) (CategoryTheory.Limits.terminal.from P)

@[simp]

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

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

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

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

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

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

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

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

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

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

def CategoryTheory.Limits.coprod.braiding {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.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} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasBinaryCoproducts C] (P Q : C) : (CategoryTheory.Limits.coprod.braiding P Q).inv = CategoryTheory.Limits.coprod.desc CategoryTheory.Limits.coprod.inr CategoryTheory.Limits.coprod.inl

@[simp]

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

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

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

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

The braiding isomorphism is symmetric.

def CategoryTheory.Limits.coprod.associator {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.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} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasBinaryCoproducts C] (P Q R : C) : (CategoryTheory.Limits.coprod.associator P Q R).inv = CategoryTheory.Limits.coprod.desc (CategoryTheory.CategoryStruct.comp CategoryTheory.Limits.coprod.inl CategoryTheory.Limits.coprod.inl) (CategoryTheory.Limits.coprod.desc (CategoryTheory.CategoryStruct.comp CategoryTheory.Limits.coprod.inr CategoryTheory.Limits.coprod.inl) CategoryTheory.Limits.coprod.inr)

@[simp]

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

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

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

def CategoryTheory.Limits.coprod.leftUnitor {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasBinaryCoproducts C] [CategoryTheory.Limits.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} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasBinaryCoproducts C] [CategoryTheory.Limits.HasInitial C] (P : C) : (CategoryTheory.Limits.coprod.leftUnitor P).inv = CategoryTheory.Limits.coprod.inr

@[simp]

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

def CategoryTheory.Limits.coprod.rightUnitor {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasBinaryCoproducts C] [CategoryTheory.Limits.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} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasBinaryCoproducts C] [CategoryTheory.Limits.HasInitial C] (P : C) : (CategoryTheory.Limits.coprod.rightUnitor P).inv = CategoryTheory.Limits.coprod.inl

@[simp]

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

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

def CategoryTheory.Limits.prod.functor {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasBinaryProducts C] : CategoryTheory.Functor C (CategoryTheory.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} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasBinaryProducts C] (X Y : C) : (CategoryTheory.Limits.prod.functor.obj X).obj Y = (X ⨯ Y)

@[simp]

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

@[simp]

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

def CategoryTheory.Limits.prod.functorLeftComp {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasBinaryProducts C] (X Y : C) : CategoryTheory.Limits.prod.functor.obj (X ⨯ Y) ≅ (CategoryTheory.Limits.prod.functor.obj Y).comp (CategoryTheory.Limits.prod.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} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasBinaryCoproducts C] : CategoryTheory.Functor C (CategoryTheory.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} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasBinaryCoproducts C] {X✝ Y✝ : C} (f : X✝ ⟶ Y✝) (T : C) : (CategoryTheory.Limits.coprod.functor.map f).app T = CategoryTheory.Limits.coprod.map f (CategoryTheory.CategoryStruct.id T)

@[simp]

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

@[simp]

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

def CategoryTheory.Limits.coprod.functorLeftComp {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasBinaryCoproducts C] (X Y : C) : CategoryTheory.Limits.coprod.functor.obj (X ⨿ Y) ≅ (CategoryTheory.Limits.coprod.functor.obj Y).comp (CategoryTheory.Limits.coprod.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} [CategoryTheory.Category.{v, u} C] {D : Type u₂} [CategoryTheory.Category.{w, u₂} D] (F : CategoryTheory.Functor C D) (A B : C) [CategoryTheory.Limits.HasBinaryProduct A B] [CategoryTheory.Limits.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} [CategoryTheory.Category.{v, u} C] {D : Type u₂} [CategoryTheory.Category.{w, u₂} D] (F : CategoryTheory.Functor C D) (A B : C) [CategoryTheory.Limits.HasBinaryProduct A B] [CategoryTheory.Limits.HasBinaryProduct (F.obj A) (F.obj B)] : CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.prodComparison F A B) CategoryTheory.Limits.prod.fst = F.map CategoryTheory.Limits.prod.fst

@[simp]

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

@[simp]

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

@[simp]

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

theorem CategoryTheory.Limits.prodComparison_natural {C : Type u} [CategoryTheory.Category.{v, u} C] {D : Type u₂} [CategoryTheory.Category.{w, u₂} D] (F : CategoryTheory.Functor C D) {A A' B B' : C} [CategoryTheory.Limits.HasBinaryProduct A B] [CategoryTheory.Limits.HasBinaryProduct A' B'] [CategoryTheory.Limits.HasBinaryProduct (F.obj A) (F.obj B)] [CategoryTheory.Limits.HasBinaryProduct (F.obj A') (F.obj B')] (f : A ⟶ A') (g : B ⟶ B') : CategoryTheory.CategoryStruct.comp (F.map (CategoryTheory.Limits.prod.map f g)) (CategoryTheory.Limits.prodComparison F A' B') = CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.prodComparison F A B) (CategoryTheory.Limits.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} [CategoryTheory.Category.{v, u} C] {D : Type u₂} [CategoryTheory.Category.{w, u₂} D] (F : CategoryTheory.Functor C D) {A A' B B' : C} [CategoryTheory.Limits.HasBinaryProduct A B] [CategoryTheory.Limits.HasBinaryProduct A' B'] [CategoryTheory.Limits.HasBinaryProduct (F.obj A) (F.obj B)] [CategoryTheory.Limits.HasBinaryProduct (F.obj A') (F.obj B')] (f : A ⟶ A') (g : B ⟶ B') {Z : D} (h : F.obj A' ⨯ F.obj B' ⟶ Z) : CategoryTheory.CategoryStruct.comp (F.map (CategoryTheory.Limits.prod.map f g)) (CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.prodComparison F A' B') h) = CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.prodComparison F A B) (CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.prod.map (F.map f) (F.map g)) h)

def CategoryTheory.Limits.prodComparisonNatTrans {C : Type u} [CategoryTheory.Category.{v, u} C] {D : Type u₂} [CategoryTheory.Category.{w, u₂} D] [CategoryTheory.Limits.HasBinaryProducts C] [CategoryTheory.Limits.HasBinaryProducts D] (F : CategoryTheory.Functor C D) (A : C) : (CategoryTheory.Limits.prod.functor.obj A).comp F ⟶ F.comp (CategoryTheory.Limits.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} [CategoryTheory.Category.{v, u} C] {D : Type u₂} [CategoryTheory.Category.{w, u₂} D] [CategoryTheory.Limits.HasBinaryProducts C] [CategoryTheory.Limits.HasBinaryProducts D] (F : CategoryTheory.Functor C D) (A B : C) : (CategoryTheory.Limits.prodComparisonNatTrans F A).app B = CategoryTheory.Limits.prodComparison F A B

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

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

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

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

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

def CategoryTheory.Limits.prodComparisonNatIso {C : Type u} [CategoryTheory.Category.{v, u} C] {D : Type u₂} [CategoryTheory.Category.{w, u₂} D] (F : CategoryTheory.Functor C D) [CategoryTheory.Limits.HasBinaryProducts C] [CategoryTheory.Limits.HasBinaryProducts D] (A : C) [∀ (B : C), CategoryTheory.IsIso (CategoryTheory.Limits.prodComparison F A B)] : (CategoryTheory.Limits.prod.functor.obj A).comp F ≅ F.comp (CategoryTheory.Limits.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} [CategoryTheory.Category.{v, u} C] {D : Type u₂} [CategoryTheory.Category.{w, u₂} D] (F : CategoryTheory.Functor C D) [CategoryTheory.Limits.HasBinaryProducts C] [CategoryTheory.Limits.HasBinaryProducts D] (A : C) [∀ (B : C), CategoryTheory.IsIso (CategoryTheory.Limits.prodComparison F A B)] : (CategoryTheory.Limits.prodComparisonNatIso F A).inv = (CategoryTheory.asIso { app := fun (B : C) => CategoryTheory.Limits.prodComparison F A B, naturality := ⋯ }).inv

@[simp]

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

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

def CategoryTheory.Limits.coprodComparison {C : Type u} [CategoryTheory.Category.{v, u} C] {D : Type u₂} [CategoryTheory.Category.{w, u₂} D] (F : CategoryTheory.Functor C D) (A B : C) [CategoryTheory.Limits.HasBinaryCoproduct A B] [CategoryTheory.Limits.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} [CategoryTheory.Category.{v, u} C] {D : Type u₂} [CategoryTheory.Category.{w, u₂} D] (F : CategoryTheory.Functor C D) {A B : C} [CategoryTheory.Limits.HasBinaryCoproduct A B] [CategoryTheory.Limits.HasBinaryCoproduct (F.obj A) (F.obj B)] : CategoryTheory.CategoryStruct.comp CategoryTheory.Limits.coprod.inl (CategoryTheory.Limits.coprodComparison F A B) = F.map CategoryTheory.Limits.coprod.inl

@[simp]

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

@[simp]

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

@[simp]

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

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

Naturality of the coprod_comparison morphism in both arguments.

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

def CategoryTheory.Limits.coprodComparisonNatTrans {C : Type u} [CategoryTheory.Category.{v, u} C] {D : Type u₂} [CategoryTheory.Category.{w, u₂} D] [CategoryTheory.Limits.HasBinaryCoproducts C] [CategoryTheory.Limits.HasBinaryCoproducts D] (F : CategoryTheory.Functor C D) (A : C) : F.comp (CategoryTheory.Limits.coprod.functor.obj (F.obj A)) ⟶ (CategoryTheory.Limits.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} [CategoryTheory.Category.{v, u} C] {D : Type u₂} [CategoryTheory.Category.{w, u₂} D] [CategoryTheory.Limits.HasBinaryCoproducts C] [CategoryTheory.Limits.HasBinaryCoproducts D] (F : CategoryTheory.Functor C D) (A B : C) : (CategoryTheory.Limits.coprodComparisonNatTrans F A).app B = CategoryTheory.Limits.coprodComparison F A B

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

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

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

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

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

def CategoryTheory.Limits.coprodComparisonNatIso {C : Type u} [CategoryTheory.Category.{v, u} C] {D : Type u₂} [CategoryTheory.Category.{w, u₂} D] (F : CategoryTheory.Functor C D) [CategoryTheory.Limits.HasBinaryCoproducts C] [CategoryTheory.Limits.HasBinaryCoproducts D] (A : C) [∀ (B : C), CategoryTheory.IsIso (CategoryTheory.Limits.coprodComparison F A B)] : F.comp (CategoryTheory.Limits.coprod.functor.obj (F.obj A)) ≅ (CategoryTheory.Limits.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} [CategoryTheory.Category.{v, u} C] {D : Type u₂} [CategoryTheory.Category.{w, u₂} D] (F : CategoryTheory.Functor C D) [CategoryTheory.Limits.HasBinaryCoproducts C] [CategoryTheory.Limits.HasBinaryCoproducts D] (A : C) [∀ (B : C), CategoryTheory.IsIso (CategoryTheory.Limits.coprodComparison F A B)] : (CategoryTheory.Limits.coprodComparisonNatIso F A).inv = (CategoryTheory.asIso { app := fun (B : C) => CategoryTheory.Limits.coprodComparison F A B, naturality := ⋯ }).inv

@[simp]

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

noncomputable def CategoryTheory.Over.coprodObj {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasBinaryCoproducts C] {A : C} : CategoryTheory.Over A → CategoryTheory.Functor (CategoryTheory.Over A) (CategoryTheory.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} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasBinaryCoproducts C] {A : C} (a✝ g : CategoryTheory.Over A) : a✝.coprodObj.obj g = CategoryTheory.Over.mk (CategoryTheory.Limits.coprod.desc a✝.hom g.hom)

@[simp]

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

noncomputable def CategoryTheory.Over.coprod {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasBinaryCoproducts C] {A : C} : CategoryTheory.Functor (CategoryTheory.Over A) (CategoryTheory.Functor (CategoryTheory.Over A) (CategoryTheory.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} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasBinaryCoproducts C] {A : C} {X✝ Y✝ : CategoryTheory.Over A} (k : X✝ ⟶ Y✝) (g : CategoryTheory.Over A) : (CategoryTheory.Over.coprod.map k).app g = CategoryTheory.Over.homMk (CategoryTheory.Limits.coprod.map k.left (CategoryTheory.CategoryStruct.id ((CategoryTheory.Functor.id C).obj g.left))) ⋯

@[simp]

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