opensFunctor_map_homOfLE — Mathlib

English

For open immersions f: X → Y and g: Y → Z, the opensRange of f ≫ g equals the image of f.opensRange under g.

Русский

Для открытых вложений f: X → Y и g: Y → Z, открытый диапазон f ≫ g равен образу f.opensRange под действием g.

LaTeX

$$$ (f ≫ g).opensRange = g \\;''^\\!\\mathrm{ opensRange}(f) $$$

Lean4

@[simp]
theorem opensFunctor_map_homOfLE {U V : X.Opens} (e : U ≤ V) :
    (Scheme.Hom.opensFunctor f).map (homOfLE e) = homOfLE (f.image_le_image_of_le e) :=
  rfl

Похожие утверждения