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.

instance LightProfinite.instHasExplicitPullbacksAndTotallyDisconnectedSpaceCarrierSecondCountableTopology : CompHausLike.HasExplicitPullbacks fun (Y : TopCat) => TotallyDisconnectedSpace ↑Y ∧ SecondCountableTopology ↑Y

instance LightProfinite.instHasExplicitFiniteCoproductsAndTotallyDisconnectedSpaceCarrierSecondCountableTopology : CompHausLike.HasExplicitFiniteCoproducts fun (Y : TopCat) => TotallyDisconnectedSpace ↑Y ∧ SecondCountableTopology ↑Y

@[reducible, inline]

abbrev LightProfinite.isTerminalPUnit : CategoryTheory.Limits.IsTerminal (of PUnit.{u + 1})

A one-element space is terminal in Profinite

Equations

• LightProfinite.isTerminalPUnit = CompHausLike.isTerminalPUnit