isoOfLE_hom_ι — Mathlib

English

For opens U ≤ V, the morphism (Scheme.Opens.isoOfLE hUV).hom composed with U.ι equals the inclusion of V into U after restriction.

Русский

Для U ≤ V: (Scheme.Opens.isoOfLE hUV).hom ∘ U.ι = (V.ι ⁻¹ᵁ U).ι ∘ V.ι.

LaTeX

$$(Scheme.Opens.isoOfLE hUV).hom ≫ U.ι = (V.ι ⁻¹ᵁ U).ι ≫ V.ι$$

Lean4

@[reassoc (attr := simp)]
theorem isoOfLE_hom_ι {X : Scheme.{u}} {U V : X.Opens} (hUV : U ≤ V) :
    (Scheme.Opens.isoOfLE hUV).hom ≫ U.ι = (V.ι ⁻¹ᵁ U).ι ≫ V.ι := by simp [isoOfLE]

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