Products and coproducts in `C` and `Cᵒᵖ` #

We construct products and coproducts in the opposite categories.

instance CategoryTheory.Limits.hasCoproductsOfShape_opposite {C : Type u₁} [Category.{v₁, u₁} C] (X : Type v₂) [HasProductsOfShape X C] :

HasCoproductsOfShape X Cᵒᵖ

If C has products indexed by X, then Cᵒᵖ has coproducts indexed by X.

source

theorem CategoryTheory.Limits.hasCoproductsOfShape_of_opposite {C : Type u₁} [Category.{v₁, u₁} C] (X : Type v₂) [HasProductsOfShape X Cᵒᵖ] :

HasCoproductsOfShape X C

source

instance CategoryTheory.Limits.hasProductsOfShape_opposite {C : Type u₁} [Category.{v₁, u₁} C] (X : Type v₂) [HasCoproductsOfShape X C] :

HasProductsOfShape X Cᵒᵖ

If C has coproducts indexed by X, then Cᵒᵖ has products indexed by X.

source

theorem CategoryTheory.Limits.hasProductsOfShape_of_opposite {C : Type u₁} [Category.{v₁, u₁} C] (X : Type v₂) [HasCoproductsOfShape X Cᵒᵖ] :

HasProductsOfShape X C

source

instance CategoryTheory.Limits.hasProducts_opposite {C : Type u₁} [Category.{v₁, u₁} C] [HasCoproducts C] :

HasProducts Cᵒᵖ

source

theorem CategoryTheory.Limits.hasProducts_of_opposite {C : Type u₁} [Category.{v₁, u₁} C] [HasCoproducts Cᵒᵖ] :

HasProducts C

source

instance CategoryTheory.Limits.hasCoproducts_opposite {C : Type u₁} [Category.{v₁, u₁} C] [HasProducts C] :

HasCoproducts Cᵒᵖ

source

theorem CategoryTheory.Limits.hasCoproducts_of_opposite {C : Type u₁} [Category.{v₁, u₁} C] [HasProducts Cᵒᵖ] :

HasCoproducts C

source

instance CategoryTheory.Limits.hasFiniteCoproducts_opposite {C : Type u₁} [Category.{v₁, u₁} C] [HasFiniteProducts C] :

HasFiniteCoproducts Cᵒᵖ

source

theorem CategoryTheory.Limits.hasFiniteCoproducts_of_opposite {C : Type u₁} [Category.{v₁, u₁} C] [HasFiniteProducts Cᵒᵖ] :

HasFiniteCoproducts C

source

instance CategoryTheory.Limits.hasFiniteProducts_opposite {C : Type u₁} [Category.{v₁, u₁} C] [HasFiniteCoproducts C] :

HasFiniteProducts Cᵒᵖ

source

theorem CategoryTheory.Limits.hasFiniteProducts_of_opposite {C : Type u₁} [Category.{v₁, u₁} C] [HasFiniteCoproducts Cᵒᵖ] :

HasFiniteProducts C

source

instance CategoryTheory.Limits.instHasLimitOppositeDiscreteOpFunctor {C : Type u₁} [Category.{v₁, u₁} C] {α : Type u_1} {Z : α → C} [HasCoproduct Z] :

HasLimit (Discrete.functor Z).op

source

instance CategoryTheory.Limits.instHasLimitDiscreteOppositeCompInverseOppositeOpFunctor {C : Type u₁} [Category.{v₁, u₁} C] {α : Type u_1} {Z : α → C} [HasCoproduct Z] :

HasLimit ((Discrete.opposite α).inverse.comp (Discrete.functor Z).op)

source

instance CategoryTheory.Limits.instHasProductOppositeOp {C : Type u₁} [Category.{v₁, u₁} C] {α : Type u_1} {Z : α → C} [HasCoproduct Z] :

HasProduct fun (x : α) => Opposite.op (Z x)

source

@[implicit_reducible]

def CategoryTheory.Limits.Cofan.op {C : Type u₁} [Category.{v₁, u₁} C] {α : Type u_1} {Z : α → C} (c : Cofan Z) :

Fan fun (x : α) => Opposite.op (Z x)

A Cofan gives a Fan in the opposite category.

Equations

c.op = CategoryTheory.Limits.Fan.mk (Opposite.op c.pt) fun (a : α) => (c.inj a).op

Instances For

source

noncomputable def CategoryTheory.Limits.Cofan.IsColimit.op {C : Type u₁} [Category.{v₁, u₁} C] {α : Type u_1} {Z : α → C} {c : Cofan Z} (hc : IsColimit c) :

