spanFunctor — Mathlib

Lean4
/-- For a given compact subset `C` of `I → Bool`, `spanFunctor` is the functor from the poset of finsets
of `I` to `Profinite`, sending a finite subset set `J` to the image of `C` under the projection
`Proj J`.
-/
noncomputable def spanFunctor [∀ (s : Finset I) (i : I), Decidable (i ∈ s)] (hC : IsCompact C) :
    (Finset I)ᵒᵖ ⥤ Profinite.{u}
    where
  obj
    s :=
    @Profinite.of (π C (· ∈ (unop s))) _ (by rw [← isCompact_iff_compactSpace]; exact hC.image (continuous_proj _)) _ _
  map
    h :=
    @CompHausLike.ofHom _ _ _ (_) (_) (_) (_) (_) (_) (_) (_)
      ⟨(ProjRestricts C (leOfHom h.unop)), continuous_projRestricts _ _⟩
  map_id J := by simp only [projRestricts_eq_id C (· ∈ (unop J))]; rfl
  map_comp _ _ := by rw [← CompHausLike.ofHom_comp]; congr; dsimp; rw [projRestricts_eq_comp]
Похожие утверждения