affineCover — Mathlib

Lean4
/-- The affine cover of a scheme. -/
def affineCover (X : Scheme.{u}) : OpenCover X where
  I₀ := X
  X x := Spec (X.local_affine x).choose_spec.choose
  f x := ⟨(X.local_affine x).choose_spec.choose_spec.some.inv ≫ X.toLocallyRingedSpace.ofRestrict _⟩
  mem₀ := by
    rw [presieve₀_mem_precoverage_iff]
    refine ⟨fun x ↦ ?_, inferInstance⟩
    use x
    simp only [LocallyRingedSpace.comp_toShHom, SheafedSpace.comp_base, TopCat.hom_comp, ContinuousMap.coe_comp]
    rw [Set.range_comp, Set.range_eq_univ.mpr, Set.image_univ]
    · erw [Subtype.range_coe_subtype]
      exact (X.local_affine x).choose.2
    rw [← TopCat.epi_iff_surjective]
    change Epi ((SheafedSpace.forget _).map (LocallyRingedSpace.forgetToSheafedSpace.map _))
    infer_instance
Похожие утверждения