IsLimit c.op

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

Equations

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

Instances For

source

noncomputable def CategoryTheory.Limits.opCoproductIsoProduct' {C : Type u₁} [Category.{v₁, u₁} C] {α : Type u_1} {Z : α → C} {c : Cofan Z} {f : Fan fun (x : α) => Opposite.op (Z x)} (hc : IsColimit c) (hf : IsLimit f) :

Opposite.op c.pt ≅ f.pt

The canonical isomorphism from the opposite of an abstract coproduct to the corresponding product in the opposite category.

Equations

CategoryTheory.Limits.opCoproductIsoProduct' hc hf = (CategoryTheory.Limits.Cofan.IsColimit.op hc).conePointUniqueUpToIso hf

Instances For

source

noncomputable def CategoryTheory.Limits.opCoproductIsoProduct {C : Type u₁} [Category.{v₁, u₁} C] {α : Type u_1} (Z : α → C) [HasCoproduct Z] :

Opposite.op (∐ Z) ≅ ∏ᶜ fun (x : α) => Opposite.op (Z x)

The canonical isomorphism from the opposite of the coproduct to the product in the opposite category.

Equations

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

Instances For

source

@[simp]

theorem CategoryTheory.Limits.opCoproductIsoProduct'_hom_comp_proj {C : Type u₁} [Category.{v₁, u₁} C] {α : Type u_1} {Z : α → C} {c : Cofan Z} {f : Fan fun (x : α) => Opposite.op (Z x)} (hc : IsColimit c) (hf : IsLimit f) (i : α) :

