# Documentation

Mathlib.Topology.Category.Stonean.Limits

# 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.

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

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

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.

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
@[simp]

The coproduct cocone associated to the explicit finite coproduct.

Instances For
@[simp]
theorem Stonean.finiteCoproduct.isColimit_desc {α : Type} [] (s : ) :
= Stonean.finiteCoproduct.desc (fun a => F.obj a) fun a => s.app a

The explicit finite coproduct cocone is a colimit cocone.

Instances For

The category of extremally disconnected spaces has finite coproducts.

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

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

Instances For
@[simp]
theorem Stonean.finiteCoproduct.isColimit'_desc {α : Type} [] (X : αStonean) :
= Stonean.finiteCoproduct.desc (fun a => X a) fun a => s.app { as := a }

The more explicit finite coproduct cocone is a colimit cocone.

Instances For
noncomputable def Stonean.coproductIsoCoproduct {α : Type} [] (X : αStonean) :

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

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.

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.

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.

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.

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.

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 : ) :
().π = CategoryTheory.NatTrans.mk fun j => Option.rec () (fun val => ) j
@[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.

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.

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 : ) :
@[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 (_ : 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 : ) :

The isomorphism from the explicit pullback to the abstract pullback.

Instances For