gluedScheme — Mathlib

Lean4
/-- (Implementation). The glued scheme of a glue data.
This should not be used outside this file. Use `AlgebraicGeometry.Scheme.GlueData.glued` instead. -/
def gluedScheme : Scheme :=
  by
  apply LocallyRingedSpace.IsOpenImmersion.scheme D.toLocallyRingedSpaceGlueData.toGlueData.glued
  intro x
  obtain ⟨i, y, rfl⟩ := D.toLocallyRingedSpaceGlueData.ι_jointly_surjective x
  obtain ⟨j, z, hz⟩ := (D.U i).affineCover.exists_eq y
  refine ⟨_, ((D.U i).affineCover.f j).toLRSHom ≫ D.toLocallyRingedSpaceGlueData.toGlueData.ι i, ?_⟩
  constructor
  · simp only [LocallyRingedSpace.comp_toShHom, SheafedSpace.comp_base, TopCat.hom_comp, ContinuousMap.coe_comp,
      Set.range_comp]
    exact Set.mem_image_of_mem _ ⟨z, hz⟩
  · infer_instance
Похожие утверждения