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

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

Equations
Instances For
def Stonean.finiteCoproduct.ι {α : Type} [] (X : αStonean) (a : α) :

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

Equations
• = { toFun := fun (x : ((fun (x : Stonean) => x.compHaus) (X a)).toTop) => a, x, continuous_toFun := }
Instances For
def Stonean.finiteCoproduct.desc {α : Type} [] (X : αStonean) {B : Stonean} (e : (a : α) → X a 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.
Instances For
@[simp]
theorem Stonean.finiteCoproduct.ι_desc_assoc {α : Type} [] (X : αStonean) {B : Stonean} (e : (a : α) → X a B) (a : α) {Z : Stonean} (h : B Z) :
@[simp]
theorem Stonean.finiteCoproduct.ι_desc {α : Type} [] (X : αStonean) {B : Stonean} (e : (a : α) → X a B) (a : α) :
theorem Stonean.finiteCoproduct.hom_ext {α : Type} [] (X : αStonean) {B : Stonean} (f : ) (g : ) (h : ∀ (a : α), ) :
f = g
@[reducible, inline]
abbrev Stonean.finiteCoproduct.cofan {α : Type} [] (X : αStonean) :

The coproduct cocone associated to the explicit finite coproduct.

Equations
Instances For
def Stonean.finiteCoproduct.isColimit {α : Type} [] (X : αStonean) :

The explicit finite coproduct cocone is a colimit cocone.

Equations
• One or more equations did not get rendered due to their size.
Instances For
noncomputable def Stonean.coproductIsoCoproduct {α : Type} [] (X : αStonean) :

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

Equations
• = .coconePointUniqueUpToIso
Instances For
theorem Stonean.finiteCoproduct.openEmbedding_ι {α : Type} [] (Z : αStonean) (a : α) :

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

theorem Stonean.Sigma.openEmbedding_ι {α : Type} [] (Z : αStonean) (a : α) :

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

Equations
• One or more equations did not get rendered due to their size.
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 : ) :

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
Instances For
def Stonean.pullback.fst {X : Stonean} {Y : Stonean} {Z : Stonean} (f : X Z) {i : Y Z} (hi : ) :
X

The projection from the pullback to the first component.

Equations
• = { toFun := Subtype.val, continuous_toFun := }
Instances For
noncomputable def Stonean.pullback.snd {X : Stonean} {Y : Stonean} {Z : Stonean} (f : X Z) {i : Y Z} (hi : ) :
Y

The projection from the pullback to the second component.

Equations
Instances For
def Stonean.pullback.lift {X : Stonean} {Y : Stonean} {Z : Stonean} {W : Stonean} (f : X Z) {i : Y Z} (hi : ) (a : W X) (b : W Y) :
W

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 := }
Instances For
theorem Stonean.pullback.condition {X : Stonean} {Y : Stonean} {Z : Stonean} (f : X Z) {i : Y Z} (hi : ) :
@[simp]
theorem Stonean.pullback.lift_fst_assoc {X : Stonean} {Y : Stonean} {Z : Stonean} (f : X Z✝) {i : Y Z✝} (hi : ) {W : Stonean} (a : W X) (b : W Y) {Z : Stonean} (h : X Z) :
@[simp]
theorem Stonean.pullback.lift_fst {X : Stonean} {Y : Stonean} {Z : Stonean} (f : X Z) {i : Y Z} (hi : ) {W : Stonean} (a : W X) (b : W Y) :
@[simp]
theorem Stonean.pullback.lift_snd_assoc {X : Stonean} {Y : Stonean} {Z : Stonean} {W : Stonean} (f : X Z✝) {i : Y Z✝} (hi : ) (a : W X) (b : W Y) {Z : Stonean} (h : Y Z) :
@[simp]
theorem Stonean.pullback.lift_snd {X : Stonean} {Y : Stonean} {Z : Stonean} {W : Stonean} (f : X Z) {i : Y Z} (hi : ) (a : W X) (b : W Y) :
@[simp]
theorem Stonean.pullback.cone_π {X : Stonean} {Y : Stonean} {Z : Stonean} (f : X Z) {i : Y Z} (hi : ) :
() = { app := fun (j : CategoryTheory.Limits.WalkingCospan) => Option.rec (fun (val : CategoryTheory.Limits.WalkingPair) => ) j, naturality := }
@[simp]
theorem Stonean.pullback.cone_pt {X : Stonean} {Y : Stonean} {Z : Stonean} (f : X Z) {i : Y Z} (hi : ) :
().pt =
noncomputable def Stonean.pullback.cone {X : Stonean} {Y : Stonean} {Z : Stonean} (f : X Z) {i : Y Z} (hi : ) :

The pullback cone whose cone point is the explicit pullback.

Equations
Instances For
theorem Stonean.pullback.hom_ext {X : Stonean} {Y : Stonean} {Z : Stonean} {W : Stonean} (f : X Z) {i : Y Z} (hi : ) (a : W ().pt) (b : W ().pt) (hfst : ) :
a = b
def Stonean.pullback.isLimit {X : Stonean} {Y : Stonean} {Z : Stonean} (f : X Z) {i : Y Z} (hi : ) :

The explicit pullback cone is a limit cone.

Equations
Instances For
theorem Stonean.HasPullbackOpenEmbedding {X : Stonean} {Y : Stonean} {Z : Stonean} (f : X Z) {i : Y Z} (hi : ) :
@[simp]
theorem Stonean.pullbackIsoPullback_hom {X : Stonean} {Y : Stonean} {Z : Stonean} (f : X Z) {i : Y Z} (hi : ) :
().hom =
@[simp]
theorem Stonean.pullbackIsoPullback_inv {X : Stonean} {Y : Stonean} {Z : Stonean} (f : X Z) {i : Y Z} (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 : ) :

The isomorphism from the explicit pullback to the abstract pullback.

Equations
• One or more equations did not get rendered due to their size.
Instances For
noncomputable def Stonean.createsPullbacksOfOpenEmbedding {X : Stonean} {Y : Stonean} {Z : Stonean} (f : X Z) {i : Y Z} (hi : ) :

The forgetful from Stonean to TopCat creates pullbacks along open embeddings

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