ΓIsoTop — Mathlib

English

The hom component of the isomorphism satisfies (isoOfRangeEq f g e).hom ≫ g = f.

Русский

Гом-компонента изоморфизма удовлетворяет (isoOfRangeEq f g e).hom ≫ g = f.

LaTeX

$$$ (\text{isoOfRangeEq } f g e).hom \;\gg\; g = f $$$

Lean4

/-- Given an open immersion `f : U ⟶ X`, the isomorphism between global sections
  of `U` and the sections of `X` at the image of `f`. -/
noncomputable def ΓIsoTop {X Y : Scheme.{u}} (f : X ⟶ Y) [IsOpenImmersion f] : Γ(X, ⊤) ≅ Γ(Y, f.opensRange) :=
  (f.appIso ⊤).symm ≪≫ Y.presheaf.mapIso (eqToIso f.image_top_eq_opensRange.symm).op

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