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

instance CompHaus.instHasExplicitPullbacksTrue : CompHausLike.HasExplicitPullbacks fun (x : TopCat) => True

instance CompHaus.instHasExplicitFiniteCoproductsTrue : CompHausLike.HasExplicitFiniteCoproducts fun (x : TopCat) => True

@[reducible, inline]

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

A one-element space is terminal in CompHaus

Equations

• CompHaus.isTerminalPUnit = CompHausLike.isTerminalPUnit

noncomputable def CompHaus.terminalIsoPUnit : ⊤_ CompHaus ≅ CompHaus.of PUnit.{u + 1}

The isomorphism from an arbitrary terminal object of CompHaus to a one-element space.

Equations

• CompHaus.terminalIsoPUnit = CategoryTheory.Limits.terminalIsTerminal.uniqueUpToIso CompHaus.isTerminalPUnit