Formal Coproducts

In this file we construct the category of formal coproducts given a category.

Main definitions

• FormalCoproduct: the category of formal coproducts, which are indexed sets of objects in a category. A morphism ∐ i : X.I, X.obj i ⟶ ∐ j : Y.I, Y.obj j is given by a function f : X.I → Y.I and maps X.obj i ⟶ Y.obj (f i) for each i : X.I.
• FormalCoproduct.eval : (Cᵒᵖ ⥤ A) ⥤ ((FormalCoproduct C)ᵒᵖ ⥤ A): the universal property that a presheaf on C where the target category has arbitrary coproducts, can be extended to a presheaf on FormalCoproduct C.

TODO

• FormalCoproduct.incl C : C ⥤ FormalCoproduct.{w} C probably preserves every limit?

structure CategoryTheory.Limits.FormalCoproduct (C : Type u) : Type (max u (w + 1))

A formal coproduct is an indexed set of objects, where ⟨I, f⟩ corresponds to the "formal coproduct" ⨿ (i : I), f i, where f i : C is the iᵗʰ component.

• I : Type w

  The indexing type.

• obj (i : self.I) : C

  The object in the original category indexed by x : I.

structure CategoryTheory.Limits.FormalCoproduct.Hom {C : Type u} [Category.{v, u} C] (X Y : FormalCoproduct C) : Type (max v w)

A morphism (⨿ (i : X.I), X.obj i) ⟶ (⨿ (j : Y.I), Y.obj i) is given by first a function on the indexing sets f : X.I → Y.I, and then for each i : X.I a morphism X.obj i ⟶ Y.obj (f i).

• f : X.I → Y.I

  The function on the indexing sets.

• φ (i : X.I) : X.obj i ⟶ Y.obj (self.f i)

  The map on each component.

instance CategoryTheory.Limits.FormalCoproduct.category {C : Type u} [Category.{v, u} C] : Category.{max w v, max (w + 1) u} (FormalCoproduct C)

Equations

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

@[simp]

theorem CategoryTheory.Limits.FormalCoproduct.category_id_φ {C : Type u} [Category.{v, u} C] (X : FormalCoproduct C) (x✝ : X.I) : (CategoryStruct.id X).φ x✝ = CategoryStruct.id (X.obj x✝)

@[simp]

theorem CategoryTheory.Limits.FormalCoproduct.category_comp_φ {C : Type u} [Category.{v, u} C] {X✝ Y✝ Z✝ : FormalCoproduct C} (α : X✝.Hom Y✝) (β : Y✝.Hom Z✝) (x✝ : X✝.I) : (CategoryStruct.comp α β).φ x✝ = CategoryStruct.comp (α.φ x✝) (β.φ (α.f x✝))

@[simp]

theorem CategoryTheory.Limits.FormalCoproduct.category_id_f {C : Type u} [Category.{v, u} C] (X : FormalCoproduct C) (a : X.I) : (CategoryStruct.id X).f a = a

@[simp]

theorem CategoryTheory.Limits.FormalCoproduct.category_comp_f {C : Type u} [Category.{v, u} C] {X✝ Y✝ Z✝ : FormalCoproduct C} (α : X✝.Hom Y✝) (β : Y✝.Hom Z✝) (a✝ : X✝.I) : (CategoryStruct.comp α β).f a✝ = β.f (α.f a✝)

theorem CategoryTheory.Limits.FormalCoproduct.hom_ext {C : Type u} [Category.{v, u} C] {X Y : FormalCoproduct C} {f g : X ⟶ Y} (h₁ : f.f = g.f) (h₂ : ∀ (i : X.I), CategoryStruct.comp (f.φ i) (eqToHom ⋯) = g.φ i) : f = g

theorem CategoryTheory.Limits.FormalCoproduct.hom_ext_iff {C : Type u} [Category.{v, u} C] {X Y : FormalCoproduct C} (f g : X ⟶ Y) : f = g ↔ ∃ (h₁ : f.f = g.f), ∀ (i : X.I), CategoryStruct.comp (f.φ i) (eqToHom ⋯) = g.φ i

theorem CategoryTheory.Limits.FormalCoproduct.hom_ext_iff' {C : Type u} [Category.{v, u} C] {X Y : FormalCoproduct C} (f g : X ⟶ Y) : f = g ↔ ∀ (i : X.I), ∃ (h₁ : f.f i = g.f i), CategoryStruct.comp (f.φ i) (eqToHom ⋯) = g.φ i

def CategoryTheory.Limits.FormalCoproduct.isoOfComponents {C : Type u} [Category.{v, u} C] {X Y : FormalCoproduct C} (e : X.I ≃ Y.I) (h : (i : X.I) → X.obj i ≅ Y.obj (e i)) : X ≅ Y

A way to create isomorphisms in the category of formal coproducts, by creating an Equiv between the indexing sets, and then correspondingly isomorphisms of each component.

Equations

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

@[simp]

theorem CategoryTheory.Limits.FormalCoproduct.isoOfComponents_hom_f {C : Type u} [Category.{v, u} C] {X Y : FormalCoproduct C} (e : X.I ≃ Y.I) (h : (i : X.I) → X.obj i ≅ Y.obj (e i)) (a : X.I) : (isoOfComponents e h).hom.f a = e a

@[simp]

theorem CategoryTheory.Limits.FormalCoproduct.isoOfComponents_inv_φ {C : Type u} [Category.{v, u} C] {X Y : FormalCoproduct C} (e : X.I ≃ Y.I) (h : (i : X.I) → X.obj i ≅ Y.obj (e i)) (i : Y.I) : (isoOfComponents e h).inv.φ i = CategoryStruct.comp (eqToHom ⋯) (h (e.symm i)).inv

@[simp]

