Categorical (co)products #
This file defines (co)products as special cases of (co)limits.
A product is the categorical generalization of the object Π i, f i where f : ι → C. It is a
limit cone over the diagram formed by f, implemented by converting f into a functor
Discrete ι ⥤ C.
A coproduct is the dual concept.
Main definitions #
- a
Fanis a cone over a discrete category Fan.mkconstructs a fan from an indexed collection of maps- a
Piis alimit (Discrete.functor f)
Each of these has a dual.
Implementation notes #
As with the other special shapes in the limits library, all the definitions here are given as
abbreviations of the general statements for limits, so all the simp lemmas and theorems about
general limits can be used.
@[reducible, inline]
abbrev
CategoryTheory.Limits.Fan
{β : Type w}
{C : Type u}
[CategoryTheory.Category.{v, u} C]
(f : β → C)
:
Type (max (max w u) v)
A fan over f : β → C consists of a collection of maps from an object P to every f b.
@[reducible, inline]
abbrev
CategoryTheory.Limits.Cofan
{β : Type w}
{C : Type u}
[CategoryTheory.Category.{v, u} C]
(f : β → C)
:
Type (max (max w u) v)
A cofan over f : β → C consists of a collection of maps from every f b to an object P.
def
CategoryTheory.Limits.Fan.mk
{β : Type w}
{C : Type u}
[CategoryTheory.Category.{v, u} C]
{f : β → C}
(P : C)
(p : (b : β) → P ⟶ f b)
:
A fan over f : β → C consists of a collection of maps from an object P to every f b.
Equations
- CategoryTheory.Limits.Fan.mk P p = { pt := P, π := CategoryTheory.Discrete.natTrans fun (X : CategoryTheory.Discrete β) => p X.as }
@[simp]
theorem
CategoryTheory.Limits.Fan.mk_π_app
{β : Type w}
{C : Type u}
[CategoryTheory.Category.{v, u} C]
{f : β → C}
(P : C)
(p : (b : β) → P ⟶ f b)
(X : CategoryTheory.Discrete β)
:
(CategoryTheory.Limits.Fan.mk P p).π.app X = p X.as
@[simp]
theorem
CategoryTheory.Limits.Fan.mk_pt
{β : Type w}
{C : Type u}
[CategoryTheory.Category.{v, u} C]
{f : β → C}
(P : C)
(p : (b : β) → P ⟶ f b)
:
(CategoryTheory.Limits.Fan.mk P p).pt = P
def
CategoryTheory.Limits.Cofan.mk
{β : Type w}
{C : Type u}
[CategoryTheory.Category.{v, u} C]
{f : β → C}
(P : C)
(p : (b : β) → f b ⟶ P)
:
A cofan over f : β → C consists of a collection of maps from every f b to an object P.
Equations
- CategoryTheory.Limits.Cofan.mk P p = { pt := P, ι := CategoryTheory.Discrete.natTrans fun (X : CategoryTheory.Discrete β) => p X.as }
@[simp]
theorem
CategoryTheory.Limits.Cofan.mk_pt
{β : Type w}
{C : Type u}
[CategoryTheory.Category.{v, u} C]
{f : β → C}
(P : C)
(p : (b : β) → f b ⟶ P)
:
(CategoryTheory.Limits.Cofan.mk P p).pt = P
@[simp]
theorem
CategoryTheory.Limits.Cofan.mk_ι_app
{β : Type w}
{C : Type u}
[CategoryTheory.Category.{v, u} C]
{f : β → C}
(P : C)
(p : (b : β) → f b ⟶ P)
(X : CategoryTheory.Discrete β)
:
(CategoryTheory.Limits.Cofan.mk P p).ι.app X = p X.as
def
CategoryTheory.Limits.Fan.proj
{β : Type w}
{C : Type u}
[CategoryTheory.Category.{v, u} C]
{f : β → C}
(p : CategoryTheory.Limits.Fan f)
(j : β)
:
p.pt ⟶ f j
Get the jth "projection" in the fan.
(Note that the initial letter of proj matches the greek letter in Cone.π.)
Equations
- p.proj j = p.π.app { as := j }
def
CategoryTheory.Limits.Cofan.inj
{β : Type w}
{C : Type u}
[CategoryTheory.Category.{v, u} C]
{f : β → C}
(p : CategoryTheory.Limits.Cofan f)
(j : β)
:
f j ⟶ p.pt
Get the jth "injection" in the cofan.
(Note that the initial letter of inj matches the greek letter in Cocone.ι.)
Equations
- p.inj j = p.ι.app { as := j }
@[simp]
theorem
CategoryTheory.Limits.fan_mk_proj
{β : Type w}
{C : Type u}
[CategoryTheory.Category.{v, u} C]
{f : β → C}
(P : C)
(p : (b : β) → P ⟶ f b)
(j : β)
:
(CategoryTheory.Limits.Fan.mk P p).proj j = p j
@[simp]
theorem
CategoryTheory.Limits.cofan_mk_inj
{β : Type w}
{C : Type u}
[CategoryTheory.Category.{v, u} C]
{f : β → C}
(P : C)
(p : (b : β) → f b ⟶ P)
(j : β)
:
(CategoryTheory.Limits.Cofan.mk P p).inj j = p j
@[reducible, inline]
abbrev
CategoryTheory.Limits.HasProduct
{β : Type w}
{C : Type u}
[CategoryTheory.Category.{v, u} C]
(f : β → C)
:
An abbreviation for HasLimit (Discrete.functor f).
@[reducible, inline]
abbrev
CategoryTheory.Limits.HasCoproduct
{β : Type w}
{C : Type u}
[CategoryTheory.Category.{v, u} C]
(f : β → C)
:
An abbreviation for HasColimit (Discrete.functor f).
theorem
CategoryTheory.Limits.hasCoproduct_of_equiv_of_iso
{β : Type w}
{α : Type w₂}
{C : Type u}
[CategoryTheory.Category.{v, u} C]
(f : α → C)
(g : β → C)
[CategoryTheory.Limits.HasCoproduct f]
(e : β ≃ α)
(iso : (j : β) → g j ≅ f (e j))
:
theorem
CategoryTheory.Limits.hasProduct_of_equiv_of_iso
{β : Type w}
{α : Type w₂}
{C : Type u}
[CategoryTheory.Category.{v, u} C]
(f : α → C)
(g : β → C)
[CategoryTheory.Limits.HasProduct f]
(e : β ≃ α)
(iso : (j : β) → g j ≅ f (e j))
:
def
CategoryTheory.Limits.mkFanLimit
{β : Type w}
{C : Type u}
[CategoryTheory.Category.{v, u} C]
{f : β → C}
(t : CategoryTheory.Limits.Fan f)
(lift : (s : CategoryTheory.Limits.Fan f) → s.pt ⟶ t.pt)
(fac :
∀ (s : CategoryTheory.Limits.Fan f) (j : β), CategoryTheory.CategoryStruct.comp (lift s) (t.proj j) = s.proj j := by
aesop_cat)
(uniq :
∀ (s : CategoryTheory.Limits.Fan f) (m : s.pt ⟶ t.pt),
(∀ (j : β), CategoryTheory.CategoryStruct.comp m (t.proj j) = s.proj j) → m = lift s := by
aesop_cat)
:
Make a fan f into a limit fan by providing lift, fac, and uniq --
just a convenience lemma to avoid having to go through Discrete
Equations
- CategoryTheory.Limits.mkFanLimit t lift fac uniq = { lift := lift, fac := ⋯, uniq := ⋯ }
@[simp]
theorem
CategoryTheory.Limits.mkFanLimit_lift
{β : Type w}
{C : Type u}
[CategoryTheory.Category.{v, u} C]
{f : β → C}
(t : CategoryTheory.Limits.Fan f)
(lift : (s : CategoryTheory.Limits.Fan f) → s.pt ⟶ t.pt)
(fac :
∀ (s : CategoryTheory.Limits.Fan f) (j : β), CategoryTheory.CategoryStruct.comp (lift s) (t.proj j) = s.proj j := by
aesop_cat)
(uniq :
∀ (s : CategoryTheory.Limits.Fan f) (m : s.pt ⟶ t.pt),
(∀ (j : β), CategoryTheory.CategoryStruct.comp m (t.proj j) = s.proj j) → m = lift s := by
aesop_cat)
(s : CategoryTheory.Limits.Fan f)
:
(CategoryTheory.Limits.mkFanLimit t lift fac uniq).lift s = lift s
def
CategoryTheory.Limits.Fan.IsLimit.desc
{β : Type w}
{C : Type u}
[CategoryTheory.Category.{v, u} C]
{F : β → C}
{c : CategoryTheory.Limits.Fan F}
(hc : CategoryTheory.Limits.IsLimit c)
{A : C}
(f : (i : β) → A ⟶ F i)
:
A ⟶ c.pt
Constructor for morphisms to the point of a limit fan.
Equations
- CategoryTheory.Limits.Fan.IsLimit.desc hc f = hc.lift (CategoryTheory.Limits.Fan.mk A f)
@[simp]
theorem
CategoryTheory.Limits.Fan.IsLimit.fac
{β : Type w}
{C : Type u}
[CategoryTheory.Category.{v, u} C]
{F : β → C}
{c : CategoryTheory.Limits.Fan F}
(hc : CategoryTheory.Limits.IsLimit c)
{A : C}
(f : (i : β) → A ⟶ F i)
(i : β)
:
CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.Fan.IsLimit.desc hc f) (c.proj i) = f i
@[simp]
theorem
CategoryTheory.Limits.Fan.IsLimit.fac_assoc
{β : Type w}
{C : Type u}
[CategoryTheory.Category.{v, u} C]
{F : β → C}
{c : CategoryTheory.Limits.Fan F}
(hc : CategoryTheory.Limits.IsLimit c)
{A : C}
(f : (i : β) → A ⟶ F i)
(i : β)
{Z : C}
(h : F i ⟶ Z)
:
theorem
CategoryTheory.Limits.Fan.IsLimit.hom_ext
{C : Type u}
[CategoryTheory.Category.{v, u} C]
{I : Type u_1}
{F : I → C}
{c : CategoryTheory.Limits.Fan F}
(hc : CategoryTheory.Limits.IsLimit c)
{A : C}
(f g : A ⟶ c.pt)
(h : ∀ (i : I), CategoryTheory.CategoryStruct.comp f (c.proj i) = CategoryTheory.CategoryStruct.comp g (c.proj i))
:
f = g
def
CategoryTheory.Limits.mkCofanColimit
{β : Type w}
{C : Type u}
[CategoryTheory.Category.{v, u} C]
{f : β → C}
(s : CategoryTheory.Limits.Cofan f)
(desc : (t : CategoryTheory.Limits.Cofan f) → s.pt ⟶ t.pt)
(fac :
∀ (t : CategoryTheory.Limits.Cofan f) (j : β), CategoryTheory.CategoryStruct.comp (s.inj j) (desc t) = t.inj j := by
aesop_cat)
(uniq :
∀ (t : CategoryTheory.Limits.Cofan f) (m : s.pt ⟶ t.pt),
(∀ (j : β), CategoryTheory.CategoryStruct.comp (s.inj j) m = t.inj j) → m = desc t := by
aesop_cat)
:
Make a cofan f into a colimit cofan by providing desc, fac, and uniq --
just a convenience lemma to avoid having to go through Discrete
Equations
- CategoryTheory.Limits.mkCofanColimit s desc fac uniq = { desc := desc, fac := ⋯, uniq := ⋯ }
@[simp]
theorem
CategoryTheory.Limits.mkCofanColimit_desc
{β : Type w}
{C : Type u}
[CategoryTheory.Category.{v, u} C]
{f : β → C}
(s : CategoryTheory.Limits.Cofan f)
(desc : (t : CategoryTheory.Limits.Cofan f) → s.pt ⟶ t.pt)
(fac :
∀ (t : CategoryTheory.Limits.Cofan f) (j : β), CategoryTheory.CategoryStruct.comp (s.inj j) (desc t) = t.inj j := by
aesop_cat)
(uniq :
∀ (t : CategoryTheory.Limits.Cofan f) (m : s.pt ⟶ t.pt),
(∀ (j : β), CategoryTheory.CategoryStruct.comp (s.inj j) m = t.inj j) → m = desc t := by
aesop_cat)
(t : CategoryTheory.Limits.Cofan f)
:
(CategoryTheory.Limits.mkCofanColimit s desc fac uniq).desc t = desc t
def
CategoryTheory.Limits.Cofan.IsColimit.desc
{β : Type w}
{C : Type u}
[CategoryTheory.Category.{v, u} C]
{F : β → C}
{c : CategoryTheory.Limits.Cofan F}
(hc : CategoryTheory.Limits.IsColimit c)
{A : C}
(f : (i : β) → F i ⟶ A)
:
c.pt ⟶ A
Constructor for morphisms from the point of a colimit cofan.
Equations
- CategoryTheory.Limits.Cofan.IsColimit.desc hc f = hc.desc (CategoryTheory.Limits.Cofan.mk A f)
@[simp]
theorem
CategoryTheory.Limits.Cofan.IsColimit.fac
{β : Type w}
{C : Type u}
[CategoryTheory.Category.{v, u} C]
{F : β → C}
{c : CategoryTheory.Limits.Cofan F}
(hc : CategoryTheory.Limits.IsColimit c)
{A : C}
(f : (i : β) → F i ⟶ A)
(i : β)
:
CategoryTheory.CategoryStruct.comp (c.inj i) (CategoryTheory.Limits.Cofan.IsColimit.desc hc f) = f i
@[simp]
theorem
CategoryTheory.Limits.Cofan.IsColimit.fac_assoc
{β : Type w}
{C : Type u}
[CategoryTheory.Category.{v, u} C]
{F : β → C}
{c : CategoryTheory.Limits.Cofan F}
(hc : CategoryTheory.Limits.IsColimit c)
{A : C}
(f : (i : β) → F i ⟶ A)
(i : β)
{Z : C}
(h : A ⟶ Z)
:
theorem
CategoryTheory.Limits.Cofan.IsColimit.hom_ext
{C : Type u}
[CategoryTheory.Category.{v, u} C]
{I : Type u_1}
{F : I → C}
{c : CategoryTheory.Limits.Cofan F}
(hc : CategoryTheory.Limits.IsColimit c)
{A : C}
(f g : c.pt ⟶ A)
(h : ∀ (i : I), CategoryTheory.CategoryStruct.comp (c.inj i) f = CategoryTheory.CategoryStruct.comp (c.inj i) g)
:
f = g
@[reducible, inline]
abbrev
CategoryTheory.Limits.HasProductsOfShape
(β : Type v)
(C : Type u_1)
[CategoryTheory.Category.{u_2, u_1} C]
:
An abbreviation for HasLimitsOfShape (Discrete f).
@[reducible, inline]
abbrev
CategoryTheory.Limits.HasCoproductsOfShape
(β : Type v)
(C : Type u_1)
[CategoryTheory.Category.{u_2, u_1} C]
:
An abbreviation for HasColimitsOfShape (Discrete f).
@[reducible, inline]
abbrev
CategoryTheory.Limits.piObj
{β : Type w}
{C : Type u}
[CategoryTheory.Category.{v, u} C]
(f : β → C)
[CategoryTheory.Limits.HasProduct f]
:
C
piObj f computes the product of a family of elements f.
(It is defined as an abbreviation for limit (Discrete.functor f),
so for most facts about piObj f, you will just use general facts about limits.)
Equations
@[reducible, inline]
abbrev
CategoryTheory.Limits.sigmaObj
{β : Type w}
{C : Type u}
[CategoryTheory.Category.{v, u} C]
(f : β → C)
[CategoryTheory.Limits.HasCoproduct f]
:
C
sigmaObj f computes the coproduct of a family of elements f.
(It is defined as an abbreviation for colimit (Discrete.functor f),
so for most facts about sigmaObj f, you will just use general facts about colimits.)
Equations
notation for categorical products. We need ᶜ to avoid conflict with Finset.prod.
Equations
- CategoryTheory.Limits.«term∏ᶜ_» = Lean.ParserDescr.node `CategoryTheory.Limits.«term∏ᶜ_» 1022 (Lean.ParserDescr.binary `andthen (Lean.ParserDescr.symbol "∏ᶜ ") (Lean.ParserDescr.cat `term 60))
notation for categorical coproducts
Equations
- CategoryTheory.Limits.«term∐_» = Lean.ParserDescr.node `CategoryTheory.Limits.«term∐_» 1022 (Lean.ParserDescr.binary `andthen (Lean.ParserDescr.symbol "∐ ") (Lean.ParserDescr.cat `term 60))
@[reducible, inline]
abbrev
CategoryTheory.Limits.Pi.π
{β : Type w}
{C : Type u}
[CategoryTheory.Category.{v, u} C]
(f : β → C)
[CategoryTheory.Limits.HasProduct f]
(b : β)
:
The b-th projection from the pi object over f has the form ∏ᶜ f ⟶ f b.
Equations
- CategoryTheory.Limits.Pi.π f b = CategoryTheory.Limits.limit.π (CategoryTheory.Discrete.functor f) { as := b }
Instances For
@[reducible, inline]
abbrev
CategoryTheory.Limits.Sigma.ι
{β : Type w}
{C : Type u}
[CategoryTheory.Category.{v, u} C]
(f : β → C)
[CategoryTheory.Limits.HasCoproduct f]
(b : β)
:
The b-th inclusion into the sigma object over f has the form f b ⟶ ∐ f.
Equations
- CategoryTheory.Limits.Sigma.ι f b = CategoryTheory.Limits.colimit.ι (CategoryTheory.Discrete.functor f) { as := b }
Instances For
theorem
CategoryTheory.Limits.Pi.hom_ext
{β : Type w}
{C : Type u}
[CategoryTheory.Category.{v, u} C]
{f : β → C}
[CategoryTheory.Limits.HasProduct f]
{X : C}
(g₁ g₂ : X ⟶ ∏ᶜ f)
(h :
∀ (b : β),
CategoryTheory.CategoryStruct.comp g₁ (CategoryTheory.Limits.Pi.π f b) = CategoryTheory.CategoryStruct.comp g₂ (CategoryTheory.Limits.Pi.π f b))
:
g₁ = g₂
theorem
CategoryTheory.Limits.Sigma.hom_ext
{β : Type w}
{C : Type u}
[CategoryTheory.Category.{v, u} C]
{f : β → C}
[CategoryTheory.Limits.HasCoproduct f]
{X : C}
(g₁ g₂ : ∐ f ⟶ X)
(h :
∀ (b : β),
CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.Sigma.ι f b) g₁ = CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.Sigma.ι f b) g₂)
:
g₁ = g₂
def
CategoryTheory.Limits.productIsProduct
{β : Type w}
{C : Type u}
[CategoryTheory.Category.{v, u} C]
(f : β → C)
[CategoryTheory.Limits.HasProduct f]
:
The fan constructed of the projections from the product is limiting.
Equations
- One or more equations did not get rendered due to their size.
def
CategoryTheory.Limits.coproductIsCoproduct
{β : Type w}
{C : Type u}
[CategoryTheory.Category.{v, u} C]
(f : β → C)
[CategoryTheory.Limits.HasCoproduct f]
:
The cofan constructed of the inclusions from the coproduct is colimiting.
Equations
- One or more equations did not get rendered due to their size.
@[simp]
theorem
CategoryTheory.Limits.Pi.π_comp_eqToHom
{C : Type u}
[CategoryTheory.Category.{v, u} C]
{J : Type u_1}
(f : J → C)
[CategoryTheory.Limits.HasProduct f]
{j j' : J}
(w : j = j')
:
@[simp]
theorem
CategoryTheory.Limits.Pi.π_comp_eqToHom_assoc
{C : Type u}
[CategoryTheory.Category.{v, u} C]
{J : Type u_1}
(f : J → C)
[CategoryTheory.Limits.HasProduct f]
{j j' : J}
(w : j = j')
{Z : C}
(h : f j' ⟶ Z)
:
@[simp]
theorem
CategoryTheory.Limits.Sigma.eqToHom_comp_ι
{C : Type u}
[CategoryTheory.Category.{v, u} C]
{J : Type u_1}
(f : J → C)
[CategoryTheory.Limits.HasCoproduct f]
{j j' : J}
(w : j = j')
:
@[simp]
theorem
CategoryTheory.Limits.Sigma.eqToHom_comp_ι_assoc
{C : Type u}
[CategoryTheory.Category.{v, u} C]
{J : Type u_1}
(f : J → C)
[CategoryTheory.Limits.HasCoproduct f]
{j j' : J}
(w : j = j')
{Z : C}
(h : ∐ f ⟶ Z)
:
@[reducible, inline]
abbrev
CategoryTheory.Limits.Pi.lift
{β : Type w}
{C : Type u}
[CategoryTheory.Category.{v, u} C]
{f : β → C}
[CategoryTheory.Limits.HasProduct f]
{P : C}
(p : (b : β) → P ⟶ f b)
:
A collection of morphisms P ⟶ f b induces a morphism P ⟶ ∏ᶜ f.
theorem
CategoryTheory.Limits.Pi.lift_π
{C : Type u}
[CategoryTheory.Category.{v, u} C]
{β : Type w}
{f : β → C}
[CategoryTheory.Limits.HasProduct f]
{P : C}
(p : (b : β) → P ⟶ f b)
(b : β)
:
def
CategoryTheory.Limits.Fan.ext
{β : Type w}
{C : Type u}
[CategoryTheory.Category.{v, u} C]
{f : β → C}
{c₁ c₂ : CategoryTheory.Limits.Fan f}
(e : c₁.pt ≅ c₂.pt)
(w : ∀ (b : β), c₁.proj b = CategoryTheory.CategoryStruct.comp e.hom (c₂.proj b) := by aesop_cat)
:
c₁ ≅ c₂
A version of Cones.ext for Fans.
Equations
@[simp]
theorem
CategoryTheory.Limits.Fan.ext_inv_hom
{β : Type w}
{C : Type u}
[CategoryTheory.Category.{v, u} C]
{f : β → C}
{c₁ c₂ : CategoryTheory.Limits.Fan f}
(e : c₁.pt ≅ c₂.pt)
(w : ∀ (b : β), c₁.proj b = CategoryTheory.CategoryStruct.comp e.hom (c₂.proj b) := by aesop_cat)
:
(CategoryTheory.Limits.Fan.ext e w).inv.hom = e.inv
@[simp]
theorem
CategoryTheory.Limits.Fan.ext_hom_hom
{β : Type w}
{C : Type u}
[CategoryTheory.Category.{v, u} C]
{f : β → C}
{c₁ c₂ : CategoryTheory.Limits.Fan f}
(e : c₁.pt ≅ c₂.pt)
(w : ∀ (b : β), c₁.proj b = CategoryTheory.CategoryStruct.comp e.hom (c₂.proj b) := by aesop_cat)
:
(CategoryTheory.Limits.Fan.ext e w).hom.hom = e.hom
@[reducible, inline]
abbrev
CategoryTheory.Limits.Sigma.desc
{β : Type w}
{C : Type u}
[CategoryTheory.Category.{v, u} C]
{f : β → C}
[CategoryTheory.Limits.HasCoproduct f]
{P : C}
(p : (b : β) → f b ⟶ P)
:
A collection of morphisms f b ⟶ P induces a morphism ∐ f ⟶ P.
Equations
Instances For
theorem
CategoryTheory.Limits.Sigma.ι_desc
{C : Type u}
[CategoryTheory.Category.{v, u} C]
{β : Type w}
{f : β → C}
[CategoryTheory.Limits.HasCoproduct f]
{P : C}
(p : (b : β) → f b ⟶ P)
(b : β)
:
instance
CategoryTheory.Limits.instIsIsoDescι
{β : Type w}
{C : Type u}
[CategoryTheory.Category.{v, u} C]
{f : β → C}
[CategoryTheory.Limits.HasCoproduct f]
:
CategoryTheory.IsIso (CategoryTheory.Limits.Sigma.desc fun (a : β) => CategoryTheory.Limits.Sigma.ι f a)
Equations
- ⋯ = ⋯
def
CategoryTheory.Limits.Cofan.ext
{β : Type w}
{C : Type u}
[CategoryTheory.Category.{v, u} C]
{f : β → C}
{c₁ c₂ : CategoryTheory.Limits.Cofan f}
(e : c₁.pt ≅ c₂.pt)
(w : ∀ (b : β), CategoryTheory.CategoryStruct.comp (c₁.inj b) e.hom = c₂.inj b := by aesop_cat)
:
c₁ ≅ c₂
A version of Cocones.ext for Cofans.
Equations
@[simp]
theorem
CategoryTheory.Limits.Cofan.ext_hom_hom
{β : Type w}
{C : Type u}
[CategoryTheory.Category.{v, u} C]
{f : β → C}
{c₁ c₂ : CategoryTheory.Limits.Cofan f}
(e : c₁.pt ≅ c₂.pt)
(w : ∀ (b : β), CategoryTheory.CategoryStruct.comp (c₁.inj b) e.hom = c₂.inj b := by aesop_cat)
:
(CategoryTheory.Limits.Cofan.ext e w).hom.hom = e.hom
@[simp]
theorem
CategoryTheory.Limits.Cofan.ext_inv_hom
{β : Type w}
{C : Type u}
[CategoryTheory.Category.{v, u} C]
{f : β → C}
{c₁ c₂ : CategoryTheory.Limits.Cofan f}
(e : c₁.pt ≅ c₂.pt)
(w : ∀ (b : β), CategoryTheory.CategoryStruct.comp (c₁.inj b) e.hom = c₂.inj b := by aesop_cat)
:
(CategoryTheory.Limits.Cofan.ext e w).inv.hom = e.inv
def
CategoryTheory.Limits.Cofan.isColimitOfIsIsoSigmaDesc
{β : Type w}
{C : Type u}
[CategoryTheory.Category.{v, u} C]
{f : β → C}
[CategoryTheory.Limits.HasCoproduct f]
(c : CategoryTheory.Limits.Cofan f)
[hc : CategoryTheory.IsIso (CategoryTheory.Limits.Sigma.desc c.inj)]
:
A cofan c on f such that the induced map ∐ f ⟶ c.pt is an iso, is a coproduct.
Equations
- One or more equations did not get rendered due to their size.
theorem
CategoryTheory.Limits.Cofan.isColimit_iff_isIso_sigmaDesc
{β : Type w}
{C : Type u}
[CategoryTheory.Category.{v, u} C]
{f : β → C}
[CategoryTheory.Limits.HasCoproduct f]
(c : CategoryTheory.Limits.Cofan f)
:
def
CategoryTheory.Limits.Cofan.isColimitTrans
{α : Type w₂}
{C : Type u}
[CategoryTheory.Category.{v, u} C]
{X : α → C}
(c : CategoryTheory.Limits.Cofan X)
(hc : CategoryTheory.Limits.IsColimit c)
{β : α → Type u_1}
{Y : (a : α) → β a → C}
(π : (a : α) → (b : β a) → Y a b ⟶ X a)
(hs : (a : α) → CategoryTheory.Limits.IsColimit (CategoryTheory.Limits.Cofan.mk (X a) (π a)))
:
CategoryTheory.Limits.IsColimit
(CategoryTheory.Limits.Cofan.mk c.pt fun (x : (a : α) × β a) =>
match x with
| ⟨a, b⟩ => CategoryTheory.CategoryStruct.comp (π a b) (c.inj a))
A coproduct of coproducts is a coproduct
Equations
- One or more equations did not get rendered due to their size.
@[reducible, inline]
abbrev
CategoryTheory.Limits.Pi.map
{β : Type w}
{C : Type u}
[CategoryTheory.Category.{v, u} C]
{f g : β → C}
[CategoryTheory.Limits.HasProduct f]
[CategoryTheory.Limits.HasProduct g]
(p : (b : β) → f b ⟶ g b)
:
Construct a morphism between categorical products (indexed by the same type) from a family of morphisms between the factors.
Equations
- CategoryTheory.Limits.Pi.map p = CategoryTheory.Limits.limMap (CategoryTheory.Discrete.natTrans fun (X : CategoryTheory.Discrete β) => p X.as)
@[simp]
theorem
CategoryTheory.Limits.Pi.map_id
{α : Type w₂}
{C : Type u}
[CategoryTheory.Category.{v, u} C]
{f : α → C}
[CategoryTheory.Limits.HasProduct f]
:
(CategoryTheory.Limits.Pi.map fun (a : α) => CategoryTheory.CategoryStruct.id (f a)) = CategoryTheory.CategoryStruct.id (∏ᶜ f)
theorem
CategoryTheory.Limits.Pi.map_comp_map
{α : Type w₂}
{C : Type u}
[CategoryTheory.Category.{v, u} C]
{f g h : α → C}
[CategoryTheory.Limits.HasProduct f]
[CategoryTheory.Limits.HasProduct g]
[CategoryTheory.Limits.HasProduct h]
(q : (a : α) → f a ⟶ g a)
(q' : (a : α) → g a ⟶ h a)
:
CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.Pi.map q) (CategoryTheory.Limits.Pi.map q') = CategoryTheory.Limits.Pi.map fun (a : α) => CategoryTheory.CategoryStruct.comp (q a) (q' a)
instance
CategoryTheory.Limits.Pi.map_mono
{β : Type w}
{C : Type u}
[CategoryTheory.Category.{v, u} C]
{f g : β → C}
[CategoryTheory.Limits.HasProduct f]
[CategoryTheory.Limits.HasProduct g]
(p : (b : β) → f b ⟶ g b)
[∀ (i : β), CategoryTheory.Mono (p i)]
:
Equations
- ⋯ = ⋯
def
CategoryTheory.Limits.Pi.map'
{β : Type w}
{α : Type w₂}
{C : Type u}
[CategoryTheory.Category.{v, u} C]
{f : α → C}
{g : β → C}
[CategoryTheory.Limits.HasProduct f]
[CategoryTheory.Limits.HasProduct g]
(p : β → α)
(q : (b : β) → f (p b) ⟶ g b)
:
Construct a morphism between categorical products from a family of morphisms between the factors.
Equations
- CategoryTheory.Limits.Pi.map' p q = CategoryTheory.Limits.Pi.lift fun (a : β) => CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.Pi.π f (p a)) (q a)
@[simp]
theorem
CategoryTheory.Limits.Pi.map'_comp_π
{β : Type w}
{α : Type w₂}
{C : Type u}
[CategoryTheory.Category.{v, u} C]
{f : α → C}
{g : β → C}
[CategoryTheory.Limits.HasProduct f]
[CategoryTheory.Limits.HasProduct g]
(p : β → α)
(q : (b : β) → f (p b) ⟶ g b)
(b : β)
:
@[simp]
theorem
CategoryTheory.Limits.Pi.map'_comp_π_assoc
{β : Type w}
{α : Type w₂}
{C : Type u}
[CategoryTheory.Category.{v, u} C]
{f : α → C}
{g : β → C}
[CategoryTheory.Limits.HasProduct f]
[CategoryTheory.Limits.HasProduct g]
(p : β → α)
(q : (b : β) → f (p b) ⟶ g b)
(b : β)
{Z : C}
(h : g b ⟶ Z)
:
theorem
CategoryTheory.Limits.Pi.map'_id_id
{α : Type w₂}
{C : Type u}
[CategoryTheory.Category.{v, u} C]
{f : α → C}
[CategoryTheory.Limits.HasProduct f]
:
(CategoryTheory.Limits.Pi.map' id fun (a : α) => CategoryTheory.CategoryStruct.id (f a)) = CategoryTheory.CategoryStruct.id (∏ᶜ f)
@[simp]
theorem
CategoryTheory.Limits.Pi.map'_id
{α : Type w₂}
{C : Type u}
[CategoryTheory.Category.{v, u} C]
{f g : α → C}
[CategoryTheory.Limits.HasProduct f]
[CategoryTheory.Limits.HasProduct g]
(p : (b : α) → f b ⟶ g b)
:
theorem
CategoryTheory.Limits.Pi.map'_comp_map'
{β : Type w}
{α : Type w₂}
{γ : Type w₃}
{C : Type u}
[CategoryTheory.Category.{v, u} C]
{f : α → C}
{g : β → C}
{h : γ → C}
[CategoryTheory.Limits.HasProduct f]
[CategoryTheory.Limits.HasProduct g]
[CategoryTheory.Limits.HasProduct h]
(p : β → α)
(p' : γ → β)
(q : (b : β) → f (p b) ⟶ g b)
(q' : (c : γ) → g (p' c) ⟶ h c)
:
CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.Pi.map' p q) (CategoryTheory.Limits.Pi.map' p' q') = CategoryTheory.Limits.Pi.map' (p ∘ p') fun (c : γ) => CategoryTheory.CategoryStruct.comp (q (p' c)) (q' c)
theorem
CategoryTheory.Limits.Pi.map'_comp_map
{β : Type w}
{α : Type w₂}
{C : Type u}
[CategoryTheory.Category.{v, u} C]
{f : α → C}
{g h : β → C}
[CategoryTheory.Limits.HasProduct f]
[CategoryTheory.Limits.HasProduct g]
[CategoryTheory.Limits.HasProduct h]
(p : β → α)
(q : (b : β) → f (p b) ⟶ g b)
(q' : (b : β) → g b ⟶ h b)
:
CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.Pi.map' p q) (CategoryTheory.Limits.Pi.map q') = CategoryTheory.Limits.Pi.map' p fun (b : β) => CategoryTheory.CategoryStruct.comp (q b) (q' b)
theorem
CategoryTheory.Limits.Pi.map_comp_map'
{β : Type w}
{α : Type w₂}
{C : Type u}
[CategoryTheory.Category.{v, u} C]
{f g : α → C}
{h : β → C}
[CategoryTheory.Limits.HasProduct f]
[CategoryTheory.Limits.HasProduct g]
[CategoryTheory.Limits.HasProduct h]
(p : β → α)
(q : (a : α) → f a ⟶ g a)
(q' : (b : β) → g (p b) ⟶ h b)
:
CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.Pi.map q) (CategoryTheory.Limits.Pi.map' p q') = CategoryTheory.Limits.Pi.map' p fun (b : β) => CategoryTheory.CategoryStruct.comp (q (p b)) (q' b)
theorem
CategoryTheory.Limits.Pi.map'_eq
{β : Type w}
{α : Type w₂}
{C : Type u}
[CategoryTheory.Category.{v, u} C]
{f : α → C}
{g : β → C}
[CategoryTheory.Limits.HasProduct f]
[CategoryTheory.Limits.HasProduct g]
{p p' : β → α}
{q : (b : β) → f (p b) ⟶ g b}
{q' : (b : β) → f (p' b) ⟶ g b}
(hp : p = p')
(hq : ∀ (b : β), CategoryTheory.CategoryStruct.comp (CategoryTheory.eqToHom ⋯) (q b) = q' b)
:
@[reducible, inline]
abbrev
CategoryTheory.Limits.Pi.mapIso
{β : Type w}
{C : Type u}
[CategoryTheory.Category.{v, u} C]
{f g : β → C}
[CategoryTheory.Limits.HasProductsOfShape β C]
(p : (b : β) → f b ≅ g b)
:
Construct an isomorphism between categorical products (indexed by the same type) from a family of isomorphisms between the factors.
Equations
- CategoryTheory.Limits.Pi.mapIso p = CategoryTheory.Limits.lim.mapIso (CategoryTheory.Discrete.natIso fun (X : CategoryTheory.Discrete β) => p X.as)
instance
CategoryTheory.Limits.Pi.map_isIso
{β : Type w}
{C : Type u}
[CategoryTheory.Category.{v, u} C]
{f g : β → C}
[CategoryTheory.Limits.HasProductsOfShape β C]
(p : (b : β) → f b ⟶ g b)
[∀ (b : β), CategoryTheory.IsIso (p b)]
:
Equations
- ⋯ = ⋯
def
CategoryTheory.Limits.Pi.cone
{α : Type w₂}
{C : Type u}
[CategoryTheory.Category.{v, u} C]
(X : CategoryTheory.Functor (CategoryTheory.Discrete α) C)
[CategoryTheory.Limits.HasProduct fun (j : α) => X.obj { as := j }]
:
A limit cone for X : Discrete α ⥤ C that is given
by ∏ᶜ (fun j => X.obj (Discrete.mk j)).
Equations
- One or more equations did not get rendered due to their size.
@[simp]
theorem
CategoryTheory.Limits.Pi.cone_pt
{α : Type w₂}
{C : Type u}
[CategoryTheory.Category.{v, u} C]
(X : CategoryTheory.Functor (CategoryTheory.Discrete α) C)
[CategoryTheory.Limits.HasProduct fun (j : α) => X.obj { as := j }]
:
(CategoryTheory.Limits.Pi.cone X).pt = ∏ᶜ fun (j : α) => X.obj { as := j }
@[simp]
theorem
CategoryTheory.Limits.Pi.cone_π
{α : Type w₂}
{C : Type u}
[CategoryTheory.Category.{v, u} C]
(X : CategoryTheory.Functor (CategoryTheory.Discrete α) C)
[CategoryTheory.Limits.HasProduct fun (j : α) => X.obj { as := j }]
:
(CategoryTheory.Limits.Pi.cone X).π = CategoryTheory.Discrete.natTrans fun (x : CategoryTheory.Discrete α) =>
CategoryTheory.Limits.Pi.π (fun (j : α) => X.obj { as := j }) x.as
def
CategoryTheory.Limits.productIsProduct'
{α : Type w₂}
{C : Type u}
[CategoryTheory.Category.{v, u} C]
(X : CategoryTheory.Functor (CategoryTheory.Discrete α) C)
[CategoryTheory.Limits.HasProduct fun (j : α) => X.obj { as := j }]
:
The cone Pi.cone X is a limit cone.
Equations
- CategoryTheory.Limits.productIsProduct' X = { lift := fun (s : CategoryTheory.Limits.Cone X) => CategoryTheory.Limits.Pi.lift fun (j : α) => s.π.app { as := j }, fac := ⋯, uniq := ⋯ }
def
CategoryTheory.Limits.Pi.isoLimit
{α : Type w₂}
{C : Type u}
[CategoryTheory.Category.{v, u} C]
(X : CategoryTheory.Functor (CategoryTheory.Discrete α) C)
[CategoryTheory.Limits.HasProduct fun (j : α) => X.obj { as := j }]
[CategoryTheory.Limits.HasLimit X]
:
(∏ᶜ fun (j : α) => X.obj { as := j }) ≅ CategoryTheory.Limits.limit X
The isomorphism ∏ᶜ (fun j => X.obj (Discrete.mk j)) ≅ limit X.
Equations
- CategoryTheory.Limits.Pi.isoLimit X = (CategoryTheory.Limits.productIsProduct' X).conePointUniqueUpToIso (CategoryTheory.Limits.limit.isLimit X)
@[simp]
theorem
CategoryTheory.Limits.Pi.isoLimit_inv_π
{α : Type w₂}
{C : Type u}
[CategoryTheory.Category.{v, u} C]
(X : CategoryTheory.Functor (CategoryTheory.Discrete α) C)
[CategoryTheory.Limits.HasProduct fun (j : α) => X.obj { as := j }]
[CategoryTheory.Limits.HasLimit X]
(j : α)
:
CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.Pi.isoLimit X).inv
(CategoryTheory.Limits.Pi.π (fun (j : α) => X.obj { as := j }) j) = CategoryTheory.Limits.limit.π X { as := j }
@[simp]
theorem
CategoryTheory.Limits.Pi.isoLimit_inv_π_assoc
{α : Type w₂}
{C : Type u}
[CategoryTheory.Category.{v, u} C]
(X : CategoryTheory.Functor (CategoryTheory.Discrete α) C)
[CategoryTheory.Limits.HasProduct fun (j : α) => X.obj { as := j }]
[CategoryTheory.Limits.HasLimit X]
(j : α)
{Z : C}
(h : X.obj { as := j } ⟶ Z)
:
CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.Pi.isoLimit X).inv
(CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.Pi.π (fun (j : α) => X.obj { as := j }) j) h) = CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.limit.π X { as := j }) h
@[simp]
theorem
CategoryTheory.Limits.Pi.isoLimit_hom_π
{α : Type w₂}
{C : Type u}
[CategoryTheory.Category.{v, u} C]
(X : CategoryTheory.Functor (CategoryTheory.Discrete α) C)
[CategoryTheory.Limits.HasProduct fun (j : α) => X.obj { as := j }]
[CategoryTheory.Limits.HasLimit X]
(j : α)
:
CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.Pi.isoLimit X).hom
(CategoryTheory.Limits.limit.π X { as := j }) = CategoryTheory.Limits.Pi.π (fun (j : α) => X.obj { as := j }) j
@[simp]
theorem
CategoryTheory.Limits.Pi.isoLimit_hom_π_assoc
{α : Type w₂}
{C : Type u}
[CategoryTheory.Category.{v, u} C]
(X : CategoryTheory.Functor (CategoryTheory.Discrete α) C)
[CategoryTheory.Limits.HasProduct fun (j : α) => X.obj { as := j }]
[CategoryTheory.Limits.HasLimit X]
(j : α)
{Z : C}
(h : X.obj { as := j } ⟶ Z)
:
CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.Pi.isoLimit X).hom
(CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.limit.π X { as := j }) h) = CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.Pi.π (fun (j : α) => X.obj { as := j }) j) h
@[reducible, inline]
abbrev
CategoryTheory.Limits.Sigma.map
{β : Type w}
{C : Type u}
[CategoryTheory.Category.{v, u} C]
{f g : β → C}
[CategoryTheory.Limits.HasCoproduct f]
[CategoryTheory.Limits.HasCoproduct g]
(p : (b : β) → f b ⟶ g b)
:
Construct a morphism between categorical coproducts (indexed by the same type) from a family of morphisms between the factors.
Equations
- CategoryTheory.Limits.Sigma.map p = CategoryTheory.Limits.colimMap (CategoryTheory.Discrete.natTrans fun (X : CategoryTheory.Discrete β) => p X.as)
@[simp]
theorem
CategoryTheory.Limits.Sigma.map_id
{α : Type w₂}
{C : Type u}
[CategoryTheory.Category.{v, u} C]
{f : α → C}
[CategoryTheory.Limits.HasCoproduct f]
:
(CategoryTheory.Limits.Sigma.map fun (a : α) => CategoryTheory.CategoryStruct.id (f a)) = CategoryTheory.CategoryStruct.id (∐ f)
theorem
CategoryTheory.Limits.Sigma.map_comp_map
{α : Type w₂}
{C : Type u}
[CategoryTheory.Category.{v, u} C]
{f g h : α → C}
[CategoryTheory.Limits.HasCoproduct f]
[CategoryTheory.Limits.HasCoproduct g]
[CategoryTheory.Limits.HasCoproduct h]
(q : (a : α) → f a ⟶ g a)
(q' : (a : α) → g a ⟶ h a)
:
CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.Sigma.map q) (CategoryTheory.Limits.Sigma.map q') = CategoryTheory.Limits.Sigma.map fun (a : α) => CategoryTheory.CategoryStruct.comp (q a) (q' a)
instance
CategoryTheory.Limits.Sigma.map_epi
{β : Type w}
{C : Type u}
[CategoryTheory.Category.{v, u} C]
{f g : β → C}
[CategoryTheory.Limits.HasCoproduct f]
[CategoryTheory.Limits.HasCoproduct g]
(p : (b : β) → f b ⟶ g b)
[∀ (i : β), CategoryTheory.Epi (p i)]
:
Equations
- ⋯ = ⋯
def
CategoryTheory.Limits.Sigma.map'
{β : Type w}
{α : Type w₂}
{C : Type u}
[CategoryTheory.Category.{v, u} C]
{f : α → C}
{g : β → C}
[CategoryTheory.Limits.HasCoproduct f]
[CategoryTheory.Limits.HasCoproduct g]
(p : α → β)
(q : (a : α) → f a ⟶ g (p a))
:
Construct a morphism between categorical coproducts from a family of morphisms between the factors.
Equations
- CategoryTheory.Limits.Sigma.map' p q = CategoryTheory.Limits.Sigma.desc fun (a : α) => CategoryTheory.CategoryStruct.comp (q a) (CategoryTheory.Limits.Sigma.ι g (p a))
@[simp]
theorem
CategoryTheory.Limits.Sigma.ι_comp_map'
{β : Type w}
{α : Type w₂}
{C : Type u}
[CategoryTheory.Category.{v, u} C]
{f : α → C}
{g : β → C}
[CategoryTheory.Limits.HasCoproduct f]
[CategoryTheory.Limits.HasCoproduct g]
(p : α → β)
(q : (a : α) → f a ⟶ g (p a))
(a : α)
:
@[simp]
theorem
CategoryTheory.Limits.Sigma.ι_comp_map'_assoc
{β : Type w}
{α : Type w₂}
{C : Type u}
[CategoryTheory.Category.{v, u} C]
{f : α → C}
{g : β → C}
[CategoryTheory.Limits.HasCoproduct f]
[CategoryTheory.Limits.HasCoproduct g]
(p : α → β)
(q : (a : α) → f a ⟶ g (p a))
(a : α)
{Z : C}
(h : ∐ g ⟶ Z)
:
theorem
CategoryTheory.Limits.Sigma.map'_id_id
{α : Type w₂}
{C : Type u}
[CategoryTheory.Category.{v, u} C]
{f : α → C}
[CategoryTheory.Limits.HasCoproduct f]
:
(CategoryTheory.Limits.Sigma.map' id fun (a : α) => CategoryTheory.CategoryStruct.id (f a)) = CategoryTheory.CategoryStruct.id (∐ f)
@[simp]
theorem
CategoryTheory.Limits.Sigma.map'_id
{α : Type w₂}
{C : Type u}
[CategoryTheory.Category.{v, u} C]
{f g : α → C}
[CategoryTheory.Limits.HasCoproduct f]
[CategoryTheory.Limits.HasCoproduct g]
(p : (b : α) → f b ⟶ g b)
:
theorem
CategoryTheory.Limits.Sigma.map'_comp_map'
{β : Type w}
{α : Type w₂}
{γ : Type w₃}
{C : Type u}
[CategoryTheory.Category.{v, u} C]
{f : α → C}
{g : β → C}
{h : γ → C}
[CategoryTheory.Limits.HasCoproduct f]
[CategoryTheory.Limits.HasCoproduct g]
[CategoryTheory.Limits.HasCoproduct h]
(p : α → β)
(p' : β → γ)
(q : (a : α) → f a ⟶ g (p a))
(q' : (b : β) → g b ⟶ h (p' b))
:
CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.Sigma.map' p q) (CategoryTheory.Limits.Sigma.map' p' q') = CategoryTheory.Limits.Sigma.map' (p' ∘ p) fun (a : α) => CategoryTheory.CategoryStruct.comp (q a) (q' (p a))
theorem
CategoryTheory.Limits.Sigma.map'_comp_map
{β : Type w}
{α : Type w₂}
{C : Type u}
[CategoryTheory.Category.{v, u} C]
{f : α → C}
{g h : β → C}
[CategoryTheory.Limits.HasCoproduct f]
[CategoryTheory.Limits.HasCoproduct g]
[CategoryTheory.Limits.HasCoproduct h]
(p : α → β)
(q : (a : α) → f a ⟶ g (p a))
(q' : (b : β) → g b ⟶ h b)
:
CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.Sigma.map' p q) (CategoryTheory.Limits.Sigma.map q') = CategoryTheory.Limits.Sigma.map' p fun (a : α) => CategoryTheory.CategoryStruct.comp (q a) (q' (p a))
theorem
CategoryTheory.Limits.Sigma.map_comp_map'
{β : Type w}
{α : Type w₂}
{C : Type u}
[CategoryTheory.Category.{v, u} C]
{f g : α → C}
{h : β → C}
[CategoryTheory.Limits.HasCoproduct f]
[CategoryTheory.Limits.HasCoproduct g]
[CategoryTheory.Limits.HasCoproduct h]
(p : α → β)
(q : (a : α) → f a ⟶ g a)
(q' : (a : α) → g a ⟶ h (p a))
:
CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.Sigma.map q) (CategoryTheory.Limits.Sigma.map' p q') = CategoryTheory.Limits.Sigma.map' p fun (a : α) => CategoryTheory.CategoryStruct.comp (q a) (q' a)
theorem
CategoryTheory.Limits.Sigma.map'_eq
{β : Type w}
{α : Type w₂}
{C : Type u}
[CategoryTheory.Category.{v, u} C]
{f : α → C}
{g : β → C}
[CategoryTheory.Limits.HasCoproduct f]
[CategoryTheory.Limits.HasCoproduct g]
{p p' : α → β}
{q : (a : α) → f a ⟶ g (p a)}
{q' : (a : α) → f a ⟶ g (p' a)}
(hp : p = p')
(hq : ∀ (a : α), CategoryTheory.CategoryStruct.comp (q a) (CategoryTheory.eqToHom ⋯) = q' a)
:
@[reducible, inline]
abbrev
CategoryTheory.Limits.Sigma.mapIso
{β : Type w}
{C : Type u}
[CategoryTheory.Category.{v, u} C]
{f g : β → C}
[CategoryTheory.Limits.HasCoproductsOfShape β C]
(p : (b : β) → f b ≅ g b)
:
Construct an isomorphism between categorical coproducts (indexed by the same type) from a family of isomorphisms between the factors.
Equations
- CategoryTheory.Limits.Sigma.mapIso p = CategoryTheory.Limits.colim.mapIso (CategoryTheory.Discrete.natIso fun (X : CategoryTheory.Discrete β) => p X.as)
instance
CategoryTheory.Limits.Sigma.map_isIso
{β : Type w}
{C : Type u}
[CategoryTheory.Category.{v, u} C]
{f g : β → C}
[CategoryTheory.Limits.HasCoproductsOfShape β C]
(p : (b : β) → f b ⟶ g b)
[∀ (b : β), CategoryTheory.IsIso (p b)]
:
Equations
- ⋯ = ⋯
def
CategoryTheory.Limits.Sigma.cocone
{α : Type w₂}
{C : Type u}
[CategoryTheory.Category.{v, u} C]
(X : CategoryTheory.Functor (CategoryTheory.Discrete α) C)
[CategoryTheory.Limits.HasCoproduct fun (j : α) => X.obj { as := j }]
:
A colimit cocone for X : Discrete α ⥤ C that is given
by ∐ (fun j => X.obj (Discrete.mk j)).
Equations
- One or more equations did not get rendered due to their size.
@[simp]
theorem
CategoryTheory.Limits.Sigma.cocone_pt
{α : Type w₂}
{C : Type u}
[CategoryTheory.Category.{v, u} C]
(X : CategoryTheory.Functor (CategoryTheory.Discrete α) C)
[CategoryTheory.Limits.HasCoproduct fun (j : α) => X.obj { as := j }]
:
(CategoryTheory.Limits.Sigma.cocone X).pt = ∐ fun (j : α) => X.obj { as := j }
@[simp]
theorem
CategoryTheory.Limits.Sigma.cocone_ι
{α : Type w₂}
{C : Type u}
[CategoryTheory.Category.{v, u} C]
(X : CategoryTheory.Functor (CategoryTheory.Discrete α) C)
[CategoryTheory.Limits.HasCoproduct fun (j : α) => X.obj { as := j }]
:
(CategoryTheory.Limits.Sigma.cocone X).ι = CategoryTheory.Discrete.natTrans fun (x : CategoryTheory.Discrete α) =>
CategoryTheory.Limits.Sigma.ι (fun (j : α) => X.obj { as := j }) x.as
def
CategoryTheory.Limits.coproductIsCoproduct'
{α : Type w₂}
{C : Type u}
[CategoryTheory.Category.{v, u} C]
(X : CategoryTheory.Functor (CategoryTheory.Discrete α) C)
[CategoryTheory.Limits.HasCoproduct fun (j : α) => X.obj { as := j }]
:
The cocone Sigma.cocone X is a colimit cocone.
Equations
- One or more equations did not get rendered due to their size.
def
CategoryTheory.Limits.Sigma.isoColimit
{α : Type w₂}
{C : Type u}
[CategoryTheory.Category.{v, u} C]
(X : CategoryTheory.Functor (CategoryTheory.Discrete α) C)
[CategoryTheory.Limits.HasCoproduct fun (j : α) => X.obj { as := j }]
[CategoryTheory.Limits.HasColimit X]
:
(∐ fun (j : α) => X.obj { as := j }) ≅ CategoryTheory.Limits.colimit X
The isomorphism ∐ (fun j => X.obj (Discrete.mk j)) ≅ colimit X.
Equations
- CategoryTheory.Limits.Sigma.isoColimit X = (CategoryTheory.Limits.coproductIsCoproduct' X).coconePointUniqueUpToIso (CategoryTheory.Limits.colimit.isColimit X)
@[simp]
theorem
CategoryTheory.Limits.Sigma.ι_isoColimit_hom
{α : Type w₂}
{C : Type u}
[CategoryTheory.Category.{v, u} C]
(X : CategoryTheory.Functor (CategoryTheory.Discrete α) C)
[CategoryTheory.Limits.HasCoproduct fun (j : α) => X.obj { as := j }]
[CategoryTheory.Limits.HasColimit X]
(j : α)
:
CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.Sigma.ι (fun (j : α) => X.obj { as := j }) j)
(CategoryTheory.Limits.Sigma.isoColimit X).hom = CategoryTheory.Limits.colimit.ι X { as := j }
@[simp]
theorem
CategoryTheory.Limits.Sigma.ι_isoColimit_hom_assoc
{α : Type w₂}
{C : Type u}
[CategoryTheory.Category.{v, u} C]
(X : CategoryTheory.Functor (CategoryTheory.Discrete α) C)
[CategoryTheory.Limits.HasCoproduct fun (j : α) => X.obj { as := j }]
[CategoryTheory.Limits.HasColimit X]
(j : α)
{Z : C}
(h : CategoryTheory.Limits.colimit X ⟶ Z)
:
CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.Sigma.ι (fun (j : α) => X.obj { as := j }) j)
(CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.Sigma.isoColimit X).hom h) = CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.colimit.ι X { as := j }) h
@[simp]
theorem
CategoryTheory.Limits.Sigma.ι_isoColimit_inv
{α : Type w₂}
{C : Type u}
[CategoryTheory.Category.{v, u} C]
(X : CategoryTheory.Functor (CategoryTheory.Discrete α) C)
[CategoryTheory.Limits.HasCoproduct fun (j : α) => X.obj { as := j }]
[CategoryTheory.Limits.HasColimit X]
(j : α)
:
CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.colimit.ι X { as := j })
(CategoryTheory.Limits.Sigma.isoColimit X).inv = CategoryTheory.Limits.Sigma.ι (fun (j : α) => X.obj { as := j }) j
@[simp]
theorem
CategoryTheory.Limits.Sigma.ι_isoColimit_inv_assoc
{α : Type w₂}
{C : Type u}
[CategoryTheory.Category.{v, u} C]
(X : CategoryTheory.Functor (CategoryTheory.Discrete α) C)
[CategoryTheory.Limits.HasCoproduct fun (j : α) => X.obj { as := j }]
[CategoryTheory.Limits.HasColimit X]
(j : α)
{Z : C}
(h : (∐ fun (j : α) => X.obj { as := j }) ⟶ Z)
:
CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.colimit.ι X { as := j })
(CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.Sigma.isoColimit X).inv h) = CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.Sigma.ι (fun (j : α) => X.obj { as := j }) j) h
def
CategoryTheory.Limits.Pi.whiskerEquiv
{C : Type u}
[CategoryTheory.Category.{v, u} C]
{J : Type u_1}
{K : Type u_2}
{f : J → C}
{g : K → C}
(e : J ≃ K)
(w : (j : J) → g (e j) ≅ f j)
[CategoryTheory.Limits.HasProduct f]
[CategoryTheory.Limits.HasProduct g]
:
Two products which differ by an equivalence in the indexing type, and up to isomorphism in the factors, are isomorphic.
Equations
- One or more equations did not get rendered due to their size.
@[simp]
theorem
CategoryTheory.Limits.Pi.whiskerEquiv_inv
{C : Type u}
[CategoryTheory.Category.{v, u} C]
{J : Type u_1}
{K : Type u_2}
{f : J → C}
{g : K → C}
(e : J ≃ K)
(w : (j : J) → g (e j) ≅ f j)
[CategoryTheory.Limits.HasProduct f]
[CategoryTheory.Limits.HasProduct g]
:
(CategoryTheory.Limits.Pi.whiskerEquiv e w).inv = CategoryTheory.Limits.Pi.map' ⇑e fun (j : J) => (w j).hom
@[simp]
theorem
CategoryTheory.Limits.Pi.whiskerEquiv_hom
{C : Type u}
[CategoryTheory.Category.{v, u} C]
{J : Type u_1}
{K : Type u_2}
{f : J → C}
{g : K → C}
(e : J ≃ K)
(w : (j : J) → g (e j) ≅ f j)
[CategoryTheory.Limits.HasProduct f]
[CategoryTheory.Limits.HasProduct g]
:
(CategoryTheory.Limits.Pi.whiskerEquiv e w).hom = CategoryTheory.Limits.Pi.map' ⇑e.symm fun (k : K) =>
CategoryTheory.CategoryStruct.comp (w (e.symm k)).inv (CategoryTheory.eqToHom ⋯)
def
CategoryTheory.Limits.Sigma.whiskerEquiv
{C : Type u}
[CategoryTheory.Category.{v, u} C]
{J : Type u_1}
{K : Type u_2}
{f : J → C}
{g : K → C}
(e : J ≃ K)
(w : (j : J) → g (e j) ≅ f j)
[CategoryTheory.Limits.HasCoproduct f]
[CategoryTheory.Limits.HasCoproduct g]
:
Two coproducts which differ by an equivalence in the indexing type, and up to isomorphism in the factors, are isomorphic.
Equations
- One or more equations did not get rendered due to their size.
@[simp]
theorem
CategoryTheory.Limits.Sigma.whiskerEquiv_hom
{C : Type u}
[CategoryTheory.Category.{v, u} C]
{J : Type u_1}
{K : Type u_2}
{f : J → C}
{g : K → C}
(e : J ≃ K)
(w : (j : J) → g (e j) ≅ f j)
[CategoryTheory.Limits.HasCoproduct f]
[CategoryTheory.Limits.HasCoproduct g]
:
(CategoryTheory.Limits.Sigma.whiskerEquiv e w).hom = CategoryTheory.Limits.Sigma.map' ⇑e fun (j : J) => (w j).inv
@[simp]
theorem
CategoryTheory.Limits.Sigma.whiskerEquiv_inv
{C : Type u}
[CategoryTheory.Category.{v, u} C]
{J : Type u_1}
{K : Type u_2}
{f : J → C}
{g : K → C}
(e : J ≃ K)
(w : (j : J) → g (e j) ≅ f j)
[CategoryTheory.Limits.HasCoproduct f]
[CategoryTheory.Limits.HasCoproduct g]
:
(CategoryTheory.Limits.Sigma.whiskerEquiv e w).inv = CategoryTheory.Limits.Sigma.map' ⇑e.symm fun (k : K) =>
CategoryTheory.CategoryStruct.comp (CategoryTheory.eqToHom ⋯) (w (e.symm k)).hom
instance
CategoryTheory.Limits.instHasProductSigmaFstSndOfPiObj
{C : Type u}
[CategoryTheory.Category.{v, u} C]
{ι : Type u_1}
(f : ι → Type u_2)
(g : (i : ι) → f i → C)
[∀ (i : ι), CategoryTheory.Limits.HasProduct (g i)]
[CategoryTheory.Limits.HasProduct fun (i : ι) => ∏ᶜ g i]
:
CategoryTheory.Limits.HasProduct fun (p : (i : ι) × f i) => g p.fst p.snd
Equations
- ⋯ = ⋯
def
CategoryTheory.Limits.piPiIso
{C : Type u}
[CategoryTheory.Category.{v, u} C]
{ι : Type u_1}
(f : ι → Type u_2)
(g : (i : ι) → f i → C)
[∀ (i : ι), CategoryTheory.Limits.HasProduct (g i)]
[CategoryTheory.Limits.HasProduct fun (i : ι) => ∏ᶜ g i]
:
An iterated product is a product over a sigma type.
Equations
- One or more equations did not get rendered due to their size.
@[simp]
theorem
CategoryTheory.Limits.piPiIso_hom
{C : Type u}
[CategoryTheory.Category.{v, u} C]
{ι : Type u_1}
(f : ι → Type u_2)
(g : (i : ι) → f i → C)
[∀ (i : ι), CategoryTheory.Limits.HasProduct (g i)]
[CategoryTheory.Limits.HasProduct fun (i : ι) => ∏ᶜ g i]
:
(CategoryTheory.Limits.piPiIso f g).hom = CategoryTheory.Limits.Pi.lift fun (x : (i : ι) × f i) =>
match x with
| ⟨i, x⟩ =>
CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.Pi.π (fun (i : ι) => ∏ᶜ g i) i)
(CategoryTheory.Limits.Pi.π (g i) x)
@[simp]
theorem
CategoryTheory.Limits.piPiIso_inv
{C : Type u}
[CategoryTheory.Category.{v, u} C]
{ι : Type u_1}
(f : ι → Type u_2)
(g : (i : ι) → f i → C)
[∀ (i : ι), CategoryTheory.Limits.HasProduct (g i)]
[CategoryTheory.Limits.HasProduct fun (i : ι) => ∏ᶜ g i]
:
(CategoryTheory.Limits.piPiIso f g).inv = CategoryTheory.Limits.Pi.lift fun (i : ι) =>
CategoryTheory.Limits.Pi.lift fun (x : f i) =>
CategoryTheory.Limits.Pi.π (fun (p : (i : ι) × f i) => g p.fst p.snd) ⟨i, x⟩
instance
CategoryTheory.Limits.instHasCoproductSigmaFstSndOfSigmaObj
{C : Type u}
[CategoryTheory.Category.{v, u} C]
{ι : Type u_1}
(f : ι → Type u_2)
(g : (i : ι) → f i → C)
[∀ (i : ι), CategoryTheory.Limits.HasCoproduct (g i)]
[CategoryTheory.Limits.HasCoproduct fun (i : ι) => ∐ g i]
:
CategoryTheory.Limits.HasCoproduct fun (p : (i : ι) × f i) => g p.fst p.snd
Equations
- ⋯ = ⋯
def
CategoryTheory.Limits.sigmaSigmaIso
{C : Type u}
[CategoryTheory.Category.{v, u} C]
{ι : Type u_1}
(f : ι → Type u_2)
(g : (i : ι) → f i → C)
[∀ (i : ι), CategoryTheory.Limits.HasCoproduct (g i)]
[CategoryTheory.Limits.HasCoproduct fun (i : ι) => ∐ g i]
:
An iterated coproduct is a coproduct over a sigma type.
Equations
- One or more equations did not get rendered due to their size.
@[simp]
theorem
CategoryTheory.Limits.sigmaSigmaIso_inv
{C : Type u}
[CategoryTheory.Category.{v, u} C]
{ι : Type u_1}
(f : ι → Type u_2)
(g : (i : ι) → f i → C)
[∀ (i : ι), CategoryTheory.Limits.HasCoproduct (g i)]
[CategoryTheory.Limits.HasCoproduct fun (i : ι) => ∐ g i]
:
(CategoryTheory.Limits.sigmaSigmaIso f g).inv = CategoryTheory.Limits.Sigma.desc fun (x : (i : ι) × f i) =>
match x with
| ⟨i, x⟩ =>
CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.Sigma.ι (g i) x)
(CategoryTheory.Limits.Sigma.ι (fun (i : ι) => ∐ g i) i)
@[simp]
theorem
CategoryTheory.Limits.sigmaSigmaIso_hom
{C : Type u}
[CategoryTheory.Category.{v, u} C]
{ι : Type u_1}
(f : ι → Type u_2)
(g : (i : ι) → f i → C)
[∀ (i : ι), CategoryTheory.Limits.HasCoproduct (g i)]
[CategoryTheory.Limits.HasCoproduct fun (i : ι) => ∐ g i]
:
(CategoryTheory.Limits.sigmaSigmaIso f g).hom = CategoryTheory.Limits.Sigma.desc fun (i : ι) =>
CategoryTheory.Limits.Sigma.desc fun (x : f i) =>
CategoryTheory.Limits.Sigma.ι (fun (p : (i : ι) × f i) => g p.fst p.snd) ⟨i, x⟩
def
CategoryTheory.Limits.piComparison
{β : Type w}
{C : Type u}
[CategoryTheory.Category.{v, u} C]
{D : Type u₂}
[CategoryTheory.Category.{v₂, u₂} D]
(G : CategoryTheory.Functor C D)
(f : β → C)
[CategoryTheory.Limits.HasProduct f]
[CategoryTheory.Limits.HasProduct fun (b : β) => G.obj (f b)]
:
The comparison morphism for the product of f. This is an iso iff G preserves the product
of f, see PreservesProduct.ofIsoComparison.
Equations
- CategoryTheory.Limits.piComparison G f = CategoryTheory.Limits.Pi.lift fun (b : β) => G.map (CategoryTheory.Limits.Pi.π f b)
@[simp]
theorem
CategoryTheory.Limits.piComparison_comp_π
{β : Type w}
{C : Type u}
[CategoryTheory.Category.{v, u} C]
{D : Type u₂}
[CategoryTheory.Category.{v₂, u₂} D]
(G : CategoryTheory.Functor C D)
(f : β → C)
[CategoryTheory.Limits.HasProduct f]
[CategoryTheory.Limits.HasProduct fun (b : β) => G.obj (f b)]
(b : β)
:
CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.piComparison G f)
(CategoryTheory.Limits.Pi.π (fun (b : β) => G.obj (f b)) b) = G.map (CategoryTheory.Limits.Pi.π f b)
@[simp]
theorem
CategoryTheory.Limits.piComparison_comp_π_assoc
{β : Type w}
{C : Type u}
[CategoryTheory.Category.{v, u} C]
{D : Type u₂}
[CategoryTheory.Category.{v₂, u₂} D]
(G : CategoryTheory.Functor C D)
(f : β → C)
[CategoryTheory.Limits.HasProduct f]
[CategoryTheory.Limits.HasProduct fun (b : β) => G.obj (f b)]
(b : β)
{Z : D}
(h : G.obj (f b) ⟶ Z)
:
CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.piComparison G f)
(CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.Pi.π (fun (b : β) => G.obj (f b)) b) h) = CategoryTheory.CategoryStruct.comp (G.map (CategoryTheory.Limits.Pi.π f b)) h
@[simp]
theorem
CategoryTheory.Limits.map_lift_piComparison
{β : Type w}
{C : Type u}
[CategoryTheory.Category.{v, u} C]
{D : Type u₂}
[CategoryTheory.Category.{v₂, u₂} D]
(G : CategoryTheory.Functor C D)
(f : β → C)
[CategoryTheory.Limits.HasProduct f]
[CategoryTheory.Limits.HasProduct fun (b : β) => G.obj (f b)]
(P : C)
(g : (j : β) → P ⟶ f j)
:
CategoryTheory.CategoryStruct.comp (G.map (CategoryTheory.Limits.Pi.lift g)) (CategoryTheory.Limits.piComparison G f) = CategoryTheory.Limits.Pi.lift fun (j : β) => G.map (g j)
@[simp]
theorem
CategoryTheory.Limits.map_lift_piComparison_assoc
{β : Type w}
{C : Type u}
[CategoryTheory.Category.{v, u} C]
{D : Type u₂}
[CategoryTheory.Category.{v₂, u₂} D]
(G : CategoryTheory.Functor C D)
(f : β → C)
[CategoryTheory.Limits.HasProduct f]
[CategoryTheory.Limits.HasProduct fun (b : β) => G.obj (f b)]
(P : C)
(g : (j : β) → P ⟶ f j)
{Z : D}
(h : (∏ᶜ fun (b : β) => G.obj (f b)) ⟶ Z)
:
CategoryTheory.CategoryStruct.comp (G.map (CategoryTheory.Limits.Pi.lift g))
(CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.piComparison G f) h) = CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.Pi.lift fun (j : β) => G.map (g j)) h
def
CategoryTheory.Limits.sigmaComparison
{β : Type w}
{C : Type u}
[CategoryTheory.Category.{v, u} C]
{D : Type u₂}
[CategoryTheory.Category.{v₂, u₂} D]
(G : CategoryTheory.Functor C D)
(f : β → C)
[CategoryTheory.Limits.HasCoproduct f]
[CategoryTheory.Limits.HasCoproduct fun (b : β) => G.obj (f b)]
:
The comparison morphism for the coproduct of f. This is an iso iff G preserves the coproduct
of f, see PreservesCoproduct.ofIsoComparison.
Equations
- CategoryTheory.Limits.sigmaComparison G f = CategoryTheory.Limits.Sigma.desc fun (b : β) => G.map (CategoryTheory.Limits.Sigma.ι f b)
@[simp]
theorem
CategoryTheory.Limits.ι_comp_sigmaComparison
{β : Type w}
{C : Type u}
[CategoryTheory.Category.{v, u} C]
{D : Type u₂}
[CategoryTheory.Category.{v₂, u₂} D]
(G : CategoryTheory.Functor C D)
(f : β → C)
[CategoryTheory.Limits.HasCoproduct f]
[CategoryTheory.Limits.HasCoproduct fun (b : β) => G.obj (f b)]
(b : β)
:
CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.Sigma.ι (fun (b : β) => G.obj (f b)) b)
(CategoryTheory.Limits.sigmaComparison G f) = G.map (CategoryTheory.Limits.Sigma.ι f b)
@[simp]
theorem
CategoryTheory.Limits.ι_comp_sigmaComparison_assoc
{β : Type w}
{C : Type u}
[CategoryTheory.Category.{v, u} C]
{D : Type u₂}
[CategoryTheory.Category.{v₂, u₂} D]
(G : CategoryTheory.Functor C D)
(f : β → C)
[CategoryTheory.Limits.HasCoproduct f]
[CategoryTheory.Limits.HasCoproduct fun (b : β) => G.obj (f b)]
(b : β)
{Z : D}
(h : G.obj (∐ f) ⟶ Z)
:
CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.Sigma.ι (fun (b : β) => G.obj (f b)) b)
(CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.sigmaComparison G f) h) = CategoryTheory.CategoryStruct.comp (G.map (CategoryTheory.Limits.Sigma.ι f b)) h
@[simp]
theorem
CategoryTheory.Limits.sigmaComparison_map_desc
{β : Type w}
{C : Type u}
[CategoryTheory.Category.{v, u} C]
{D : Type u₂}
[CategoryTheory.Category.{v₂, u₂} D]
(G : CategoryTheory.Functor C D)
(f : β → C)
[CategoryTheory.Limits.HasCoproduct f]
[CategoryTheory.Limits.HasCoproduct fun (b : β) => G.obj (f b)]
(P : C)
(g : (j : β) → f j ⟶ P)
:
CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.sigmaComparison G f)
(G.map (CategoryTheory.Limits.Sigma.desc g)) = CategoryTheory.Limits.Sigma.desc fun (j : β) => G.map (g j)
@[simp]
theorem
CategoryTheory.Limits.sigmaComparison_map_desc_assoc
{β : Type w}
{C : Type u}
[CategoryTheory.Category.{v, u} C]
{D : Type u₂}
[CategoryTheory.Category.{v₂, u₂} D]
(G : CategoryTheory.Functor C D)
(f : β → C)
[CategoryTheory.Limits.HasCoproduct f]
[CategoryTheory.Limits.HasCoproduct fun (b : β) => G.obj (f b)]
(P : C)
(g : (j : β) → f j ⟶ P)
{Z : D}
(h : G.obj P ⟶ Z)
:
CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.sigmaComparison G f)
(CategoryTheory.CategoryStruct.comp (G.map (CategoryTheory.Limits.Sigma.desc g)) h) = CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.Sigma.desc fun (j : β) => G.map (g j)) h
@[reducible, inline]
An abbreviation for Π J, HasLimitsOfShape (Discrete J) C
Equations
- CategoryTheory.Limits.HasProducts C = ∀ (J : Type ?u.18), CategoryTheory.Limits.HasLimitsOfShape (CategoryTheory.Discrete J) C
@[reducible, inline]
An abbreviation for Π J, HasColimitsOfShape (Discrete J) C
Equations
- CategoryTheory.Limits.HasCoproducts C = ∀ (J : Type ?u.18), CategoryTheory.Limits.HasColimitsOfShape (CategoryTheory.Discrete J) C
theorem
CategoryTheory.Limits.hasProducts_of_limit_fans
{C : Type u}
[CategoryTheory.Category.{v, u} C]
(lf : {J : Type w} → (f : J → C) → CategoryTheory.Limits.Fan f)
(lf_isLimit : {J : Type w} → (f : J → C) → CategoryTheory.Limits.IsLimit (lf f))
:
@[instance 100]
instance
CategoryTheory.Limits.hasProductsOfShape_of_hasProducts
{C : Type u}
[CategoryTheory.Category.{v, u} C]
[CategoryTheory.Limits.HasProducts C]
(J : Type w)
:
Equations
- ⋯ = ⋯
@[instance 100]
instance
CategoryTheory.Limits.hasCoproductsOfShape_of_hasCoproducts
{C : Type u}
[CategoryTheory.Category.{v, u} C]
[CategoryTheory.Limits.HasCoproducts C]
(J : Type w)
:
Equations
- ⋯ = ⋯
(Co)products over a type with a unique term.
def
CategoryTheory.Limits.limitConeOfUnique
{β : Type w}
{C : Type u}
[CategoryTheory.Category.{v, u} C]
[Unique β]
(f : β → C)
:
The limit cone for the product over an index type with exactly one term.
Equations
- One or more equations did not get rendered due to their size.
@[simp]
theorem
CategoryTheory.Limits.limitConeOfUnique_isLimit_lift
{β : Type w}
{C : Type u}
[CategoryTheory.Category.{v, u} C]
[Unique β]
(f : β → C)
(s : CategoryTheory.Limits.Cone (CategoryTheory.Discrete.functor f))
:
(CategoryTheory.Limits.limitConeOfUnique f).isLimit.lift s = s.π.app default
@[simp]
theorem
CategoryTheory.Limits.limitConeOfUnique_cone_pt
{β : Type w}
{C : Type u}
[CategoryTheory.Category.{v, u} C]
[Unique β]
(f : β → C)
:
(CategoryTheory.Limits.limitConeOfUnique f).cone.pt = f default
@[simp]
theorem
CategoryTheory.Limits.limitConeOfUnique_cone_π
{β : Type w}
{C : Type u}
[CategoryTheory.Category.{v, u} C]
[Unique β]
(f : β → C)
:
(CategoryTheory.Limits.limitConeOfUnique f).cone.π = CategoryTheory.Discrete.natTrans fun (x : CategoryTheory.Discrete β) =>
match x with
| { as := j } => CategoryTheory.eqToHom ⋯
@[instance 100]
instance
CategoryTheory.Limits.hasProduct_unique
{β : Type w}
{C : Type u}
[CategoryTheory.Category.{v, u} C]
[Nonempty β]
[Subsingleton β]
(f : β → C)
:
Equations
- ⋯ = ⋯
def
CategoryTheory.Limits.productUniqueIso
{β : Type w}
{C : Type u}
[CategoryTheory.Category.{v, u} C]
[Unique β]
(f : β → C)
:
A product over an index type with exactly one term is just the object over that term.
Equations
- CategoryTheory.Limits.productUniqueIso f = (CategoryTheory.Limits.limit.isLimit (CategoryTheory.Discrete.functor f)).conePointUniqueUpToIso (CategoryTheory.Limits.limitConeOfUnique f).isLimit
@[simp]
theorem
CategoryTheory.Limits.productUniqueIso_inv
{β : Type w}
{C : Type u}
[CategoryTheory.Category.{v, u} C]
[Unique β]
(f : β → C)
:
@[simp]
theorem
CategoryTheory.Limits.productUniqueIso_hom
{β : Type w}
{C : Type u}
[CategoryTheory.Category.{v, u} C]
[Unique β]
(f : β → C)
:
def
CategoryTheory.Limits.colimitCoconeOfUnique
{β : Type w}
{C : Type u}
[CategoryTheory.Category.{v, u} C]
[Unique β]
(f : β → C)
:
The colimit cocone for the coproduct over an index type with exactly one term.
Equations
- One or more equations did not get rendered due to their size.
@[simp]
theorem
CategoryTheory.Limits.colimitCoconeOfUnique_cocone_ι
{β : Type w}
{C : Type u}
[CategoryTheory.Category.{v, u} C]
[Unique β]
(f : β → C)
:
(CategoryTheory.Limits.colimitCoconeOfUnique f).cocone.ι = CategoryTheory.Discrete.natTrans fun (x : CategoryTheory.Discrete β) =>
match x with
| { as := j } => CategoryTheory.eqToHom ⋯
@[simp]
theorem
CategoryTheory.Limits.colimitCoconeOfUnique_cocone_pt
{β : Type w}
{C : Type u}
[CategoryTheory.Category.{v, u} C]
[Unique β]
(f : β → C)
:
(CategoryTheory.Limits.colimitCoconeOfUnique f).cocone.pt = f default
@[simp]
theorem
CategoryTheory.Limits.colimitCoconeOfUnique_isColimit_desc
{β : Type w}
{C : Type u}
[CategoryTheory.Category.{v, u} C]
[Unique β]
(f : β → C)
(s : CategoryTheory.Limits.Cocone (CategoryTheory.Discrete.functor f))
:
(CategoryTheory.Limits.colimitCoconeOfUnique f).isColimit.desc s = s.ι.app default
@[instance 100]
instance
CategoryTheory.Limits.hasCoproduct_unique
{β : Type w}
{C : Type u}
[CategoryTheory.Category.{v, u} C]
[Nonempty β]
[Subsingleton β]
(f : β → C)
:
Equations
- ⋯ = ⋯
def
CategoryTheory.Limits.coproductUniqueIso
{β : Type w}
{C : Type u}
[CategoryTheory.Category.{v, u} C]
[Unique β]
(f : β → C)
:
A coproduct over an index type with exactly one term is just the object over that term.
Equations
- One or more equations did not get rendered due to their size.
@[simp]
theorem
CategoryTheory.Limits.coproductUniqueIso_inv
{β : Type w}
{C : Type u}
[CategoryTheory.Category.{v, u} C]
[Unique β]
(f : β → C)
:
@[simp]
theorem
CategoryTheory.Limits.coproductUniqueIso_hom
{β : Type w}
{C : Type u}
[CategoryTheory.Category.{v, u} C]
[Unique β]
(f : β → C)
:
def
CategoryTheory.Limits.Pi.reindex
{β : Type w}
{C : Type u}
[CategoryTheory.Category.{v, u} C]
{γ : Type w'}
(ε : β ≃ γ)
(f : γ → C)
[CategoryTheory.Limits.HasProduct f]
[CategoryTheory.Limits.HasProduct (f ∘ ⇑ε)]
:
Reindex a categorical product via an equivalence of the index types.
Equations
- One or more equations did not get rendered due to their size.
@[simp]
theorem
CategoryTheory.Limits.Pi.reindex_hom_π
{β : Type w}
{C : Type u}
[CategoryTheory.Category.{v, u} C]
{γ : Type w'}
(ε : β ≃ γ)
(f : γ → C)
[CategoryTheory.Limits.HasProduct f]
[CategoryTheory.Limits.HasProduct (f ∘ ⇑ε)]
(b : β)
:
CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.Pi.reindex ε f).hom (CategoryTheory.Limits.Pi.π f (ε b)) = CategoryTheory.Limits.Pi.π (f ∘ ⇑ε) b
@[simp]
theorem
CategoryTheory.Limits.Pi.reindex_hom_π_assoc
{β : Type w}
{C : Type u}
[CategoryTheory.Category.{v, u} C]
{γ : Type w'}
(ε : β ≃ γ)
(f : γ → C)
[CategoryTheory.Limits.HasProduct f]
[CategoryTheory.Limits.HasProduct (f ∘ ⇑ε)]
(b : β)
{Z : C}
(h : f (ε b) ⟶ Z)
:
@[simp]
theorem
CategoryTheory.Limits.Pi.reindex_inv_π
{β : Type w}
{C : Type u}
[CategoryTheory.Category.{v, u} C]
{γ : Type w'}
(ε : β ≃ γ)
(f : γ → C)
[CategoryTheory.Limits.HasProduct f]
[CategoryTheory.Limits.HasProduct (f ∘ ⇑ε)]
(b : β)
:
CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.Pi.reindex ε f).inv (CategoryTheory.Limits.Pi.π (f ∘ ⇑ε) b) = CategoryTheory.Limits.Pi.π f (ε b)
@[simp]
theorem
CategoryTheory.Limits.Pi.reindex_inv_π_assoc
{β : Type w}
{C : Type u}
[CategoryTheory.Category.{v, u} C]
{γ : Type w'}
(ε : β ≃ γ)
(f : γ → C)
[CategoryTheory.Limits.HasProduct f]
[CategoryTheory.Limits.HasProduct (f ∘ ⇑ε)]
(b : β)
{Z : C}
(h : (f ∘ ⇑ε) b ⟶ Z)
:
def
CategoryTheory.Limits.Sigma.reindex
{β : Type w}
{C : Type u}
[CategoryTheory.Category.{v, u} C]
{γ : Type w'}
(ε : β ≃ γ)
(f : γ → C)
[CategoryTheory.Limits.HasCoproduct f]
[CategoryTheory.Limits.HasCoproduct (f ∘ ⇑ε)]
:
Reindex a categorical coproduct via an equivalence of the index types.
Equations
- One or more equations did not get rendered due to their size.
@[simp]
theorem
CategoryTheory.Limits.Sigma.ι_reindex_hom
{β : Type w}
{C : Type u}
[CategoryTheory.Category.{v, u} C]
{γ : Type w'}
(ε : β ≃ γ)
(f : γ → C)
[CategoryTheory.Limits.HasCoproduct f]
[CategoryTheory.Limits.HasCoproduct (f ∘ ⇑ε)]
(b : β)
:
CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.Sigma.ι (f ∘ ⇑ε) b)
(CategoryTheory.Limits.Sigma.reindex ε f).hom = CategoryTheory.Limits.Sigma.ι f (ε b)
@[simp]
theorem
CategoryTheory.Limits.Sigma.ι_reindex_hom_assoc
{β : Type w}
{C : Type u}
[CategoryTheory.Category.{v, u} C]
{γ : Type w'}
(ε : β ≃ γ)
(f : γ → C)
[CategoryTheory.Limits.HasCoproduct f]
[CategoryTheory.Limits.HasCoproduct (f ∘ ⇑ε)]
(b : β)
{Z : C}
(h : ∐ f ⟶ Z)
:
@[simp]
theorem
CategoryTheory.Limits.Sigma.ι_reindex_inv
{β : Type w}
{C : Type u}
[CategoryTheory.Category.{v, u} C]
{γ : Type w'}
(ε : β ≃ γ)
(f : γ → C)
[CategoryTheory.Limits.HasCoproduct f]
[CategoryTheory.Limits.HasCoproduct (f ∘ ⇑ε)]
(b : β)
:
CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.Sigma.ι f (ε b))
(CategoryTheory.Limits.Sigma.reindex ε f).inv = CategoryTheory.Limits.Sigma.ι (f ∘ ⇑ε) b
@[simp]
theorem
CategoryTheory.Limits.Sigma.ι_reindex_inv_assoc
{β : Type w}
{C : Type u}
[CategoryTheory.Category.{v, u} C]
{γ : Type w'}
(ε : β ≃ γ)
(f : γ → C)
[CategoryTheory.Limits.HasCoproduct f]
[CategoryTheory.Limits.HasCoproduct (f ∘ ⇑ε)]
(b : β)
{Z : C}
(h : ∐ f ∘ ⇑ε ⟶ Z)
: