Projective

📁 Source: Mathlib/Topology/Category/Profinite/Projective.lean

Statistics

Metric	Count
Definitions Projective, projectivePresentation, Projective	3
Theorems instEnoughProjectives, projective_ultrafilter	2
Total	5

CompactT2

Definitions

Name	Category	Theorems
Projective 📖	MathDef	3 math math: StoneCech.projective, projective_iff_extremallyDisconnected, ExtremallyDisconnected.projective

Profinite

Definitions

Name	Category	Theorems
projectivePresentation 📖	CompOp	—

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
instEnoughProjectives 📖	mathematical	—	CategoryTheory.EnoughProjectives Profinite CompHausLike.category TotallyDisconnectedSpace TopCat.carrier TopCat.str	—	—
projective_ultrafilter 📖	mathematical	—	CategoryTheory.Projective Profinite CompHausLike.category TotallyDisconnectedSpace TopCat.carrier TopCat.str of Ultrafilter Ultrafilter.topologicalSpace ultrafilter_compact Ultrafilter.t2Space instTotallyDisconnectedSpaceUltrafilter	—	ultrafilter_compact Ultrafilter.t2Space instTotallyDisconnectedSpaceUltrafilter Function.Surjective.hasRightInverse epi_iff_surjective continuous_ultrafilter_extend CompHausLike.is_hausdorff CompHausLike.is_compact instHasPropTotallyDisconnectedSpaceCarrier instTotallyDisconnectedSpaceCarrierToTop CategoryTheory.ConcreteCategory.coe_ext DenseRange.equalizer denseRange_pure Continuous.comp ContinuousMap.continuous Function.RightInverse.comp_eq_id Function.comp_assoc ultrafilter_extend_extends

WeierstrassCurve

Definitions

Name	Category	Theorems
Projective 📖	CompOp	—

---

← Back to Index