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} [CompHausLike.HasExplicitFiniteCoproducts P] {α : Type u} [Finite α] (σ : α → Type u) [(a : α) → TopologicalSpace (σ a)] [∀ (a : α), CompactSpace (σ a)] [∀ (a : α), T2Space (σ a)] [∀ (a : α), CompHausLike.HasProp P (σ a)] : CompHausLike.HasProp P ((a : α) × σ a)

def CompHausLike.sigmaComparison {P : TopCat → Prop} [CompHausLike.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 : α), CompHausLike.HasProp P (σ a)] : X.obj (Opposite.op (CompHausLike.of P ((a : α) × σ a))) ⟶ (a : α) → X.obj (Opposite.op (CompHausLike.of P (σ 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

• CompHausLike.sigmaComparison X σ x a = X.map (Opposite.op { toFun := Sigma.mk a, continuous_toFun := ⋯ }) x

theorem CompHausLike.sigmaComparison_eq_comp_isos {P : TopCat → Prop} [CompHausLike.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 : α), CompHausLike.HasProp P (σ a)] : CompHausLike.sigmaComparison X σ = CategoryTheory.CategoryStruct.comp (X.mapIso (CategoryTheory.Limits.opCoproductIsoProduct' (CompHausLike.finiteCoproduct.isColimit fun (a : α) => CompHausLike.of P (σ a)) (CategoryTheory.Limits.productIsProduct fun (x : α) => Opposite.op (CompHausLike.of P (σ x))))).hom (CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.PreservesProduct.iso X fun (a : α) => Opposite.op (CompHausLike.of P (σ a))).hom (CategoryTheory.Limits.Types.productIso fun (a : α) => X.obj (Opposite.op (CompHausLike.of P (σ a)))).hom)

instance CompHausLike.isIsoSigmaComparison {P : TopCat → Prop} [CompHausLike.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 : α), CompHausLike.HasProp P (σ a)] : CategoryTheory.IsIso (CompHausLike.sigmaComparison X σ)