theorem CategoryTheory.Limits.FormalCoproduct.isoOfComponents_hom_φ {C : Type u} [Category.{v, u} C] {X Y : FormalCoproduct C} (e : X.I ≃ Y.I) (h : (i : X.I) → X.obj i ≅ Y.obj (e i)) (i : X.I) : (isoOfComponents e h).hom.φ i = (h i).hom

@[simp]

theorem CategoryTheory.Limits.FormalCoproduct.isoOfComponents_inv_f {C : Type u} [Category.{v, u} C] {X Y : FormalCoproduct C} (e : X.I ≃ Y.I) (h : (i : X.I) → X.obj i ≅ Y.obj (e i)) (a : Y.I) : (isoOfComponents e h).inv.f a = e.symm a

def CategoryTheory.Limits.FormalCoproduct.incl (C : Type u) [Category.{v, u} C] : Functor C (FormalCoproduct C)

An object of the original category produces a formal coproduct on that object only, so indexed by PUnit, the type with one element.

Equations

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

@[simp]

theorem CategoryTheory.Limits.FormalCoproduct.incl_obj_obj (C : Type u) [Category.{v, u} C] (X : C) (x✝ : PUnit.{w + 1}) : ((incl C).obj X).obj x✝ = X

@[simp]

theorem CategoryTheory.Limits.FormalCoproduct.incl_map_φ (C : Type u) [Category.{v, u} C] {X✝ Y✝ : C} (f : X✝ ⟶ Y✝) (x✝ : { I := PUnit.{w + 1}, obj := fun (x : PUnit.{w + 1}) => X✝ }.I) : ((incl C).map f).φ x✝ = f

@[simp]

theorem CategoryTheory.Limits.FormalCoproduct.incl_obj_I (C : Type u) [Category.{v, u} C] (X : C) : ((incl C).obj X).I = PUnit.{w + 1}

@[simp]

theorem CategoryTheory.Limits.FormalCoproduct.incl_map_f (C : Type u) [Category.{v, u} C] {X✝ Y✝ : C} (f : X✝ ⟶ Y✝) (x✝ : { I := PUnit.{w + 1}, obj := fun (x : PUnit.{w + 1}) => X✝ }.I) : ((incl C).map f).f x✝ = PUnit.unit

def CategoryTheory.Limits.FormalCoproduct.Hom.fromIncl {C : Type u} [Category.{v, u} C] {X : C} {Y : FormalCoproduct C} (i : Y.I) (f : X ⟶ Y.obj i) : (incl C).obj X ⟶ Y

A map incl(X) ⟶ Y is specified by an element of Y's indexing set, and then a morphism X ⟶ Y.obj i in the original category.

Equations

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

@[simp]

theorem CategoryTheory.Limits.FormalCoproduct.Hom.fromIncl_φ {C : Type u} [Category.{v, u} C] {X : C} {Y : FormalCoproduct C} (i : Y.I) (f : X ⟶ Y.obj i) (x✝ : ((incl C).obj X).I) : (fromIncl i f).φ x✝ = f

@[simp]

theorem CategoryTheory.Limits.FormalCoproduct.Hom.fromIncl_f {C : Type u} [Category.{v, u} C] {X : C} {Y : FormalCoproduct C} (i : Y.I) (f : X ⟶ Y.obj i) (x✝ : ((incl C).obj X).I) : (fromIncl i f).f x✝ = i

def CategoryTheory.Limits.FormalCoproduct.Hom.asSigma {C : Type u} [Category.{v, u} C] {X : C} {Y : FormalCoproduct C} (f : (incl C).obj X ⟶ Y) : (i : Y.I) × (X ⟶ Y.obj i)

A map incl(X) ⟶ Y is specified by an element of Y's indexing set, and then a morphism X ⟶ Y.obj i in the original category.

Equations

• CategoryTheory.Limits.FormalCoproduct.Hom.asSigma f = ⟨f.f PUnit.unit, f.φ PUnit.unit⟩

theorem CategoryTheory.Limits.FormalCoproduct.Hom.fromIncl_asSigma {C : Type u} [Category.{v, u} C] {X : C} {Y : FormalCoproduct C} (f : (incl C).obj X ⟶ Y) : fromIncl (asSigma f).fst (asSigma f).snd = f

def CategoryTheory.Limits.FormalCoproduct.inclHomEquiv {C : Type u} [Category.{v, u} C] (X : C) (Y : FormalCoproduct C) : ((incl C).obj X ⟶ Y) ≃ (i : Y.I) × (X ⟶ Y.obj i)

A map incl(X) ⟶ Y is specified by an element of Y's indexing set, and then a morphism X ⟶ Y.obj i in the original category.

Equations

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

@[simp]

theorem CategoryTheory.Limits.FormalCoproduct.inclHomEquiv_symm_apply_φ {C : Type u} [Category.{v, u} C] (X : C) (Y : FormalCoproduct C) (f : (i : Y.I) × (X ⟶ Y.obj i)) (x✝ : ((incl C).obj X).I) : ((inclHomEquiv X Y).symm f).φ x✝ = f.snd

@[simp]

theorem CategoryTheory.Limits.FormalCoproduct.inclHomEquiv_apply_snd {C : Type u} [Category.{v, u} C] (X : C) (Y : FormalCoproduct C) (f : (incl C).obj X ⟶ Y) : ((inclHomEquiv X Y) f).snd = f.φ PUnit.unit

@[simp]

theorem CategoryTheory.Limits.FormalCoproduct.inclHomEquiv_apply_fst {C : Type u} [Category.{v, u} C] (X : C) (Y : FormalCoproduct C) (f : (incl C).obj X ⟶ Y) : ((inclHomEquiv X Y) f).fst = f.f PUnit.unit

@[simp]

