Theorems · Definition · commutative algebra

HomogeneousLocalization

{ι : Type u_1} →
  {A : Type u_2} → {σ : Type u_3} → [inst : CommRing A] → [SetLike σ A] → (ι → σ) → Submonoid A → Type (max u_1 u_2)

For x : prime ideal of A, HomogeneousLocalization 𝒜 x is NumDenSameDeg 𝒜 x modulo the kernel of embedding 𝒜 x. This is essentially the subring of Aₓ where the numerator and denominator share the same grading.

Defined in

Mathlib.RingTheory.GradedAlgebra.HomogeneousLocalization

Cited by

69 results in Mathlib

Foundations

Depth 24 from the axioms · uses propext

Assumes

CommRingSetLike