some lemmas about preimage and image in schemes

Stream: Is there code for X?

[Kenny Lau]

import Mathlib

universe u

namespace AlgebraicGeometry.Scheme

open CategoryTheory

@[simp] lemma image_comp {X Y Z : Scheme.{u}} {f : X ⟶ Y} {g : Y ⟶ Z}
    [IsOpenImmersion f] [IsOpenImmersion g] (U : X.Opens) :
    (f ≫ g) ''ᵁ U = g ''ᵁ f ''ᵁ U :=
  TopologicalSpace.Opens.ext <| Set.image_comp g.base f.base (U : Set X)

lemma image_id' {X : Scheme.{u}} {f : X ⟶ X} [IsOpenImmersion f] (hf : f = 𝟙 X) {U : X.Opens} :
    f ''ᵁ U = U := by
  subst hf; exact TopologicalSpace.Opens.ext <| Set.image_id _

@[simp] lemma preimage_inv {X Y : Scheme.{u}} {f : X ≅ Y} (V : Y.Opens) :
    f.inv ''ᵁ V = f.hom ⁻¹ᵁ V := by
  rw [← f.hom.preimage_image_eq (f.inv ''ᵁ V), ← image_comp, image_id' (by simp)]

end AlgebraicGeometry.Scheme