theorem CategoryTheory.Limits.FormalCoproduct.inclHomEquiv_symm_apply_f {C : Type u} [Category.{v, u} C] (X : C) (Y : FormalCoproduct C) (f : (i : Y.I) × (X ⟶ Y.obj i)) (x✝ : ((incl C).obj X).I) : ((inclHomEquiv X Y).symm f).f x✝ = f.fst

def CategoryTheory.Limits.FormalCoproduct.fullyFaithfulIncl {C : Type u} [Category.{v, u} C] : (incl C).FullyFaithful

incl is fully faithful, which means that (X ⟶ Y) ≃ (incl(X) ⟶ incl(Y)).

Equations

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

@[simp]

theorem CategoryTheory.Limits.FormalCoproduct.fullyFaithfulIncl_preimage {C : Type u} [Category.{v, u} C] {X✝ Y✝ : C} (f : (incl C).obj X✝ ⟶ (incl C).obj Y✝) : fullyFaithfulIncl.preimage f = f.φ PUnit.unit

instance CategoryTheory.Limits.FormalCoproduct.instFullIncl {C : Type u} [Category.{v, u} C] : (incl C).Full

instance CategoryTheory.Limits.FormalCoproduct.instFaithfulIncl {C : Type u} [Category.{v, u} C] : (incl C).Faithful

def CategoryTheory.Limits.FormalCoproduct.homOfPiHom {C : Type u} [Category.{v, u} C] (X : C) {J : Type w} (f : J → C) (φ : (j : J) → f j ⟶ X) : { I := J, obj := f } ⟶ (incl C).obj X

A family of maps with the same target can be turned into one arrow in the category of formal coproducts. This is used in Čech cohomology.

Equations

• CategoryTheory.Limits.FormalCoproduct.homOfPiHom X f φ = { f := fun (x : { I := J, obj := f }.I) => PUnit.unit, φ := φ }

@[simp]

theorem CategoryTheory.Limits.FormalCoproduct.homOfPiHom_f {C : Type u} [Category.{v, u} C] (X : C) {J : Type w} (f : J → C) (φ : (j : J) → f j ⟶ X) (x✝ : { I := J, obj := f }.I) : (homOfPiHom X f φ).f x✝ = PUnit.unit

@[simp]

theorem CategoryTheory.Limits.FormalCoproduct.homOfPiHom_φ {C : Type u} [Category.{v, u} C] (X : C) {J : Type w} (f : J → C) (φ : (j : J) → f j ⟶ X) (j : J) : (homOfPiHom X f φ).φ j = φ j

def CategoryTheory.Limits.FormalCoproduct.cofan {C : Type u} [Category.{v, u} C] (𝒜 : Type w) (f : 𝒜 → FormalCoproduct C) : Cofan f

We construct explicitly the data that specify the coproduct of a given family of formal coproducts.

Equations

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

theorem CategoryTheory.Limits.FormalCoproduct.cofan_inj {C : Type u} [Category.{v, u} C] {𝒜 : Type w} {f : 𝒜 → FormalCoproduct C} (i : 𝒜) : (cofan 𝒜 f).inj i = { f := fun (x : (f i).I) => ⟨i, x⟩, φ := fun (x : (f i).I) => CategoryStruct.id ((f i).obj x) }

@[simp]

theorem CategoryTheory.Limits.FormalCoproduct.cofan_inj_f_fst {C : Type u} [Category.{v, u} C] {𝒜 : Type w} {f : 𝒜 → FormalCoproduct C} (i : 𝒜) (x : (f i).I) : (((cofan 𝒜 f).inj i).f x).fst = i

@[simp]

theorem CategoryTheory.Limits.FormalCoproduct.cofan_inj_f_snd {C : Type u} [Category.{v, u} C] {𝒜 : Type w} {f : 𝒜 → FormalCoproduct C} (i : 𝒜) (x : (f i).I) : (((cofan 𝒜 f).inj i).f x).snd = x

@[simp]

theorem CategoryTheory.Limits.FormalCoproduct.cofan_inj_φ {C : Type u} [Category.{v, u} C] {𝒜 : Type w} {f : 𝒜 → FormalCoproduct C} (i : 𝒜) (x : (f i).I) : ((cofan 𝒜 f).inj i).φ x = CategoryStruct.id ((f i).obj x)

def CategoryTheory.Limits.FormalCoproduct.cofanHomEquiv {C : Type u} [Category.{v, u} C] (𝒜 : Type w) (f : 𝒜 → FormalCoproduct C) (t : FormalCoproduct C) : ((cofan 𝒜 f).pt ⟶ t) ≃ ((i : 𝒜) → f i ⟶ t)

The explicit Equiv between maps from the constructed coproduct cofan 𝒜 f and families of maps from each component, which is the universal property of coproducts.

Equations

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

@[simp]

theorem CategoryTheory.Limits.FormalCoproduct.cofanHomEquiv_apply_f {C : Type u} [Category.{v, u} C] (𝒜 : Type w) (f : 𝒜 → FormalCoproduct C) (t : FormalCoproduct C) (m : (cofan 𝒜 f).pt ⟶ t) (i : 𝒜) (a✝ : (f i).I) : ((cofanHomEquiv 𝒜 f t) m i).f a✝ = m.f (((cofan 𝒜 f).inj i).f a✝)

@[simp]

theorem CategoryTheory.Limits.FormalCoproduct.cofanHomEquiv_apply_φ {C : Type u} [Category.{v, u} C] (𝒜 : Type w) (f : 𝒜 → FormalCoproduct C) (t : FormalCoproduct C) (m : (cofan 𝒜 f).pt ⟶ t) (i : 𝒜) (x✝ : (f i).I) : ((cofanHomEquiv 𝒜 f t) m i).φ x✝ = m.φ (((cofan 𝒜 f).inj i).f x✝)

@[simp]

