isoOfEq_hom_ι — Mathlib

English

If X is a scheme and U, V opens with equality e: U = V, then the morphism (X.isoOfEq e).hom composed with V.ι equals U.ι.

Русский

Для схемы X и открытых U, V c равенством e: U = V, выполняется (X.isoOfEq e).hom ∘ V.ι = U.ι.

LaTeX

$$$(X.isoOfEq e).hom \\circ V.\\iota = U.\\iota$$$

Lean4

@[reassoc (attr := simp)]
theorem isoOfEq_hom_ι (X : Scheme.{u}) {U V : X.Opens} (e : U = V) : (X.isoOfEq e).hom ≫ V.ι = U.ι :=
  IsOpenImmersion.isoOfRangeEq_hom_fac _ _ _

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