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) to the special case of LightProfinite.

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

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

@[reducible, inline]

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

A one-element space is terminal in Profinite

Equations

• LightProfinite.isTerminalPUnit = CompHausLike.isTerminalPUnit