theorem CategoryTheory.Limits.FormalCoproduct.cofanHomEquiv_symm_apply_φ {C : Type u} [Category.{v, u} C] (𝒜 : Type w) (f : 𝒜 → FormalCoproduct C) (t : FormalCoproduct C) (s : (i : 𝒜) → f i ⟶ t) (p : (cofan 𝒜 f).pt.I) : ((cofanHomEquiv 𝒜 f t).symm s).φ p = (s p.fst).φ p.snd

@[simp]

theorem CategoryTheory.Limits.FormalCoproduct.cofanHomEquiv_symm_apply_f {C : Type u} [Category.{v, u} C] (𝒜 : Type w) (f : 𝒜 → FormalCoproduct C) (t : FormalCoproduct C) (s : (i : 𝒜) → f i ⟶ t) (p : (cofan 𝒜 f).pt.I) : ((cofanHomEquiv 𝒜 f t).symm s).f p = (s p.fst).f p.snd

def CategoryTheory.Limits.FormalCoproduct.isColimitCofan {C : Type u} [Category.{v, u} C] (𝒜 : Type w) (f : 𝒜 → FormalCoproduct C) : IsColimit (cofan 𝒜 f)

cofan 𝒜 f is a coproduct of f.

Equations

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

@[simp]

theorem CategoryTheory.Limits.FormalCoproduct.isColimitCofan_desc_f {C : Type u} [Category.{v, u} C] (𝒜 : Type w) (f : 𝒜 → FormalCoproduct C) (t : Cofan f) (p : (cofan 𝒜 f).pt.I) : ((isColimitCofan 𝒜 f).desc t).f p = (t.inj p.fst).f p.snd

@[simp]

theorem CategoryTheory.Limits.FormalCoproduct.isColimitCofan_desc_φ {C : Type u} [Category.{v, u} C] (𝒜 : Type w) (f : 𝒜 → FormalCoproduct C) (t : Cofan f) (p : (cofan 𝒜 f).pt.I) : ((isColimitCofan 𝒜 f).desc t).φ p = (t.inj p.fst).φ p.snd

instance CategoryTheory.Limits.FormalCoproduct.instHasCoproducts {C : Type u} [Category.{v, u} C] : HasCoproducts (FormalCoproduct C)

noncomputable def CategoryTheory.Limits.FormalCoproduct.coproductIsoCofanPt {C : Type u} [Category.{v, u} C] (𝒜 : Type w) (f : 𝒜 → FormalCoproduct C) : ∐ f ≅ (cofan 𝒜 f).pt

The arbitrary choice of the coproduct is isomorphic to our constructed coproduct cofan 𝒜 f.

Equations

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

@[simp]

theorem CategoryTheory.Limits.FormalCoproduct.ι_comp_coproductIsoCofanPt {C : Type u} [Category.{v, u} C] {𝒜 : Type w} {f : 𝒜 → FormalCoproduct C} (i : 𝒜) : CategoryStruct.comp (Sigma.ι f i) (coproductIsoCofanPt 𝒜 f).hom = (cofan 𝒜 f).inj i

@[simp]

theorem CategoryTheory.Limits.FormalCoproduct.ι_comp_coproductIsoCofanPt_assoc {C : Type u} [Category.{v, u} C] {𝒜 : Type w} {f : 𝒜 → FormalCoproduct C} (i : 𝒜) {Z : FormalCoproduct C} (h : (cofan 𝒜 f).pt ⟶ Z) : CategoryStruct.comp (Sigma.ι f i) (CategoryStruct.comp (coproductIsoCofanPt 𝒜 f).hom h) = CategoryStruct.comp ((cofan 𝒜 f).inj i) h

def CategoryTheory.Limits.FormalCoproduct.toFun {C : Type u} [Category.{v, u} C] (X : FormalCoproduct C) : X.I → FormalCoproduct C

Each X : FormalCoproduct.{w} C is actually itself a coproduct of objects of the original category (after coercion using incl C). This is the function that specifies the family for which X is a coproduct of.

Equations

• X.toFun = (CategoryTheory.Limits.FormalCoproduct.incl C).obj ∘ X.obj

def CategoryTheory.Limits.FormalCoproduct.cofanPtIsoSelf {C : Type u} [Category.{v, u} C] (X : FormalCoproduct C) : (cofan X.I X.toFun).pt ≅ X

The witness that each X : FormalCoproduct.{w} C is itself a coproduct of objects of the original category (after coercion using incl C), specified by X.toFun.

Equations

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

@[simp]

theorem CategoryTheory.Limits.FormalCoproduct.inj_comp_cofanPtIsoSelf_hom {C : Type u} [Category.{v, u} C] (X : FormalCoproduct C) (i : X.I) : CategoryStruct.comp ((cofan X.I X.toFun).inj i) X.cofanPtIsoSelf.hom = Hom.fromIncl i (CategoryStruct.id (X.obj i))

@[simp]

theorem CategoryTheory.Limits.FormalCoproduct.inj_comp_cofanPtIsoSelf_hom_assoc {C : Type u} [Category.{v, u} C] (X : FormalCoproduct C) (i : X.I) {Z : FormalCoproduct C} (h : X ⟶ Z) : CategoryStruct.comp ((cofan X.I X.toFun).inj i) (CategoryStruct.comp X.cofanPtIsoSelf.hom h) = CategoryStruct.comp (Hom.fromIncl i (CategoryStruct.id (X.obj i))) h

@[simp]

theorem CategoryTheory.Limits.FormalCoproduct.fromIncl_comp_cofanPtIsoSelf_inv {C : Type u} [Category.{v, u} C] (X : FormalCoproduct C) (i : X.I) : CategoryStruct.comp (Hom.fromIncl i (CategoryStruct.id (X.obj i))) X.cofanPtIsoSelf.inv = (cofan X.I X.toFun).inj i

@[simp]

