Documentation Verification Report

Basic

📁 Source: Mathlib/Topology/Category/Stonean/Basic.lean

Statistics

Metric	Count
Definitions `presentation`, `π`, `toStonean`, `presentation`, `π`, `Stonean`, `compHaus`, `fullyFaithfulToCompHaus`, `mkFinite`, `of`, `toCompHaus`, `toProfinite`	12
Theorems `Gleason`, `instExtremallyDisconnectedCarrierToTopTrueOfProjective`, `lift_lifts`, `lift_lifts_assoc`, `epi_π`, `toStonean_toTop`, `lift_lifts`, `lift_lifts_assoc`, `epi_π`, `projective_of_extrDisc`, `epi_iff_surjective`, `instExtremallyDisconnectedCarrierToTop`, `instHasPropExtremallyDisconnectedCarrier`, `instProjective`, `instProjectiveCompHausCompHaus`, `instProjectiveProfiniteObjToProfinite`	16
Total	28

CompHaus

Definitions

Name	Category	Theorems
`presentation` 📖	CompOp	1 math math: `presentation.epi_π`
`toStonean` 📖	CompOp	1 math math: `toStonean_toTop`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`Gleason` 📖	mathematical	—	`CategoryTheory.Projective` `CompHaus` `CompHausLike.category` `ExtremallyDisconnected` `TopCat.carrier` `CompHausLike.toTop` `TopCat.str`	—	`Stonean.instExtremallyDisconnectedCarrierToTop` `instCompactSpaceCarrierToTopTrue` `instT2SpaceCarrierToTopTrue` `Stonean.instProjectiveCompHausCompHaus`
`instExtremallyDisconnectedCarrierToTopTrueOfProjective` 📖	mathematical	—	`ExtremallyDisconnected` `TopCat.carrier` `CompHausLike.toTop` `TopCat.str`	—	`CompactT2.Projective.extremallyDisconnected` `instCompactSpaceCarrierToTopTrue` `instT2SpaceCarrierToTopTrue` `CompHausLike.is_compact` `CompHausLike.is_hausdorff` `instHasPropTrue` `epi_iff_surjective` `CategoryTheory.Projective.factors` `ContinuousMap.continuous_toFun`
`lift_lifts` 📖	mathematical	—	`CategoryTheory.CategoryStruct.comp` `CompHaus` `CategoryTheory.Category.toCategoryStruct` `CompHausLike.category` `Stonean.compHaus` `lift`	—	`CategoryTheory.Projective.factorThru_comp` `Stonean.instProjectiveCompHausCompHaus`
`lift_lifts_assoc` 📖	mathematical	—	`CategoryTheory.CategoryStruct.comp` `CompHaus` `CategoryTheory.Category.toCategoryStruct` `CompHausLike.category` `Stonean.compHaus` `lift`	—	`CategoryTheory.Category.assoc` `Mathlib.Tactic.Reassoc.eq_whisker'` `lift_lifts`
`toStonean_toTop` 📖	mathematical	—	`CompHausLike.toTop` `ExtremallyDisconnected` `TopCat.carrier` `TopCat.str` `toStonean`	—	—

CompHaus.presentation

Definitions

Name	Category	Theorems
`π` 📖	CompOp	1 math math: `epi_π`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`epi_π` 📖	mathematical	—	`CategoryTheory.Epi` `CompHaus` `CompHausLike.category` `CategoryTheory.Functor.obj` `Stonean` `ExtremallyDisconnected` `TopCat.carrier` `TopCat.str` `Stonean.toCompHaus` `CompHaus.presentation` `π`	—	`CategoryTheory.ProjectivePresentation.epi`

Profinite

Definitions

