The Cech object for formal coproducts

Let C be a category that has finite products. In this file, we define a functor cechFunctor : FormalCoproduct C ⥤ SimplicialObject (FormalCoproduct C) which sends a formal coproduct of objects U j (for j : ι) to the simplicial object which sends ⦋n⦌ to the formal coproduct, indexed by i : Fin (n + 1) → ι, of the products of the objects U (i a) for all a : Fin (n + 1).

noncomputable def CategoryTheory.Limits.FormalCoproduct.power {C : Type u} [Category.{v, u} C] (U : FormalCoproduct C) (α : Type t) [HasProductsOfShape α C] : FormalCoproduct C

Given U : FormalCoproduct C and a type α, this is the formal coproduct indexed by all i : α → U.I of the products of the objects U.obj (i a) for all a : α.

Equations

• U.power α = { I := α → U.I, obj := fun (i : α → U.I) => ∏ᶜ U.obj ∘ i }

@[simp]

theorem CategoryTheory.Limits.FormalCoproduct.power_obj {C : Type u} [Category.{v, u} C] (U : FormalCoproduct C) (α : Type t) [HasProductsOfShape α C] (i : α → U.I) : (U.power α).obj i = ∏ᶜ U.obj ∘ i

@[simp]

theorem CategoryTheory.Limits.FormalCoproduct.power_I {C : Type u} [Category.{v, u} C] (U : FormalCoproduct C) (α : Type t) [HasProductsOfShape α C] : (U.power α).I = (α → U.I)

noncomputable def CategoryTheory.Limits.FormalCoproduct.powerπ {C : Type u} [Category.{v, u} C] (U : FormalCoproduct C) {α : Type} [HasProductsOfShape α C] (a : α) : U.power α ⟶ U

The projection U.power α ⟶ U for each a : α.

Equations

• U.powerπ a = { f := fun (i : (U.power α).I) => i a, φ := fun (x : (U.power α).I) => CategoryTheory.Limits.Pi.π (U.obj ∘ x) a }

@[simp]

theorem CategoryTheory.Limits.FormalCoproduct.powerπ_φ {C : Type u} [Category.{v, u} C] (U : FormalCoproduct C) {α : Type} [HasProductsOfShape α C] (a : α) (x✝ : (U.power α).I) : (U.powerπ a).φ x✝ = Pi.π (U.obj ∘ x✝) a

@[simp]

theorem CategoryTheory.Limits.FormalCoproduct.powerπ_f {C : Type u} [Category.{v, u} C] (U : FormalCoproduct C) {α : Type} [HasProductsOfShape α C] (a : α) (i : (U.power α).I) : (U.powerπ a).f i = i a

@[reducible, inline]

noncomputable abbrev CategoryTheory.Limits.FormalCoproduct.powerFan {C : Type u} [Category.{v, u} C] (U : FormalCoproduct C) (α : Type) [HasProductsOfShape α C] : Fan fun (x : α) => U

The (limit) fan expressing that U.power α is a product of copies of U indexed by α.

Equations

• U.powerFan α = CategoryTheory.Limits.Fan.mk (U.power α) U.powerπ

noncomputable def CategoryTheory.Limits.FormalCoproduct.isLimitPowerFan {C : Type u} [Category.{v, u} C] (U : FormalCoproduct C) (α : Type) [HasProductsOfShape α C] : IsLimit (U.powerFan α)

U.power α identifies to the product of copies of U indexed by α.

Equations

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

noncomputable def CategoryTheory.Limits.FormalCoproduct.powerMap {C : Type u} [Category.{v, u} C] {U V : FormalCoproduct C} (f : U ⟶ V) (α : Type t) [HasProductsOfShape α C] : U.power α ⟶ V.power α

For any morphism f : U ⟶ V in FormalCoproduct C and a type α, this is the induced map U.power α ⟶ V.power α.

Equations

• CategoryTheory.Limits.FormalCoproduct.powerMap f α = { f := fun (i : (U.power α).I) => f.f ∘ i, φ := fun (i : (U.power α).I) => CategoryTheory.Limits.Pi.map fun (a : α) => f.φ (i a) }

@[simp]

theorem CategoryTheory.Limits.FormalCoproduct.powerMap_f {C : Type u} [Category.{v, u} C] {U V : FormalCoproduct C} (f : U ⟶ V) (α : Type t) [HasProductsOfShape α C] : (powerMap f α).f = fun (i : (U.power α).I) => f.f ∘ i

@[simp]

theorem CategoryTheory.Limits.FormalCoproduct.powerMap_φ {C : Type u} [Category.{v, u} C] {U V : FormalCoproduct C} (f : U ⟶ V) (α : Type t) [HasProductsOfShape α C] : (powerMap f α).φ = fun (i : (U.power α).I) => Pi.map fun (a : α) => f.φ (i a)

@[simp]

theorem CategoryTheory.Limits.FormalCoproduct.powerMap_id {C : Type u} [Category.{v, u} C] (U : FormalCoproduct C) (α : Type t) [HasProductsOfShape α C] : powerMap (CategoryStruct.id U) α = CategoryStruct.id (U.power α)

