isoOfIsAffine_inv_appTop_coord — Mathlib

English

For i ∈ n, the i-th coordinate under the inverse of the affine-space isomorphism corresponds to X_i under the ΓSpecIso.

Русский

Для i из n, i-й координат под действием обратного изоморфизма аффайн-пространства соответствует X_i через ΓSpecIso.

LaTeX

$$$(\\mathrm{isoOfIsAffine}\\; n\\; S)^{-1} \\circ \\mathrm{coord}_S(i) = (\\mathrm{ΓSpecIso}(.{\\rm of})).^{-1}(\\mathrm{X}_i).$$$

Lean4

@[simp]
theorem isoOfIsAffine_inv_appTop_coord [IsAffine S] (i) :
    (isoOfIsAffine n S).inv.appTop (coord _ i) = (Scheme.ΓSpecIso (.of _)).inv (.X i) :=
  homOfVector_appTop_coord _ _ _

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