theorem CategoryTheory.Limits.FormalCoproduct.fromIncl_comp_cofanPtIsoSelf_inv_assoc {C : Type u} [Category.{v, u} C] (X : FormalCoproduct C) (i : X.I) {Z : FormalCoproduct C} (h : (cofan X.I X.toFun).pt ⟶ Z) : CategoryStruct.comp (Hom.fromIncl i (CategoryStruct.id (X.obj i))) (CategoryStruct.comp X.cofanPtIsoSelf.inv h) = CategoryStruct.comp ((cofan X.I X.toFun).inj i) h

noncomputable def CategoryTheory.Limits.FormalCoproduct.coproductIsoSelf {C : Type u} [Category.{v, u} C] (X : FormalCoproduct C) : ∐ X.toFun ≅ X

The isomorphism between the coproduct of X.toFun and the object X itself.

Equations

• X.coproductIsoSelf = CategoryTheory.Limits.FormalCoproduct.coproductIsoCofanPt X.I X.toFun ≪≫ X.cofanPtIsoSelf

@[simp]

theorem CategoryTheory.Limits.FormalCoproduct.coproductIsoSelf_inv_f {C : Type u} [Category.{v, u} C] (X : FormalCoproduct C) (a✝ : X.I) : X.coproductIsoSelf.inv.f a✝ = (coproductIsoCofanPt X.I X.toFun).inv.f (X.cofanPtIsoSelf.inv.f a✝)

@[simp]

theorem CategoryTheory.Limits.FormalCoproduct.coproductIsoSelf_hom_φ {C : Type u} [Category.{v, u} C] (X : FormalCoproduct C) (x✝ : (∐ X.toFun).I) : X.coproductIsoSelf.hom.φ x✝ = CategoryStruct.comp ((coproductIsoCofanPt X.I X.toFun).hom.φ x✝) (X.cofanPtIsoSelf.hom.φ ((coproductIsoCofanPt X.I X.toFun).hom.f x✝))

@[simp]

theorem CategoryTheory.Limits.FormalCoproduct.coproductIsoSelf_hom_f {C : Type u} [Category.{v, u} C] (X : FormalCoproduct C) (a✝ : (∐ X.toFun).I) : X.coproductIsoSelf.hom.f a✝ = X.cofanPtIsoSelf.hom.f ((coproductIsoCofanPt X.I X.toFun).hom.f a✝)

@[simp]

theorem CategoryTheory.Limits.FormalCoproduct.coproductIsoSelf_inv_φ {C : Type u} [Category.{v, u} C] (X : FormalCoproduct C) (x✝ : X.I) : X.coproductIsoSelf.inv.φ x✝ = CategoryStruct.comp (X.cofanPtIsoSelf.inv.φ x✝) ((coproductIsoCofanPt X.I X.toFun).inv.φ (X.cofanPtIsoSelf.inv.f x✝))

@[simp]

theorem CategoryTheory.Limits.FormalCoproduct.ι_comp_coproductIsoSelf_hom {C : Type u} [Category.{v, u} C] (X : FormalCoproduct C) (i : X.I) : CategoryStruct.comp (Sigma.ι X.toFun i) X.coproductIsoSelf.hom = Hom.fromIncl i (CategoryStruct.id (X.obj i))

@[simp]

theorem CategoryTheory.Limits.FormalCoproduct.ι_comp_coproductIsoSelf_hom_assoc {C : Type u} [Category.{v, u} C] (X : FormalCoproduct C) (i : X.I) {Z : FormalCoproduct C} (h : X ⟶ Z) : CategoryStruct.comp (Sigma.ι X.toFun i) (CategoryStruct.comp X.coproductIsoSelf.hom h) = CategoryStruct.comp (Hom.fromIncl i (CategoryStruct.id (X.obj i))) h

@[simp]

theorem CategoryTheory.Limits.FormalCoproduct.fromIncl_comp_coproductIsoSelf_inv {C : Type u} [Category.{v, u} C] (X : FormalCoproduct C) (i : X.I) : CategoryStruct.comp (Hom.fromIncl i (CategoryStruct.id (X.obj i))) X.coproductIsoSelf.inv = Sigma.ι X.toFun i

@[simp]

theorem CategoryTheory.Limits.FormalCoproduct.fromIncl_comp_coproductIsoSelf_inv_assoc {C : Type u} [Category.{v, u} C] (X : FormalCoproduct C) (i : X.I) {Z : FormalCoproduct C} (h : ∐ X.toFun ⟶ Z) : CategoryStruct.comp (Hom.fromIncl i (CategoryStruct.id (X.obj i))) (CategoryStruct.comp X.coproductIsoSelf.inv h) = CategoryStruct.comp (Sigma.ι X.toFun i) h

def CategoryTheory.Limits.FormalCoproduct.isTerminalIncl {C : Type u} [Category.{v, u} C] (T : C) (ht : IsTerminal T) : IsTerminal ((incl C).obj T)

Given a terminal object T in the original category, we show that incl(T) is a terminal object in the category of formal coproducts.

Equations

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

instance CategoryTheory.Limits.FormalCoproduct.instHasTerminal {C : Type u} [Category.{v, u} C] [HasTerminal C] : HasTerminal (FormalCoproduct C)

def CategoryTheory.Limits.FormalCoproduct.pullbackCone {C : Type u} [Category.{v, u} C] {X Y Z : FormalCoproduct C} (f : X ⟶ Z) (g : Y ⟶ Z) (pb : (i : Function.Pullback f.f g.f) → PullbackCone (CategoryStruct.comp (f.φ (↑i).1) (eqToHom ⋯)) (g.φ (↑i).2)) : PullbackCone f g

Given two morphisms f : X ⟶ Z and g : Y ⟶ Z, given pullback in C over each component, construct the pullback in FormalCategory.{w} C.

Equations

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

@[simp]

