instProjective — Mathlib

English

Every Stonean space is projective in Stonean itself.

Русский

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

LaTeX

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

Lean4

/-- Every Stonean space is projective in `Stonean`. -/
instance (X : Stonean) : Projective X where
  factors := by
    intro B C φ f _
    haveI : ExtremallyDisconnected X.toTop := X.prop
    have hf : Function.Surjective f := by rwa [← Stonean.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 _

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