Explicit (co)limits in the category of Stonean spaces

This file describes some explicit (co)limits in Stonean

Overview

We define explicit finite coproducts in Stonean as sigma types (disjoint unions) and explicit pullbacks where one of the maps is an open embedding

This section defines the finite Coproduct of a finite family of profinite spaces X : α → Stonean.{u}

Notes: The content is mainly copied from Mathlib/Topology/Category/CompHaus/Limits.lean

def Stonean.finiteCoproduct {α : Type} [Finite α] (X : α → Stonean) : Stonean

The coproduct of a finite family of objects in Stonean, constructed as the disjoint union with its usual topology.

Equations

• Stonean.finiteCoproduct X = Stonean.of ((a : α) × CoeSort.coe (X a))

def Stonean.finiteCoproduct.ι {α : Type} [Finite α] (X : α → Stonean) (a : α) : X a ⟶ Stonean.finiteCoproduct X

The inclusion of one of the factors into the explicit finite coproduct.

Equations

• Stonean.finiteCoproduct.ι X a = { toFun := fun (x : ↑((fun (x : Stonean) => x.compHaus) (X a)).toTop) => ⟨a, x⟩, continuous_toFun := ⋯ }

def Stonean.finiteCoproduct.desc {α : Type} [Finite α] (X : α → Stonean) {B : Stonean} (e : (a : α) → X a ⟶ B) : Stonean.finiteCoproduct X ⟶ B

To construct a morphism from the explicit finite coproduct, it suffices to specify a morphism from each of its factors. This is essentially the universal property of the coproduct.

Equations

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

@[simp]

theorem Stonean.finiteCoproduct.ι_desc_assoc {α : Type} [Finite α] (X : α → Stonean) {B : Stonean} (e : (a : α) → X a ⟶ B) (a : α) {Z : Stonean} (h : B ⟶ Z) : CategoryTheory.CategoryStruct.comp (Stonean.finiteCoproduct.ι X a) (CategoryTheory.CategoryStruct.comp (Stonean.finiteCoproduct.desc X e) h) = CategoryTheory.CategoryStruct.comp (e a) h

@[simp]

theorem Stonean.finiteCoproduct.ι_desc {α : Type} [Finite α] (X : α → Stonean) {B : Stonean} (e : (a : α) → X a ⟶ B) (a : α) : CategoryTheory.CategoryStruct.comp (Stonean.finiteCoproduct.ι X a) (Stonean.finiteCoproduct.desc X e) = e a

theorem Stonean.finiteCoproduct.hom_ext {α : Type} [Finite α] (X : α → Stonean) {B : Stonean} (f : Stonean.finiteCoproduct X ⟶ B) (g : Stonean.finiteCoproduct X ⟶ B) (h : ∀ (a : α), CategoryTheory.CategoryStruct.comp (Stonean.finiteCoproduct.ι X a) f = CategoryTheory.CategoryStruct.comp (Stonean.finiteCoproduct.ι X a) g) : f = g

@[reducible, inline]

abbrev Stonean.finiteCoproduct.cofan {α : Type} [Finite α] (X : α → Stonean) : CategoryTheory.Limits.Cofan X

The coproduct cocone associated to the explicit finite coproduct.

Equations

• Stonean.finiteCoproduct.cofan X = CategoryTheory.Limits.Cofan.mk (Stonean.finiteCoproduct X) (Stonean.finiteCoproduct.ι X)

def Stonean.finiteCoproduct.isColimit {α : Type} [Finite α] (X : α → Stonean) : CategoryTheory.Limits.IsColimit (Stonean.finiteCoproduct.cofan X)

The explicit finite coproduct cocone is a colimit cocone.

Equations

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

instance Stonean.instHasColimitDiscreteFinFunctorCompObjMk (n : ℕ) (F : CategoryTheory.Functor (CategoryTheory.Discrete (Fin n)) Stonean) : CategoryTheory.Limits.HasColimit (CategoryTheory.Discrete.functor (F.obj ∘ CategoryTheory.Discrete.mk))

Equations

• ⋯ = ⋯

instance Stonean.instHasFiniteCoproducts : CategoryTheory.Limits.HasFiniteCoproducts Stonean

Equations