CategoryStruct.comp (opCoproductIsoProduct' hc hf).hom (f.proj i) = (c.inj i).op

source

@[simp]

theorem CategoryTheory.Limits.opCoproductIsoProduct'_hom_comp_proj_assoc {C : Type u₁} [Category.{v₁, u₁} C] {α : Type u_1} {Z : α → C} {c : Cofan Z} {f : Fan fun (x : α) => Opposite.op (Z x)} (hc : IsColimit c) (hf : IsLimit f) (i : α) {Z✝ : Cᵒᵖ} (h : Opposite.op (Z i) ⟶ Z✝) :

CategoryStruct.comp (opCoproductIsoProduct' hc hf).hom (CategoryStruct.comp (f.proj i) h) = CategoryStruct.comp (c.inj i).op h

source

@[simp]

theorem CategoryTheory.Limits.opCoproductIsoProduct_hom_comp_π {C : Type u₁} [Category.{v₁, u₁} C] {α : Type u_1} {Z : α → C} [HasCoproduct Z] (i : α) :

CategoryStruct.comp (opCoproductIsoProduct Z).hom (Pi.π (fun (x : α) => Opposite.op (Z x)) i) = (Sigma.ι Z i).op

source

@[simp]

theorem CategoryTheory.Limits.opCoproductIsoProduct_hom_comp_π_assoc {C : Type u₁} [Category.{v₁, u₁} C] {α : Type u_1} {Z : α → C} [HasCoproduct Z] (i : α) {Z✝ : Cᵒᵖ} (h : Opposite.op (Z i) ⟶ Z✝) :

CategoryStruct.comp (opCoproductIsoProduct Z).hom (CategoryStruct.comp (Pi.π (fun (x : α) => Opposite.op (Z x)) i) h) = CategoryStruct.comp (Sigma.ι Z i).op h

source

theorem CategoryTheory.Limits.opCoproductIsoProduct'_inv_comp_inj {C : Type u₁} [Category.{v₁, u₁} C] {α : Type u_1} {Z : α → C} {c : Cofan Z} {f : Fan fun (x : α) => Opposite.op (Z x)} (hc : IsColimit c) (hf : IsLimit f) (b : α) :

CategoryStruct.comp (opCoproductIsoProduct' hc hf).inv (c.inj b).op = f.proj b

source

theorem CategoryTheory.Limits.opCoproductIsoProduct'_comp_self {C : Type u₁} [Category.{v₁, u₁} C] {α : Type u_1} {Z : α → C} {c c' : Cofan Z} {f : Fan fun (x : α) => Opposite.op (Z x)} (hc : IsColimit c) (hc' : IsColimit c') (hf : IsLimit f) :

CategoryStruct.comp (opCoproductIsoProduct' hc hf).hom (opCoproductIsoProduct' hc' hf).inv = (hc.coconePointUniqueUpToIso hc').op.inv

source

theorem CategoryTheory.Limits.opCoproductIsoProduct_inv_comp_ι {C : Type u₁} [Category.{v₁, u₁} C] {α : Type u_1} (Z : α → C) [HasCoproduct Z] (b : α) :

CategoryStruct.comp (opCoproductIsoProduct Z).inv (Sigma.ι Z b).op = Pi.π (fun (x : α) => Opposite.op (Z x)) b

source

theorem CategoryTheory.Limits.desc_op_comp_opCoproductIsoProduct'_hom {C : Type u₁} [Category.{v₁, u₁} C] {α : Type u_1} {Z : α → C} {c : Cofan Z} {f : Fan fun (x : α) => Opposite.op (Z x)} (hc : IsColimit c) (hf : IsLimit f) (c' : Cofan Z) :

CategoryStruct.comp (hc.desc c').op (opCoproductIsoProduct' hc hf).hom = hf.lift c'.op

source

theorem CategoryTheory.Limits.desc_op_comp_opCoproductIsoProduct_hom {C : Type u₁} [Category.{v₁, u₁} C] {α : Type u_1} {Z : α → C} [HasCoproduct Z] {X : C} (π : (a : α) → Z a ⟶ X) :

CategoryStruct.comp (Sigma.desc π).op (opCoproductIsoProduct Z).hom = Pi.lift fun (a : α) => (π a).op

source

instance CategoryTheory.Limits.instHasColimitOppositeDiscreteOpFunctor {C : Type u₁} [Category.{v₁, u₁} C] {α : Type u_1} {Z : α → C} [HasProduct Z] :

HasColimit (Discrete.functor Z).op

source

instance CategoryTheory.Limits.instHasColimitDiscreteOppositeCompInverseOppositeOpFunctor {C : Type u₁} [Category.{v₁, u₁} C] {α : Type u_1} {Z : α → C} [HasProduct Z] :

HasColimit ((Discrete.opposite α).inverse.comp (Discrete.functor Z).op)

source

instance CategoryTheory.Limits.instHasCoproductOppositeOp {C : Type u₁} [Category.{v₁, u₁} C] {α : Type u_1} {Z : α → C} [HasProduct Z] :

HasCoproduct fun (x : α) => Opposite.op (Z x)

source

def CategoryTheory.Limits.Fan.op {C : Type u₁} [Category.{v₁, u₁} C] {α : Type u_1} {Z : α → C} (f : Fan Z) :

Cofan fun (x : α) => Opposite.op (Z x)

A Fan gives a Cofan in the opposite category.

Equations

f.op = CategoryTheory.Limits.Cofan.mk (Opposite.op f.pt) fun (a : α) => (f.proj a).op

Instances For

source

noncomputable def CategoryTheory.Limits.Fan.IsLimit.op {C : Type u₁} [Category.{v₁, u₁} C] {α : Type u_1} {Z : α → C} {f : Fan Z} (hf : IsLimit f) :

IsColimit f.op

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

Equations

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

Instances For

source

noncomputable def CategoryTheory.Limits.opProductIsoCoproduct' {C : Type u₁} [Category.{v₁, u₁} C] {α : Type u_1} {Z : α → C} {f : Fan Z} {c : Cofan fun (x : α) => Opposite.op (Z x)} (hf : IsLimit f) (hc : IsColimit c) :

Opposite.op f.pt ≅ c.pt

The canonical isomorphism from the opposite of an abstract product to the corresponding coproduct in the opposite category.

Equations

CategoryTheory.Limits.opProductIsoCoproduct' hf hc = (CategoryTheory.Limits.Fan.IsLimit.op hf).coconePointUniqueUpToIso hc

Instances For

source

noncomputable def CategoryTheory.Limits.opProductIsoCoproduct {C : Type u₁} [Category.{v₁, u₁} C] {α : Type u_1} (Z : α → C) [HasProduct Z] :

Opposite.op (∏ᶜ Z) ≅ ∐ fun (x : α) => Opposite.op (Z x)

The canonical isomorphism from the opposite of the product to the coproduct in the opposite category.

Equations

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

Instances For

source

theorem CategoryTheory.Limits.proj_comp_opProductIsoCoproduct'_hom {C : Type u₁} [Category.{v₁, u₁} C] {α : Type u_1} {Z : α → C} {f : Fan Z} {c : Cofan fun (x : α) => Opposite.op (Z x)} (hf : IsLimit f) (hc : IsColimit c) (b : α) :

CategoryStruct.comp (f.proj b).op (opProductIsoCoproduct' hf hc).hom = c.inj b

source

theorem CategoryTheory.Limits.opProductIsoCoproduct'_comp_self {C : Type u₁} [Category.{v₁, u₁} C] {α : Type u_1} {Z : α → C} {f f' : Fan Z} {c : Cofan fun (x : α) => Opposite.op (Z x)} (hf : IsLimit f) (hf' : IsLimit f') (hc : IsColimit c) :

CategoryStruct.comp (opProductIsoCoproduct' hf hc).hom (opProductIsoCoproduct' hf' hc).inv = (hf.conePointUniqueUpToIso hf').op.inv

source

theorem CategoryTheory.Limits.π_comp_opProductIsoCoproduct_hom {C : Type u₁} [Category.{v₁, u₁} C] {α : Type u_1} (Z : α → C) [HasProduct Z] (b : α) :

CategoryStruct.comp (Pi.π Z b).op (opProductIsoCoproduct Z).hom = Sigma.ι (fun (x : α) => Opposite.op (Z x)) b

source

theorem CategoryTheory.Limits.opProductIsoCoproduct'_inv_comp_lift {C : Type u₁} [Category.{v₁, u₁} C] {α : Type u_1} {Z : α → C} {f : Fan Z} {c : Cofan fun (x : α) => Opposite.op (Z x)} (hf : IsLimit f) (hc : IsColimit c) (f' : Fan Z) :

