The sigma-comparison map

This file defines the map CompHausLike.sigmaComparison associated to a presheaf X on CompHausLike P, and a finite family S₁,...,Sₙ of spaces in CompHausLike P, where P is stable under taking finite disjoint unions.

The map sigmaComparison is the canonical map X(S₁ ⊔ ... ⊔ Sₙ) ⟶ X(S₁) × ... × X(Sₙ) induced by the inclusion maps Sᵢ ⟶ S₁ ⊔ ... ⊔ Sₙ, and it is an isomorphism when X preserves finite products.

instance CompHausLike.instHasPropSigma {P : TopCat → Prop} [HasExplicitFiniteCoproducts P] {α : Type u} [Finite α] (σ : α → Type u) [(a : α) → TopologicalSpace (σ a)] [∀ (a : α), CompactSpace (σ a)] [∀ (a : α), T2Space (σ a)] [∀ (a : α), HasProp P (σ a)] : HasProp P ((a : α) × σ a)

def CompHausLike.sigmaComparison {P : TopCat → Prop} [HasExplicitFiniteCoproducts P] (X : CategoryTheory.Functor (CompHausLike P)ᵒᵖ (Type (max u w))) {α : Type u} [Finite α] (σ : α → Type u) [(a : α) → TopologicalSpace (σ a)] [∀ (a : α), CompactSpace (σ a)] [∀ (a : α), T2Space (σ a)] [∀ (a : α), HasProp P (σ a)] : X.obj (Opposite.op ↧((a : α) × σ a)) ⟶ (a : α) → X.obj (Opposite.op ↧(σ a))

The comparison map from the value of a condensed set on a finite coproduct to the product of the values on the components.

Equations

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

theorem CompHausLike.sigmaComparison_eq_comp_isos {P : TopCat → Prop} [HasExplicitFiniteCoproducts P] (X : CategoryTheory.Functor (CompHausLike P)ᵒᵖ (Type (max u w))) [CategoryTheory.Limits.PreservesFiniteProducts X] {α : Type u} [Finite α] (σ : α → Type u) [(a : α) → TopologicalSpace (σ a)] [∀ (a : α), CompactSpace (σ a)] [∀ (a : α), T2Space (σ a)] [∀ (a : α), HasProp P (σ a)] : sigmaComparison X σ = CategoryTheory.CategoryStruct.comp (X.mapIso (CategoryTheory.Limits.opCoproductIsoProduct' (finiteCoproduct.isColimit fun (a : α) => ↧(σ a)) (CategoryTheory.Limits.productIsProduct fun (x : α) => Opposite.op ↧(σ x)))).hom (CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.PreservesProduct.iso X fun (a : α) => Opposite.op ↧(σ a)).hom (CategoryTheory.Limits.Types.productIso fun (a : α) => X.obj (Opposite.op ↧(σ a))).hom)

instance CompHausLike.isIsoSigmaComparison {P : TopCat → Prop} [HasExplicitFiniteCoproducts P] (X : CategoryTheory.Functor (CompHausLike P)ᵒᵖ (Type (max u w))) [CategoryTheory.Limits.PreservesFiniteProducts X] {α : Type u} [Finite α] (σ : α → Type u) [(a : α) → TopologicalSpace (σ a)] [∀ (a : α), CompactSpace (σ a)] [∀ (a : α), T2Space (σ a)] [∀ (a : α), HasProp P (σ a)] : CategoryTheory.IsIso (sigmaComparison X σ)