Mathlib.CategoryTheory.Limits.Shapes.Products

CategoryTheory.Limits.Fan abbrev

(f : β → C)

Full source

/-- A fan over `f : β → C` consists of a collection of maps from an object `P` to every `f b`. -/
abbrev Fan (f : β → C) :=
  Cone (Discrete.functor f)

Categorical Fan Construction

Informal description

Given a category $\mathcal{C}$ and a family of objects $\{f(b)\}_{b \in \beta}$ in $\mathcal{C}$ indexed by a type $\beta$, a *fan* over $f$ consists of: 1. An object $P$ in $\mathcal{C}$ 2. For each $b \in \beta$, a morphism $\pi_b : P \to f(b)$ in $\mathcal{C}$

CategoryTheory.Limits.Cofan abbrev

(f : β → C)

Full source

/-- A cofan over `f : β → C` consists of a collection of maps from every `f b` to an object `P`. -/
abbrev Cofan (f : β → C) :=
  Cocone (Discrete.functor f)

Cofan Construction in Category Theory

Informal description

A cofan over a family of objects $\{f(b)\}_{b \in \beta}$ in a category $C$ consists of an object $P$ in $C$ together with a collection of morphisms $\{f(b) \to P\}_{b \in \beta}$.

CategoryTheory.Limits.Fan.mk definition

{f : β → C} (P : C) (p : ∀ b, P ⟶ f b) : Fan f

Full source

/-- A fan over `f : β → C` consists of a collection of maps from an object `P` to every `f b`. -/
@[simps! pt π_app]
def Fan.mk {f : β → C} (P : C) (p : ∀ b, P ⟶ f b) : Fan f where
  pt := P
  π := Discrete.natTrans (fun X => p X.as)

Construction of a fan in a category

Informal description

Given a category $\mathcal{C}$, an object $P$ in $\mathcal{C}$, and a family of morphisms $\{p_b : P \to f(b)\}_{b \in \beta}$ where $f : \beta \to \mathcal{C}$ is an indexed family of objects, the function `Fan.mk` constructs a fan over $f$ with apex $P$ and projections $p_b$.

CategoryTheory.Limits.Cofan.mk definition

{f : β → C} (P : C) (p : ∀ b, f b ⟶ P) : Cofan f

Full source

/-- A cofan over `f : β → C` consists of a collection of maps from every `f b` to an object `P`. -/
@[simps! pt ι_app]
def Cofan.mk {f : β → C} (P : C) (p : ∀ b, f b ⟶ P) : Cofan f where
  pt := P
  ι := Discrete.natTrans (fun X => p X.as)

Cofan construction from morphisms

Informal description

Given a family of objects $\{f(b)\}_{b \in \beta}$ in a category $C$, an object $P$ in $C$, and a collection of morphisms $\{p_b : f(b) \to P\}_{b \in \beta}$, the function `Cofan.mk` constructs a cofan with apex $P$ and injections $p_b$.

CategoryTheory.Limits.Fan.proj definition

{f : β → C} (p : Fan f) (j : β) : p.pt ⟶ f j

Full source

/-- Get the `j`th "projection" in the fan.
(Note that the initial letter of `proj` matches the greek letter in `Cone.π`.) -/
def Fan.proj {f : β → C} (p : Fan f) (j : β) : p.pt ⟶ f j :=
  p.π.app (Discrete.mk j)

Projection morphism of a fan

Informal description

Given a fan $p$ over a family of objects $\{f(b)\}_{b \in \beta}$ in a category $\mathcal{C}$, the projection morphism $\pi_j : p.\text{pt} \to f(j)$ associated to an index $j \in \beta$ is obtained by evaluating the natural transformation $p.\pi$ at the discrete object corresponding to $j$.

CategoryTheory.Limits.Cofan.inj definition

{f : β → C} (p : Cofan f) (j : β) : f j ⟶ p.pt

Full source

/-- Get the `j`th "injection" in the cofan.
(Note that the initial letter of `inj` matches the greek letter in `Cocone.ι`.) -/
def Cofan.inj {f : β → C} (p : Cofan f) (j : β) : f j ⟶ p.pt :=
  p.ι.app (Discrete.mk j)

$j$-th injection of a cofan

Informal description

For a cofan $p$ over a family of objects $\{f(b)\}_{b \in \beta}$ in a category $C$, the morphism $f(j) \to p.\text{pt}$ is the $j$-th injection map from the $j$-th object in the family to the apex of the cofan.

CategoryTheory.Limits.fan_mk_proj theorem

{f : β → C} (P : C) (p : ∀ b, P ⟶ f b) : (Fan.mk P p).proj = p

Full source

@[simp]
theorem fan_mk_proj {f : β → C} (P : C) (p : ∀ b, P ⟶ f b) : (Fan.mk P p).proj = p :=
  rfl

Projections of Constructed Fan are Given Morphisms

Informal description

Given a category $\mathcal{C}$, an object $P$ in $\mathcal{C}$, and a family of morphisms $\{p_b : P \to f(b)\}_{b \in \beta}$ where $f : \beta \to \mathcal{C}$ is an indexed family of objects, the projection morphisms of the fan constructed via `Fan.mk P p` are exactly the morphisms $p_b$. That is, for each $b \in \beta$, the projection $(Fan.mk P p).proj_b$ equals $p_b$.

CategoryTheory.Limits.cofan_mk_inj theorem

{f : β → C} (P : C) (p : ∀ b, f b ⟶ P) : (Cofan.mk P p).inj = p

Full source

@[simp]
theorem cofan_mk_inj {f : β → C} (P : C) (p : ∀ b, f b ⟶ P) : (Cofan.mk P p).inj = p :=
  rfl

Injections of Constructed Cofan are Given Morphisms

Informal description

Given a family of objects $\{f(b)\}_{b \in \beta}$ in a category $C$, an object $P$ in $C$, and a collection of morphisms $\{p_b : f(b) \to P\}_{b \in \beta}$, the injections of the cofan constructed via `Cofan.mk P p` are exactly the morphisms $p_b$.

CategoryTheory.Limits.HasProduct abbrev

(f : β → C)

Full source

/-- An abbreviation for `HasLimit (Discrete.functor f)`. -/
abbrev HasProduct (f : β → C) :=
  HasLimit (Discrete.functor f)

Existence of Products in a Category

Informal description

A category $\mathcal{C}$ has products indexed by a type $\beta$ for a family of objects $\{f(b)\}_{b \in \beta}$ in $\mathcal{C}$ if the functor $\text{Discrete}(\beta) \to \mathcal{C}$ sending each $b \in \beta$ to $f(b)$ has a limit.

CategoryTheory.Limits.HasCoproduct abbrev

(f : β → C)

Full source

/-- An abbreviation for `HasColimit (Discrete.functor f)`. -/
abbrev HasCoproduct (f : β → C) :=
  HasColimit (Discrete.functor f)

Existence of Coproducts in a Category

Informal description

A category $\mathcal{C}$ has coproducts indexed by a type $\beta$ for a family of objects $\{f(b)\}_{b \in \beta}$ in $\mathcal{C}$ if the functor $\text{Discrete}(\beta) \to \mathcal{C}$ sending each $b \in \beta$ to $f(b)$ has a colimit.

CategoryTheory.Limits.hasCoproduct_of_equiv_of_iso theorem

(f : α → C) (g : β → C) [HasCoproduct f] (e : β ≃ α) (iso : ∀ j, g j ≅ f (e j)) : HasCoproduct g

Full source

lemma hasCoproduct_of_equiv_of_iso (f : α → C) (g : β → C)
    [HasCoproduct f] (e : β ≃ α) (iso : ∀ j, g j ≅ f (e j)) : HasCoproduct g := by
  have : HasColimit ((Discrete.equivalence e).functor ⋙ Discrete.functor f) :=
    hasColimit_equivalence_comp _
  have α : Discrete.functorDiscrete.functor g ≅ (Discrete.equivalence e).functor ⋙ Discrete.functor f :=
    Discrete.natIso (fun ⟨j⟩ => iso j)
  exact hasColimit_of_iso α

Existence of Coproducts under Index Equivalence and Object Isomorphism

Informal description

Let $\mathcal{C}$ be a category, and let $f : \alpha \to \mathcal{C}$ and $g : \beta \to \mathcal{C}$ be families of objects in $\mathcal{C}$. If $\mathcal{C}$ has a coproduct for the family $f$, and there exists an equivalence $e : \beta \simeq \alpha$ and isomorphisms $g(j) \cong f(e(j))$ for each $j \in \beta$, then $\mathcal{C}$ also has a coproduct for the family $g$.

CategoryTheory.Limits.hasProduct_of_equiv_of_iso theorem

(f : α → C) (g : β → C) [HasProduct f] (e : β ≃ α) (iso : ∀ j, g j ≅ f (e j)) : HasProduct g

Full source

lemma hasProduct_of_equiv_of_iso (f : α → C) (g : β → C)
    [HasProduct f] (e : β ≃ α) (iso : ∀ j, g j ≅ f (e j)) : HasProduct g := by
  have : HasLimit ((Discrete.equivalence e).functor ⋙ Discrete.functor f) :=
    hasLimitEquivalenceComp _
  have α : Discrete.functorDiscrete.functor g ≅ (Discrete.equivalence e).functor ⋙ Discrete.functor f :=
    Discrete.natIso (fun ⟨j⟩ => iso j)
  exact hasLimit_of_iso α.symm

Existence of Products under Index Equivalence and Object Isomorphism

Informal description

Let $\mathcal{C}$ be a category, and let $f : \alpha \to \mathcal{C}$ and $g : \beta \to \mathcal{C}$ be families of objects in $\mathcal{C}$. If $\mathcal{C}$ has a product for the family $f$, and there exists an equivalence $e : \beta \simeq \alpha$ and isomorphisms $g(j) \cong f(e(j))$ for each $j \in \beta$, then $\mathcal{C}$ also has a product for the family $g$.

CategoryTheory.Limits.Fan.IsLimit.desc definition

{F : β → C} {c : Fan F} (hc : IsLimit c) {A : C} (f : ∀ i, A ⟶ F i) : A ⟶ c.pt

Full source

/-- Constructor for morphisms to the point of a limit fan. -/
def Fan.IsLimit.desc {F : β → C} {c : Fan F} (hc : IsLimit c) {A : C}
    (f : ∀ i, A ⟶ F i) : A ⟶ c.pt :=
  hc.lift (Fan.mk A f)

Universal property of limit fan morphisms

Informal description

Given a category $\mathcal{C}$, a family of objects $\{F(b)\}_{b \in \beta}$ in $\mathcal{C}$, and a limit fan $c$ over $F$, the function `Fan.IsLimit.desc` constructs the unique morphism from any object $A$ in $\mathcal{C}$ to the apex of $c$ that commutes with the projections. Specifically, for any family of morphisms $\{f_b : A \to F(b)\}_{b \in \beta}$, there exists a unique morphism $A \to c.\text{pt}$ such that the composition with each projection $c.\text{proj}_b$ equals $f_b$.

CategoryTheory.Limits.Fan.IsLimit.fac theorem

 {F : β → C} {c : Fan F} (hc : IsLimit c) {A : C} (f : ∀ i, A ⟶ F i) (i : β) : Fan.IsLimit.desc hc f ≫ c.proj i = f i

Full source

@[reassoc (attr := simp)]
lemma Fan.IsLimit.fac {F : β → C} {c : Fan F} (hc : IsLimit c) {A : C}
    (f : ∀ i, A ⟶ F i) (i : β) :
    Fan.IsLimit.descFan.IsLimit.desc hc f ≫ c.proj i = f i :=
  hc.fac (Fan.mk A f) ⟨i⟩

Commutativity of Limit Fan Induced Morphism with Projections

Informal description

Given a category $\mathcal{C}$, a family of objects $\{F(b)\}_{b \in \beta}$ in $\mathcal{C}$, and a limit fan $c$ over $F$ with universal property witness $hc$, for any object $A$ in $\mathcal{C}$ and any family of morphisms $\{f_b : A \to F(b)\}_{b \in \beta}$, the composition of the induced morphism $\mathrm{desc}(hc, f)$ with the projection $\pi_i : c.\mathrm{pt} \to F(i)$ equals $f_i$ for each index $i \in \beta$. That is, the following diagram commutes for all $i \in \beta$: \[ \mathrm{desc}(hc, f) \circ \pi_i = f_i \]

CategoryTheory.Limits.Fan.IsLimit.hom_ext theorem

 {I : Type*} {F : I → C} {c : Fan F} (hc : IsLimit c) {A : C} (f g : A ⟶ c.pt) (h : ∀ i, f ≫ c.proj i = g ≫ c.proj i) :
  f = g

Full source

lemma Fan.IsLimit.hom_ext {I : Type*} {F : I → C} {c : Fan F} (hc : IsLimit c) {A : C}
    (f g : A ⟶ c.pt) (h : ∀ i, f ≫ c.proj i = g ≫ c.proj i) : f = g :=
  hc.hom_ext (fun ⟨i⟩ => h i)

Uniqueness of Morphisms into Limit Fan via Projections

Informal description

Let $\mathcal{C}$ be a category, $I$ a type, and $F \colon I \to \mathcal{C}$ a family of objects in $\mathcal{C}$. Given a limit fan $c$ over $F$ with apex $c.\mathrm{pt}$ and projections $\pi_i \colon c.\mathrm{pt} \to F(i)$ for each $i \in I$, and two morphisms $f, g \colon A \to c.\mathrm{pt}$ from some object $A$ in $\mathcal{C}$, if $f \circ \pi_i = g \circ \pi_i$ for all $i \in I$, then $f = g$.

CategoryTheory.Limits.Cofan.IsColimit.desc definition

{F : β → C} {c : Cofan F} (hc : IsColimit c) {A : C} (f : ∀ i, F i ⟶ A) : c.pt ⟶ A

Full source

/-- Constructor for morphisms from the point of a colimit cofan. -/
def Cofan.IsColimit.desc {F : β → C} {c : Cofan F} (hc : IsColimit c) {A : C}
    (f : ∀ i, F i ⟶ A) : c.pt ⟶ A :=
  hc.desc (Cofan.mk A f)

Universal property of colimit cofan

Informal description

Given a cofan $c$ over a family of objects $\{F(i)\}_{i \in \beta}$ in a category $C$, where $c$ is a colimit cofan (i.e., $hc$ is a proof that $c$ is a colimit), and given a collection of morphisms $\{f_i : F(i) \to A\}_{i \in \beta}$ for some object $A$ in $C$, the function `Cofan.IsColimit.desc` constructs the unique morphism $c.\mathrm{pt} \to A$ that factors each $f_i$ through the cofan's injections $c.\mathrm{inj}_i : F(i) \to c.\mathrm{pt}$.

CategoryTheory.Limits.Cofan.IsColimit.fac theorem

 {F : β → C} {c : Cofan F} (hc : IsColimit c) {A : C} (f : ∀ i, F i ⟶ A) (i : β) :
  c.inj i ≫ Cofan.IsColimit.desc hc f = f i

Full source

@[reassoc (attr := simp)]
lemma Cofan.IsColimit.fac {F : β → C} {c : Cofan F} (hc : IsColimit c) {A : C}
    (f : ∀ i, F i ⟶ A) (i : β) :
    c.inj i ≫ Cofan.IsColimit.desc hc f = f i :=
  hc.fac (Cofan.mk A f) ⟨i⟩

Factorization Property of Colimit Cofan via Descending Morphism

Informal description

Let $\{F(i)\}_{i \in \beta}$ be a family of objects in a category $C$, and let $c$ be a cofan over this family with apex $P$ and injections $\iota_i : F(i) \to P$. If $c$ is a colimit cofan (i.e., $hc$ proves $c$ is a colimit), then for any object $A$ in $C$ and any collection of morphisms $\{f_i : F(i) \to A\}_{i \in \beta}$, the composition of the $i$-th injection $\iota_i$ with the induced morphism $\mathrm{desc}(hc, f) : P \to A$ equals $f_i$, i.e., $\iota_i \circ \mathrm{desc}(hc, f) = f_i$ for all $i \in \beta$.

CategoryTheory.Limits.Cofan.IsColimit.hom_ext theorem

 {I : Type*} {F : I → C} {c : Cofan F} (hc : IsColimit c) {A : C} (f g : c.pt ⟶ A)
  (h : ∀ i, c.inj i ≫ f = c.inj i ≫ g) : f = g

