isoImage_hom_ι — Mathlib

English

For an open immersion f: X → Y and any open U ⊆ X, the canonical morphism on opens satisfies f.isoOpensRange.hom ≫ f.opensRange.ι = f, i.e., the image and range inclusions compose to f.

Русский

Для открого внедрения f: X → Y и любого открытого U ⊆ X выполняется равенство указательных отображений: f.isoOpensRange.hom ∘ f.opensRange.ι = f.

LaTeX

$$$(f.isoOpensRange.hom) \\;\\circ\\; (f.opensRange.\\iota) = f$$$

Lean4

@[reassoc (attr := simp)]
theorem isoImage_hom_ι {X Y : Scheme.{u}} (f : X ⟶ Y) [IsOpenImmersion f] (U : X.Opens) :
    (f.isoImage U).hom ≫ (f ''ᵁ U).ι = U.ι ≫ f :=
  IsOpenImmersion.isoOfRangeEq_hom_fac _ _ _

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