theorem CategoryTheory.Limits.FormalCoproduct.pullbackCone_fst_f {C : Type u} [Category.{v, u} C] {X Y Z : FormalCoproduct C} (f : X ⟶ Z) (g : Y ⟶ Z) (pb : (i : Function.Pullback f.f g.f) → PullbackCone (CategoryStruct.comp (f.φ (↑i).1) (eqToHom ⋯)) (g.φ (↑i).2)) (i : (pullbackCone f g pb).pt.I) : (pullbackCone f g pb).fst.f i = (↑i).1

@[simp]

theorem CategoryTheory.Limits.FormalCoproduct.pullbackCone_fst_φ {C : Type u} [Category.{v, u} C] {X Y Z : FormalCoproduct C} (f : X ⟶ Z) (g : Y ⟶ Z) (pb : (i : Function.Pullback f.f g.f) → PullbackCone (CategoryStruct.comp (f.φ (↑i).1) (eqToHom ⋯)) (g.φ (↑i).2)) (i : (pullbackCone f g pb).pt.I) : (pullbackCone f g pb).fst.φ i = (pb i).fst

@[simp]

theorem CategoryTheory.Limits.FormalCoproduct.pullbackCone_snd_f {C : Type u} [Category.{v, u} C] {X Y Z : FormalCoproduct C} (f : X ⟶ Z) (g : Y ⟶ Z) (pb : (i : Function.Pullback f.f g.f) → PullbackCone (CategoryStruct.comp (f.φ (↑i).1) (eqToHom ⋯)) (g.φ (↑i).2)) (i : (pullbackCone f g pb).pt.I) : (pullbackCone f g pb).snd.f i = (↑i).2

@[simp]

theorem CategoryTheory.Limits.FormalCoproduct.pullbackCone_snd_φ {C : Type u} [Category.{v, u} C] {X Y Z : FormalCoproduct C} (f : X ⟶ Z) (g : Y ⟶ Z) (pb : (i : Function.Pullback f.f g.f) → PullbackCone (CategoryStruct.comp (f.φ (↑i).1) (eqToHom ⋯)) (g.φ (↑i).2)) (i : (pullbackCone f g pb).pt.I) : (pullbackCone f g pb).snd.φ i = (pb i).snd

@[simp]

theorem CategoryTheory.Limits.FormalCoproduct.pullbackCone_condition {C : Type u} [Category.{v, u} C] {X Y Z : FormalCoproduct C} (f : X ⟶ Z) (g : Y ⟶ Z) (pb : (i : Function.Pullback f.f g.f) → PullbackCone (CategoryStruct.comp (f.φ (↑i).1) (eqToHom ⋯)) (g.φ (↑i).2)) : CategoryStruct.comp (pullbackCone f g pb).fst f = CategoryStruct.comp (pullbackCone f g pb).snd g

