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

instance Profinite.instHasExplicitPullbacksTotallyDisconnectedSpaceαTopologicalSpace : CompHausLike.HasExplicitPullbacks fun (Y : TopCat) => TotallyDisconnectedSpace ↑Y

Equations

• Profinite.instHasExplicitPullbacksTotallyDisconnectedSpaceαTopologicalSpace = ⋯

instance Profinite.instHasExplicitFiniteCoproductsTotallyDisconnectedSpaceαTopologicalSpace : CompHausLike.HasExplicitFiniteCoproducts fun (Y : TopCat) => TotallyDisconnectedSpace ↑Y

Equations

• Profinite.instHasExplicitFiniteCoproductsTotallyDisconnectedSpaceαTopologicalSpace = ⋯

@[reducible, inline]

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

A one-element space is terminal in Profinite

Equations

• Profinite.isTerminalPUnit = CompHausLike.isTerminalPUnit