Name	Category	Theorems
`presentation` 📖	CompOp	1 math math: `presentation.epi_π`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`lift_lifts` 📖	mathematical	—	`CategoryTheory.CategoryStruct.comp` `Profinite` `CategoryTheory.Category.toCategoryStruct` `CompHausLike.category` `TotallyDisconnectedSpace` `TopCat.carrier` `TopCat.str` `CategoryTheory.Functor.obj` `Stonean` `ExtremallyDisconnected` `Stonean.toProfinite` `lift`	—	`CategoryTheory.Projective.factorThru_comp` `Stonean.instProjectiveProfiniteObjToProfinite`
`lift_lifts_assoc` 📖	mathematical	—	`CategoryTheory.CategoryStruct.comp` `Profinite` `CategoryTheory.Category.toCategoryStruct` `CompHausLike.category` `TotallyDisconnectedSpace` `TopCat.carrier` `TopCat.str` `CategoryTheory.Functor.obj` `Stonean` `ExtremallyDisconnected` `Stonean.toProfinite` `lift`	—	`CategoryTheory.Category.assoc` `Mathlib.Tactic.Reassoc.eq_whisker'` `lift_lifts`
`projective_of_extrDisc` 📖	mathematical	—	`CategoryTheory.Projective` `Profinite` `CompHausLike.category` `TotallyDisconnectedSpace` `TopCat.carrier` `TopCat.str`	—	`CompHausLike.is_compact` `CompHausLike.is_hausdorff` `Stonean.instProjectiveProfiniteObjToProfinite`

Profinite.presentation

Definitions

Name	Category	Theorems
`π` 📖	CompOp	1 math math: `epi_π`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`epi_π` 📖	mathematical	—	`CategoryTheory.Epi` `Profinite` `CompHausLike.category` `TotallyDisconnectedSpace` `TopCat.carrier` `TopCat.str` `CategoryTheory.Functor.obj` `Stonean` `ExtremallyDisconnected` `Stonean.toProfinite` `Profinite.presentation` `π`	—	`CategoryTheory.ProjectivePresentation.epi` `Profinite.epi_iff_surjective` `CompHaus.epi_iff_surjective`

Stonean

Definitions

