isoSpec_hom_appTop — Mathlib

English

The appTop of the forward isoSpec morphism is the composition (Γ SpecIso).hom ≫ U.topIso.inv; i.e., the action on appTop is determined by the Γ-spec isomorphism and the inverse of the topological isomorphism.

Русский

Компонента appTop прямого морфизма isoSpec равна композиции (Γ SpecIso).hom ∘ U.topIso.inv; поведение на appTop задаётся черезϵ изоморфизм Γ-Spec и обратное отображение сверху.

LaTeX

$$hU.isoSpec.hom.appTop = (Scheme.ΓSpecIso Γ(X, U)).hom ≫ U.topIso.inv$$

Lean4

theorem isoSpec_hom_appTop : hU.isoSpec.hom.appTop = (Scheme.ΓSpecIso Γ(X, U)).hom ≫ U.topIso.inv :=
  by
  have := congr(inv $hU.isoSpec_inv_appTop)
  rw [IsIso.inv_comp, IsIso.Iso.inv_inv, IsIso.Iso.inv_hom] at this
  have := (Scheme.Γ.map_inv hU.isoSpec.inv.op).trans this
  rwa [← op_inv, IsIso.Iso.inv_inv] at this

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