toSpec_base_isIso — Mathlib

English

If f is a homogeneous element of positive degree in a graded algebra, then the base of the associated Spec morphism is an isomorphism.

Русский

Если f — однородный элемент степени положительной степени в градуированном алгебре, то база соответствующего отображения Spec является изоморфизмом.

LaTeX

$$$\\operatorname{IsIso}((\\mathrm{toSpec}\\ 𝒜\\ f).\\mathrm{base}).$$$

Lean4

theorem toSpec_base_isIso {f} {m} (f_deg : f ∈ 𝒜 m) (hm : 0 < m) : IsIso (toSpec 𝒜 f).base :=
  by
  convert (projIsoSpecTopComponent f_deg hm).isIso_hom
  exact ConcreteCategory.hom_ext _ _ <| toSpec_base_apply_eq 𝒜

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