preimageIso_hom_ι — Mathlib

English

For an isomorphism f and open U ⊆ Y, the morphism (f.preimageIso U).hom composed with U.ι equals the projection through f.

Русский

Для изоморфизма f и открытого U ⊆ Y: (f.preimageIso U).hom ∘ U.ι = (f^{-1}U).ι ∘ f

LaTeX

$$(f.preimageIso U).hom ≫ U.ι = (f ⁻¹ᵁ U).ι ≫ f$$

Lean4

@[reassoc (attr := simp)]
theorem preimageIso_hom_ι {X Y : Scheme.{u}} (f : X.Hom Y) [IsIso (C := Scheme) f] (U : Y.Opens) :
    (f.preimageIso U).hom ≫ U.ι = (f ⁻¹ᵁ U).ι ≫ f :=
  IsOpenImmersion.isoOfRangeEq_hom_fac _ _ _

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