theorem CategoryTheory.Limits.FormalCoproduct.powerMap_comp {C : Type u} [Category.{v, u} C] {U V W : FormalCoproduct C} (f : U ⟶ V) (g : V ⟶ W) (α : Type t) [HasProductsOfShape α C] : powerMap (CategoryStruct.comp f g) α = CategoryStruct.comp (powerMap f α) (powerMap g α)

theorem CategoryTheory.Limits.FormalCoproduct.powerMap_comp_assoc {C : Type u} [Category.{v, u} C] {U V W : FormalCoproduct C} (f : U ⟶ V) (g : V ⟶ W) (α : Type t) [HasProductsOfShape α C] {Z : FormalCoproduct C} (h : W.power α ⟶ Z) : CategoryStruct.comp (powerMap (CategoryStruct.comp f g) α) h = CategoryStruct.comp (powerMap f α) (CategoryStruct.comp (powerMap g α) h)

noncomputable def CategoryTheory.Limits.FormalCoproduct.powerFunctor {C : Type u} [Category.{v, u} C] (α : Type t) [HasProductsOfShape α C] : Functor (FormalCoproduct C) (FormalCoproduct C)

Given a type α, this is the functor FormalCoproduct C ⥤ FormalCoproduct C which sends U to U.power α.

Equations

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

@[simp]

theorem CategoryTheory.Limits.FormalCoproduct.powerFunctor_map {C : Type u} [Category.{v, u} C] (α : Type t) [HasProductsOfShape α C] {X✝ Y✝ : FormalCoproduct C} (f : X✝ ⟶ Y✝) : (powerFunctor α).map f = powerMap f α

@[simp]

theorem CategoryTheory.Limits.FormalCoproduct.powerFunctor_obj {C : Type u} [Category.{v, u} C] (α : Type t) [HasProductsOfShape α C] (U : FormalCoproduct C) : (powerFunctor α).obj U = U.power α

noncomputable def CategoryTheory.Limits.FormalCoproduct.mapPower {C : Type u} [Category.{v, u} C] (U : FormalCoproduct C) {α β : Type t} [HasProductsOfShape α C] [HasProductsOfShape β C] (f : α → β) : U.power β ⟶ U.power α

The functoriality of FormalCoproduct.power with respect to the index type.

Equations

• U.mapPower f = { f := fun (i : (U.power β).I) => i ∘ f, φ := fun (x : (U.power β).I) => CategoryTheory.Limits.Pi.lift fun (x_1 : α) => CategoryTheory.Limits.Pi.π (U.obj ∘ x) (f x_1) }

@[simp]

theorem CategoryTheory.Limits.FormalCoproduct.mapPower_f {C : Type u} [Category.{v, u} C] (U : FormalCoproduct C) {α β : Type t} [HasProductsOfShape α C] [HasProductsOfShape β C] (f : α → β) : (U.mapPower f).f = fun (i : (U.power β).I) => i ∘ f

@[simp]

theorem CategoryTheory.Limits.FormalCoproduct.mapPower_φ {C : Type u} [Category.{v, u} C] (U : FormalCoproduct C) {α β : Type t} [HasProductsOfShape α C] [HasProductsOfShape β C] (f : α → β) : (U.mapPower f).φ = fun (x : (U.power β).I) => Pi.lift fun (x_1 : α) => Pi.π (U.obj ∘ x) (f x_1)

@[simp]

theorem CategoryTheory.Limits.FormalCoproduct.mapPower_id {C : Type u} [Category.{v, u} C] (U : FormalCoproduct C) (α : Type t) [HasProductsOfShape α C] : U.mapPower id = CategoryStruct.id (U.power α)

theorem CategoryTheory.Limits.FormalCoproduct.mapPower_comp {C : Type u} [Category.{v, u} C] (U : FormalCoproduct C) {α β γ : Type t} [HasProductsOfShape α C] [HasProductsOfShape β C] [HasProductsOfShape γ C] (f : α → β) (g : β → γ) : U.mapPower (g ∘ f) = CategoryStruct.comp (U.mapPower g) (U.mapPower f)

theorem CategoryTheory.Limits.FormalCoproduct.mapPower_comp_assoc {C : Type u} [Category.{v, u} C] (U : FormalCoproduct C) {α β γ : Type t} [HasProductsOfShape α C] [HasProductsOfShape β C] [HasProductsOfShape γ C] (f : α → β) (g : β → γ) {Z : FormalCoproduct C} (h : U.power α ⟶ Z) : CategoryStruct.comp (U.mapPower (g ∘ f)) h = CategoryStruct.comp (U.mapPower g) (CategoryStruct.comp (U.mapPower f) h)

theorem CategoryTheory.Limits.FormalCoproduct.mapPower_powerMap {C : Type u} [Category.{v, u} C] {U V : FormalCoproduct C} (f : U ⟶ V) {α β : Type t} [HasProductsOfShape α C] [HasProductsOfShape β C] (g : α → β) : CategoryStruct.comp (U.mapPower g) (powerMap f α) = CategoryStruct.comp (powerMap f β) (V.mapPower g)

