English
If 𝒜(0) is of finite type, then Proj.instUniversallyClosedToSpecZero 𝒜 holds: the morphism to SpecZero satisfies valuative criterion.
Русский
Если 𝒜(0) конечного типа, то Proj.instUniversallyClosedToSpecZero 𝒜 выполняется: отображение к SpecZero удовлетворяет валютивному критерию.
LaTeX
$$$\mathrm{UniversallyClosed}(\mathrm{Proj.toSpecZero}(\mathcal A))$ under finite type on 𝒜(0)$$
Lean4
@[simp]
theorem mk_mem_carrier (z : HomogeneousLocalization.NumDenSameDeg 𝒜 (.powers f)) :
HomogeneousLocalization.mk z ∈ carrier x ↔ z.num.1 ∈ x.1.asHomogeneousIdeal :=
by
rw [carrier, Ideal.mem_comap, HomogeneousLocalization.algebraMap_apply, HomogeneousLocalization.val_mk,
Localization.mk_eq_mk', IsLocalization.mk'_eq_mul_mk'_one, mul_comm, Ideal.unit_mul_mem_iff_mem, ← Ideal.mem_comap,
IsLocalization.comap_map_of_isPrime_disjoint (.powers f)]
· rfl
· infer_instance
· exact (disjoint_powers_iff_notMem _ (Ideal.IsPrime.isRadical inferInstance)).mpr x.2
· exact isUnit_of_invertible _
