Documentation

Mathlib.Topology.Category.LightProfinite.Limits

Explicit limits and colimits #

This file applies the general API for explicit limits and colimits in CompHausLike P (see the file Mathlib/Topology/Category/CompHausLike/Limits.lean) to the special case of LightProfinite.

source
instance LightProfinite.instHasExplicitPullbacksAndTotallyDisconnectedSpaceCarrierSecondCountableTopology :
CompHausLike.HasExplicitPullbacks fun (Y : TopCat) => TotallyDisconnectedSpace ↑Y ∧ SecondCountableTopology ↑Y
source
instance LightProfinite.instHasExplicitFiniteCoproductsAndTotallyDisconnectedSpaceCarrierSecondCountableTopology :
CompHausLike.HasExplicitFiniteCoproducts fun (Y : TopCat) => TotallyDisconnectedSpace ↑Y ∧ SecondCountableTopology ↑Y
source
@[reducible, inline]
abbrev LightProfinite.isTerminalPUnit :
CategoryTheory.Limits.IsTerminal (of PUnit.{u + 1})

A one-element space is terminal in Profinite

Equations
Instances For
    source
    instance LightProfinite.instEpiCompHausLikeAndTotallyDisconnectedSpaceCarrierSecondCountableTopologyFst {X Y Z : LightProfinite} (f : X ⟶ Z) (g : Y ⟶ Z) [h : CategoryTheory.Epi g] :
    CategoryTheory.Epi (CompHausLike.pullback.fst f g)
    source
    instance LightProfinite.instEpiCompHausLikeAndTotallyDisconnectedSpaceCarrierSecondCountableTopologySnd {X Y Z : LightProfinite} (f : X ⟶ Z) (g : Y ⟶ Z) [h : CategoryTheory.Epi f] :
    CategoryTheory.Epi (CompHausLike.pullback.snd f g)