theorem CategoryTheory.Limits.FormalCoproduct.mapPower_powerMap_assoc {C : Type u} [Category.{v, u} C] {U V : FormalCoproduct C} (f : U ⟶ V) {α β : Type t} [HasProductsOfShape α C] [HasProductsOfShape β C] (g : α → β) {Z : FormalCoproduct C} (h : V.power α ⟶ Z) : CategoryStruct.comp (U.mapPower g) (CategoryStruct.comp (powerMap f α) h) = CategoryStruct.comp (powerMap f β) (CategoryStruct.comp (V.mapPower g) h)

@[simp]

theorem CategoryTheory.Limits.FormalCoproduct.mapPower_π {C : Type u} [Category.{v, u} C] (U : FormalCoproduct C) {α β : Type} [HasProductsOfShape α C] [HasProductsOfShape β C] (f : α → β) (a : α) : CategoryStruct.comp (U.mapPower f) (U.powerπ a) = U.powerπ (f a)

@[simp]

theorem CategoryTheory.Limits.FormalCoproduct.mapPower_π_assoc {C : Type u} [Category.{v, u} C] (U : FormalCoproduct C) {α β : Type} [HasProductsOfShape α C] [HasProductsOfShape β C] (f : α → β) (a : α) {Z : FormalCoproduct C} (h : U ⟶ Z) : CategoryStruct.comp (U.mapPower f) (CategoryStruct.comp (U.powerπ a) h) = CategoryStruct.comp (U.powerπ (f a)) h

noncomputable def CategoryTheory.Limits.FormalCoproduct.powerBifunctor {C : Type u} [Category.{v, u} C] [HasProducts C] : Functor Type tᵒᵖ (Functor (FormalCoproduct C) (FormalCoproduct C))

The functor (Type t)ᵒᵖ ⥤ FormalCoproduct.{w} C ⥤ FormalCoproduct.{max w t} C which sends a type α and U : FormalCoproduct C to U.power α.

Equations

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

@[simp]

theorem CategoryTheory.Limits.FormalCoproduct.powerBifunctor_obj {C : Type u} [Category.{v, u} C] [HasProducts C] (α : Type tᵒᵖ) : powerBifunctor.obj α = powerFunctor (Opposite.unop α)

@[simp]

theorem CategoryTheory.Limits.FormalCoproduct.powerBifunctor_map_app {C : Type u} [Category.{v, u} C] [HasProducts C] {X✝ Y✝ : Type tᵒᵖ} (f : X✝ ⟶ Y✝) (x✝ : FormalCoproduct C) : (powerBifunctor.map f).app x✝ = x✝.mapPower ⇑(ConcreteCategory.hom f.unop)

noncomputable def CategoryTheory.Limits.FormalCoproduct.cech {C : Type u} [Category.{v, u} C] [HasFiniteProducts C] (U : FormalCoproduct C) : SimplicialObject (FormalCoproduct C)

Given U : FormalCoproduct C, this is the simplicial object in FormalCoproduct C which sends ⦋n⦌ to U.power (Fin (n + 1)).

Equations

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

@[simp]

theorem CategoryTheory.Limits.FormalCoproduct.cech_obj {C : Type u} [Category.{v, u} C] [HasFiniteProducts C] (U : FormalCoproduct C) (n : SimplexCategoryᵒᵖ) : U.cech.obj n = U.power (ToType (Opposite.unop n))

@[simp]

theorem CategoryTheory.Limits.FormalCoproduct.cech_map {C : Type u} [Category.{v, u} C] [HasFiniteProducts C] (U : FormalCoproduct C) {X✝ Y✝ : SimplexCategoryᵒᵖ} (f : X✝ ⟶ Y✝) : U.cech.map f = U.mapPower (SimplexCategory.Hom.toOrderHom f.unop).toFun

noncomputable def CategoryTheory.Limits.FormalCoproduct.cechFunctor {C : Type u} [Category.{v, u} C] [HasFiniteProducts C] : Functor (FormalCoproduct C) (SimplicialObject (FormalCoproduct C))

The functor FormalCoproduct C ⥤ SimplicialObject (FormalCoproduct C) which sends a formal coproduct to its Cech object.

Equations

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

@[simp]

theorem CategoryTheory.Limits.FormalCoproduct.cechFunctor_map_app {C : Type u} [Category.{v, u} C] [HasFiniteProducts C] {X✝ Y✝ : FormalCoproduct C} (f : X✝ ⟶ Y✝) (x✝ : SimplexCategoryᵒᵖ) : (cechFunctor.map f).app x✝ = powerMap f (ToType (Opposite.unop x✝))

@[simp]

theorem CategoryTheory.Limits.FormalCoproduct.cechFunctor_obj {C : Type u} [Category.{v, u} C] [HasFiniteProducts C] (U : FormalCoproduct C) : cechFunctor.obj U = U.cech