• Stonean.instHasFiniteCoproducts = ⋯

noncomputable def Stonean.coproductIsoCoproduct {α : Type} [Finite α] (X : α → Stonean) : Stonean.finiteCoproduct X ≅ ∐ X

The isomorphism from the explicit finite coproducts to the abstract coproduct.

Equations

• Stonean.coproductIsoCoproduct X = (Stonean.finiteCoproduct.isColimit X).coconePointUniqueUpToIso (CategoryTheory.Limits.colimit.isColimit (CategoryTheory.Discrete.functor X))

theorem Stonean.finiteCoproduct.openEmbedding_ι {α : Type} [Finite α] (Z : α → Stonean) (a : α) : OpenEmbedding ⇑(Stonean.finiteCoproduct.ι Z a)

The inclusion maps into the explicit finite coproduct are open embeddings.

theorem Stonean.Sigma.openEmbedding_ι {α : Type} [Finite α] (Z : α → Stonean) (a : α) : OpenEmbedding ⇑(CategoryTheory.Limits.Sigma.ι Z a)

The inclusion maps into the abstract finite coproduct are open embeddings.

instance Stonean.instPreservesFiniteCoproductsCompHausToCompHaus : CategoryTheory.Limits.PreservesFiniteCoproducts Stonean.toCompHaus

Equations

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

instance Stonean.instPreservesFiniteCoproductsProfiniteToProfinite : CategoryTheory.Limits.PreservesFiniteCoproducts Stonean.toProfinite

Equations

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

def Stonean.pullback {X : Stonean} {Y : Stonean} {Z : Stonean} (f : X ⟶ Z) {i : Y ⟶ Z} (hi : OpenEmbedding ⇑i) : Stonean

The pullback of a morphism f and an open embedding i in Stonean, constructed explicitly as the preimage under fof the image of i with the subspace topology.

Equations

