ΓIso_inv — Mathlib

English

Equality relating ΓIsoTop to the canonical opens functor on opens.

Русский

Равенство между ΓIsoTop и каноническим отображением функций открытых множеств.

LaTeX

$$$ \Gamma\text{IsoTop } f U = (\text{opens functor}) $$$

Lean4

@[simp]
theorem ΓIso_inv {X Y : Scheme.{u}} (f : X ⟶ Y) [IsOpenImmersion f] (U : Y.Opens) :
    (ΓIso f U).inv =
      f.appLE (f.opensRange ⊓ U) (f ⁻¹ᵁ U) (by rw [← f.image_preimage_eq_opensRange_inter, f.preimage_image_eq]) :=
  by
  simp only [ΓIso, Iso.trans_inv, Functor.mapIso_inv, Iso.op_inv, eqToIso.inv, eqToHom_op, Iso.symm_inv,
    Scheme.Hom.appIso_hom', Scheme.Hom.map_appLE]

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