arrowResLEAppIso — Mathlib

English

A membership relation between opens translates into a preimage inclusion criterion for resLE via theopens mapping and the inclusion maps.

Русский

Членство между открытыми множествами переводится в критерий включения через прообраз для resLE с помощью отображений открытий.

LaTeX

$$$W \le (f.resLE\, U\, V\, e)^{-1}\!O \iff V.ι''W \le f^{-1}\!U.ι''O$$$

Lean4

/-- `f.resLE U V` induces `f.appLE U V` on global sections. -/
noncomputable def arrowResLEAppIso (f : X ⟶ Y) (U : Y.Opens) (V : X.Opens) (e : V ≤ f ⁻¹ᵁ U) :
    Arrow.mk ((f.resLE U V e).appTop) ≅ Arrow.mk (f.appLE U V e) :=
  Arrow.isoMk U.topIso V.topIso <|
    by
    simp only [Arrow.mk_left, Arrow.mk_right, Functor.id_obj, Scheme.Opens.topIso_hom, eqToHom_op, Arrow.mk_hom,
      Scheme.Hom.map_appLE]
    rw [Scheme.Hom.appTop, ← Scheme.Hom.appLE_eq_app, Scheme.Hom.resLE_appLE, Scheme.Hom.appLE_map]

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