Name	Category	Theorems
`compHaus` 📖	CompOp	5 math math: `Condensed.epi_iff_surjective_on_stonean`, `CompHaus.lift_lifts`, `CondensedMod.epi_iff_surjective_on_stonean`, `CondensedSet.epi_iff_surjective_on_stonean`, `CompHaus.lift_lifts_assoc`
`fullyFaithfulToCompHaus` 📖	CompOp	—
`mkFinite` 📖	CompOp	—
`of` 📖	CompOp	—
`toCompHaus` 📖	CompOp	5 math math: `instEffectivelyEnoughCompHausToCompHaus`, `CompHaus.presentation.epi_π`, `instReflectsEffectiveEpisCompHausToCompHaus`, `instProjectiveCompHausCompHaus`, `instPreservesEffectiveEpisCompHausToCompHaus`
`toProfinite` 📖	CompOp	7 math math: `Profinite.lift_lifts_assoc`, `Profinite.lift_lifts`, `Condensed.StoneanProfinite.instPreservesEffectiveEpisStoneanProfiniteToProfinite`, `Condensed.StoneanProfinite.instEffectivelyEnoughStoneanProfiniteToProfinite`, `Condensed.StoneanProfinite.instReflectsEffectiveEpisStoneanProfiniteToProfinite`, `instProjectiveProfiniteObjToProfinite`, `Profinite.presentation.epi_π`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`epi_iff_surjective` 📖	mathematical	—	`CategoryTheory.Epi` `Stonean` `CompHausLike.category` `ExtremallyDisconnected` `TopCat.carrier` `TopCat.str` `DFunLike.coe` `CategoryTheory.ConcreteCategory.hom` `ContinuousMap` `CompHausLike.toTop` `ContinuousMap.instFunLike` `CompHausLike.concreteCategory`	—	`IsCompact.isClosed` `CompHausLike.is_hausdorff` `isCompact_range` `CompHausLike.is_compact` `ContinuousMap.continuous` `IsClosed.compl_mem_nhds` `TopologicalSpace.IsTopologicalBasis.mem_nhds_iff` `isTopologicalBasis_isClopen` `TotallySeparatedSpace.totallyDisconnectedSpace` `instTotallySeparatedSpaceOfExtremallyDisconnectedOfT2Space` `instExtremallyDisconnectedCarrierToTop` `instFiniteULift` `Finite.of_fintype` `instDiscreteTopologyULift` `instDiscreteTopologyFin` `LocallyConstant.continuous` `continuous_const` `CategoryTheory.cancel_epi` `CategoryTheory.ConcreteCategory.ext` `ContinuousMap.ext` `ULift.ext` `one_ne_zero` `Fin.instNeZeroHAddNatOfNat_mathlib_1` `CategoryTheory.ConcreteCategory.epi_of_surjective`
`instExtremallyDisconnectedCarrierToTop` 📖	mathematical	—	`ExtremallyDisconnected` `TopCat.carrier` `CompHausLike.toTop` `TopCat.str`	—	`CompHausLike.prop`
`instHasPropExtremallyDisconnectedCarrier` 📖	mathematical	—	`CompHausLike.HasProp` `ExtremallyDisconnected` `TopCat.carrier` `TopCat.str`	—	—
`instProjective` 📖	mathematical	—	`CategoryTheory.Projective` `Stonean` `CompHausLike.category` `ExtremallyDisconnected` `TopCat.carrier` `TopCat.str`	—	`epi_iff_surjective` `CompactT2.ExtremallyDisconnected.projective` `CompHausLike.prop` `CompHausLike.is_compact` `CompHausLike.is_hausdorff` `ContinuousMap.continuous` `instHasPropExtremallyDisconnectedCarrier` `instExtremallyDisconnectedCarrierToTop` `CategoryTheory.ConcreteCategory.ext` `ContinuousMap.ext`
`instProjectiveCompHausCompHaus` 📖	mathematical	—	`CategoryTheory.Projective` `CompHaus` `CompHausLike.category` `CategoryTheory.Functor.obj` `Stonean` `ExtremallyDisconnected` `TopCat.carrier` `TopCat.str` `toCompHaus`	—	`CompHaus.epi_iff_surjective` `CompactT2.ExtremallyDisconnected.projective` `CompHausLike.prop` `CompHaus.instCompactSpaceCarrierToTopTrue` `CompHaus.instT2SpaceCarrierToTopTrue` `ContinuousMap.continuous` `CompHausLike.is_compact` `CompHausLike.is_hausdorff` `CompHaus.instHasPropTrue` `CategoryTheory.ConcreteCategory.ext` `ContinuousMap.ext`
`instProjectiveProfiniteObjToProfinite` 📖	mathematical	—	`CategoryTheory.Projective` `Profinite` `CompHausLike.category` `TotallyDisconnectedSpace` `TopCat.carrier` `TopCat.str` `CategoryTheory.Functor.obj` `Stonean` `ExtremallyDisconnected` `toProfinite`	—	`Profinite.epi_iff_surjective` `CompactT2.ExtremallyDisconnected.projective` `CompHausLike.prop` `CompHausLike.is_compact` `CompHausLike.is_hausdorff` `ContinuousMap.continuous` `Profinite.instHasPropTotallyDisconnectedSpaceCarrier` `TotallySeparatedSpace.totallyDisconnectedSpace` `instTotallySeparatedSpaceOfExtremallyDisconnectedOfT2Space` `instExtremallyDisconnectedCarrierToTop` `Profinite.instTotallyDisconnectedSpaceCarrierToTop` `CategoryTheory.ConcreteCategory.ext` `ContinuousMap.ext`

(root)

Definitions

Name	Category	Theorems
`Stonean` 📖	CompOp	19 math math: `Stonean.instProjective`, `Stonean.instEffectivelyEnoughCompHausToCompHaus`, `Stonean.effectiveEpiFamily_tfae`, `Stonean.epi_iff_surjective`, `Stonean.instPreregular`, `Stonean.forget.preservesLimits`, `Profinite.lift_lifts_assoc`, `Profinite.lift_lifts`, `Condensed.StoneanProfinite.instPreservesEffectiveEpisStoneanProfiniteToProfinite`, `Condensed.StoneanProfinite.instEffectivelyEnoughStoneanProfiniteToProfinite`, `CompHaus.presentation.epi_π`, `Condensed.instPreservesFiniteProductsOppositeStoneanVal`, `Condensed.StoneanProfinite.instReflectsEffectiveEpisStoneanProfiniteToProfinite`, `Stonean.instReflectsEffectiveEpisCompHausToCompHaus`, `Stonean.instProjectiveCompHausCompHaus`, `Stonean.instProjectiveProfiniteObjToProfinite`, `Profinite.presentation.epi_π`, `Stonean.instPreservesEffectiveEpisCompHausToCompHaus`, `Stonean.effectiveEpi_tfae`

---

← Back to Index