diff --git a/Mathlib/Algebra/DirectSum/Basic.lean b/Mathlib/Algebra/DirectSum/Basic.lean
index c71c83f4d803e..94c0bb58601cb 100644
--- a/Mathlib/Algebra/DirectSum/Basic.lean
+++ b/Mathlib/Algebra/DirectSum/Basic.lean
@@ -399,6 +399,7 @@ section map
 variable {ι : Type*} [DecidableEq ι] {α : ι → Type*} {β : ι → Type*} [∀ i, AddCommMonoid (α i)]
 variable [∀ i, AddCommMonoid (β i)] (f : ∀(i : ι), α i →+ β i)
 
+/-- create a homomorphism from `⨁ i, α i` to `⨁ i, β i` by giving the component-wise map `f`. -/
 def map : (⨁ i, α i) →+ ⨁ i, β i :=
   DirectSum.toAddMonoid (fun i : ι ↦ (of β i).comp (f i))
 
diff --git a/Mathlib/RingTheory/GradedAlgebra/Basic.lean b/Mathlib/RingTheory/GradedAlgebra/Basic.lean
index e8425a595986c..0c4ab4f8569d4 100644
--- a/Mathlib/RingTheory/GradedAlgebra/Basic.lean
+++ b/Mathlib/RingTheory/GradedAlgebra/Basic.lean
@@ -346,9 +346,14 @@ section GradedRing
 variable {σ : Type*} [SetLike σ A] [AddSubmonoidClass σ A] (𝒜 : ι → σ)
 variable {M : ι → σ} [SetLike.GradedMonoid M]
 
+/-- The canonical isomorphism of an internal direct sum with the ambient ring -/
 noncomputable def coeRingEquiv (hM : DirectSum.IsInternal M) :
     (DirectSum ι fun i => ↥(M i)) ≃+* A := RingEquiv.ofBijective (DirectSum.coeRingHom M) hM
 
+/-- Given an `R`-algebra `A` and a family `ι → σ` of submonoids parameterized by an additive monoid
+ `ι` and satisfying `SetLike.GradedMonoid M` (essentially, is multiplicative), such that
+ `DirectSum.IsInternal M` (`A` is the direct sum of the `M i`), we endow `A` with the structure of a
+  graded ring. The submonoids are the *homogeneous* parts. -/
 noncomputable def gradedRing (hM : DirectSum.IsInternal M) : GradedRing M :=
   { (inferInstance : SetLike.GradedMonoid M) with
     decompose' := hM.coeRingEquiv.symm
diff --git a/Mathlib/RingTheory/GradedAlgebra/HomogeneousRelation.lean b/Mathlib/RingTheory/GradedAlgebra/HomogeneousRelation.lean
index 45082e6779f2f..d2c7c0c1d8416 100644
--- a/Mathlib/RingTheory/GradedAlgebra/HomogeneousRelation.lean
+++ b/Mathlib/RingTheory/GradedAlgebra/HomogeneousRelation.lean
@@ -26,6 +26,9 @@ In this file, we define the property of an ideal being homogeneous.
 variable {ι : Type*} [DecidableEq ι] [AddMonoid ι]
 variable {A : Type*} [Semiring A]
 
+/-- a relation `r : A → A → Prop` is homogeneous with respect to the grading `𝒜` if `r x y` implies
+  that for every index `i`, the projection of `x` and `y` onto the `i`-th grading piece satisfies
+  the equivalence relation generated by `r`. -/
 class IsHomogeneousRelation {σ : Type*} [SetLike σ A] [AddSubmonoidClass σ A] (𝒜 : ι → σ)
   [GradedRing 𝒜] (r : A → A → Prop) : Prop where
   is_homogeneous' : ∀ {x y : A}, r x y →
@@ -92,7 +95,7 @@ lemma Finset.relation_sum_induction {α : Type*} {s : Finset α} [DecidableEq α
   | insert _ _ => simp_all
 
 lemma coe_mul_sum_support_subset {ι : Type*} {σ : Type*} {R : Type*} [DecidableEq ι] [Semiring R]
-    [SetLike σ R] [AddSubmonoidClass σ R] (A : ι → σ) [AddMonoid ι] [SetLike.GradedMonoid A]
+    [SetLike σ R] [AddSubmonoidClass σ R] (A : ι → σ) [AddMonoid ι]
     [(i : ι) → (x : ↥(A i)) → Decidable (x ≠ 0)] (r r' : DirectSum ι fun i ↦ ↥(A i))
     {S T: Finset ι} (hS : DFinsupp.support r ⊆ S) (hT : DFinsupp.support r' ⊆ T)
     (p : ι × ι → Prop) [DecidablePred p] :
@@ -108,7 +111,7 @@ lemma coe_mul_sum_support_subset {ι : Type*} {σ : Type*} {R : Type*} [Decidabl
     · simp [hx h]
   simp [this]
 
-noncomputable local instance : (i : ι) → (x : ↥(𝒜 i)) → Decidable (x ≠ 0) :=
+noncomputable private instance : (i : ι) → (x : ↥(𝒜 i)) → Decidable (x ≠ 0) :=
     fun _ x ↦ Classical.propDecidable (x ≠ 0)
 
 theorem eqvGen_proj_mul_right {a b c : A} (n : ι)