sigma — Mathlib

Lean4
/-- A refinement of coverings induces a refinement on the single object coverings. -/
@[simps]
noncomputable def sigma (f : 𝒰 ⟶ 𝒱) : 𝒰.sigma ⟶ 𝒱.sigma
    where
  idx _ := default
  app _ := Sigma.desc fun j ↦ f.app j ≫ Sigma.ι _ (f.idx j)
  w _ := Sigma.hom_ext _ _ (by simp)
  app_prop
    _ :=
    by
    simp only [sigma_X, sigma_I₀, PUnit.default_eq_unit,
      IsZariskiLocalAtSource.iff_of_openCover (Scheme.IsLocallyDirected.openCover _), Discrete.functor_obj_eq_as,
      IsLocallyDirected.openCover_I₀, IsLocallyDirected.openCover_X, IsLocallyDirected.openCover_f, colimit.ι_desc,
      Cofan.mk_pt, Cofan.mk_ι_app]
    intro i
    exact P.comp_mem _ _ (f.app_prop i.1) (IsZariskiLocalAtSource.of_isOpenImmersion _)
Похожие утверждения