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} [Fintype α] (X : α → Stonean) : Stonean

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

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

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

def Stonean.finiteCoproduct.desc {α : Type} [Fintype α] (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.

@[simp]

theorem Stonean.finiteCoproduct.ι_desc_assoc {α : Type} [Fintype α] (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} [Fintype α] (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} [Fintype α] (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

@[simp]

theorem Stonean.finiteCoproduct.cocone_ι {α : Type} [Fintype α] (F : CategoryTheory.Functor (CategoryTheory.Discrete α) Stonean) : (Stonean.finiteCoproduct.cocone F).ι = CategoryTheory.Discrete.natTrans fun a => Stonean.finiteCoproduct.ι F.obj a

@[simp]

theorem Stonean.finiteCoproduct.cocone_pt {α : Type} [Fintype α] (F : CategoryTheory.Functor (CategoryTheory.Discrete α) Stonean) : (Stonean.finiteCoproduct.cocone F).pt = Stonean.finiteCoproduct F.obj

def Stonean.finiteCoproduct.cocone {α : Type} [Fintype α] (F : CategoryTheory.Functor (CategoryTheory.Discrete α) Stonean) : CategoryTheory.Limits.Cocone F

The coproduct cocone associated to the explicit finite coproduct.

@[simp]

theorem Stonean.finiteCoproduct.isColimit_desc {α : Type} [Fintype α] (F : CategoryTheory.Functor (CategoryTheory.Discrete α) Stonean) (s : CategoryTheory.Limits.Cocone F) : CategoryTheory.Limits.IsColimit.desc (Stonean.finiteCoproduct.isColimit F) s = Stonean.finiteCoproduct.desc (fun a => F.obj a) fun a => s.ι.app a

def Stonean.finiteCoproduct.isColimit {α : Type} [Fintype α] (F : CategoryTheory.Functor (CategoryTheory.Discrete α) Stonean) : CategoryTheory.Limits.IsColimit (Stonean.finiteCoproduct.cocone F)

The explicit finite coproduct cocone is a colimit cocone.

instance Stonean.hasFiniteCoproducts : CategoryTheory.Limits.HasFiniteCoproducts Stonean

The category of extremally disconnected spaces has finite coproducts.

@[simp]

theorem Stonean.finiteCoproduct.explicitCocone_ι {α : Type} [Fintype α] (X : α → Stonean) : (Stonean.finiteCoproduct.explicitCocone X).ι = CategoryTheory.Discrete.natTrans fun x => match x with | { as := a } => Stonean.finiteCoproduct.ι X a

@[simp]

theorem Stonean.finiteCoproduct.explicitCocone_pt {α : Type} [Fintype α] (X : α → Stonean) : (Stonean.finiteCoproduct.explicitCocone X).pt = Stonean.finiteCoproduct X

def Stonean.finiteCoproduct.explicitCocone {α : Type} [Fintype α] (X : α → Stonean) : CategoryTheory.Limits.Cocone (CategoryTheory.Discrete.functor X)

A coproduct cocone associated to the explicit finite coproduct with cone point finiteCoproduct X.

@[simp]

theorem Stonean.finiteCoproduct.isColimit'_desc {α : Type} [Fintype α] (X : α → Stonean) (s : CategoryTheory.Limits.Cocone (CategoryTheory.Discrete.functor X)) : CategoryTheory.Limits.IsColimit.desc (Stonean.finiteCoproduct.isColimit' X) s = Stonean.finiteCoproduct.desc (fun a => X a) fun a => s.ι.app { as := a }

def Stonean.finiteCoproduct.isColimit' {α : Type} [Fintype α] (X : α → Stonean) : CategoryTheory.Limits.IsColimit (Stonean.finiteCoproduct.explicitCocone X)

The more explicit finite coproduct cocone is a colimit cocone.

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

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

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

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

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

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

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.

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.

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.

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.

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).π = CategoryTheory.NatTrans.mk fun j => Option.rec (CategoryTheory.CategoryStruct.comp (Stonean.pullback.fst f hi) f) (fun val => CategoryTheory.Limits.WalkingPair.rec (Stonean.pullback.fst f hi) (Stonean.pullback.snd f hi) val) j

@[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.

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.

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) (_ : CategoryTheory.CategoryStruct.comp (Stonean.pullback.fst f hi) f = CategoryTheory.CategoryStruct.comp (Stonean.pullback.snd f hi) i)

@[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 (_ : CategoryTheory.CategoryStruct.comp CategoryTheory.Limits.pullback.fst f = CategoryTheory.CategoryStruct.comp CategoryTheory.Limits.pullback.snd i)

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.