isUnit_res_basicOpen — Mathlib

English

Compatibility of basicOpen under restriction maps; res respects basicOpen via iso.

Русский

Совместимость basicOpen под ограничениями: сохранение через изоморфизм.

LaTeX

$$$@basicOpen X (unop V) (X.presheaf.map i f) = unop V \cap @basicOpen X (unop U) f$$$

Lean4

/-- The restriction of a section `f` to the basic open of `f` is a unit. -/
theorem isUnit_res_basicOpen {U : Opens X} (f : X.presheaf.obj (op U)) :
    IsUnit (X.presheaf.map (@homOfLE (Opens X) _ _ _ (X.basicOpen_le f)).op f) :=
  by
  apply isUnit_of_isUnit_germ
  rintro x ⟨hxU, hx⟩
  convert hx
  exact X.presheaf.germ_res_apply _ _ _ _

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