English
For opens U ⊆ Y and V ⊆ X with e: V ≤ f⁻¹ᵁ U, the composite f.appLE U V e ≫ (f.appIso U).inv equals a presheaf map: X.presheaf.map (homOfLE ...).
Русский
Для открытых U ⊆ Y и V ⊆ X и e: V ⊆ f⁻¹ᵁ U выполняется тождество: f.appLE U V e ≫ (f.appIso U).inv = X.presheaf.map (homOfLE ...).
LaTeX
$$$$ f.appLE U V e \;≫ (f.appIso V).inv = X.presheaf.map(homOfLE(\dots)).op $$$$
Lean4
/-- If `X ⟶ Y` is an open immersion, and `Y` is a scheme, then so is `X`. -/
def toScheme : Scheme :=
by
apply LocallyRingedSpace.IsOpenImmersion.scheme (toLocallyRingedSpace _ f)
intro x
obtain ⟨R, i, _, h₁, h₂⟩ :=
Scheme.exists_affine_mem_range_and_range_subset (U := ⟨_, H.base_open.isOpen_range⟩) ⟨x, rfl⟩
refine ⟨R, LocallyRingedSpace.IsOpenImmersion.lift (toLocallyRingedSpaceHom _ f) _ h₂, ?_, ?_⟩
· rw [LocallyRingedSpace.IsOpenImmersion.lift_range]; exact h₁
· delta LocallyRingedSpace.IsOpenImmersion.lift; infer_instance
