preimageIso_inv_ι — Mathlib

English

For f: X → Y an isomorphism and open U ⊆ Y, the composite (f.preimageIso U).inv ≫ (f ⁻¹ᵁ U).ι ≫ f equals U.ι.

Русский

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

LaTeX

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

Lean4

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

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