AlgebraicGeometry.ProjIsoSpecTopComponent.FromSpec.carrier.denom_not_mem

theorem AlgebraicGeometry.ProjIsoSpecTopComponent.FromSpec.carrier.denom_not_mem : ∀ {R : Type u_1} {A : Type u_2} [inst : CommRing R] [inst_1 : CommRing A] [inst_2 : Algebra R A] {𝒜 : ℕ → Submodule R A} [inst_3 : GradedAlgebra 𝒜] {f : A} {m : ℕ} (f_deg : f ∈ 𝒜 m) (hm : 0 < m) (q : ↑↑(AlgebraicGeometry.Spec.locallyRingedSpaceObj (CommRingCat.of (HomogeneousLocalization.Away 𝒜 f))).toPresheafedSpace), f ∉ AlgebraicGeometry.ProjIsoSpecTopComponent.FromSpec.carrier.asIdeal f_deg hm q

This theorem states that for any commutative ring `R`, another ring `A` which is an algebra over `R`, a grading on `A` by natural numbers represented by `𝒜`, and any element `f` of `A` that belongs to the `m`-th graded part of `A` where `m` is positive, if we consider the spectrum of the localized ring at `f` as a locally ringed space, then `f` is not an element of the ideal associated with the carrier of the projective morphism from the spectrum of the top component of the localization of `A` at `f` to the spectrum of `R`. In other words, `f` is not in the ideal of the corresponding point in the projective scheme. This is a key property in the construction of projective schemes in algebraic geometry.

More concisely: For any commutative ring `R`, an algebra `A` over `R` with a positive grading `𝒜`, and an element `f` in the `m`-th graded part of `A`, `f` is not in the ideal of the corresponding point in the projective scheme of `A` localized at `f`.