def CategoryTheory.Limits.FormalCoproduct.homPullbackEquiv {C : Type u} [Category.{v, u} C] {X Y Z : FormalCoproduct C} (f : X ⟶ Z) (g : Y ⟶ Z) (pb : (i : Function.Pullback f.f g.f) → PullbackCone (CategoryStruct.comp (f.φ (↑i).1) (eqToHom ⋯)) (g.φ (↑i).2)) (hpb : (i : Function.Pullback f.f g.f) → IsLimit (pb i)) (T : FormalCoproduct C) : (T ⟶ (pullbackCone f g pb).pt) ≃ { p : (T ⟶ X) × (T ⟶ Y) // CategoryStruct.comp p.1 f = CategoryStruct.comp p.2 g }

The Equiv that witnesses that pullbackCone f g pb is actually a pullback. This is the universal property of pullbacks.

Equations

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

@[simp]

theorem CategoryTheory.Limits.FormalCoproduct.homPullbackEquiv_symm_apply_f_coe {C : Type u} [Category.{v, u} C] {X Y Z : FormalCoproduct C} (f : X ⟶ Z) (g : Y ⟶ Z) (pb : (i : Function.Pullback f.f g.f) → PullbackCone (CategoryStruct.comp (f.φ (↑i).1) (eqToHom ⋯)) (g.φ (↑i).2)) (hpb : (i : Function.Pullback f.f g.f) → IsLimit (pb i)) (T : FormalCoproduct C) (s : { p : (T ⟶ X) × (T ⟶ Y) // CategoryStruct.comp p.1 f = CategoryStruct.comp p.2 g }) (i : T.I) : ↑(((homPullbackEquiv f g pb hpb T).symm s).f i) = ((↑s).1.f i, (↑s).2.f i)

@[simp]

theorem CategoryTheory.Limits.FormalCoproduct.homPullbackEquiv_apply_coe {C : Type u} [Category.{v, u} C] {X Y Z : FormalCoproduct C} (f : X ⟶ Z) (g : Y ⟶ Z) (pb : (i : Function.Pullback f.f g.f) → PullbackCone (CategoryStruct.comp (f.φ (↑i).1) (eqToHom ⋯)) (g.φ (↑i).2)) (hpb : (i : Function.Pullback f.f g.f) → IsLimit (pb i)) (T : FormalCoproduct C) (m : T ⟶ (pullbackCone f g pb).pt) : ↑((homPullbackEquiv f g pb hpb T) m) = (CategoryStruct.comp m (pullbackCone f g pb).fst, CategoryStruct.comp m (pullbackCone f g pb).snd)

@[simp]

theorem CategoryTheory.Limits.FormalCoproduct.homPullbackEquiv_symm_apply_φ {C : Type u} [Category.{v, u} C] {X Y Z : FormalCoproduct C} (f : X ⟶ Z) (g : Y ⟶ Z) (pb : (i : Function.Pullback f.f g.f) → PullbackCone (CategoryStruct.comp (f.φ (↑i).1) (eqToHom ⋯)) (g.φ (↑i).2)) (hpb : (i : Function.Pullback f.f g.f) → IsLimit (pb i)) (T : FormalCoproduct C) (s : { p : (T ⟶ X) × (T ⟶ Y) // CategoryStruct.comp p.1 f = CategoryStruct.comp p.2 g }) (i : T.I) : ((homPullbackEquiv f g pb hpb T).symm s).φ i = (hpb ⟨((↑s).1.f i, (↑s).2.f i), ⋯⟩).lift (PullbackCone.mk ((↑s).1.φ i) ((↑s).2.φ i) ⋯)

def CategoryTheory.Limits.FormalCoproduct.isLimitPullbackCone {C : Type u} [Category.{v, u} C] {X Y Z : FormalCoproduct C} (f : X ⟶ Z) (g : Y ⟶ Z) (pb : (i : Function.Pullback f.f g.f) → PullbackCone (CategoryStruct.comp (f.φ (↑i).1) (eqToHom ⋯)) (g.φ (↑i).2)) (hpb : (i : Function.Pullback f.f g.f) → IsLimit (pb i)) : IsLimit (pullbackCone f g pb)

pullbackCone f g pb is a pullback.

Equations

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

theorem CategoryTheory.Limits.FormalCoproduct.hasPullback_of_pullbackCone {C : Type u} [Category.{v, u} C] {X Y Z : FormalCoproduct C} (f : X ⟶ Z) (g : Y ⟶ Z) (pb : (i : Function.Pullback f.f g.f) → PullbackCone (CategoryStruct.comp (f.φ (↑i).1) (eqToHom ⋯)) (g.φ (↑i).2)) (hpb : (i : Function.Pullback f.f g.f) → IsLimit (pb i)) : HasPullback f g

theorem CategoryTheory.Limits.FormalCoproduct.isPullback {C : Type u} [Category.{v, u} C] {X Y Z : FormalCoproduct C} (f : X ⟶ Z) (g : Y ⟶ Z) (pb : (i : Function.Pullback f.f g.f) → PullbackCone (CategoryStruct.comp (f.φ (↑i).1) (eqToHom ⋯)) (g.φ (↑i).2)) (hpb : (i : Function.Pullback f.f g.f) → IsLimit (pb i)) : IsPullback (pullbackCone f g pb).fst (pullbackCone f g pb).snd f g

instance CategoryTheory.Limits.FormalCoproduct.instHasPullback {C : Type u} [Category.{v, u} C] {X Y Z : FormalCoproduct C} (f : X ⟶ Z) (g : Y ⟶ Z) [HasPullbacks C] : HasPullback f g

instance CategoryTheory.Limits.FormalCoproduct.instHasPullbacks {C : Type u} [Category.{v, u} C] [HasPullbacks C] : HasPullbacks (FormalCoproduct C)

def CategoryTheory.Limits.FormalCoproduct.eval (C : Type u) [Category.{v, u} C] (A : Type u₁) [Category.{v₁, u₁} A] [HasCoproducts A] : Functor (Functor C A) (Functor (FormalCoproduct C) A)

A copresheaf valued in a category A with arbitrary coproducts, can be extended to the category of formal coproducts.

Equations

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

@[simp]

theorem CategoryTheory.Limits.FormalCoproduct.eval_obj_obj (C : Type u) [Category.{v, u} C] (A : Type u₁) [Category.{v₁, u₁} A] [HasCoproducts A] (F : Functor C A) (X : FormalCoproduct C) : ((eval C A).obj F).obj X = ∐ fun (i : X.I) => F.obj (X.obj i)

@[simp]

theorem CategoryTheory.Limits.FormalCoproduct.eval_map_app (C : Type u) [Category.{v, u} C] (A : Type u₁) [Category.{v₁, u₁} A] [HasCoproducts A] {X✝ Y✝ : Functor C A} (α : X✝ ⟶ Y✝) (f : FormalCoproduct C) : ((eval C A).map α).app f = Sigma.map fun (i : f.I) => α.app (f.obj i)

@[simp]

theorem CategoryTheory.Limits.FormalCoproduct.eval_obj_map (C : Type u) [Category.{v, u} C] (A : Type u₁) [Category.{v₁, u₁} A] [HasCoproducts A] (F : Functor C A) {X Y : FormalCoproduct C} (f : X ⟶ Y) : ((eval C A).obj F).map f = Sigma.desc fun (i : X.I) => CategoryStruct.comp (F.map (f.φ i)) (Sigma.ι (F.obj ∘ Y.obj) (f.f i))

def CategoryTheory.Limits.FormalCoproduct.evalCompInclIsoId (C : Type u) [Category.{v, u} C] (A : Type u₁) [Category.{v₁, u₁} A] [HasCoproducts A] : (eval C A).comp ((Functor.whiskeringLeft C (FormalCoproduct C) A).obj (incl C)) ≅ Functor.id (Functor C A)

eval(F) restricted to the original category (via incl) is the original copresheaf F.

Equations

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

@[simp]

theorem CategoryTheory.Limits.FormalCoproduct.evalCompInclIsoId_inv_app_app (C : Type u) [Category.{v, u} C] (A : Type u₁) [Category.{v₁, u₁} A] [HasCoproducts A] (X : Functor C A) (X✝ : C) : ((evalCompInclIsoId C A).inv.app X).app X✝ = Sigma.ι (fun (x : PUnit.{w + 1}) => X.obj X✝) PUnit.unit

@[simp]

theorem CategoryTheory.Limits.FormalCoproduct.evalCompInclIsoId_hom_app_app (C : Type u) [Category.{v, u} C] (A : Type u₁) [Category.{v₁, u₁} A] [HasCoproducts A] (X : Functor C A) (X✝ : C) : ((evalCompInclIsoId C A).hom.app X).app X✝ = Sigma.desc fun (x : PUnit.{w + 1}) => CategoryStruct.id (X.obj X✝)

def CategoryTheory.Limits.FormalCoproduct.isColimitEvalMapCoconeCofan {C : Type u} [Category.{v, u} C] {A : Type u₁} [Category.{v₁, u₁} A] [HasCoproducts A] (J : Type w) (f : J → FormalCoproduct C) (F : Functor C A) : IsColimit (((eval C A).obj F).mapCocone (cofan J f))

eval(F) preserves arbitrary coproducts.

Equations

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

instance CategoryTheory.Limits.FormalCoproduct.instPreservesColimitDiscreteFunctorObjFunctorEval {C : Type u} [Category.{v, u} C] {A : Type u₁} [Category.{v₁, u₁} A] [HasCoproducts A] (J : Type w) (f : J → FormalCoproduct C) (F : Functor C A) : PreservesColimit (Discrete.functor f) ((eval C A).obj F)

instance CategoryTheory.Limits.FormalCoproduct.instPreservesColimitsOfShapeDiscreteObjFunctorEval {C : Type u} [Category.{v, u} C] {A : Type u₁} [Category.{v₁, u₁} A] [HasCoproducts A] (J : Type w) (F : Functor C A) : PreservesColimitsOfShape (Discrete J) ((eval C A).obj F)

def CategoryTheory.Limits.FormalCoproduct.evalOp (C : Type u) [Category.{v, u} C] (A : Type u₁) [Category.{v₁, u₁} A] [HasProducts A] : Functor (Functor Cᵒᵖ A) (Functor (FormalCoproduct C)ᵒᵖ A)

A presheaf valued in a category A with arbitrary products can be extended to the category of formal coproducts.

Equations

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

@[simp]

theorem CategoryTheory.Limits.FormalCoproduct.evalOp_obj_obj (C : Type u) [Category.{v, u} C] (A : Type u₁) [Category.{v₁, u₁} A] [HasProducts A] (F : Functor Cᵒᵖ A) (X : (FormalCoproduct C)ᵒᵖ) : ((evalOp C A).obj F).obj X = ∏ᶜ fun (i : (Opposite.unop X).I) => F.obj (Opposite.op ((Opposite.unop X).obj i))

@[simp]

theorem CategoryTheory.Limits.FormalCoproduct.evalOp_map_app (C : Type u) [Category.{v, u} C] (A : Type u₁) [Category.{v₁, u₁} A] [HasProducts A] {X✝ Y✝ : Functor Cᵒᵖ A} (α : X✝ ⟶ Y✝) (f : (FormalCoproduct C)ᵒᵖ) : ((evalOp C A).map α).app f = Pi.map fun (i : (Opposite.unop f).I) => α.app (Opposite.op ((Opposite.unop f).obj i))

@[simp]

theorem CategoryTheory.Limits.FormalCoproduct.evalOp_obj_map (C : Type u) [Category.{v, u} C] (A : Type u₁) [Category.{v₁, u₁} A] [HasProducts A] (F : Functor Cᵒᵖ A) {X✝ Y✝ : (FormalCoproduct C)ᵒᵖ} (f : X✝ ⟶ Y✝) : ((evalOp C A).obj F).map f = Pi.lift fun (i : (Opposite.unop Y✝).I) => CategoryStruct.comp (Pi.π (fun (i : (Opposite.unop X✝).I) => F.obj (Opposite.op ((Opposite.unop X✝).obj i))) (f.unop.f i)) (F.map (f.unop.φ i).op)

def CategoryTheory.Limits.FormalCoproduct.evalOpCompInlIsoId (C : Type u) [Category.{v, u} C] (A : Type u₁) [Category.{v₁, u₁} A] [HasProducts A] : (evalOp C A).comp ((Functor.whiskeringLeft Cᵒᵖ (FormalCoproduct C)ᵒᵖ A).obj (incl C).op) ≅ Functor.id (Functor Cᵒᵖ A)

evalOp(F) restricted to the original category (via incl) is the original presheaf F.

Equations

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

@[simp]

theorem CategoryTheory.Limits.FormalCoproduct.evalOpCompInlIsoId_inv_app_app (C : Type u) [Category.{v, u} C] (A : Type u₁) [Category.{v₁, u₁} A] [HasProducts A] (X : Functor Cᵒᵖ A) (X✝ : Cᵒᵖ) : ((evalOpCompInlIsoId C A).inv.app X).app X✝ = Pi.lift fun (x : PUnit.{w + 1}) => CategoryStruct.id (X.obj X✝)

@[simp]

theorem CategoryTheory.Limits.FormalCoproduct.evalOpCompInlIsoId_hom_app_app (C : Type u) [Category.{v, u} C] (A : Type u₁) [Category.{v₁, u₁} A] [HasProducts A] (X : Functor Cᵒᵖ A) (X✝ : Cᵒᵖ) : ((evalOpCompInlIsoId C A).hom.app X).app X✝ = Pi.π (fun (i : PUnit.{w + 1}) => X.obj X✝) PUnit.unit

def CategoryTheory.Limits.FormalCoproduct.isLimitEvalMapConeCofanOp {C : Type u} [Category.{v, u} C] {A : Type u₁} [Category.{v₁, u₁} A] [HasProducts A] (J : Type w) (f : J → FormalCoproduct C) (F : Functor Cᵒᵖ A) : IsLimit (((evalOp C A).obj F).mapCone (cofan J f).op)

evalOp(F) preserves arbitrary products.

Equations

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

instance CategoryTheory.Limits.FormalCoproduct.instPreservesLimitOppositeDiscreteFunctorCompOpObjFunctorEvalOp {C : Type u} [Category.{v, u} C] {A : Type u₁} [Category.{v₁, u₁} A] [HasProducts A] (J : Type w) (f : J → FormalCoproduct C) (F : Functor Cᵒᵖ A) : PreservesLimit (Discrete.functor (Opposite.op ∘ f)) ((evalOp C A).obj F)