projectivePresentation — Mathlib

English

A specific instance showing every Ultrafilter object yields a projective object in Profinite.

Русский

Специфический пример: каждый Ultrafilter-объект порождает проективный объект в Profinite.

LaTeX

$$$\\text{Projective}(\\mathrm{Ultrafilter} X)$$$

Lean4

/-- For any profinite `X`, the natural map `Ultrafilter X → X` is a projective presentation. -/
def projectivePresentation (X : Profinite.{u}) : ProjectivePresentation X
    where
  p := of <| Ultrafilter X
  f := CompHausLike.ofHom _ ⟨_, continuous_ultrafilter_extend id⟩
  projective := Profinite.projective_ultrafilter X
  epi :=
    ConcreteCategory.epi_of_surjective _ fun x =>
      ⟨(pure x : Ultrafilter X), congr_fun (ultrafilter_extend_extends (𝟙 X)) x⟩

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