CategoryStruct.comp (opProductIsoCoproduct' hf hc).inv (hf.lift f').op = hc.desc f'.op

source

theorem CategoryTheory.Limits.opProductIsoCoproduct_inv_comp_lift {C : Type u₁} [Category.{v₁, u₁} C] {α : Type u_1} {Z : α → C} [HasProduct Z] {X : C} (π : (a : α) → X ⟶ Z a) :

CategoryStruct.comp (opProductIsoCoproduct Z).inv (Pi.lift π).op = Sigma.desc fun (a : α) => (π a).op

source

instance CategoryTheory.Limits.instHasBinaryCoproductOppositeOp {C : Type u₁} [Category.{v₁, u₁} C] {A B : C} [HasBinaryProduct A B] :

HasBinaryCoproduct (Opposite.op A) (Opposite.op B)

source

noncomputable def CategoryTheory.Limits.opProdIsoCoprod {C : Type u₁} [Category.{v₁, u₁} C] (A B : C) [HasBinaryProduct A B] :

Opposite.op (A ⨯ B) ≅ Opposite.op A ⨿ Opposite.op B

The canonical isomorphism from the opposite of the binary product to the coproduct in the opposite category.

Equations

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

Instances For

source

@[simp]

theorem CategoryTheory.Limits.fst_opProdIsoCoprod_hom {C : Type u₁} [Category.{v₁, u₁} C] {A B : C} [HasBinaryProduct A B] :

CategoryStruct.comp prod.fst.op (opProdIsoCoprod A B).hom = coprod.inl

source

@[simp]

theorem CategoryTheory.Limits.fst_opProdIsoCoprod_hom_assoc {C : Type u₁} [Category.{v₁, u₁} C] {A B : C} [HasBinaryProduct A B] {Z : Cᵒᵖ} (h : Opposite.op A ⨿ Opposite.op B ⟶ Z) :

CategoryStruct.comp prod.fst.op (CategoryStruct.comp (opProdIsoCoprod A B).hom h) = CategoryStruct.comp coprod.inl h

source

@[simp]

theorem CategoryTheory.Limits.snd_opProdIsoCoprod_hom {C : Type u₁} [Category.{v₁, u₁} C] {A B : C} [HasBinaryProduct A B] :

CategoryStruct.comp prod.snd.op (opProdIsoCoprod A B).hom = coprod.inr

source

@[simp]

theorem CategoryTheory.Limits.snd_opProdIsoCoprod_hom_assoc {C : Type u₁} [Category.{v₁, u₁} C] {A B : C} [HasBinaryProduct A B] {Z : Cᵒᵖ} (h : Opposite.op A ⨿ Opposite.op B ⟶ Z) :

CategoryStruct.comp prod.snd.op (CategoryStruct.comp (opProdIsoCoprod A B).hom h) = CategoryStruct.comp coprod.inr h

source

@[simp]

theorem CategoryTheory.Limits.inl_opProdIsoCoprod_inv {C : Type u₁} [Category.{v₁, u₁} C] {A B : C} [HasBinaryProduct A B] :

CategoryStruct.comp coprod.inl (opProdIsoCoprod A B).inv = prod.fst.op

source

@[simp]

