instProjectiveProfiniteObjToProfinite

English

Every Stonean space is projective in Profinite.

Русский

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

LaTeX

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

Lean4

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

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