instProjectiveCompHausCompHaus — Mathlib

English

Every Stonean space is projective in CompHaus.

Русский

Каждое Stonean-пространство проективно в категории CompHaus.

LaTeX

$$$\forall X:\text{Stonean},\ \text{Projective}(\text{toCompHaus.obj}(X))$$$

Lean4

/-- Every Stonean space is projective in `CompHaus` -/
instance instProjectiveCompHausCompHaus (X : Stonean) : Projective (toCompHaus.obj X) where
  factors := by
    intro B C φ f _
    haveI : ExtremallyDisconnected (toCompHaus.obj X).toTop := X.prop
    have hf : Function.Surjective f := by rwa [← CompHaus.epi_iff_surjective]
    obtain ⟨f', h⟩ := CompactT2.ExtremallyDisconnected.projective φ.hom.continuous f.hom.continuous hf
    use ofHom _ ⟨f', h.left⟩
    ext
    exact congr_fun h.right _

Похожие утверждения