theorem CategoryTheory.Limits.inl_opProdIsoCoprod_inv_assoc {C : Type u₁} [Category.{v₁, u₁} C] {A B : C} [HasBinaryProduct A B] {Z : Cᵒᵖ} (h : Opposite.op (A ⨯ B) ⟶ Z) :

CategoryStruct.comp coprod.inl (CategoryStruct.comp (opProdIsoCoprod A B).inv h) = CategoryStruct.comp prod.fst.op h

source

@[simp]

theorem CategoryTheory.Limits.inr_opProdIsoCoprod_inv {C : Type u₁} [Category.{v₁, u₁} C] {A B : C} [HasBinaryProduct A B] :

CategoryStruct.comp coprod.inr (opProdIsoCoprod A B).inv = prod.snd.op

source

@[simp]

theorem CategoryTheory.Limits.inr_opProdIsoCoprod_inv_assoc {C : Type u₁} [Category.{v₁, u₁} C] {A B : C} [HasBinaryProduct A B] {Z : Cᵒᵖ} (h : Opposite.op (A ⨯ B) ⟶ Z) :

CategoryStruct.comp coprod.inr (CategoryStruct.comp (opProdIsoCoprod A B).inv h) = CategoryStruct.comp prod.snd.op h

source

@[simp]

theorem CategoryTheory.Limits.opProdIsoCoprod_hom_fst {C : Type u₁} [Category.{v₁, u₁} C] {A B : C} [HasBinaryProduct A B] :

CategoryStruct.comp (opProdIsoCoprod A B).hom.unop prod.fst = coprod.inl.unop

source

@[simp]

theorem CategoryTheory.Limits.opProdIsoCoprod_hom_fst_assoc {C : Type u₁} [Category.{v₁, u₁} C] {A B : C} [HasBinaryProduct A B] {Z : C} (h : A ⟶ Z) :

CategoryStruct.comp (opProdIsoCoprod A B).hom.unop (CategoryStruct.comp prod.fst h) = CategoryStruct.comp coprod.inl.unop h

source

@[simp]

theorem CategoryTheory.Limits.opProdIsoCoprod_hom_snd {C : Type u₁} [Category.{v₁, u₁} C] {A B : C} [HasBinaryProduct A B] :

CategoryStruct.comp (opProdIsoCoprod A B).hom.unop prod.snd = coprod.inr.unop

source

@[simp]

theorem CategoryTheory.Limits.opProdIsoCoprod_hom_snd_assoc {C : Type u₁} [Category.{v₁, u₁} C] {A B : C} [HasBinaryProduct A B] {Z : C} (h : B ⟶ Z) :

CategoryStruct.comp (opProdIsoCoprod A B).hom.unop (CategoryStruct.comp prod.snd h) = CategoryStruct.comp coprod.inr.unop h

source

@[simp]

theorem CategoryTheory.Limits.opProdIsoCoprod_inv_inl {C : Type u₁} [Category.{v₁, u₁} C] {A B : C} [HasBinaryProduct A B] :

CategoryStruct.comp (opProdIsoCoprod A B).inv.unop coprod.inl.unop = prod.fst

source

@[simp]

theorem CategoryTheory.Limits.opProdIsoCoprod_inv_inl_assoc {C : Type u₁} [Category.{v₁, u₁} C] {A B : C} [HasBinaryProduct A B] {Z : C} (h : A ⟶ Z) :

CategoryStruct.comp (opProdIsoCoprod A B).inv.unop (CategoryStruct.comp coprod.inl.unop h) = CategoryStruct.comp prod.fst h

source

@[simp]

theorem CategoryTheory.Limits.opProdIsoCoprod_inv_inr {C : Type u₁} [Category.{v₁, u₁} C] {A B : C} [HasBinaryProduct A B] :

CategoryStruct.comp (opProdIsoCoprod A B).inv.unop coprod.inr.unop = prod.snd

source

@[simp]

theorem CategoryTheory.Limits.opProdIsoCoprod_inv_inr_assoc {C : Type u₁} [Category.{v₁, u₁} C] {A B : C} [HasBinaryProduct A B] {Z : C} (h : B ⟶ Z) :

CategoryStruct.comp (opProdIsoCoprod A B).inv.unop (CategoryStruct.comp coprod.inr.unop h) = CategoryStruct.comp prod.snd h

Documentation

Mathlib.CategoryTheory.Limits.Shapes.Opposites.Products

Products and coproducts in `C` and `Cᵒᵖ` #

Products and coproducts in C and Cᵒᵖ #

Products and coproducts in `C` and `Cᵒᵖ` #