basicOpenToSpec_app_top — Mathlib

English

The app of basicOpenToSpec at the top open equals the composition described in the lemma.

Русский

Применение basicOpenToSpec в верхнем открытом равняется композиции, описанной леммой.

LaTeX

$$(basicOpenToSpec 𝒜 f).app ⊤ = (Scheme.ΓSpecIso _).hom ≫ awayToSection 𝒜 f ≫ (basicOpen 𝒜 f).topIso.inv$$

Lean4

theorem basicOpenToSpec_app_top :
    (basicOpenToSpec 𝒜 f).app ⊤ = (Scheme.ΓSpecIso _).hom ≫ awayToSection 𝒜 f ≫ (basicOpen 𝒜 f).topIso.inv :=
  by
  rw [basicOpenToSpec]
  simp only [Scheme.comp_coeBase, TopologicalSpace.Opens.map_comp_obj, TopologicalSpace.Opens.map_top, Scheme.comp_app,
    Scheme.Opens.topIso_inv, eqToHom_op]
  erw [Scheme.comp_app]
  simp

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