Full source

lemma Cofan.IsColimit.hom_ext {I : Type*} {F : I → C} {c : Cofan F} (hc : IsColimit c) {A : C}
    (f g : c.pt ⟶ A) (h : ∀ i, c.inj i ≫ f = c.inj i ≫ g) : f = g :=
  hc.hom_ext (fun ⟨i⟩ => h i)

Uniqueness of Morphisms from Colimit Cofan via Cofan Injections

Informal description

Let $I$ be a type, $\{F(i)\}_{i \in I}$ a family of objects in a category $C$, and $c$ a cofan over this family with apex $P$. If $c$ is a colimit cofan (i.e., $hc$ proves $c$ is a colimit), then for any object $A$ in $C$ and any two morphisms $f, g : P \to A$, if $f \circ c.\mathrm{inj}_i = g \circ c.\mathrm{inj}_i$ for all $i \in I$, then $f = g$.

CategoryTheory.Limits.HasProductsOfShape abbrev

(β : Type v)

Full source

/-- An abbreviation for `HasLimitsOfShape (Discrete f)`. -/
abbrev HasProductsOfShape (β : Type v) :=
  HasLimitsOfShape.{v} (Discrete β)

Existence of Products for Indexed Families in a Category

Informal description

A category $\mathcal{C}$ has products of shape $\beta$ (where $\beta$ is a type) if it has limits for all diagrams indexed by the discrete category on $\beta$. This means that for every family of objects $\{F_i\}_{i \in \beta}$ in $\mathcal{C}$, there exists a product object $\prod_{i \in \beta} F_i$ together with projection morphisms satisfying the universal property of products.

CategoryTheory.Limits.HasCoproductsOfShape abbrev

(β : Type v)

Full source

/-- An abbreviation for `HasColimitsOfShape (Discrete f)`. -/
abbrev HasCoproductsOfShape (β : Type v) :=
  HasColimitsOfShape.{v} (Discrete β)

Existence of $\beta$-shaped coproducts in a category

Informal description

A category $C$ has coproducts of shape $\beta$ if it has colimits for all functors from the discrete category on $\beta$ to $C$.

CategoryTheory.Limits.piObj abbrev

(f : β → C) [HasProduct f]

Full source

/-- `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.) -/
abbrev piObj (f : β → C) [HasProduct f] :=
  limit (Discrete.functor f)

Categorical Product of Indexed Family

Informal description

Given a family of objects $\{f(b)\}_{b \in \beta}$ in a category $\mathcal{C}$ that has products indexed by $\beta$, the categorical product $\prod_{b \in \beta} f(b)$ exists and is defined as the limit of the diagram formed by $f$ when viewed as a functor from the discrete category on $\beta$ to $\mathcal{C}$.

CategoryTheory.Limits.sigmaObj abbrev

(f : β → C) [HasCoproduct f]

Full source

/-- `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.) -/
abbrev sigmaObj (f : β → C) [HasCoproduct f] :=
  colimit (Discrete.functor f)

Categorical Coproduct of a Family of Objects

Informal description

Given a family of objects $\{f(b)\}_{b \in \beta}$ in a category $\mathcal{C}$ that has coproducts indexed by $\beta$, the coproduct $\coprod_{b \in \beta} f(b)$ exists in $\mathcal{C}$.

CategoryTheory.Limits.term∏ᶜ_ definition

: Lean.ParserDescr✝

Full source

/-- notation for categorical products. We need `ᶜ` to avoid conflict with `Finset.prod`. -/
notation "∏ᶜ " f:60 => piObj f

Categorical product notation

Informal description

The notation $\prodᶜ$ represents the categorical product of a family of objects in a category, where $f$ is the indexing function. This is used to avoid conflict with the notation for finite set products.

CategoryTheory.Limits.term∐_ definition

: Lean.ParserDescr✝

Full source

/-- notation for categorical coproducts -/
notation "∐ " f:60 => sigmaObj f

Categorical coproduct notation

Informal description

The notation $\coprod f$ represents the categorical coproduct of the family of objects $f$.

CategoryTheory.Limits.Pi.π abbrev

(f : β → C) [HasProduct f] (b : β) : ∏ᶜ f ⟶ f b

Full source

/-- The `b`-th projection from the pi object over `f` has the form `∏ᶜ f ⟶ f b`. -/
abbrev Pi.π (f : β → C) [HasProduct f] (b : β) : ∏ᶜ f∏ᶜ f ⟶ f b :=
  limit.π (Discrete.functor f) (Discrete.mk b)

Projection Morphism from Product

Informal description

For a family of objects $\{f(b)\}_{b \in \beta}$ in a category $\mathcal{C}$ that has products indexed by $\beta$, the $b$-th projection morphism $\pi_b : \prod_{b \in \beta} f(b) \to f(b)$ is the canonical morphism from the product to the $b$-th object.

CategoryTheory.Limits.Sigma.ι abbrev

(f : β → C) [HasCoproduct f] (b : β) : f b ⟶ ∐ f

Full source

/-- The `b`-th inclusion into the sigma object over `f` has the form `f b ⟶ ∐ f`. -/
abbrev Sigma.ι (f : β → C) [HasCoproduct f] (b : β) : f b ⟶ ∐ f :=
  colimit.ι (Discrete.functor f) (Discrete.mk b)

Coprojection Morphism into Coproduct

Informal description

For a family of objects $\{f(b)\}_{b \in \beta}$ in a category $\mathcal{C}$ that has coproducts indexed by $\beta$, the $b$-th coprojection morphism $\iota_b : f(b) \to \coprod_{b \in \beta} f(b)$ is the canonical morphism from the $b$-th object to the coproduct.

CategoryTheory.Limits.Pi.hom_ext theorem

 {f : β → C} [HasProduct f] {X : C} (g₁ g₂ : X ⟶ ∏ᶜ f) (h : ∀ (b : β), g₁ ≫ Pi.π f b = g₂ ≫ Pi.π f b) : g₁ = g₂

Full source

@[ext 1050]
lemma Pi.hom_ext {f : β → C} [HasProduct f] {X : C} (g₁ g₂ : X ⟶ ∏ᶜ f)
    (h : ∀ (b : β), g₁ ≫ Pi.π f b = g₂ ≫ Pi.π f b) : g₁ = g₂ :=
  limit.hom_ext (fun ⟨j⟩ => h j)

Uniqueness of Morphisms into Product via Projections

Informal description

Let $\mathcal{C}$ be a category with products indexed by a type $\beta$, and let $\{f(b)\}_{b \in \beta}$ be a family of objects in $\mathcal{C}$. For any object $X$ in $\mathcal{C}$ and any pair of morphisms $g_1, g_2 : X \to \prod_{b \in \beta} f(b)$, if for every $b \in \beta$ the compositions $g_1 \circ \pi_b$ and $g_2 \circ \pi_b$ are equal (where $\pi_b : \prod_{b \in \beta} f(b) \to f(b)$ is the projection morphism), then $g_1 = g_2$.

CategoryTheory.Limits.Sigma.hom_ext theorem

 {f : β → C} [HasCoproduct f] {X : C} (g₁ g₂ : ∐ f ⟶ X) (h : ∀ (b : β), Sigma.ι f b ≫ g₁ = Sigma.ι f b ≫ g₂) : g₁ = g₂

Full source

@[ext 1050]
lemma Sigma.hom_ext {f : β → C} [HasCoproduct f] {X : C} (g₁ g₂ : ∐ f∐ f ⟶ X)
    (h : ∀ (b : β), Sigma.ιSigma.ι f b ≫ g₁ = Sigma.ιSigma.ι f b ≫ g₂) : g₁ = g₂ :=
  colimit.hom_ext (fun ⟨j⟩ => h j)

Uniqueness of Morphisms from Coproduct via Coprojections

Informal description

Let $\mathcal{C}$ be a category with coproducts indexed by a type $\beta$, and let $\{f(b)\}_{b \in \beta}$ be a family of objects in $\mathcal{C}$. For any object $X$ in $\mathcal{C}$ and any pair of morphisms $g_1, g_2 : \coprod_{b \in \beta} f(b) \to X$, if for every $b \in \beta$ the compositions $\iota_b \circ g_1$ and $\iota_b \circ g_2$ are equal (where $\iota_b : f(b) \to \coprod_{b \in \beta} f(b)$ is the coprojection morphism), then $g_1 = g_2$.

CategoryTheory.Limits.productIsProduct definition

(f : β → C) [HasProduct f] : IsLimit (Fan.mk _ (Pi.π f))

Full source

/-- The fan constructed of the projections from the product is limiting. -/
def productIsProduct (f : β → C) [HasProduct f] : IsLimit (Fan.mk _ (Pi.π f)) :=
  IsLimit.ofIsoLimit (limit.isLimit (Discrete.functor f)) (Cones.ext (Iso.refl _))

Universal property of categorical products

Informal description

For a family of objects $\{f(b)\}_{b \in \beta}$ in a category $\mathcal{C}$ that has products indexed by $\beta$, the fan constructed from the product $\prod_{b \in \beta} f(b)$ with the canonical projection morphisms $\pi_b : \prod_{b \in \beta} f(b) \to f(b)$ is a limiting cone. This means it satisfies the universal property of products in $\mathcal{C}$.

CategoryTheory.Limits.coproductIsCoproduct definition

(f : β → C) [HasCoproduct f] : IsColimit (Cofan.mk _ (Sigma.ι f))

Full source

/-- The cofan constructed of the inclusions from the coproduct is colimiting. -/
def coproductIsCoproduct (f : β → C) [HasCoproduct f] : IsColimit (Cofan.mk _ (Sigma.ι f)) :=
  IsColimit.ofIsoColimit (colimit.isColimit (Discrete.functor f)) (Cocones.ext (Iso.refl _))

Universal property of categorical coproducts

Informal description

For a family of objects $\{f(b)\}_{b \in \beta}$ in a category $\mathcal{C}$ that has coproducts indexed by $\beta$, the cofan constructed from the coproduct $\coprod_{b \in \beta} f(b)$ with the canonical coprojection morphisms $\iota_b : f(b) \to \coprod_{b \in \beta} f(b)$ is a colimiting cocone. This means it satisfies the universal property of coproducts in $\mathcal{C}$.

CategoryTheory.Limits.Pi.π_comp_eqToHom theorem

{J : Type*} (f : J → C) [HasProduct f] {j j' : J} (w : j = j') : Pi.π f j ≫ eqToHom (by simp [w]) = Pi.π f j'

Full source

@[reassoc (attr := simp, nolint simpNF)]
theorem Pi.π_comp_eqToHom {J : Type*} (f : J → C) [HasProduct f] {j j' : J} (w : j = j') :
    Pi.πPi.π f j ≫ eqToHom (by simp [w]) = Pi.π f j' := by
  cases w
  simp

Compatibility of Projection with Equality Morphism in Categorical Products

Informal description

