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
The inclusion of one of the factors into the explicit finite coproduct.
Instances For
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
The coproduct cocone associated to the explicit finite coproduct.
Instances For
The explicit finite coproduct cocone is a colimit cocone.
Instances For
The category of extremally disconnected spaces has finite coproducts.
A coproduct cocone associated to the explicit finite coproduct with cone point finiteCoproduct X
.
Instances For
The more explicit finite coproduct cocone is a colimit cocone.
Instances For
The isomorphism from the explicit finite coproducts to the abstract coproduct.
Instances For
The inclusion maps into the explicit finite coproduct are open embeddings.
The inclusion maps into the abstract finite coproduct are open embeddings.
The pullback of a morphism f
and an open embedding i
in Stonean
, constructed explicitly as
the preimage under f
of the image of i
with the subspace topology.
Instances For
The projection from the pullback to the first component.
Instances For
The projection from the pullback to the second component.
Instances For
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
The pullback cone whose cone point is the explicit pullback.
Instances For
The explicit pullback cone is a limit cone.
Instances For
The isomorphism from the explicit pullback to the abstract pullback.