English
If 𝒜 is finitely generated in the graded sense and A is of finite type over 𝒜0, then the homogeneous localization Away 𝒜 f is also of finite type over 𝒜0 for any f ∈ A of some degree.
Русский
Если 𝒜 — конечномерно порождаемая градуированная алгебра, и A является конечного типа над 𝒜0, тогда локализация Away 𝒜 f также имеет конечный тип над 𝒜0 для любого f ∈ A.
LaTeX
$$$$ \text{If } 𝒜 \text{ is finitely generated as an algebra over } 𝒜_0 \text{ and } A/𝒜_0 \text{ is finite type}, \\ \text{then } \text{Away } 𝒜 f \text{ is a finite type } 𝒜_0\text{-algebra}.$$$$
Lean4
theorem finiteType (f : A) (d : ℕ) (hf : f ∈ 𝒜 d) : Algebra.FiniteType (𝒜 0) (Away 𝒜 f) :=
by
constructor
obtain ⟨s, hs, hs'⟩ := GradedAlgebra.exists_finset_adjoin_eq_top_and_homogeneous_ne_zero 𝒜
choose dx hdx hxd using Subtype.forall'.mp hs'
simp_rw [Subalgebra.fg_def, ← top_le_iff, ← Away.adjoin_mk_prod_pow_eq_top hf (ι' := s) Subtype.val (by simpa) dx hxd]
rcases d.eq_zero_or_pos with hd | hd
· let f' := Away.mk 𝒜 hf 1 1 (by simp [hd, GradedOne.one_mem])
refine ⟨{ f' }, Set.finite_singleton f', ?_⟩
rw [Algebra.adjoin_le_iff]
rintro _ ⟨a, ai, hai, hai', rfl⟩
obtain rfl : ai = 0 := funext <| by simpa [hd, hdx] using hai
simp only [Finset.univ_eq_attach, Pi.zero_apply, pow_zero, Finset.prod_const_one, mem_coe]
convert pow_mem (Algebra.self_mem_adjoin_singleton (𝒜 0) f') a using 1
ext
simp [f', Localization.mk_pow]
refine ⟨_, ?_, le_rfl⟩
let b := ∑ i, dx i
let s' : Set ((Fin (b + 1)) × (s → Fin (d + 1))) := {ai | ∑ i, (ai.2 i).1 * dx i = ai.1 * d}
let F : s' → Away 𝒜 f := fun ai ↦
Away.mk 𝒜 hf ai.1.1.1 (∏ i, i ^ (ai.1.2 i).1)
(by convert SetLike.prod_pow_mem_graded _ _ _ _ fun i _ ↦ hxd i; exact ai.2.symm)
apply (Set.finite_range F).subset
rintro _ ⟨a, ai, hai, hai', rfl⟩
refine ⟨⟨⟨⟨a, ?_⟩, fun i ↦ ⟨ai i, (hai' i).trans_lt d.lt_succ_self⟩⟩, hai⟩, rfl⟩
rw [Nat.lt_succ, ← mul_le_mul_iff_of_pos_right hd, ← smul_eq_mul, ← hai, Finset.sum_mul]
simp_rw [smul_eq_mul, mul_comm _ d]
gcongr
exact hai' _