Let $\mathcal{C}$ be a category with products indexed by a type $J$, and let $f : J \to \mathcal{C}$ be a family of objects in $\mathcal{C}$. For any two indices $j, j' \in J$ such that $j = j'$, the composition of the projection morphism $\pi_j : \prod_{i \in J} f(i) \to f(j)$ with the equality morphism $\text{eqToHom}$ (induced by the equality $j = j'$) equals the projection morphism $\pi_{j'}$. In symbols: \[ \pi_j \circ \text{eqToHom}(\text{by simp }[w]) = \pi_{j'} \]

CategoryTheory.Limits.Sigma.eqToHom_comp_ι theorem

 {J : Type*} (f : J → C) [HasCoproduct f] {j j' : J} (w : j = j') : eqToHom (by simp [w]) ≫ Sigma.ι f j' = Sigma.ι f j

Full source

@[reassoc (attr := simp, nolint simpNF)]
theorem Sigma.eqToHom_comp_ι {J : Type*} (f : J → C) [HasCoproduct f] {j j' : J} (w : j = j') :
    eqToHomeqToHom (by simp [w]) ≫ Sigma.ι f j' = Sigma.ι f j := by
  cases w
  simp

Compatibility of Coprojection with Equality Morphism

Informal description

Let $\mathcal{C}$ be a category with coproducts indexed by a type $J$, and let $f : J \to \mathcal{C}$ be a family of objects in $\mathcal{C}$. For any two indices $j, j' \in J$ such that $j = j'$, the composition of the equality morphism $\text{eqToHom}$ (induced by the equality $j = j'$) with the coprojection morphism $\iota_{j'}$ equals the coprojection morphism $\iota_j$. In symbols: \[ \text{eqToHom}(\text{by simp }[w]) \circ \iota_{j'} = \iota_j \]

CategoryTheory.Limits.Pi.lift abbrev

{f : β → C} [HasProduct f] {P : C} (p : ∀ b, P ⟶ f b) : P ⟶ ∏ᶜ f

Full source

/-- A collection of morphisms `P ⟶ f b` induces a morphism `P ⟶ ∏ᶜ f`. -/
abbrev Pi.lift {f : β → C} [HasProduct f] {P : C} (p : ∀ b, P ⟶ f b) : P ⟶ ∏ᶜ f :=
  limit.lift _ (Fan.mk P p)

Universal Property of Categorical Product

Informal description

Given a category $\mathcal{C}$ with products indexed by a type $\beta$, for any object $P$ in $\mathcal{C}$ and a family of morphisms $\{p_b : P \to f(b)\}_{b \in \beta}$, there exists a unique morphism $P \to \prod_{b \in \beta} f(b)$ that commutes with the projections.

CategoryTheory.Limits.Pi.lift_π theorem

{β : Type w} {f : β → C} [HasProduct f] {P : C} (p : ∀ b, P ⟶ f b) (b : β) : Pi.lift p ≫ Pi.π f b = p b

Full source

theorem Pi.lift_π {β : Type w} {f : β → C} [HasProduct f] {P : C} (p : ∀ b, P ⟶ f b) (b : β) :
    Pi.liftPi.lift p ≫ Pi.π f b = p b := by
  simp only [limit.lift_π, Fan.mk_pt, Fan.mk_π_app]

Commutativity of Product Lift with Projections

Informal description

Let $\mathcal{C}$ be a category with products indexed by a type $\beta$, and let $\{f(b)\}_{b \in \beta}$ be a family of objects in $\mathcal{C}$. For any object $P$ in $\mathcal{C}$ and a family of morphisms $\{p_b : P \to f(b)\}_{b \in \beta}$, the composition of the product's universal morphism $\text{Pi.lift}\, p$ with the projection $\pi_b$ equals $p_b$ for each $b \in \beta$. In symbols: \[ \text{Pi.lift}\, p \circ \pi_b = p_b \]

CategoryTheory.Limits.Sigma.desc abbrev

{f : β → C} [HasCoproduct f] {P : C} (p : ∀ b, f b ⟶ P) : ∐ f ⟶ P

Full source

/-- A collection of morphisms `f b ⟶ P` induces a morphism `∐ f ⟶ P`. -/
abbrev Sigma.desc {f : β → C} [HasCoproduct f] {P : C} (p : ∀ b, f b ⟶ P) : ∐ f∐ f ⟶ P :=
  colimit.desc _ (Cofan.mk P p)

Universal Property of Categorical Coproduct

Informal description

Given a family of objects $\{f(b)\}_{b \in \beta}$ in a category $\mathcal{C}$ that has coproducts indexed by $\beta$, and an object $P$ in $\mathcal{C}$ with a collection of morphisms $\{p_b : f(b) \to P\}_{b \in \beta}$, there exists a unique morphism $\coprod_{b \in \beta} f(b) \to P$ that commutes with the coprojections.

CategoryTheory.Limits.Sigma.ι_desc theorem

 {β : Type w} {f : β → C} [HasCoproduct f] {P : C} (p : ∀ b, f b ⟶ P) (b : β) : Sigma.ι f b ≫ Sigma.desc p = p b

Full source

theorem Sigma.ι_desc {β : Type w} {f : β → C} [HasCoproduct f] {P : C} (p : ∀ b, f b ⟶ P) (b : β) :
    Sigma.ιSigma.ι f b ≫ Sigma.desc p = p b := by
  simp only [colimit.ι_desc, Cofan.mk_pt, Cofan.mk_ι_app]

Commutativity of Coprojection with Universal Morphism in Coproduct

Informal description

Let $\mathcal{C}$ be a category with coproducts indexed by a type $\beta$, and let $\{f(b)\}_{b \in \beta}$ be a family of objects in $\mathcal{C}$. For any object $P$ in $\mathcal{C}$ and a family of morphisms $\{p_b : f(b) \to P\}_{b \in \beta}$, the composition of the $b$-th coprojection $\iota_b : f(b) \to \coprod_{b \in \beta} f(b)$ with the universal morphism $\text{Sigma.desc}\, p : \coprod_{b \in \beta} f(b) \to P$ equals $p_b$ for each $b \in \beta$. In symbols: \[ \iota_b \circ \text{Sigma.desc}\, p = p_b \]

CategoryTheory.Limits.instIsIsoDescι instance

{f : β → C} [HasCoproduct f] : IsIso (Sigma.desc (fun a ↦ Sigma.ι f a))

Full source

instance {f : β → C} [HasCoproduct f] : IsIso (Sigma.desc (fun a ↦ Sigma.ι f a)) := by
  convert IsIso.id _
  ext
  simp

Canonical Coproduct Morphism is an Isomorphism

Informal description

For any family of objects $\{f(b)\}_{b \in \beta}$ in a category $\mathcal{C}$ that has coproducts indexed by $\beta$, the canonical morphism $\coprod_{b \in \beta} f(b) \to \coprod_{b \in \beta} f(b)$ induced by the coprojections $\iota_b : f(b) \to \coprod_{b \in \beta} f(b)$ is an isomorphism.

CategoryTheory.Limits.Cofan.isColimitOfIsIsoSigmaDesc definition

{f : β → C} [HasCoproduct f] (c : Cofan f) [hc : IsIso (Sigma.desc c.inj)] : IsColimit c

Full source

/-- A cofan `c` on `f` such that the induced map `∐ f ⟶ c.pt` is an iso, is a coproduct. -/
def Cofan.isColimitOfIsIsoSigmaDesc {f : β → C} [HasCoproduct f] (c : Cofan f)
    [hc : IsIso (Sigma.desc c.inj)] : IsColimit c :=
  IsColimit.ofIsoColimit (colimit.isColimit (Discrete.functor f))
    (Cofan.ext (@asIso _ _ _ _ _ hc) (fun _ => colimit.ι_desc _ _))

Cofan is colimit if induced coproduct morphism is isomorphism

Informal description

Given a family of objects $\{f(b)\}_{b \in \beta}$ in a category $\mathcal{C}$ that has coproducts, and a cofan $c$ over this family, if the induced morphism $\coprod_{b \in \beta} f(b) \to c.\text{pt}$ (constructed via the universal property of coproducts) is an isomorphism, then $c$ is a colimit cofan for the family $\{f(b)\}_{b \in \beta}$.

CategoryTheory.Limits.Cofan.isColimit_iff_isIso_sigmaDesc theorem

{f : β → C} [HasCoproduct f] (c : Cofan f) : IsIso (Sigma.desc c.inj) ↔ Nonempty (IsColimit c)

Full source

lemma Cofan.isColimit_iff_isIso_sigmaDesc {f : β → C} [HasCoproduct f] (c : Cofan f) :
    IsIsoIsIso (Sigma.desc c.inj) ↔ Nonempty (IsColimit c) := by
  refine ⟨fun h ↦ ⟨isColimitOfIsIsoSigmaDesc c⟩, fun ⟨hc⟩ ↦ ?_⟩
  have : IsIso (((coproductIsCoproduct f).coconePointUniqueUpToIso hc).hom ≫ hc.desc c) := by
    simp; infer_instance
  convert this
  ext
  simp only [colimit.ι_desc, mk_pt, mk_ι_app, IsColimit.coconePointUniqueUpToIso,
    coproductIsCoproduct, colimit.cocone_x, Functor.mapIso_hom, IsColimit.uniqueUpToIso_hom,
    Cocones.forget_map, IsColimit.descCoconeMorphism_hom, IsColimit.ofIsoColimit_desc,
    Cocones.ext_inv_hom, Iso.refl_inv, colimit.isColimit_desc, Category.id_comp,
    IsColimit.desc_self, Category.comp_id]
  rfl

Characterization of Colimit Cofans via Isomorphism of Coproduct Morphism

Informal description

For a family of objects $\{f(b)\}_{b \in \beta}$ in a category $\mathcal{C}$ that has coproducts indexed by $\beta$, and a cofan $c$ over this family, the induced morphism $\coprod_{b \in \beta} f(b) \to c.\text{pt}$ is an isomorphism if and only if $c$ is a colimit cofan (up to isomorphism).

CategoryTheory.Limits.Cofan.isColimitTrans definition

 {X : α → C} (c : Cofan X) (hc : IsColimit c) {β : α → Type*} {Y : (a : α) → β a → C}
  (π : (a : α) → (b : β a) → Y a b ⟶ X a) (hs : ∀ a, IsColimit (Cofan.mk (X a) (π a))) :
  IsColimit (Cofan.mk (f := fun ⟨a, b⟩ => Y a b) c.pt (fun (⟨a, b⟩ : Σ a, _) ↦ π a b ≫ c.inj a))

Full source

/-- A coproduct of coproducts is a coproduct -/
def Cofan.isColimitTrans {X : α → C} (c : Cofan X) (hc : IsColimit c)
    {β : α → Type*} {Y : (a : α) → β a → C} (π : (a : α) → (b : β a) → Y a b ⟶ X a)
      (hs : ∀ a, IsColimit (Cofan.mk (X a) (π a))) :
        IsColimit (Cofan.mk (f := fun ⟨a,b⟩ => Y a b) c.pt
          (fun (⟨a, b⟩ : Σ a, _) ↦ π a b ≫ c.inj a)) := by
  refine mkCofanColimit _ ?_ ?_ ?_
  · exact fun t ↦ hc.desc (Cofan.mk _ fun a ↦ (hs a).desc (Cofan.mk t.pt (fun b ↦ t.inj ⟨a, b⟩)))
  · intro t ⟨a, b⟩
    simp only [mk_pt, cofan_mk_inj, Category.assoc]
    erw [hc.fac, (hs a).fac]
    rfl
  · intro t m h
    refine hc.hom_ext fun ⟨a⟩ ↦ (hs a).hom_ext fun ⟨b⟩ ↦ ?_
    erw [hc.fac, (hs a).fac]
    simpa using h ⟨a, b⟩

Transitivity of colimit cofans under composition

Informal description

Given a cofan $c$ over a family of objects $\{X(a)\}_{a \in \alpha}$ in a category $\mathcal{C}$ that is a colimit, and for each $a \in \alpha$, a family of objects $\{Y(a, b)\}_{b \in \beta(a)}$ with colimit cofans $\pi(a, \cdot) : Y(a, \cdot) \to X(a)$, the cofan constructed by composing the injections $\pi(a, b) : Y(a, b) \to X(a)$ with the cofan injections $c.\text{inj}(a) : X(a) \to c.\text{pt}$ is also a colimit cofan for the family $\{Y(a, b)\}_{(a, b) \in \Sigma_{a \in \alpha} \beta(a)}$.

CategoryTheory.Limits.Pi.map abbrev

{f g : β → C} [HasProduct f] [HasProduct g] (p : ∀ b, f b ⟶ g b) : ∏ᶜ f ⟶ ∏ᶜ g

Full source

/-- Construct a morphism between categorical products (indexed by the same type)
from a family of morphisms between the factors.
-/
abbrev Pi.map {f g : β → C} [HasProduct f] [HasProduct g] (p : ∀ b, f b ⟶ g b) : ∏ᶜ f∏ᶜ f ⟶ ∏ᶜ g :=
  limMap (Discrete.natTrans fun X => p X.as)

Induced Morphism Between Categorical Products

Informal description

Given a family of morphisms $\{p_b : f(b) \to g(b)\}_{b \in \beta}$ between two families of objects $\{f(b)\}_{b \in \beta}$ and $\{g(b)\}_{b \in \beta}$ in a category $\mathcal{C}$ that has products indexed by $\beta$, there exists a unique morphism $\prod_{b \in \beta} f(b) \to \prod_{b \in \beta} g(b)$ induced by the family of morphisms $p_b$.

CategoryTheory.Limits.Pi.map_id theorem

{f : α → C} [HasProduct f] : Pi.map (fun a => 𝟙 (f a)) = 𝟙 (∏ᶜ f)

Full source

@[simp]
lemma Pi.map_id {f : α → C} [HasProduct f] : Pi.map (fun a => 𝟙 (f a)) = 𝟙 (∏ᶜ f) := by
  ext; simp

Identity Morphism Induces Identity on Product

Informal description

For any family of objects $\{f(a)\}_{a \in \alpha}$ in a category $\mathcal{C}$ that has products indexed by $\alpha$, the morphism induced by the identity morphisms $\text{id}_{f(a)} : f(a) \to f(a)$ for each $a \in \alpha$ is equal to the identity morphism on the product $\prod_{a \in \alpha} f(a)$.

CategoryTheory.Limits.Pi.map_comp_map theorem

 {f g h : α → C} [HasProduct f] [HasProduct g] [HasProduct h] (q : ∀ (a : α), f a ⟶ g a) (q' : ∀ (a : α), g a ⟶ h a) :
  Pi.map q ≫ Pi.map q' = Pi.map (fun a => q a ≫ q' a)

Full source

lemma Pi.map_comp_map {f g h : α → C} [HasProduct f] [HasProduct g] [HasProduct h]
    (q : ∀ (a : α), f a ⟶ g a) (q' : ∀ (a : α), g a ⟶ h a) :
    Pi.mapPi.map q ≫ Pi.map q' = Pi.map (fun a => q a ≫ q' a) := by
  ext; simp

Composition of Induced Morphisms on Products Equals Induced Morphism of Compositions

Informal description

Let $\mathcal{C}$ be a category with products indexed by a type $\alpha$, and let $\{f(a)\}_{a \in \alpha}$, $\{g(a)\}_{a \in \alpha}$, and $\{h(a)\}_{a \in \alpha}$ be families of objects in $\mathcal{C}$. For any families of morphisms $q_a : f(a) \to g(a)$ and $q'_a : g(a) \to h(a)$ for each $a \in \alpha$, the composition of the induced morphisms $\prod_{a \in \alpha} f(a) \xrightarrow{\Pi q} \prod_{a \in \alpha} g(a) \xrightarrow{\Pi q'} \prod_{a \in \alpha} h(a)$ is equal to the morphism induced by the componentwise compositions $q_a \circ q'_a : f(a) \to h(a)$ for each $a \in \alpha$, i.e., \[ \Pi q \circ \Pi q' = \Pi (q \circ q'). \]

CategoryTheory.Limits.Pi.map_mono instance

{f g : β → C} [HasProduct f] [HasProduct g] (p : ∀ b, f b ⟶ g b) [∀ i, Mono (p i)] : Mono <| Pi.map p

Full source

instance Pi.map_mono {f g : β → C} [HasProduct f] [HasProduct g] (p : ∀ b, f b ⟶ g b)
    [∀ i, Mono (p i)] : Mono <| Pi.map p :=
  @Limits.limMap_mono _ _ _ _ (Discrete.functor f) (Discrete.functor g) _ _
    (Discrete.natTrans fun X => p X.as) (by dsimp; infer_instance)

Monomorphisms Induce Monomorphisms on Products

Informal description

For any two families of objects $\{f(b)\}_{b \in \beta}$ and $\{g(b)\}_{b \in \beta}$ in a category $\mathcal{C}$ with products indexed by $\beta$, if each morphism $p_b : f(b) \to g(b)$ is a monomorphism, then the induced morphism $\prod_{b \in \beta} f(b) \to \prod_{b \in \beta} g(b)$ is also a monomorphism.

CategoryTheory.Limits.Pi.map' definition

 {f : α → C} {g : β → C} [HasProduct f] [HasProduct g] (p : β → α) (q : ∀ (b : β), f (p b) ⟶ g b) : ∏ᶜ f ⟶ ∏ᶜ g

Full source

/-- Construct a morphism between categorical products from a family of morphisms between the
    factors. -/
def Pi.map' {f : α → C} {g : β → C} [HasProduct f] [HasProduct g] (p : β → α)
    (q : ∀ (b : β), f (p b) ⟶ g b) : ∏ᶜ f∏ᶜ f ⟶ ∏ᶜ g :=
  Pi.lift (fun a => Pi.πPi.π _ _ ≫ q a)

Induced morphism between products via reindexing and component morphisms

Informal description

Given two families of objects $\{f(a)\}_{a \in \alpha}$ and $\{g(b)\}_{b \in \beta}$ in a category $\mathcal{C}$ that has products indexed by $\alpha$ and $\beta$ respectively, a reindexing function $p : \beta \to \alpha$, and a family of morphisms $\{q_b : f(p(b)) \to g(b)\}_{b \in \beta}$, there exists a unique morphism $\prod_{a \in \alpha} f(a) \to \prod_{b \in \beta} g(b)$ induced by the composition of the projection $\pi_{p(b)} : \prod_{a \in \alpha} f(a) \to f(p(b))$ with $q_b$ for each $b \in \beta$.

CategoryTheory.Limits.Pi.map'_comp_π theorem

 {f : α → C} {g : β → C} [HasProduct f] [HasProduct g] (p : β → α) (q : ∀ (b : β), f (p b) ⟶ g b) (b : β) :
  Pi.map' p q ≫ Pi.π g b = Pi.π f (p b) ≫ q b

Full source

@[reassoc (attr := simp)]
lemma Pi.map'_comp_π {f : α → C} {g : β → C} [HasProduct f] [HasProduct g] (p : β → α)
    (q : ∀ (b : β), f (p b) ⟶ g b) (b : β) : Pi.map'Pi.map' p q ≫ Pi.π g b = Pi.πPi.π f (p b) ≫ q b :=
  limit.lift_π _ _

Commutativity of Product Morphism with Projections via Reindexing

Informal description

Given two families of objects $\{f(a)\}_{a \in \alpha}$ and $\{g(b)\}_{b \in \beta}$ in a category $\mathcal{C}$ with products indexed by $\alpha$ and $\beta$ respectively, a reindexing function $p : \beta \to \alpha$, and a family of morphisms $\{q_b : f(p(b)) \to g(b)\}_{b \in \beta}$, the composition of the induced morphism $\prod_{a \in \alpha} f(a) \to \prod_{b \in \beta} g(b)$ with the $b$-th projection $\pi_b : \prod_{b \in \beta} g(b) \to g(b)$ equals the composition of the $p(b)$-th projection $\pi_{p(b)} : \prod_{a \in \alpha} f(a) \to f(p(b))$ with $q_b$.

CategoryTheory.Limits.Pi.map'_id_id theorem

{f : α → C} [HasProduct f] : Pi.map' id (fun a => 𝟙 (f a)) = 𝟙 (∏ᶜ f)

Full source

lemma Pi.map'_id_id {f : α → C} [HasProduct f] : Pi.map' id (fun a => 𝟙 (f a)) = 𝟙 (∏ᶜ f) := by
  ext; simp

Identity Product Morphism via Identity Reindexing and Component Identities

Informal description

For any family of objects $\{f(a)\}_{a \in \alpha}$ in a category $\mathcal{C}$ that has products indexed by $\alpha$, the morphism $\prod_{a \in \alpha} f(a) \to \prod_{a \in \alpha} f(a)$ induced by the identity reindexing function and the identity morphisms on each $f(a)$ is equal to the identity morphism on $\prod_{a \in \alpha} f(a)$.

CategoryTheory.Limits.Pi.map'_id theorem

{f g : α → C} [HasProduct f] [HasProduct g] (p : ∀ b, f b ⟶ g b) : Pi.map' id p = Pi.map p

Full source

@[simp]
lemma Pi.map'_id {f g : α → C} [HasProduct f] [HasProduct g] (p : ∀ b, f b ⟶ g b) :
    Pi.map' id p = Pi.map p :=
  rfl

Equality of Product Morphisms via Identity Reindexing

Informal description

Given two families of objects $\{f(a)\}_{a \in \alpha}$ and $\{g(a)\}_{a \in \alpha}$ in a category $\mathcal{C}$ that has products indexed by $\alpha$, and a family of morphisms $\{p_a : f(a) \to g(a)\}_{a \in \alpha}$, the induced morphism $\prod_{a \in \alpha} f(a) \to \prod_{a \in \alpha} g(a)$ constructed via the identity reindexing function equals the canonical product morphism induced by $p$.

CategoryTheory.Limits.Pi.map'_comp_map' theorem

 {f : α → C} {g : β → C} {h : γ → C} [HasProduct f] [HasProduct g] [HasProduct h] (p : β → α) (p' : γ → β)
  (q : ∀ (b : β), f (p b) ⟶ g b) (q' : ∀ (c : γ), g (p' c) ⟶ h c) :
  Pi.map' p q ≫ Pi.map' p' q' = Pi.map' (p ∘ p') (fun c => q (p' c) ≫ q' c)

Full source

lemma Pi.map'_comp_map' {f : α → C} {g : β → C} {h : γ → C} [HasProduct f] [HasProduct g]
    [HasProduct h] (p : β → α) (p' : γ → β) (q : ∀ (b : β), f (p b) ⟶ g b)
    (q' : ∀ (c : γ), g (p' c) ⟶ h c) :
    Pi.map'Pi.map' p q ≫ Pi.map' p' q' = Pi.map' (p ∘ p') (fun c => q (p' c) ≫ q' c) := by
  ext; simp

Composition Law for Product Morphisms via Reindexing

Informal description

Let $\mathcal{C}$ be a category with products indexed by types $\alpha$, $\beta$, and $\gamma$. Given families of objects $\{f(a)\}_{a \in \alpha}$, $\{g(b)\}_{b \in \beta}$, and $\{h(c)\}_{c \in \gamma}$ in $\mathcal{C}$, along with reindexing functions $p : \beta \to \alpha$ and $p' : \gamma \to \beta$, and families of morphisms $\{q_b : f(p(b)) \to g(b)\}_{b \in \beta}$ and $\{q'_c : g(p'(c)) \to h(c)\}_{c \in \gamma}$, the composition of the induced product morphisms equals the product morphism induced by the composition of reindexing functions and the composition of component morphisms. That is: \[ \text{map}'_p q \circ \text{map}'_{p'} q' = \text{map}'_{p \circ p'} \left(\lambda c.\, q(p'(c)) \circ q'_c\right) \]

CategoryTheory.Limits.Pi.map'_comp_map theorem

 {f : α → C} {g h : β → C} [HasProduct f] [HasProduct g] [HasProduct h] (p : β → α) (q : ∀ (b : β), f (p b) ⟶ g b)
  (q' : ∀ (b : β), g b ⟶ h b) : Pi.map' p q ≫ Pi.map q' = Pi.map' p (fun b => q b ≫ q' b)

Full source

lemma Pi.map'_comp_map {f : α → C} {g h : β → C} [HasProduct f] [HasProduct g] [HasProduct h]
    (p : β → α) (q : ∀ (b : β), f (p b) ⟶ g b) (q' : ∀ (b : β), g b ⟶ h b) :
    Pi.map'Pi.map' p q ≫ Pi.map q' = Pi.map' p (fun b => q b ≫ q' b) := by
  ext; simp

Composition Law for Product Morphisms via Reindexing and Component Morphisms

Informal description

Let $\mathcal{C}$ be a category with products indexed by types $\alpha$ and $\beta$. Given families of objects $\{f(a)\}_{a \in \alpha}$, $\{g(b)\}_{b \in \beta}$, and $\{h(b)\}_{b \in \beta}$ in $\mathcal{C}$, a reindexing function $p : \beta \to \alpha$, a family of morphisms $\{q_b : f(p(b)) \to g(b)\}_{b \in \beta}$, and a family of morphisms $\{q'_b : g(b) \to h(b)\}_{b \in \beta}$, the composition of the induced morphism $\prod_{a \in \alpha} f(a) \to \prod_{b \in \beta} g(b)$ (via $p$ and $q$) with the canonical product morphism $\prod_{b \in \beta} g(b) \to \prod_{b \in \beta} h(b)$ (via $q'$) equals the induced morphism $\prod_{a \in \alpha} f(a) \to \prod_{b \in \beta} h(b)$ via $p$ and the componentwise compositions $\{q_b \circ q'_b\}_{b \in \beta}$.

CategoryTheory.Limits.Pi.map_comp_map' theorem

 {f g : α → C} {h : β → C} [HasProduct f] [HasProduct g] [HasProduct h] (p : β → α) (q : ∀ (a : α), f a ⟶ g a)
  (q' : ∀ (b : β), g (p b) ⟶ h b) : Pi.map q ≫ Pi.map' p q' = Pi.map' p (fun b => q (p b) ≫ q' b)

Full source

lemma Pi.map_comp_map' {f g : α → C} {h : β → C} [HasProduct f] [HasProduct g] [HasProduct h]
    (p : β → α) (q : ∀ (a : α), f a ⟶ g a) (q' : ∀ (b : β), g (p b) ⟶ h b) :
    Pi.mapPi.map q ≫ Pi.map' p q' = Pi.map' p (fun b => q (p b) ≫ q' b) := by
  ext; simp

Composition Law for Product Morphisms via Reindexing and Componentwise Morphisms

Informal description

Let $\mathcal{C}$ be a category with products indexed by types $\alpha$ and $\beta$. Given families of objects $\{f(a)\}_{a \in \alpha}$, $\{g(a)\}_{a \in \alpha}$, and $\{h(b)\}_{b \in \beta}$ in $\mathcal{C}$, a reindexing function $p : \beta \to \alpha$, a family of morphisms $\{q_a : f(a) \to g(a)\}_{a \in \alpha}$, and a family of morphisms $\{q'_b : g(p(b)) \to h(b)\}_{b \in \beta}$, the composition of the canonical product morphism $\prod_{a \in \alpha} f(a) \to \prod_{a \in \alpha} g(a)$ (induced by $q$) with the morphism $\prod_{a \in \alpha} g(a) \to \prod_{b \in \beta} h(b)$ (induced by $p$ and $q'$) equals the morphism $\prod_{a \in \alpha} f(a) \to \prod_{b \in \beta} h(b)$ induced by $p$ and the componentwise compositions $\{q_{p(b)} \circ q'_b\}_{b \in \beta}$.

CategoryTheory.Limits.Pi.map'_eq theorem

 {f : α → C} {g : β → C} [HasProduct f] [HasProduct g] {p p' : β → α} {q : ∀ (b : β), f (p b) ⟶ g b}
  {q' : ∀ (b : β), f (p' b) ⟶ g b} (hp : p = p') (hq : ∀ (b : β), eqToHom (hp ▸ rfl) ≫ q b = q' b) :
  Pi.map' p q = Pi.map' p' q'

Full source

lemma Pi.map'_eq {f : α → C} {g : β → C} [HasProduct f] [HasProduct g] {p p' : β → α}
    {q : ∀ (b : β), f (p b) ⟶ g b} {q' : ∀ (b : β), f (p' b) ⟶ g b} (hp : p = p')
    (hq : ∀ (b : β), eqToHomeqToHom (hp ▸ rfl) ≫ q b = q' b) : Pi.map' p q = Pi.map' p' q' := by
  aesop_cat

Equality of Product Morphisms via Equal Reindexing and Component Morphisms

Informal description

Let $\mathcal{C}$ be a category with products indexed by types $\alpha$ and $\beta$. Given two families of objects $\{f(a)\}_{a \in \alpha}$ and $\{g(b)\}_{b \in \beta}$ in $\mathcal{C}$, two reindexing functions $p, p' : \beta \to \alpha$ with $p = p'$, and two families of morphisms $\{q_b : f(p(b)) \to g(b)\}_{b \in \beta}$ and $\{q'_b : f(p'(b)) \to g(b)\}_{b \in \beta}$ such that for each $b \in \beta$, the composition of the equality isomorphism $\text{eqToHom}(hp \cdot \text{rfl})$ with $q_b$ equals $q'_b$, then the induced morphisms $\prod_{a \in \alpha} f(a) \to \prod_{b \in \beta} g(b)$ via $p$ and $q$ and via $p'$ and $q'$ are equal.

CategoryTheory.Limits.Pi.mapIso abbrev

{f g : β → C} [HasProductsOfShape β C] (p : ∀ b, f b ≅ g b) : ∏ᶜ f ≅ ∏ᶜ g

Full source

/-- Construct an isomorphism between categorical products (indexed by the same type)
from a family of isomorphisms between the factors.
-/
abbrev Pi.mapIso {f g : β → C} [HasProductsOfShape β C] (p : ∀ b, f b ≅ g b) : ∏ᶜ f∏ᶜ f ≅ ∏ᶜ g :=
  lim.mapIso (Discrete.natIso fun X => p X.as)

Isomorphism of Products Induced by Component Isomorphisms

Informal description

Given a family of isomorphisms $\{p_b : f(b) \cong g(b)\}_{b \in \beta}$ between objects in a category $\mathcal{C}$ that has products indexed by $\beta$, there exists an induced isomorphism $\prod_{b \in \beta} f(b) \cong \prod_{b \in \beta} g(b)$ between the categorical products.

CategoryTheory.Limits.Pi.map_isIso instance

{f g : β → C} [HasProductsOfShape β C] (p : ∀ b, f b ⟶ g b) [∀ b, IsIso <| p b] : IsIso <| Pi.map p

Full source

instance Pi.map_isIso {f g : β → C} [HasProductsOfShape β C] (p : ∀ b, f b ⟶ g b)
    [∀ b, IsIso <| p b] : IsIso <| Pi.map p :=
  inferInstanceAs (IsIso (Pi.mapIso (fun b ↦ asIso (p b))).hom)

Isomorphism of Products from Component Isomorphisms

Informal description

Given a family of morphisms $\{p_b : f(b) \to g(b)\}_{b \in \beta}$ between objects in a category $\mathcal{C}$ that has products indexed by $\beta$, if each $p_b$ is an isomorphism, then the induced morphism $\prod_{b \in \beta} f(b) \to \prod_{b \in \beta} g(b)$ is also an isomorphism.

CategoryTheory.Limits.Pi.cone definition

: Cone X

Full source

/-- A limit cone for `X : Discrete α ⥤ C` that is given
by `∏ᶜ (fun j => X.obj (Discrete.mk j))`. -/
@[simps]
def Pi.cone : Cone X where
  pt := ∏ᶜ (fun j => X.obj (Discrete.mk j))
  π := Discrete.natTrans (fun _ => Pi.π _ _)

Cone for categorical product

Informal description

Given a functor $X$ from the discrete category on some index type to a category $\mathcal{C}$, the cone for the product of the family of objects $\{X(j)\}_{j}$ is constructed with the product object $\prod_j X(j)$ as its apex and the projection morphisms $\pi_j : \prod_j X(j) \to X(j)$ as its legs.

CategoryTheory.Limits.productIsProduct' definition

: IsLimit (Pi.cone X)

Full source

/-- The cone `Pi.cone X` is a limit cone. -/
def productIsProduct' :
    IsLimit (Pi.cone X) where
  lift s := Pi.lift (fun j => s.π.app ⟨j⟩)
  fac s := by simp
  uniq s m hm := by
    dsimp
    ext
    simp only [limit.lift_π, Fan.mk_pt, Fan.mk_π_app]
    apply hm

Universal property of the product cone

Informal description

The cone $\Pi.\text{cone} X$ is a limit cone, meaning it satisfies the universal property of a categorical product. Specifically, for any other cone $s$ over the same diagram, there exists a unique morphism $m$ from the apex of $s$ to the apex of $\Pi.\text{cone} X$ that makes the relevant diagrams commute. The morphism $m$ is constructed using the universal property of the product, and its uniqueness is ensured by the universal property.

CategoryTheory.Limits.Pi.isoLimit definition

: ∏ᶜ (fun j => X.obj (Discrete.mk j)) ≅ limit X

Full source

/-- The isomorphism `∏ᶜ (fun j => X.obj (Discrete.mk j)) ≅ limit X`. -/
def Pi.isoLimit :
    ∏ᶜ (fun j => X.obj (Discrete.mk j))∏ᶜ (fun j => X.obj (Discrete.mk j)) ≅ limit X :=
  IsLimit.conePointUniqueUpToIso (productIsProduct' X) (limit.isLimit X)

Isomorphism between product and limit

Informal description

The isomorphism $\prod_{j} X_j \cong \lim X$ between the categorical product of the family $\{X_j\}_{j}$ and the limit of the functor $X$ from the discrete category to $\mathcal{C}$.

CategoryTheory.Limits.Pi.isoLimit_inv_π theorem

(j : α) : (Pi.isoLimit X).inv ≫ Pi.π _ j = limit.π _ (Discrete.mk j)

Full source

@[reassoc (attr := simp)]
lemma Pi.isoLimit_inv_π (j : α) :
    (Pi.isoLimit X).inv ≫ Pi.π _ j = limit.π _ (Discrete.mk j) :=
  IsLimit.conePointUniqueUpToIso_inv_comp _ _ _

Inverse of Product-Limit Isomorphism Composes with Projection to Give Limit Projection

Informal description

For any object $j$ in the index category $\alpha$, the composition of the inverse of the isomorphism $\prod_j X_j \cong \lim X$ with the projection morphism $\pi_j$ from the product is equal to the limit projection morphism $\lim \pi_{X_j}$ corresponding to $j$.

CategoryTheory.Limits.Pi.isoLimit_hom_π theorem

(j : α) : (Pi.isoLimit X).hom ≫ limit.π _ (Discrete.mk j) = Pi.π _ j

Full source

@[reassoc (attr := simp)]
lemma Pi.isoLimit_hom_π (j : α) :
    (Pi.isoLimit X).hom ≫ limit.π _ (Discrete.mk j) = Pi.π _ j :=
  IsLimit.conePointUniqueUpToIso_hom_comp _ _ _

Compatibility of Product Isomorphism with Projections: $(Pi.isoLimit X).hom \circ \pi_j^{\lim} = \pi_j^{\prod}$

Informal description

For any object $j$ in the index category $\alpha$, the composition of the isomorphism $\prod_j X_j \cong \lim X$ with the $j$-th projection from the limit cone equals the $j$-th projection from the product cone. In symbols, the morphism $(Pi.isoLimit X).hom \circ \pi_j^{\lim} = \pi_j^{\prod}$, where $\pi_j^{\lim}$ is the $j$-th projection from the limit and $\pi_j^{\prod}$ is the $j$-th projection from the product.

CategoryTheory.Limits.Sigma.map abbrev

{f g : β → C} [HasCoproduct f] [HasCoproduct g] (p : ∀ b, f b ⟶ g b) : ∐ f ⟶ ∐ g

Full source

/-- Construct a morphism between categorical coproducts (indexed by the same type)
from a family of morphisms between the factors.
-/
abbrev Sigma.map {f g : β → C} [HasCoproduct f] [HasCoproduct g] (p : ∀ b, f b ⟶ g b) :
    ∐ f∐ f ⟶ ∐ g :=
  colimMap (Discrete.natTrans fun X => p X.as)

Induced Morphism Between Coproducts from a Family of Morphisms

Informal description

Given two families of objects $\{f(b)\}_{b \in \beta}$ and $\{g(b)\}_{b \in \beta}$ in a category $\mathcal{C}$ that has coproducts indexed by $\beta$, and a family of morphisms $p(b) : f(b) \to g(b)$ for each $b \in \beta$, there exists a unique morphism $\coprod_{b \in \beta} p(b) : \coprod_{b \in \beta} f(b) \to \coprod_{b \in \beta} g(b)$ induced by the universal property of coproducts.

CategoryTheory.Limits.Sigma.map_id theorem

{f : α → C} [HasCoproduct f] : Sigma.map (fun a => 𝟙 (f a)) = 𝟙 (∐ f)

Full source

@[simp]
lemma Sigma.map_id {f : α → C} [HasCoproduct f] : Sigma.map (fun a => 𝟙 (f a)) = 𝟙 (∐ f) := by
  ext; simp

Identity Morphism on Coproduct is Coproduct of Identity Morphisms

Informal description

For any family of objects $\{f(a)\}_{a \in \alpha}$ in a category $\mathcal{C}$ that has coproducts indexed by $\alpha$, the induced morphism $\coprod_{a \in \alpha} \text{id}_{f(a)} : \coprod_{a \in \alpha} f(a) \to \coprod_{a \in \alpha} f(a)$ is equal to the identity morphism on $\coprod_{a \in \alpha} f(a)$.

CategoryTheory.Limits.Sigma.map_comp_map theorem

 {f g h : α → C} [HasCoproduct f] [HasCoproduct g] [HasCoproduct h] (q : ∀ (a : α), f a ⟶ g a)
  (q' : ∀ (a : α), g a ⟶ h a) : Sigma.map q ≫ Sigma.map q' = Sigma.map (fun a => q a ≫ q' a)

Full source

lemma Sigma.map_comp_map {f g h : α → C} [HasCoproduct f] [HasCoproduct g] [HasCoproduct h]
    (q : ∀ (a : α), f a ⟶ g a) (q' : ∀ (a : α), g a ⟶ h a) :
    Sigma.mapSigma.map q ≫ Sigma.map q' = Sigma.map (fun a => q a ≫ q' a) := by
  ext; simp

Composition of Coproduct Morphisms Equals Coproduct of Compositions

Informal description

Let $\mathcal{C}$ be a category with coproducts indexed by a type $\alpha$, and let $\{f(a)\}_{a \in \alpha}$, $\{g(a)\}_{a \in \alpha}$, and $\{h(a)\}_{a \in \alpha}$ be families of objects in $\mathcal{C}$. Given families of morphisms $q(a) : f(a) \to g(a)$ and $q'(a) : g(a) \to h(a)$ for each $a \in \alpha$, the composition of the induced coproduct morphisms $\coprod q \circ \coprod q' : \coprod_{a \in \alpha} f(a) \to \coprod_{a \in \alpha} h(a)$ is equal to the coproduct of the composed morphisms $\coprod_{a \in \alpha} (q(a) \circ q'(a))$.

CategoryTheory.Limits.Sigma.map_epi instance

{f g : β → C} [HasCoproduct f] [HasCoproduct g] (p : ∀ b, f b ⟶ g b) [∀ i, Epi (p i)] : Epi <| Sigma.map p

Full source

instance Sigma.map_epi {f g : β → C} [HasCoproduct f] [HasCoproduct g] (p : ∀ b, f b ⟶ g b)
    [∀ i, Epi (p i)] : Epi <| Sigma.map p :=
  @Limits.colimMap_epi _ _ _ _ (Discrete.functor f) (Discrete.functor g) _ _
    (Discrete.natTrans fun X => p X.as) (by dsimp; infer_instance)

Epimorphism Property of Coproducts of Epimorphisms

Informal description

For any two families of objects $\{f(b)\}_{b \in \beta}$ and $\{g(b)\}_{b \in \beta}$ in a category $\mathcal{C}$ with coproducts, and a family of epimorphisms $p(b) : f(b) \to g(b)$ for each $b \in \beta$, the induced morphism $\coprod_{b \in \beta} p(b) : \coprod_{b \in \beta} f(b) \to \coprod_{b \in \beta} g(b)$ is an epimorphism.

CategoryTheory.Limits.Sigma.map' definition

 {f : α → C} {g : β → C} [HasCoproduct f] [HasCoproduct g] (p : α → β) (q : ∀ (a : α), f a ⟶ g (p a)) : ∐ f ⟶ ∐ g

Full source

/-- Construct a morphism between categorical coproducts from a family of morphisms between the
    factors. -/
def Sigma.map' {f : α → C} {g : β → C} [HasCoproduct f] [HasCoproduct g] (p : α → β)
    (q : ∀ (a : α), f a ⟶ g (p a)) : ∐ f∐ f ⟶ ∐ g :=
  Sigma.desc (fun a => q a ≫ Sigma.ι _ _)

Induced morphism between coproducts via reindexing and component morphisms

Informal description

Given two families of objects $\{f(a)\}_{a \in \alpha}$ and $\{g(b)\}_{b \in \beta}$ in a category $\mathcal{C}$ that has coproducts indexed by $\alpha$ and $\beta$ respectively, a function $p : \alpha \to \beta$, and a family of morphisms $q(a) : f(a) \to g(p(a))$ for each $a \in \alpha$, there exists a unique morphism $\coprod_{a \in \alpha} f(a) \to \coprod_{b \in \beta} g(b)$ induced by $p$ and $q$.

CategoryTheory.Limits.Sigma.ι_comp_map' theorem

 {f : α → C} {g : β → C} [HasCoproduct f] [HasCoproduct g] (p : α → β) (q : ∀ (a : α), f a ⟶ g (p a)) (a : α) :
  Sigma.ι f a ≫ Sigma.map' p q = q a ≫ Sigma.ι g (p a)

Full source

@[reassoc (attr := simp)]
lemma Sigma.ι_comp_map' {f : α → C} {g : β → C} [HasCoproduct f] [HasCoproduct g]
    (p : α → β) (q : ∀ (a : α), f a ⟶ g (p a)) (a : α) :
    Sigma.ιSigma.ι f a ≫ Sigma.map' p q = q a ≫ Sigma.ι g (p a) :=
  colimit.ι_desc _ _

Commutativity of Coprojections with Induced Coproduct Morphism

Informal description

Let $\{f(a)\}_{a \in \alpha}$ and $\{g(b)\}_{b \in \beta}$ be families of objects in a category $\mathcal{C}$ that has coproducts indexed by $\alpha$ and $\beta$ respectively. Given a function $p : \alpha \to \beta$ and a family of morphisms $q(a) : f(a) \to g(p(a))$ for each $a \in \alpha$, the composition of the $a$-th coprojection $\iota_a : f(a) \to \coprod_{a \in \alpha} f(a)$ with the induced morphism $\coprod_{a \in \alpha} f(a) \to \coprod_{b \in \beta} g(b)$ equals the composition of $q(a)$ with the $p(a)$-th coprojection $\iota_{p(a)} : g(p(a)) \to \coprod_{b \in \beta} g(b)$. In symbols: $$\iota_a \circ \left(\coprod_{a \in \alpha} q(a)\right) = q(a) \circ \iota_{p(a)}$$

CategoryTheory.Limits.Sigma.map'_id_id theorem

{f : α → C} [HasCoproduct f] : Sigma.map' id (fun a => 𝟙 (f a)) = 𝟙 (∐ f)

Full source

lemma Sigma.map'_id_id {f : α → C} [HasCoproduct f] :
    Sigma.map' id (fun a => 𝟙 (f a)) = 𝟙 (∐ f) := by
  ext; simp

Identity Morphism on Coproduct via Identity Reindexing and Components

Informal description

For any family of objects $\{f(a)\}_{a \in \alpha}$ in a category $\mathcal{C}$ that has coproducts indexed by $\alpha$, the induced morphism $\coprod_{a \in \alpha} f(a) \to \coprod_{a \in \alpha} f(a)$ obtained via the identity reindexing function and identity component morphisms is equal to the identity morphism on $\coprod_{a \in \alpha} f(a)$. In symbols: $$\text{map}'(\text{id}, \lambda a. \text{id}_{f(a)}) = \text{id}_{\coprod f}$$

CategoryTheory.Limits.Sigma.map'_id theorem

{f g : α → C} [HasCoproduct f] [HasCoproduct g] (p : ∀ b, f b ⟶ g b) : Sigma.map' id p = Sigma.map p

Full source

@[simp]
lemma Sigma.map'_id {f g : α → C} [HasCoproduct f] [HasCoproduct g] (p : ∀ b, f b ⟶ g b) :
    Sigma.map' id p = Sigma.map p :=
  rfl

Equality of Coproduct Morphisms via Identity Reindexing and Direct Construction

Informal description

Given two families of objects $\{f(a)\}_{a \in \alpha}$ and $\{g(a)\}_{a \in \alpha}$ in a category $\mathcal{C}$ that has coproducts indexed by $\alpha$, and a family of morphisms $p(a) : f(a) \to g(a)$ for each $a \in \alpha$, the induced morphism $\coprod_{a \in \alpha} f(a) \to \coprod_{a \in \alpha} g(a)$ obtained via the identity reindexing function and component morphisms $p$ is equal to the morphism $\coprod_{a \in \alpha} p(a)$ induced directly by the universal property of coproducts.

CategoryTheory.Limits.Sigma.map'_comp_map' theorem

 {f : α → C} {g : β → C} {h : γ → C} [HasCoproduct f] [HasCoproduct g] [HasCoproduct h] (p : α → β) (p' : β → γ)
  (q : ∀ (a : α), f a ⟶ g (p a)) (q' : ∀ (b : β), g b ⟶ h (p' b)) :
  Sigma.map' p q ≫ Sigma.map' p' q' = Sigma.map' (p' ∘ p) (fun a => q a ≫ q' (p a))

Full source

lemma Sigma.map'_comp_map' {f : α → C} {g : β → C} {h : γ → C} [HasCoproduct f] [HasCoproduct g]
    [HasCoproduct h] (p : α → β) (p' : β → γ) (q : ∀ (a : α), f a ⟶ g (p a))
    (q' : ∀ (b : β), g b ⟶ h (p' b)) :
    Sigma.map'Sigma.map' p q ≫ Sigma.map' p' q' = Sigma.map' (p' ∘ p) (fun a => q a ≫ q' (p a)) := by
  ext; simp

Composition Law for Induced Coproduct Morphisms via Reindexing

Informal description

Let $\mathcal{C}$ be a category with coproducts indexed by types $\alpha$, $\beta$, and $\gamma$. Given families of objects $\{f(a)\}_{a \in \alpha}$, $\{g(b)\}_{b \in \beta}$, and $\{h(c)\}_{c \in \gamma}$ in $\mathcal{C}$, along with functions $p : \alpha \to \beta$ and $p' : \beta \to \gamma$, and families of morphisms $q(a) : f(a) \to g(p(a))$ for each $a \in \alpha$ and $q'(b) : g(b) \to h(p'(b))$ for each $b \in \beta$, the composition of the induced coproduct morphisms $\coprod_{a \in \alpha} f(a) \to \coprod_{b \in \beta} g(b)$ and $\coprod_{b \in \beta} g(b) \to \coprod_{c \in \gamma} h(c)$ equals the induced morphism $\coprod_{a \in \alpha} f(a) \to \coprod_{c \in \gamma} h(c)$ obtained via the composite function $p' \circ p$ and the componentwise composition $q(a) \circ q'(p(a))$ for each $a \in \alpha$. In symbols: $$\left(\coprod_{a \in \alpha} q(a)\right) \circ \left(\coprod_{b \in \beta} q'(b)\right) = \coprod_{a \in \alpha} (q(a) \circ q'(p(a)))$$

CategoryTheory.Limits.Sigma.map'_comp_map theorem

 {f : α → C} {g h : β → C} [HasCoproduct f] [HasCoproduct g] [HasCoproduct h] (p : α → β) (q : ∀ (a : α), f a ⟶ g (p a))
  (q' : ∀ (b : β), g b ⟶ h b) : Sigma.map' p q ≫ Sigma.map q' = Sigma.map' p (fun a => q a ≫ q' (p a))

Full source

lemma Sigma.map'_comp_map {f : α → C} {g h : β → C} [HasCoproduct f] [HasCoproduct g]
    [HasCoproduct h] (p : α → β) (q : ∀ (a : α), f a ⟶ g (p a)) (q' : ∀ (b : β), g b ⟶ h b) :
    Sigma.map'Sigma.map' p q ≫ Sigma.map q' = Sigma.map' p (fun a => q a ≫ q' (p a)) := by
  ext; simp

Composition of Induced Coproduct Morphisms via Reindexing and Component Morphisms

Informal description

Let $\mathcal{C}$ be a category with coproducts indexed by $\alpha$ and $\beta$. Given families of objects $\{f(a)\}_{a \in \alpha}$, $\{g(b)\}_{b \in \beta}$, and $\{h(b)\}_{b \in \beta}$ in $\mathcal{C}$, a function $p : \alpha \to \beta$, a family of morphisms $q(a) : f(a) \to g(p(a))$ for each $a \in \alpha$, and a family of morphisms $q'(b) : g(b) \to h(b)$ for each $b \in \beta$, the composition of the induced morphisms satisfies: $$\left(\coprod_{a \in \alpha} q(a)\right) \circ \left(\coprod_{b \in \beta} q'(b)\right) = \coprod_{a \in \alpha} (q(a) \circ q'(p(a)))$$

CategoryTheory.Limits.Sigma.map_comp_map' theorem

 {f g : α → C} {h : β → C} [HasCoproduct f] [HasCoproduct g] [HasCoproduct h] (p : α → β) (q : ∀ (a : α), f a ⟶ g a)
  (q' : ∀ (a : α), g a ⟶ h (p a)) : Sigma.map q ≫ Sigma.map' p q' = Sigma.map' p (fun a => q a ≫ q' a)

Full source

lemma Sigma.map_comp_map' {f g : α → C} {h : β → C} [HasCoproduct f] [HasCoproduct g]
    [HasCoproduct h] (p : α → β) (q : ∀ (a : α), f a ⟶ g a) (q' : ∀ (a : α), g a ⟶ h (p a)) :
    Sigma.mapSigma.map q ≫ Sigma.map' p q' = Sigma.map' p (fun a => q a ≫ q' a) := by
  ext; simp

Composition of Induced Coproduct Morphisms via Componentwise Composition

Informal description

Let $\{f(a)\}_{a \in \alpha}$, $\{g(a)\}_{a \in \alpha}$, and $\{h(b)\}_{b \in \beta}$ be families of objects in a category $\mathcal{C}$ that has coproducts indexed by $\alpha$ and $\beta$. Given a function $p : \alpha \to \beta$, a family of morphisms $q(a) : f(a) \to g(a)$ for each $a \in \alpha$, and a family of morphisms $q'(a) : g(a) \to h(p(a))$ for each $a \in \alpha$, the composition of the induced morphism $\coprod_{a \in \alpha} q(a) : \coprod_{a \in \alpha} f(a) \to \coprod_{a \in \alpha} g(a)$ with the induced morphism $\coprod_{a \in \alpha} g(a) \to \coprod_{b \in \beta} h(b)$ via $p$ and $q'$ equals the induced morphism $\coprod_{a \in \alpha} f(a) \to \coprod_{b \in \beta} h(b)$ via $p$ and the compositions $q(a) \circ q'(a)$ for each $a \in \alpha$. In symbols: $$\left(\coprod_{a \in \alpha} q(a)\right) \circ \left(\coprod_{a \in \alpha} q'(a)\right) = \coprod_{a \in \alpha} (q(a) \circ q'(a))$$

CategoryTheory.Limits.Sigma.map'_eq theorem

 {f : α → C} {g : β → C} [HasCoproduct f] [HasCoproduct g] {p p' : α → β} {q : ∀ (a : α), f a ⟶ g (p a)}
  {q' : ∀ (a : α), f a ⟶ g (p' a)} (hp : p = p') (hq : ∀ (a : α), q a ≫ eqToHom (hp ▸ rfl) = q' a) :
  Sigma.map' p q = Sigma.map' p' q'

Full source

lemma Sigma.map'_eq {f : α → C} {g : β → C} [HasCoproduct f] [HasCoproduct g]
    {p p' : α → β} {q : ∀ (a : α), f a ⟶ g (p a)} {q' : ∀ (a : α), f a ⟶ g (p' a)}
    (hp : p = p') (hq : ∀ (a : α), q a ≫ eqToHom (hp ▸ rfl) = q' a) :
    Sigma.map' p q = Sigma.map' p' q' := by
  aesop_cat

Equality of Induced Coproduct Morphisms via Equal Reindexing Functions

Informal description

Let $\mathcal{C}$ be a category with coproducts indexed by types $\alpha$ and $\beta$, and let $\{f(a)\}_{a \in \alpha}$ and $\{g(b)\}_{b \in \beta}$ be families of objects in $\mathcal{C}$. Given two functions $p, p' : \alpha \to \beta$ with $p = p'$, and families of morphisms $q(a) : f(a) \to g(p(a))$ and $q'(a) : f(a) \to g(p'(a))$ for each $a \in \alpha$ such that for every $a \in \alpha$ the composition $q(a) \circ \text{eqToHom}(p = p')$ equals $q'(a)$, then the induced coproduct morphisms $\Sigma.map'\, p\, q$ and $\Sigma.map'\, p'\, q'$ are equal.

CategoryTheory.Limits.Sigma.mapIso abbrev

{f g : β → C} [HasCoproductsOfShape β C] (p : ∀ b, f b ≅ g b) : ∐ f ≅ ∐ g

Full source

/-- Construct an isomorphism between categorical coproducts (indexed by the same type)
from a family of isomorphisms between the factors.
-/
abbrev Sigma.mapIso {f g : β → C} [HasCoproductsOfShape β C] (p : ∀ b, f b ≅ g b) : ∐ f∐ f ≅ ∐ g :=
  colim.mapIso (Discrete.natIso fun X => p X.as)

Isomorphism of Coproducts Induced by Family of Isomorphisms

Informal description

Given a family of isomorphisms $\{p_b : f(b) \cong g(b)\}_{b \in \beta}$ between objects in a category $\mathcal{C}$ that has $\beta$-shaped coproducts, there exists an induced isomorphism $\coprod_{b \in \beta} f(b) \cong \coprod_{b \in \beta} g(b)$ between the coproducts of the families $\{f(b)\}$ and $\{g(b)\}$.

CategoryTheory.Limits.Sigma.map_isIso instance

{f g : β → C} [HasCoproductsOfShape β C] (p : ∀ b, f b ⟶ g b) [∀ b, IsIso <| p b] : IsIso (Sigma.map p)

Full source

instance Sigma.map_isIso {f g : β → C} [HasCoproductsOfShape β C] (p : ∀ b, f b ⟶ g b)
    [∀ b, IsIso <| p b] : IsIso (Sigma.map p) :=
  inferInstanceAs (IsIso (Sigma.mapIso (fun b ↦ asIso (p b))).hom)

Isomorphism of Coproducts from Componentwise Isomorphisms

Informal description

For any family of morphisms $\{p_b : f(b) \to g(b)\}_{b \in \beta}$ between objects in a category $\mathcal{C}$ that has $\beta$-shaped coproducts, if each $p_b$ is an isomorphism, then the induced morphism $\coprod_{b \in \beta} p_b : \coprod_{b \in \beta} f(b) \to \coprod_{b \in \beta} g(b)$ is also an isomorphism.

CategoryTheory.Limits.Sigma.cocone definition

: Cocone X

Full source

/-- A colimit cocone for `X : Discrete α ⥤ C` that is given
by `∐ (fun j => X.obj (Discrete.mk j))`. -/
@[simps]
def Sigma.cocone : Cocone X where
  pt := ∐ (fun j => X.obj (Discrete.mk j))
  ι := Discrete.natTrans (fun _ => Sigma.ι (fun j ↦ X.obj ⟨j⟩) _)

Coproduct cocone construction

Informal description

Given a functor $X \colon \text{Discrete}(\beta) \to \mathcal{C}$, the cocone for the coproduct $\coprod_{j \in \beta} X(j)$ is constructed with: - The cocone point being the coproduct object $\coprod_{j \in \beta} X(j)$ - The cocone morphisms being the coprojection maps $\iota_j \colon X(j) \to \coprod_{j \in \beta} X(j)$ for each $j \in \beta$

CategoryTheory.Limits.coproductIsCoproduct' definition

: IsColimit (Sigma.cocone X)

Full source

/-- The cocone `Sigma.cocone X` is a colimit cocone. -/
def coproductIsCoproduct' :
    IsColimit (Sigma.cocone X) where
  desc s := Sigma.desc (fun j => s.ι.app ⟨j⟩)
  fac s := by simp
  uniq s m hm := by
    dsimp
    ext
    simp only [colimit.ι_desc, Cofan.mk_pt, Cofan.mk_ι_app]
    apply hm

Universal property of categorical coproduct cocone

Informal description

The cocone `Sigma.cocone X` is a colimit cocone, meaning it satisfies the universal property of coproducts in the category. Specifically, for any other cocone `s` over the same diagram, there exists a unique morphism from the coproduct object to the vertex of `s` that makes the appropriate diagram commute.

CategoryTheory.Limits.Sigma.isoColimit definition

: ∐ (fun j => X.obj (Discrete.mk j)) ≅ colimit X

Full source

/-- The isomorphism `∐ (fun j => X.obj (Discrete.mk j)) ≅ colimit X`. -/
def Sigma.isoColimit :
    ∐ (fun j => X.obj (Discrete.mk j))∐ (fun j => X.obj (Discrete.mk j)) ≅ colimit X :=
  IsColimit.coconePointUniqueUpToIso (coproductIsCoproduct' X) (colimit.isColimit X)

Isomorphism between coproduct and colimit

Informal description

The isomorphism between the coproduct $\coprod_j X_j$ (where $X_j$ are the objects in the functor $X$) and the colimit of $X$, where $X$ is a functor from a discrete category. This isomorphism is constructed using the universal property of coproducts and colimits.

CategoryTheory.Limits.Sigma.ι_isoColimit_hom theorem

(j : α) : Sigma.ι _ j ≫ (Sigma.isoColimit X).hom = colimit.ι _ (Discrete.mk j)

Full source

@[reassoc (attr := simp)]
lemma Sigma.ι_isoColimit_hom (j : α) :
    Sigma.ιSigma.ι _ j ≫ (Sigma.isoColimit X).hom = colimit.ι _ (Discrete.mk j) :=
  IsColimit.comp_coconePointUniqueUpToIso_hom (coproductIsCoproduct' X) _ _

Commutativity of coprojection with coproduct-colimit isomorphism

Informal description

For any object $j$ in the indexing type $\alpha$, the composition of the coprojection morphism $\iota_j$ with the homomorphism part of the isomorphism between the coproduct and the colimit is equal to the colimit cocone morphism at $j$, i.e., the following diagram commutes: \[ \iota_j \circ (\Sigma.\text{isoColimit}\, X).\text{hom} = \text{colimit}.\iota\, (\text{Discrete.mk}\, j) \]

CategoryTheory.Limits.Sigma.ι_isoColimit_inv theorem

(j : α) : colimit.ι _ ⟨j⟩ ≫ (Sigma.isoColimit X).inv = Sigma.ι (fun j ↦ X.obj ⟨j⟩) _

Full source

@[reassoc (attr := simp)]
lemma Sigma.ι_isoColimit_inv (j : α) :
    colimit.ιcolimit.ι _ ⟨j⟩ ≫ (Sigma.isoColimit X).inv = Sigma.ι (fun j ↦ X.obj ⟨j⟩) _ :=
  IsColimit.comp_coconePointUniqueUpToIso_inv _ _ _

Compatibility of colimit coprojection with coproduct isomorphism inverse

Informal description

For any object $j$ in the indexing type $\alpha$, the composition of the $j$-th colimit coprojection morphism $\iota_j$ with the inverse of the isomorphism between the coproduct and the colimit equals the $j$-th coprojection morphism into the coproduct $\coprod_{j \in \alpha} X(j)$.

CategoryTheory.Limits.Pi.whiskerEquiv definition

 {J K : Type*} {f : J → C} {g : K → C} (e : J ≃ K) (w : ∀ j, g (e j) ≅ f j) [HasProduct f] [HasProduct g] : ∏ᶜ f ≅ ∏ᶜ g

Full source

/-- Two products which differ by an equivalence in the indexing type,
and up to isomorphism in the factors, are isomorphic.
-/
@[simps]
def Pi.whiskerEquiv {J K : Type*} {f : J → C} {g : K → C} (e : J ≃ K) (w : ∀ j, g (e j) ≅ f j)
    [HasProduct f] [HasProduct g] : ∏ᶜ f∏ᶜ f ≅ ∏ᶜ g where
  hom := Pi.map' e.symm fun k => (w (e.symm k)).inv ≫ eqToHom (by simp)
  inv := Pi.map' e fun j => (w j).hom

Isomorphism between products induced by an equivalence of indexing types

Informal description

Given an equivalence $e : J \simeq K$ between indexing types and a family of isomorphisms $w_j : g(e(j)) \cong f(j)$ for each $j \in J$, there is an isomorphism between the categorical products $\prod_{j \in J} f(j) \cong \prod_{k \in K} g(k)$. Here, $f : J \to C$ and $g : K \to C$ are families of objects in a category $\mathcal{C}$ that has products indexed by $J$ and $K$ respectively.

CategoryTheory.Limits.Sigma.whiskerEquiv definition

 {J K : Type*} {f : J → C} {g : K → C} (e : J ≃ K) (w : ∀ j, g (e j) ≅ f j) [HasCoproduct f] [HasCoproduct g] :
  ∐ f ≅ ∐ g

Full source

/-- Two coproducts which differ by an equivalence in the indexing type,
and up to isomorphism in the factors, are isomorphic.
-/
@[simps]
def Sigma.whiskerEquiv {J K : Type*} {f : J → C} {g : K → C} (e : J ≃ K) (w : ∀ j, g (e j) ≅ f j)
    [HasCoproduct f] [HasCoproduct g] : ∐ f∐ f ≅ ∐ g where
  hom := Sigma.map' e fun j => (w j).inv
  inv := Sigma.map' e.symm fun k => eqToHom (by simp) ≫ (w (e.symm k)).hom

Isomorphism between coproducts induced by an equivalence of indexing types

Informal description

Given an equivalence $e : J \simeq K$ between indexing types and a family of isomorphisms $w_j : g(e(j)) \cong f(j)$ for each $j \in J$, there is an isomorphism between the categorical coproducts $\coprod_{j \in J} f(j) \cong \coprod_{k \in K} g(k)$. Here, $f : J \to C$ and $g : K \to C$ are families of objects in a category $\mathcal{C}$ that has coproducts indexed by $J$ and $K$ respectively.

CategoryTheory.Limits.instHasProductSigmaFstSndOfPiObj instance

 {ι : Type*} (f : ι → Type*) (g : (i : ι) → (f i) → C) [∀ i, HasProduct (g i)] [HasProduct fun i => ∏ᶜ g i] :
  HasProduct fun p : Σ i, f i => g p.1 p.2

Full source

instance {ι : Type*} (f : ι → Type*) (g : (i : ι) → (f i) → C)
    [∀ i, HasProduct (g i)] [HasProduct fun i => ∏ᶜ g i] :
    HasProduct fun p : Σ i, f i => g p.1 p.2 where
  exists_limit := Nonempty.intro
    { cone := Fan.mk (∏ᶜ fun i => ∏ᶜ g i) (fun X => Pi.πPi.π (fun i => ∏ᶜ g i) X.1 ≫ Pi.π (g X.1) X.2)
      isLimit := mkFanLimit _ (fun s => Pi.lift fun b => Pi.lift fun c => s.proj ⟨b, c⟩)
        (by simp)
        (by intro s m w; simp only [Fan.mk_pt]; symm; ext i x; simp_all [Sigma.forall]) }

Existence of Products over Dependent Sum Indexing

Informal description

Given a family of types $\{f(i)\}_{i \in \iota}$ and a family of objects $\{g(i,j)\}_{j \in f(i)}$ in a category $\mathcal{C}$ for each $i \in \iota$, if $\mathcal{C}$ has products for each family $\{g(i,j)\}_{j \in f(i)}$ and also has a product for the family $\{\prod_{j \in f(i)} g(i,j)\}_{i \in \iota}$, then $\mathcal{C}$ has a product for the family $\{g(p.1, p.2)\}_{p \in \Sigma i, f(i)}$ indexed by the dependent sum type.

CategoryTheory.Limits.piPiIso definition

 {ι : Type*} (f : ι → Type*) (g : (i : ι) → (f i) → C) [∀ i, HasProduct (g i)] [HasProduct fun i => ∏ᶜ g i] :
  (∏ᶜ fun i => ∏ᶜ g i) ≅ (∏ᶜ fun p : Σ i, f i => g p.1 p.2)

Full source

/-- An iterated product is a product over a sigma type. -/
@[simps]
def piPiIso {ι : Type*} (f : ι → Type*) (g : (i : ι) → (f i) → C)
    [∀ i, HasProduct (g i)] [HasProduct fun i => ∏ᶜ g i] :
    (∏ᶜ fun i => ∏ᶜ g i) ≅ (∏ᶜ fun p : Σ i, f i => g p.1 p.2) where
  hom := Pi.lift fun ⟨i, x⟩ => Pi.π _ i ≫ Pi.π _ x
  inv := Pi.lift fun i => Pi.lift fun x => Pi.π _ (⟨i, x⟩ : Σ i, f i)

Isomorphism between iterated product and product over dependent sum indexing

Informal description

Given a family of types $\{f(i)\}_{i \in \iota}$ and a family of objects $\{g(i,j)\}_{j \in f(i)}$ in a category $\mathcal{C}$ for each $i \in \iota$, if $\mathcal{C}$ has products for each family $\{g(i,j)\}_{j \in f(i)}$ and also has a product for the family $\{\prod_{j \in f(i)} g(i,j)\}_{i \in \iota}$, then there is a natural isomorphism between the iterated product $\prod_{i \in \iota} \prod_{j \in f(i)} g(i,j)$ and the product $\prod_{p \in \Sigma i, f(i)} g(p.1, p.2)$ indexed by the dependent sum type.

CategoryTheory.Limits.instHasCoproductSigmaFstSndOfSigmaObj instance

 {ι : Type*} (f : ι → Type*) (g : (i : ι) → (f i) → C) [∀ i, HasCoproduct (g i)] [HasCoproduct fun i => ∐ g i] :
  HasCoproduct fun p : Σ i, f i => g p.1 p.2

Full source

instance {ι : Type*} (f : ι → Type*) (g : (i : ι) → (f i) → C)
    [∀ i, HasCoproduct (g i)] [HasCoproduct fun i => ∐ g i] :
    HasCoproduct fun p : Σ i, f i => g p.1 p.2 where
  exists_colimit := Nonempty.intro
    { cocone := Cofan.mk (∐ fun i => ∐ g i)
        (fun X => Sigma.ιSigma.ι (g X.1) X.2 ≫ Sigma.ι (fun i => ∐ g i) X.1)
      isColimit := mkCofanColimit _
        (fun s => Sigma.desc fun b => Sigma.desc fun c => s.inj ⟨b, c⟩)
        (by simp)
        (by intro s m w; simp only [Cofan.mk_pt]; symm; ext i x; simp_all [Sigma.forall]) }

Existence of Coproducts over Dependent Sum Indexing

Informal description

Given a family of types $\{f(i)\}_{i \in \iota}$ and a family of objects $\{g(i,j)\}_{j \in f(i)}$ in a category $\mathcal{C}$ for each $i \in \iota$, if $\mathcal{C}$ has coproducts for each family $\{g(i,j)\}_{j \in f(i)}$ and also has a coproduct for the family $\{\coprod_{j \in f(i)} g(i,j)\}_{i \in \iota}$, then $\mathcal{C}$ has a coproduct for the family $\{g(p.1, p.2)\}_{p \in \Sigma i, f(i)}$ indexed by the dependent sum type.

CategoryTheory.Limits.sigmaSigmaIso definition

 {ι : Type*} (f : ι → Type*) (g : (i : ι) → (f i) → C) [∀ i, HasCoproduct (g i)] [HasCoproduct fun i => ∐ g i] :
  (∐ fun i => ∐ g i) ≅ (∐ fun p : Σ i, f i => g p.1 p.2)

Full source

/-- An iterated coproduct is a coproduct over a sigma type. -/
@[simps]
def sigmaSigmaIso {ι : Type*} (f : ι → Type*) (g : (i : ι) → (f i) → C)
    [∀ i, HasCoproduct (g i)] [HasCoproduct fun i => ∐ g i] :
    (∐ fun i => ∐ g i) ≅ (∐ fun p : Σ i, f i => g p.1 p.2) where
  hom := Sigma.desc fun i => Sigma.desc fun x => Sigma.ι (fun p : Σ i, f i => g p.1 p.2) ⟨i, x⟩
  inv := Sigma.desc fun ⟨i, x⟩ => Sigma.ι (g i) x ≫ Sigma.ι (fun i => ∐ g i) i

Isomorphism between iterated coproduct and coproduct over dependent sum

Informal description

Given a family of types $\{f(i)\}_{i \in \iota}$ and a family of objects $\{g(i,j)\}_{j \in f(i)}$ in a category $\mathcal{C}$ for each $i \in \iota$, if $\mathcal{C}$ has coproducts for each family $\{g(i,j)\}_{j \in f(i)}$ and also has a coproduct for the family $\{\coprod_{j \in f(i)} g(i,j)\}_{i \in \iota}$, then there is a natural isomorphism between the iterated coproduct $\coprod_{i \in \iota} \coprod_{j \in f(i)} g(i,j)$ and the coproduct $\coprod_{p \in \Sigma i, f(i)} g(p.1, p.2)$ indexed by the dependent sum type.

CategoryTheory.Limits.piComparison definition

[HasProduct f] [HasProduct fun b => G.obj (f b)] : G.obj (∏ᶜ f) ⟶ ∏ᶜ fun b => G.obj (f b)

Full source

/-- The comparison morphism for the product of `f`. This is an iso iff `G` preserves the product
of `f`, see `PreservesProduct.ofIsoComparison`. -/
def piComparison [HasProduct f] [HasProduct fun b => G.obj (f b)] :
    G.obj (∏ᶜ f) ⟶ ∏ᶜ fun b => G.obj (f b) :=
  Pi.lift fun b => G.map (Pi.π f b)

Comparison morphism for products under a functor

Informal description

Given a functor $G : \mathcal{C} \to \mathcal{D}$ and a family of objects $\{f(b)\}_{b \in \beta}$ in $\mathcal{C}$ that has a product, the comparison morphism $\text{piComparison} G f$ is the canonical morphism from $G(\prod_{b \in \beta} f(b))$ to $\prod_{b \in \beta} G(f(b))$ in $\mathcal{D}$, constructed using the universal property of the product in $\mathcal{D}$ applied to the family of morphisms $\{G(\pi_b)\}_{b \in \beta}$, where $\pi_b : \prod_{b \in \beta} f(b) \to f(b)$ are the projection morphisms in $\mathcal{C}$.

CategoryTheory.Limits.piComparison_comp_π theorem

[HasProduct f] [HasProduct fun b => G.obj (f b)] (b : β) : piComparison G f ≫ Pi.π _ b = G.map (Pi.π f b)

Full source

@[reassoc (attr := simp)]
theorem piComparison_comp_π [HasProduct f] [HasProduct fun b => G.obj (f b)] (b : β) :
    piComparisonpiComparison G f ≫ Pi.π _ b = G.map (Pi.π f b) :=
  limit.lift_π _ (Discrete.mk b)

Commutativity of Product Comparison with Projections

Informal description

Let $\mathcal{C}$ and $\mathcal{D}$ be categories with products indexed by $\beta$, and let $G \colon \mathcal{C} \to \mathcal{D}$ be a functor. For any family of objects $\{f(b)\}_{b \in \beta}$ in $\mathcal{C}$ and any $b \in \beta$, the composition of the product comparison morphism $\text{piComparison}\, G\, f \colon G(\prod_{b \in \beta} f(b)) \to \prod_{b \in \beta} G(f(b))$ with the $b$-th projection $\pi_b \colon \prod_{b \in \beta} G(f(b)) \to G(f(b))$ equals the image under $G$ of the $b$-th projection $\pi_b \colon \prod_{b \in \beta} f(b) \to f(b)$ in $\mathcal{C}$. That is, the following diagram commutes: \[ \text{piComparison}\, G\, f \circ \pi_b = G(\pi_b). \]

CategoryTheory.Limits.map_lift_piComparison theorem

 [HasProduct f] [HasProduct fun b => G.obj (f b)] (P : C) (g : ∀ j, P ⟶ f j) :
  G.map (Pi.lift g) ≫ piComparison G f = Pi.lift fun j => G.map (g j)

Full source

@[reassoc (attr := simp)]
theorem map_lift_piComparison [HasProduct f] [HasProduct fun b => G.obj (f b)] (P : C)
    (g : ∀ j, P ⟶ f j) : G.map (Pi.lift g) ≫ piComparison G f = Pi.lift fun j => G.map (g j) := by
  ext j
  simp only [Discrete.functor_obj, Category.assoc, piComparison_comp_π, ← G.map_comp,
    limit.lift_π, Fan.mk_pt, Fan.mk_π_app]

Commutativity of Functor Application with Product Lifting and Comparison

Informal description

Let $\mathcal{C}$ and $\mathcal{D}$ be categories with products indexed by $\beta$, and let $G \colon \mathcal{C} \to \mathcal{D}$ be a functor. For any family of objects $\{f(b)\}_{b \in \beta}$ in $\mathcal{C}$, any object $P$ in $\mathcal{C}$, and any family of morphisms $\{g_j \colon P \to f(j)\}_{j \in \beta}$, the following diagram commutes: \[ G(\text{lift}(g)) \circ \text{piComparison}(G, f) = \text{lift}(G \circ g) \] where $\text{lift}(g) \colon P \to \prod_{b \in \beta} f(b)$ is the morphism induced by the universal property of the product in $\mathcal{C}$, and $\text{piComparison}(G, f) \colon G(\prod_{b \in \beta} f(b)) \to \prod_{b \in \beta} G(f(b))$ is the product comparison morphism in $\mathcal{D}$.

CategoryTheory.Limits.sigmaComparison definition

[HasCoproduct f] [HasCoproduct fun b => G.obj (f b)] : ∐ (fun b => G.obj (f b)) ⟶ G.obj (∐ f)

Full source

/-- The comparison morphism for the coproduct of `f`. This is an iso iff `G` preserves the coproduct
of `f`, see `PreservesCoproduct.ofIsoComparison`. -/
def sigmaComparison [HasCoproduct f] [HasCoproduct fun b => G.obj (f b)] :
    ∐ (fun b => G.obj (f b))∐ (fun b => G.obj (f b)) ⟶ G.obj (∐ f) :=
  Sigma.desc fun b => G.map (Sigma.ι f b)

Comparison Morphism for Coproducts under a Functor

Informal description

Given a functor $G \colon \mathcal{C} \to \mathcal{D}$ and a family of objects $\{f(b)\}_{b \in \beta}$ in $\mathcal{C}$ such that both $\mathcal{C}$ and $\mathcal{D}$ have coproducts indexed by $\beta$ for the respective families, the comparison morphism $\sigma \colon \coprod_{b \in \beta} G(f(b)) \to G(\coprod_{b \in \beta} f(b))$ is the unique morphism induced by the universal property of the coproduct in $\mathcal{D}$ applied to the family $\{G(\iota_b)\}_{b \in \beta}$, where $\iota_b \colon f(b) \to \coprod_{b \in \beta} f(b)$ are the coprojection morphisms in $\mathcal{C}$.

CategoryTheory.Limits.ι_comp_sigmaComparison theorem

 [HasCoproduct f] [HasCoproduct fun b => G.obj (f b)] (b : β) : Sigma.ι _ b ≫ sigmaComparison G f = G.map (Sigma.ι f b)

Full source

@[reassoc (attr := simp)]
theorem ι_comp_sigmaComparison [HasCoproduct f] [HasCoproduct fun b => G.obj (f b)] (b : β) :
    Sigma.ιSigma.ι _ b ≫ sigmaComparison G f = G.map (Sigma.ι f b) :=
  colimit.ι_desc _ (Discrete.mk b)

Compatibility of Coprojection with Comparison Morphism

Informal description

Let $\mathcal{C}$ and $\mathcal{D}$ be categories with coproducts indexed by a type $\beta$, and let $G \colon \mathcal{C} \to \mathcal{D}$ be a functor. For any family of objects $\{f(b)\}_{b \in \beta}$ in $\mathcal{C}$ and any $b \in \beta$, the composition of the $b$-th coprojection $\iota_b \colon f(b) \to \coprod_{b \in \beta} f(b)$ with the comparison morphism $\sigma \colon \coprod_{b \in \beta} G(f(b)) \to G(\coprod_{b \in \beta} f(b))$ equals the image under $G$ of the $b$-th coprojection in $\mathcal{C}$, i.e., \[ \iota_b \circ \sigma = G(\iota_b). \]

CategoryTheory.Limits.sigmaComparison_map_desc theorem

 [HasCoproduct f] [HasCoproduct fun b => G.obj (f b)] (P : C) (g : ∀ j, f j ⟶ P) :
  sigmaComparison G f ≫ G.map (Sigma.desc g) = Sigma.desc fun j => G.map (g j)

Full source

@[reassoc (attr := simp)]
theorem sigmaComparison_map_desc [HasCoproduct f] [HasCoproduct fun b => G.obj (f b)] (P : C)
    (g : ∀ j, f j ⟶ P) :
    sigmaComparisonsigmaComparison G f ≫ G.map (Sigma.desc g) = Sigma.desc fun j => G.map (g j) := by
  ext j
  simp only [Discrete.functor_obj, ι_comp_sigmaComparison_assoc, ← G.map_comp, colimit.ι_desc,
    Cofan.mk_pt, Cofan.mk_ι_app]

Commutation of Comparison Morphism with Coproduct Descent

Informal description

Let $\mathcal{C}$ and $\mathcal{D}$ be categories with coproducts indexed by a type $\beta$, and let $G \colon \mathcal{C} \to \mathcal{D}$ be a functor. For any family of objects $\{f(b)\}_{b \in \beta}$ in $\mathcal{C}$, any object $P$ in $\mathcal{C}$, and any collection of morphisms $\{g_j \colon f(j) \to P\}_{j \in \beta}$, the following diagram commutes: \[ \sigma \circ G(\coprod g) = \coprod (G \circ g) \] where $\sigma \colon \coprod_{b \in \beta} G(f(b)) \to G(\coprod_{b \in \beta} f(b))$ is the comparison morphism, $\coprod g \colon \coprod_{b \in \beta} f(b) \to P$ is the coproduct morphism induced by $\{g_j\}$, and $\coprod (G \circ g) \colon \coprod_{b \in \beta} G(f(b)) \to G(P)$ is the coproduct morphism induced by $\{G(g_j)\}$.

CategoryTheory.Limits.HasProducts abbrev

Full source

/-- An abbreviation for `Π J, HasLimitsOfShape (Discrete J) C` -/
abbrev HasProducts :=
  ∀ J : Type w, HasLimitsOfShape (Discrete J) C

Existence of Products in a Category

Informal description

A category $C$ has products if for every type $J$, it has limits of shape `Discrete J` (i.e., limits of diagrams indexed by discrete categories with objects from $J$).

CategoryTheory.Limits.HasCoproducts abbrev

Full source

/-- An abbreviation for `Π J, HasColimitsOfShape (Discrete J) C` -/
abbrev HasCoproducts :=
  ∀ J : Type w, HasColimitsOfShape (Discrete J) C

Existence of All Coproducts in a Category

Informal description

A category $\mathcal{C}$ has all coproducts indexed by any type $J$ if for every type $J$, $\mathcal{C}$ has colimits of shape $\mathrm{Discrete}\, J$. Here, $\mathrm{Discrete}\, J$ denotes the discrete category on the type $J$.

CategoryTheory.Limits.hasProducts_shrink theorem

[HasProducts.{max w w'} C] : HasProducts.{w} C

Full source

lemma hasProducts_shrink [HasProducts.{max w w'} C] : HasProducts.{w} C := fun J =>
  hasLimitsOfShape_of_equivalence (Discrete.equivalence Equiv.ulift : DiscreteDiscrete (ULift.{w'} J) ≌ _)

Shrinkage of Product Index Types in a Category

Informal description

If a category $\mathcal{C}$ has products indexed by types of size at most $\max(w, w')$, then it also has products indexed by types of size at most $w$.

CategoryTheory.Limits.hasCoproducts_shrink theorem

[HasCoproducts.{max w w'} C] : HasCoproducts.{w} C

Full source

lemma hasCoproducts_shrink [HasCoproducts.{max w w'} C] : HasCoproducts.{w} C := fun J =>
  hasColimitsOfShape_of_equivalence (Discrete.equivalence Equiv.ulift : DiscreteDiscrete (ULift.{w'} J) ≌ _)

Coproduct Index Type Size Reduction Theorem

Informal description

If a category $\mathcal{C}$ has all coproducts indexed by types of size at most $\max(w, w')$, then it also has all coproducts indexed by types of size at most $w$.

CategoryTheory.Limits.has_smallest_products_of_hasProducts theorem

[HasProducts.{w} C] : HasProducts.{0} C

Full source

theorem has_smallest_products_of_hasProducts [HasProducts.{w} C] : HasProducts.{0} C :=
  hasProducts_shrink

Finite Products from General Products Theorem

Informal description

If a category $\mathcal{C}$ has products indexed by types of arbitrary size, then it also has products indexed by finite types (types of size at most 0).

CategoryTheory.Limits.has_smallest_coproducts_of_hasCoproducts theorem

[HasCoproducts.{w} C] : HasCoproducts.{0} C

Full source

theorem has_smallest_coproducts_of_hasCoproducts [HasCoproducts.{w} C] : HasCoproducts.{0} C :=
  hasCoproducts_shrink

Finite Coproducts from General Coproducts Theorem

Informal description

If a category $\mathcal{C}$ has all coproducts indexed by types of size at most $w$, then it also has all coproducts indexed by finite types (types of size at most 0).

CategoryTheory.Limits.hasProducts_of_limit_fans theorem

 (lf : ∀ {J : Type w} (f : J → C), Fan f) (lf_isLimit : ∀ {J : Type w} (f : J → C), IsLimit (lf f)) : HasProducts.{w} C

Full source

theorem hasProducts_of_limit_fans (lf : ∀ {J : Type w} (f : J → C), Fan f)
    (lf_isLimit : ∀ {J : Type w} (f : J → C), IsLimit (lf f)) : HasProducts.{w} C :=
  fun _ : Type w =>
  { has_limit := fun F =>
      HasLimit.mk
        ⟨(Cones.postcompose Discrete.natIsoFunctor.inv).obj (lf fun j => F.obj ⟨j⟩),
          (IsLimit.postcomposeInvEquiv _ _).symm (lf_isLimit _)⟩ }

Existence of Products from Limit Fans

Informal description

Let $\mathcal{C}$ be a category. Suppose for every type $J$ and every family of objects $\{f(j)\}_{j \in J}$ in $\mathcal{C}$, there exists a fan $(P, \{\pi_j : P \to f(j)\}_{j \in J})$ that is a limit cone. Then $\mathcal{C}$ has all products indexed by arbitrary types.

CategoryTheory.Limits.hasProductsOfShape_of_hasProducts instance

[HasProducts.{w} C] (J : Type w) : HasProductsOfShape J C

Full source

instance (priority := 100) hasProductsOfShape_of_hasProducts [HasProducts.{w} C] (J : Type w) :
    HasProductsOfShape J C := inferInstance

Existence of Products for Specific Shapes from General Products

Informal description

For any category $\mathcal{C}$ that has all products indexed by arbitrary types, and for any type $J$, $\mathcal{C}$ has products of shape $J$. This means that if $\mathcal{C}$ has limits for all diagrams indexed by discrete categories of any type, then it specifically has limits for diagrams indexed by the discrete category on $J$.

CategoryTheory.Limits.hasCoproductsOfShape_of_hasCoproducts instance

[HasCoproducts.{w} C] (J : Type w) : HasCoproductsOfShape J C

Full source

instance (priority := 100) hasCoproductsOfShape_of_hasCoproducts [HasCoproducts.{w} C]
    (J : Type w) : HasCoproductsOfShape J C := inferInstance

Existence of Coproducts for All Types in a Category with All Coproducts

Informal description

For any category $\mathcal{C}$ that has all coproducts (indexed by arbitrary types), and for any type $J$, $\mathcal{C}$ has coproducts of shape $J$.

CategoryTheory.Limits.piConst definition

[Limits.HasProducts.{w} C] : C ⥤ Type wᵒᵖ ⥤ C

Full source

/-- The functor sending `(X, n)` to the product of copies of `X` indexed by `n`. -/
@[simps]
def piConst [Limits.HasProducts.{w} C] : C ⥤ Type wᵒᵖ ⥤ C where
  obj X := { obj n := ∏ᶜ fun _ : (unop n) ↦ X, map f := Limits.Pi.map' f.unop fun _ ↦ 𝟙 _ }
  map f := { app n := Limits.Pi.map fun _ ↦ f }

Constant product functor

Informal description

The functor $\text{piConst}$ sends an object $X$ in a category $\mathcal{C}$ (which has products indexed by arbitrary types) to the functor that maps each type $n$ (viewed as an object in $\text{Type } w^\text{op}$) to the product $\prod_{i \in n} X$ (where $i$ ranges over the elements of $n$), and maps each morphism $f$ in $\text{Type } w^\text{op}$ to the induced morphism between the corresponding products. For a morphism $f : X \to Y$ in $\mathcal{C}$, the functor $\text{piConst}$ maps it to the natural transformation whose component at each $n$ is the morphism $\prod_{i \in n} X \to \prod_{i \in n} Y$ induced by applying $f$ to each component.

CategoryTheory.Limits.piConstAdj definition

[Limits.HasProducts.{v} C] (X : C) : (piConst.obj X).rightOp ⊣ yoneda.obj X

Full source

/-- `n ↦ ∏ₙ X` is left adjoint to `Hom(-, X)`. -/
def piConstAdj [Limits.HasProducts.{v} C] (X : C) :
    (piConst.obj X).rightOp ⊣ yoneda.obj X where
  unit := { app n i := Limits.Pi.π (fun _ : n ↦ X) i }
  counit :=
  { app Y := (Limits.Pi.lift id).op,
    naturality _ _ _ := by apply Quiver.Hom.unop_inj; aesop_cat }
  left_triangle_components _ := by apply Quiver.Hom.unop_inj; aesop_cat

Adjunction between constant product functor and Yoneda embedding

Informal description

Given a category $\mathcal{C}$ with products indexed by arbitrary types and an object $X$ in $\mathcal{C}$, the functor $\text{piConst.obj } X$ (which sends a type $n$ to the product $\prod_{i \in n} X$) is left adjoint to the Yoneda embedding of $X$. The unit of this adjunction at a type $n$ is given by the family of projection morphisms $\pi_i : \prod_{i \in n} X \to X$ for each $i \in n$. The counit at an object $Y$ in $\mathcal{C}^\text{op}$ is the morphism $\prod_{i \in \text{Hom}(Y, X)} X \to Y$ induced by the identity morphisms on $X$.

CategoryTheory.Limits.sigmaConst definition

[Limits.HasCoproducts.{w} C] : C ⥤ Type w ⥤ C

Full source

/-- The functor sending `(X, n)` to the coproduct of copies of `X` indexed by `n`. -/
@[simps]
def sigmaConst [Limits.HasCoproducts.{w} C] : C ⥤ Type w ⥤ C where
  obj X := { obj n := ∐ fun _ : n ↦ X, map f := Limits.Sigma.map' f fun _ ↦ 𝟙 _ }
  map f := { app n := Limits.Sigma.map fun _ ↦ f }

Constant coproduct functor

Informal description

The functor $\text{sigmaConst}$ sends an object $X$ in a category $\mathcal{C}$ (which has coproducts indexed by arbitrary types) to the functor that maps each type $n$ to the coproduct $\coprod_{i \in n} X$ (where $i$ ranges over the elements of $n$), and maps each function $f \colon n \to m$ between types to the morphism $\coprod_{i \in n} X \to \coprod_{j \in m} X$ induced by $f$ and the identity morphisms on $X$. For a morphism $f \colon X \to Y$ in $\mathcal{C}$, the functor $\text{sigmaConst}$ maps it to the natural transformation whose component at each $n$ is the morphism $\coprod_{i \in n} X \to \coprod_{i \in n} Y$ induced by applying $f$ to each component.

CategoryTheory.Limits.sigmaConstAdj definition

[Limits.HasCoproducts.{v} C] (X : C) : sigmaConst.obj X ⊣ coyoneda.obj (Opposite.op X)

Full source

/-- `n ↦ ∐ₙ X` is left adjoint to `Hom(X, -)`. -/
def sigmaConstAdj [Limits.HasCoproducts.{v} C] (X : C) :
    sigmaConstsigmaConst.obj X ⊣ coyoneda.obj (Opposite.op X) where
  unit := { app n i := Limits.Sigma.ι (fun _ : n ↦ X) i }
  counit := { app Y := Limits.Sigma.desc id }

Adjunction between constant coproduct functor and hom-functor

Informal description

For a category $\mathcal{C}$ with coproducts indexed by arbitrary types, and for any object $X$ in $\mathcal{C}$, the functor $\text{sigmaConst}(X)$ that sends a type $n$ to the coproduct $\coprod_{i \in n} X$ is left adjoint to the functor $\text{Hom}(X, -)$. Here, the unit of the adjunction at a type $n$ is given by the collection of coprojection morphisms $\iota_i : X \to \coprod_{i \in n} X$ for each $i \in n$, and the counit at an object $Y$ is given by the universal morphism $\coprod_{x \in \text{Hom}(X,Y)} X \to Y$ induced by the identity map on $\text{Hom}(X,Y)$.

CategoryTheory.Limits.limitConeOfUnique definition

[Unique β] (f : β → C) : LimitCone (Discrete.functor f)

Full source

/-- The limit cone for the product over an index type with exactly one term. -/
@[simps]
def limitConeOfUnique [Unique β] (f : β → C) : LimitCone (Discrete.functor f) where
  cone :=
    { pt := f default
      π := Discrete.natTrans (fun ⟨j⟩ => eqToHom (by
        dsimp
        congr
        subsingleton)) }
  isLimit :=
    { lift := fun s => s.π.app default
      fac := fun s j => by
        have h := Subsingleton.elim j default
        subst h
        simp
      uniq := fun s m w => by
        specialize w default
        simpa using w }

Limit cone for product over a unique index type

Informal description

Given a unique index type $\beta$ (i.e., a type with exactly one term) and a functor $f \colon \beta \to C$, the limit cone for the product over $\beta$ is constructed with the object $f(\text{default})$ and the natural transformation given by the identity morphism (up to the unique isomorphism between any two terms in $\beta$). This cone is indeed a limit cone, as any other cone over the diagram factors uniquely through it.

CategoryTheory.Limits.hasProduct_unique instance

[Nonempty β] [Subsingleton β] (f : β → C) : HasProduct f

Full source

instance (priority := 100) hasProduct_unique [Nonempty β] [Subsingleton β] (f : β → C) :
    HasProduct f :=
  let ⟨_⟩ := nonempty_unique β; HasLimit.mk (limitConeOfUnique f)

Existence of Products for Families over Subsingleton Types

Informal description

For any category $\mathcal{C}$ and any nonempty subsingleton type $\beta$ (i.e., a type with at most one element), the product of any family of objects $f \colon \beta \to \mathcal{C}$ exists in $\mathcal{C}$.

CategoryTheory.Limits.productUniqueIso definition

[Unique β] (f : β → C) : ∏ᶜ f ≅ f default

Full source

/-- A product over an index type with exactly one term is just the object over that term. -/
@[simps!]
def productUniqueIso [Unique β] (f : β → C) : ∏ᶜ f∏ᶜ f ≅ f default :=
  IsLimit.conePointUniqueUpToIso (limit.isLimit _) (limitConeOfUnique f).isLimit

Isomorphism between product over unique index and its single term

Informal description

Given a category $\mathcal{C}$ and a unique index type $\beta$ (i.e., a type with exactly one term), the categorical product $\prod_{b \in \beta} f(b)$ is isomorphic to the object $f(\text{default})$, where $\text{default}$ is the unique term of $\beta$. This isomorphism arises from the fact that the limit cone for the product over $\beta$ is constructed using the object $f(\text{default})$ and the identity morphism.

CategoryTheory.Limits.colimitCoconeOfUnique definition

[Unique β] (f : β → C) : ColimitCocone (Discrete.functor f)

Full source

/-- The colimit cocone for the coproduct over an index type with exactly one term. -/
@[simps]
def colimitCoconeOfUnique [Unique β] (f : β → C) : ColimitCocone (Discrete.functor f) where
  cocone :=
    { pt := f default
      ι := Discrete.natTrans (fun ⟨j⟩ => eqToHom (by
        dsimp
        congr
        subsingleton)) }
  isColimit :=
    { desc := fun s => s.ι.app default
      fac := fun s j => by
        have h := Subsingleton.elim j default
        subst h
        apply Category.id_comp
      uniq := fun s m w => by
        specialize w default
        erw [Category.id_comp] at w
        exact w }

Colimit cocone for coproduct over a unique index type

Informal description

Given a category $C$ and an index type $\beta$ with exactly one term (i.e., `Unique β`), the colimit cocone for the coproduct of a family of objects $f : \beta \to C$ is constructed with the cocone point being $f(\text{default})$, where $\text{default}$ is the unique term of $\beta$. The cocone morphisms are given by the identity morphisms, utilizing the fact that $\beta$ has only one term. The colimit property is satisfied since any cocone over this diagram must factor uniquely through the identity morphism on $f(\text{default})$.

CategoryTheory.Limits.hasCoproduct_unique instance

[Nonempty β] [Subsingleton β] (f : β → C) : HasCoproduct f

Full source

instance (priority := 100) hasCoproduct_unique [Nonempty β] [Subsingleton β] (f : β → C) :
    HasCoproduct f :=
  let ⟨_⟩ := nonempty_unique β; HasColimit.mk (colimitCoconeOfUnique f)

Existence of Coproducts for Subsingleton Index Types

Informal description

For any category $\mathcal{C}$ and any nonempty index type $\beta$ with at most one term (i.e., $\beta$ is a subsingleton), the coproduct of a family of objects $f : \beta \to \mathcal{C}$ exists.

CategoryTheory.Limits.coproductUniqueIso definition

[Unique β] (f : β → C) : ∐ f ≅ f default

Full source

/-- A coproduct over an index type with exactly one term is just the object over that term. -/
@[simps!]
def coproductUniqueIso [Unique β] (f : β → C) : ∐ f∐ f ≅ f default :=
  IsColimit.coconePointUniqueUpToIso (colimit.isColimit _) (colimitCoconeOfUnique f).isColimit

Isomorphism between coproduct and object over unique index

Informal description

Given a category $\mathcal{C}$ and an index type $\beta$ with exactly one term (i.e., `Unique β`), the coproduct $\coprod_{b \in \beta} f(b)$ of a family of objects $f : \beta \to \mathcal{C}$ is isomorphic to the object $f(\text{default})$, where $\text{default}$ is the unique term of $\beta$.

CategoryTheory.Limits.Pi.reindex definition

: piObj (f ∘ ε) ≅ piObj f

Full source

/-- Reindex a categorical product via an equivalence of the index types. -/
def Pi.reindex : piObjpiObj (f ∘ ε) ≅ piObj f :=
  HasLimit.isoOfEquivalence (Discrete.equivalence ε) (Discrete.natIso fun _ => Iso.refl _)

Reindexing isomorphism for categorical products

Informal description

Given an equivalence $\varepsilon$ between index types $\alpha$ and $\beta$, and a family of objects $f : \beta \to \mathcal{C}$ in a category $\mathcal{C}$, there is a natural isomorphism between the product $\prod_{b \in \beta} f(b)$ and the reindexed product $\prod_{a \in \alpha} f(\varepsilon(a))$. This isomorphism is constructed using the equivalence of categories induced by $\varepsilon$ and the identity isomorphism on each object in the family.

CategoryTheory.Limits.Pi.reindex_hom_π theorem

(b : β) : (Pi.reindex ε f).hom ≫ Pi.π f (ε b) = Pi.π (f ∘ ε) b

Full source

@[reassoc (attr := simp)]
theorem Pi.reindex_hom_π (b : β) : (Pi.reindex ε f).hom ≫ Pi.π f (ε b) = Pi.π (f ∘ ε) b := by
  dsimp [Pi.reindex]
  simp only [HasLimit.isoOfEquivalence_hom_π, Discrete.equivalence_inverse, Discrete.functor_obj,
    Function.comp_apply, Functor.id_obj, Discrete.equivalence_functor, Functor.comp_obj,
    Discrete.natIso_inv_app, Iso.refl_inv, Category.id_comp]
  exact limit.w (Discrete.functor (f ∘ ε)) (Discrete.eqToHom' (ε.symm_apply_apply b))

Compatibility of reindexing isomorphism with projections: forward direction

Informal description

For any index $b \in \beta$, the composition of the forward morphism of the reindexing isomorphism $\text{Pi.reindex}\ \varepsilon\ f$ with the projection $\pi_{f(\varepsilon(b))}$ from the product $\prod_{b \in \beta} f(b)$ equals the projection $\pi_{(f \circ \varepsilon)(b)}$ from the reindexed product $\prod_{a \in \alpha} f(\varepsilon(a))$.

CategoryTheory.Limits.Pi.reindex_inv_π theorem

(b : β) : (Pi.reindex ε f).inv ≫ Pi.π (f ∘ ε) b = Pi.π f (ε b)

Full source

@[reassoc (attr := simp)]
theorem Pi.reindex_inv_π (b : β) : (Pi.reindex ε f).inv ≫ Pi.π (f ∘ ε) b = Pi.π f (ε b) := by
  simp [Iso.inv_comp_eq]

Compatibility of reindexing isomorphism with projections: inverse direction

Informal description

For any index $b \in \beta$, the composition of the inverse morphism of the reindexing isomorphism $\text{Pi.reindex}\ \varepsilon\ f$ with the projection $\pi_{(f \circ \varepsilon)(b)}$ from the reindexed product $\prod_{a \in \alpha} f(\varepsilon(a))$ equals the projection $\pi_{f(\varepsilon(b))}$ from the original product $\prod_{b \in \beta} f(b)$.

CategoryTheory.Limits.Sigma.reindex definition

: sigmaObj (f ∘ ε) ≅ sigmaObj f

Full source

/-- Reindex a categorical coproduct via an equivalence of the index types. -/
def Sigma.reindex : sigmaObjsigmaObj (f ∘ ε) ≅ sigmaObj f :=
  HasColimit.isoOfEquivalence (Discrete.equivalence ε) (Discrete.natIso fun _ => Iso.refl _)

Reindexing isomorphism for coproducts via equivalence

Informal description

Given an equivalence $\varepsilon$ between index types $\alpha$ and $\beta$, and a family of objects $\{f(b)\}_{b \in \beta}$ in a category $\mathcal{C}$, there is a natural isomorphism between the coproducts $\coprod_{b \in \beta} f(\varepsilon(b))$ and $\coprod_{a \in \alpha} f(a)$. This isomorphism is constructed using the equivalence of categories induced by $\varepsilon$ and the identity isomorphism on each object in the family.

CategoryTheory.Limits.Sigma.ι_reindex_hom theorem

(b : β) : Sigma.ι (f ∘ ε) b ≫ (Sigma.reindex ε f).hom = Sigma.ι f (ε b)

Full source

@[reassoc (attr := simp)]
theorem Sigma.ι_reindex_hom (b : β) :
    Sigma.ιSigma.ι (f ∘ ε) b ≫ (Sigma.reindex ε f).hom = Sigma.ι f (ε b) := by
  dsimp [Sigma.reindex]
  simp only [HasColimit.isoOfEquivalence_hom_π, Functor.id_obj, Discrete.functor_obj,
    Function.comp_apply, Discrete.equivalence_functor, Discrete.equivalence_inverse,
    Functor.comp_obj, Discrete.natIso_inv_app, Iso.refl_inv, Category.id_comp]
  have h := colimit.w (Discrete.functor f) (Discrete.eqToHom' (ε.apply_symm_apply (ε b)))
  simp only [Discrete.functor_obj] at h
  erw [← h, eqToHom_map, eqToHom_map, eqToHom_trans_assoc]
  all_goals { simp }

Compatibility of coprojection with reindexing isomorphism

Informal description

For any $b \in \beta$, the composition of the coprojection morphism $\iota_b \colon f(\varepsilon(b)) \to \coprod_{b \in \beta} f(\varepsilon(b))$ with the forward isomorphism $(Sigma.reindex\ \varepsilon\ f).hom \colon \coprod_{b \in \beta} f(\varepsilon(b)) \to \coprod_{a \in \alpha} f(a)$ equals the coprojection morphism $\iota_{\varepsilon(b)} \colon f(\varepsilon(b)) \to \coprod_{a \in \alpha} f(a)$.

CategoryTheory.Limits.Sigma.ι_reindex_inv theorem

(b : β) : Sigma.ι f (ε b) ≫ (Sigma.reindex ε f).inv = Sigma.ι (f ∘ ε) b

Full source

@[reassoc (attr := simp)]
theorem Sigma.ι_reindex_inv (b : β) :
    Sigma.ιSigma.ι f (ε b) ≫ (Sigma.reindex ε f).inv = Sigma.ι (f ∘ ε) b := by simp [Iso.comp_inv_eq]

Compatibility of coprojection with inverse reindexing isomorphism

Informal description

For any $b \in \beta$, the composition of the coprojection morphism $\iota_{\varepsilon(b)} \colon f(\varepsilon(b)) \to \coprod_{a \in \alpha} f(a)$ with the inverse isomorphism $(Sigma.reindex\ \varepsilon\ f).inv \colon \coprod_{a \in \alpha} f(a) \to \coprod_{b \in \beta} f(\varepsilon(b))$ equals the coprojection morphism $\iota_b \colon f(\varepsilon(b)) \to \coprod_{b \in \beta} f(\varepsilon(b))$.

Mathlib.CategoryTheory.Limits.Shapes.Products

Main definitions

Implementation notes