• Stonean.pullback f hi = Stonean.mk (CompHaus.mk (TopCat.of ↑(⇑f ⁻¹' Set.range ⇑i)))

def Stonean.pullback.fst {X : Stonean} {Y : Stonean} {Z : Stonean} (f : X ⟶ Z) {i : Y ⟶ Z} (hi : OpenEmbedding ⇑i) : Stonean.pullback f hi ⟶ X

The projection from the pullback to the first component.

Equations

• Stonean.pullback.fst f hi = { toFun := Subtype.val, continuous_toFun := ⋯ }

noncomputable def Stonean.pullback.snd {X : Stonean} {Y : Stonean} {Z : Stonean} (f : X ⟶ Z) {i : Y ⟶ Z} (hi : OpenEmbedding ⇑i) : Stonean.pullback f hi ⟶ Y

The projection from the pullback to the second component.

Equations

• Stonean.pullback.snd f hi = { toFun := ⇑(Homeomorph.ofEmbedding ⇑i ⋯).symm ∘ Set.MapsTo.restrict (⇑f) (⇑f ⁻¹' Set.range ⇑i) (Set.range ⇑i) ⋯, continuous_toFun := ⋯ }

def Stonean.pullback.lift {X : Stonean} {Y : Stonean} {Z : Stonean} {W : Stonean} (f : X ⟶ Z) {i : Y ⟶ Z} (hi : OpenEmbedding ⇑i) (a : W ⟶ X) (b : W ⟶ Y) (w : CategoryTheory.CategoryStruct.comp a f = CategoryTheory.CategoryStruct.comp b i) : W ⟶ Stonean.pullback f hi

Construct a morphism to the explicit pullback given morphisms to the factors which are compatible with the maps to the base. This is essentially the universal property of the pullback.

Equations

• Stonean.pullback.lift f hi a b w = { toFun := fun (z : ↑((fun (x : Stonean) => x.compHaus) W).toTop) => ⟨a z, ⋯⟩, continuous_toFun := ⋯ }

theorem Stonean.pullback.condition {X : Stonean} {Y : Stonean} {Z : Stonean} (f : X ⟶ Z) {i : Y ⟶ Z} (hi : OpenEmbedding ⇑i) : CategoryTheory.CategoryStruct.comp (Stonean.pullback.fst f hi) f = CategoryTheory.CategoryStruct.comp (Stonean.pullback.snd f hi) i

@[simp]

theorem Stonean.pullback.lift_fst_assoc {X : Stonean} {Y : Stonean} {Z : Stonean} (f : X ⟶ Z✝) {i : Y ⟶ Z✝} (hi : OpenEmbedding ⇑i) {W : Stonean} (a : W ⟶ X) (b : W ⟶ Y) (w : CategoryTheory.CategoryStruct.comp a f = CategoryTheory.CategoryStruct.comp b i) {Z : Stonean} (h : X ⟶ Z) : CategoryTheory.CategoryStruct.comp (Stonean.pullback.lift f hi a b w) (CategoryTheory.CategoryStruct.comp (Stonean.pullback.fst f hi) h) = CategoryTheory.CategoryStruct.comp a h

@[simp]

theorem Stonean.pullback.lift_fst {X : Stonean} {Y : Stonean} {Z : Stonean} (f : X ⟶ Z) {i : Y ⟶ Z} (hi : OpenEmbedding ⇑i) {W : Stonean} (a : W ⟶ X) (b : W ⟶ Y) (w : CategoryTheory.CategoryStruct.comp a f = CategoryTheory.CategoryStruct.comp b i) : CategoryTheory.CategoryStruct.comp (Stonean.pullback.lift f hi a b w) (Stonean.pullback.fst f hi) = a

@[simp]

theorem Stonean.pullback.lift_snd_assoc {X : Stonean} {Y : Stonean} {Z : Stonean} {W : Stonean} (f : X ⟶ Z✝) {i : Y ⟶ Z✝} (hi : OpenEmbedding ⇑i) (a : W ⟶ X) (b : W ⟶ Y) (w : CategoryTheory.CategoryStruct.comp a f = CategoryTheory.CategoryStruct.comp b i) {Z : Stonean} (h : Y ⟶ Z) : CategoryTheory.CategoryStruct.comp (Stonean.pullback.lift f hi a b w) (CategoryTheory.CategoryStruct.comp (Stonean.pullback.snd f hi) h) = CategoryTheory.CategoryStruct.comp b h

@[simp]

theorem Stonean.pullback.lift_snd {X : Stonean} {Y : Stonean} {Z : Stonean} {W : Stonean} (f : X ⟶ Z) {i : Y ⟶ Z} (hi : OpenEmbedding ⇑i) (a : W ⟶ X) (b : W ⟶ Y) (w : CategoryTheory.CategoryStruct.comp a f = CategoryTheory.CategoryStruct.comp b i) : CategoryTheory.CategoryStruct.comp (Stonean.pullback.lift f hi a b w) (Stonean.pullback.snd f hi) = b

@[simp]

theorem Stonean.pullback.cone_π {X : Stonean} {Y : Stonean} {Z : Stonean} (f : X ⟶ Z) {i : Y ⟶ Z} (hi : OpenEmbedding ⇑i) : (Stonean.pullback.cone f hi).π = { app := fun (j : CategoryTheory.Limits.WalkingCospan) => Option.rec (CategoryTheory.CategoryStruct.comp (Stonean.pullback.fst f hi) f) (fun (val : CategoryTheory.Limits.WalkingPair) => CategoryTheory.Limits.WalkingPair.rec (Stonean.pullback.fst f hi) (Stonean.pullback.snd f hi) val) j, naturality := ⋯ }

@[simp]

theorem Stonean.pullback.cone_pt {X : Stonean} {Y : Stonean} {Z : Stonean} (f : X ⟶ Z) {i : Y ⟶ Z} (hi : OpenEmbedding ⇑i) : (Stonean.pullback.cone f hi).pt = Stonean.pullback f hi

noncomputable def Stonean.pullback.cone {X : Stonean} {Y : Stonean} {Z : Stonean} (f : X ⟶ Z) {i : Y ⟶ Z} (hi : OpenEmbedding ⇑i) : CategoryTheory.Limits.PullbackCone f i

The pullback cone whose cone point is the explicit pullback.

Equations

• Stonean.pullback.cone f hi = CategoryTheory.Limits.PullbackCone.mk (Stonean.pullback.fst f hi) (Stonean.pullback.snd f hi) ⋯

theorem Stonean.pullback.hom_ext {X : Stonean} {Y : Stonean} {Z : Stonean} {W : Stonean} (f : X ⟶ Z) {i : Y ⟶ Z} (hi : OpenEmbedding ⇑i) (a : W ⟶ (Stonean.pullback.cone f hi).pt) (b : W ⟶ (Stonean.pullback.cone f hi).pt) (hfst : CategoryTheory.CategoryStruct.comp a (Stonean.pullback.fst f hi) = CategoryTheory.CategoryStruct.comp b (Stonean.pullback.fst f hi)) : a = b

def Stonean.pullback.isLimit {X : Stonean} {Y : Stonean} {Z : Stonean} (f : X ⟶ Z) {i : Y ⟶ Z} (hi : OpenEmbedding ⇑i) : CategoryTheory.Limits.IsLimit (Stonean.pullback.cone f hi)

The explicit pullback cone is a limit cone.

Equations

• Stonean.pullback.isLimit f hi = (Stonean.pullback.cone f hi).isLimitAux (fun (s : CategoryTheory.Limits.PullbackCone f i) => Stonean.pullback.lift f hi s.fst s.snd ⋯) ⋯ ⋯ ⋯

theorem Stonean.HasPullbackOpenEmbedding {X : Stonean} {Y : Stonean} {Z : Stonean} (f : X ⟶ Z) {i : Y ⟶ Z} (hi : OpenEmbedding ⇑i) : CategoryTheory.Limits.HasPullback f i

@[simp]

theorem Stonean.pullbackIsoPullback_hom {X : Stonean} {Y : Stonean} {Z : Stonean} (f : X ⟶ Z) {i : Y ⟶ Z} (hi : OpenEmbedding ⇑i) : (Stonean.pullbackIsoPullback f hi).hom = CategoryTheory.Limits.pullback.lift (Stonean.pullback.fst f hi) (Stonean.pullback.snd f hi) ⋯

@[simp]

theorem Stonean.pullbackIsoPullback_inv {X : Stonean} {Y : Stonean} {Z : Stonean} (f : X ⟶ Z) {i : Y ⟶ Z} (hi : OpenEmbedding ⇑i) : (Stonean.pullbackIsoPullback f hi).inv = Stonean.pullback.lift f hi CategoryTheory.Limits.pullback.fst CategoryTheory.Limits.pullback.snd ⋯

noncomputable def Stonean.pullbackIsoPullback {X : Stonean} {Y : Stonean} {Z : Stonean} (f : X ⟶ Z) {i : Y ⟶ Z} (hi : OpenEmbedding ⇑i) : Stonean.pullback f hi ≅ CategoryTheory.Limits.pullback f i

The isomorphism from the explicit pullback to the abstract pullback.

Equations

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

noncomputable def Stonean.createsPullbacksOfOpenEmbedding {X : Stonean} {Y : Stonean} {Z : Stonean} (f : X ⟶ Z) {i : Y ⟶ Z} (hi : OpenEmbedding ⇑i) : CategoryTheory.CreatesLimit (CategoryTheory.Limits.cospan f i) (Stonean.toCompHaus.comp compHausToTop)

The forgetful from Stonean to TopCat creates pullbacks along open embeddings

Equations

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

instance Stonean.instHasPullbacksOfInclusions : CategoryTheory.HasPullbacksOfInclusions Stonean

Equations

• Stonean.instHasPullbacksOfInclusions = ⋯

noncomputable instance Stonean.instPreservesPullbacksOfInclusionsCompHausToCompHaus : CategoryTheory.PreservesPullbacksOfInclusions Stonean.toCompHaus

Equations

• Stonean.instPreservesPullbacksOfInclusionsCompHausToCompHaus = CategoryTheory.PreservesPullbacksOfInclusions.mk

noncomputable instance Stonean.instPreservesPullbacksOfInclusionsProfiniteToProfinite : CategoryTheory.PreservesPullbacksOfInclusions Stonean.toProfinite

Equations

• Stonean.instPreservesPullbacksOfInclusionsProfiniteToProfinite = CategoryTheory.PreservesPullbacksOfInclusions.mk

instance Stonean.instFinitaryExtensive : CategoryTheory.FinitaryExtensive Stonean

Equations

• Stonean.instFinitaryExtensive = ⋯