isoOpensRange_inv_comp — Mathlib

English

For an open immersion f: X → Y, the composite f.isoOpensRange.inv ≫ f equals the inclusion f.opensRange.ι, showing the inverse of the opens-range decomposition recovers the original morphism.

Русский

Для открытого внедрения f: X → Y сопоставление inv возвращает ориентир, то есть f.isoOpensRange.inv ≫ f = f.opensRange.ι.

LaTeX

$$$f.isoOpensRange.inv \\circ f = f.opensRange.ι$$$

Lean4

@[reassoc (attr := simp)]
theorem isoOpensRange_inv_comp {X Y : Scheme.{u}} (f : X.Hom Y) [IsOpenImmersion f] :
    f.isoOpensRange.inv ≫ f = f.opensRange.ι := by simp [isoOpensRange]

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