feat(RingTheory/GradedAlgebra): homogeneous relation by xyzw12345 · Pull Request #27307 · leanprover-community/mathlib4

xyzw12345 · 2025-07-20T14:32:19Z

In this PR, we defined the concept of a homogeneous relation and proved some properties about homogeneous relations. The main result of this PR is showing that taking RingQuot by a homogeneous relation can give a graded structure on the quotient ring. This result can be used to define graded structures on rings obtained using RingQuot, e.g. the Symmetric Algebra defined in #21539 can be verified to have such a structure.

Co-authored-by:
Zhixuan Dai @atstarrysky 22300180006@m.fudan.edu.cn
Yiming Fu @pelicanhere fakegreenall@foxmail.com
Zhenyan Fu @pumpkin678 fuzhenyan@mail.dlut.edu.cn
Raphael Douglas Giles @Raph-DG raphaeldouglasgiles@gmail.com
Jiedong Jiang @jjdishere emailboxofjjd@163.com

This PR continues the work from #22279.

Original PR: #22279

This reverts commit c553de1.

This reverts commit c7f978d.

…tered-ring

and fix proof style for variable

…tered-ring

…_HomogeneousRelation

xyzw12345 · 2025-09-23T01:43:07Z

@ocfnash Thanks for the suggestion! I agree that RingQuot is more like a legacy, so we should probably not just write it for this case. Do you think that it will make more sense to talk about GradedAlgebra structure given by a surjective RingHom or AlgHom whose kernel is a homogeneous ideal?
I mean, we do have things like SymmetricAlgebra that we want to have a GradedAlgebra structure on it but it's defined by RingQuot, so we probably still want the RingQuot case. But since we would also want to have the case of taking quotient by a homogeneous ideal, maybe we can just work with a surjective RingHom?

Mathlib/Algebra/DirectSum/Module.lean

erdOne

Can you specialize everything to quotients by RingCons (and by extension HasQuotient.Quotient by [I.IsTwoSided]?

As long as this is doable and not painful I think it is fine if we are working with RingQuot here.

Mathlib/Algebra/Ring/Equiv.lean

Mathlib/Algebra/RingQuot.lean

Mathlib/RingTheory/GradedAlgebra/Basic.lean

erdOne · 2025-11-15T17:08:56Z

Mathlib/RingTheory/GradedAlgebra/Basic.lean

+
+/-- 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


Suggested change

(DirectSum ι fun i => ↥(M i)) ≃+* A := RingEquiv.ofBijective (DirectSum.coeRingHom M) hM

(DirectSum ι (M ·)) ≃+* A := RingEquiv.ofBijective (DirectSum.coeRingHom M) hM

Can you add some API for this iso?

Sure, I'll add some API, and probably split the part about direct sum and graded rings into a separate PR (if that's a reasonable to do?)

Mathlib/RingTheory/GradedAlgebra/HomogeneousRelation.lean

mathlib4-merge-conflict-bot · 2025-11-19T07:54:51Z

This pull request has conflicts, please merge master and resolve them.

Co-authored-by: Andrew Yang <36414270+erdOne@users.noreply.github.com>

xyzw12345 · 2026-02-09T15:08:27Z

Can you specialize everything to quotients by RingCons (and by extension HasQuotient.Quotient by [I.IsTwoSided]?

As long as this is doable and not painful I think it is fine if we are working with RingQuot here.

I'll try to confirm this tomorrow morning (in my time zone), sorry for postponing replying to your reviews for so long, and thanks for the review!

Co-authored-by: Andrew Yang <36414270+erdOne@users.noreply.github.com>

…mathlib4 into xyzw12345_HomogeneousRelation

Co-authored-by: Junyan Xu <junyanxu.math@gmail.com>

alreadydone

Have you proven that the Submodule.quotientRel associated to a HomogeneousIdeal is a homogeneous relation?

alreadydone · 2026-02-10T10:07:54Z

Mathlib/Algebra/DirectSum/Module.lean

+def linearMap : (⨁ i, α i) →ₗ[R] ⨁ i, β i := DFinsupp.mapRange.linearMap f
+
+@[simp] lemma linearMap_of [DecidableEq ι] (i : ι) (x : α i) :
+    (linearMap f) (of α i x) = of β i (f i x) := by


Suggested change

(linearMap f) (of α i x) = of β i (f i x) := by

linearMap f (of α i x) = of β i (f i x) := by

(optional)

I'd make variables implicit in linearMap_of/apply/id/comp since they can be inferred from both sides.

alreadydone · 2026-02-10T10:08:15Z

Mathlib/Algebra/DirectSum/Module.lean

+  change DFinsupp.mapRange.linearMap f (DFinsupp.single i x) = DFinsupp.single i (f i x)
+  simp
+
+@[simp] lemma linearMap_apply (i : ι) (x : ⨁ i, α i) : (linearMap f) x i = f i (x i) := by


Suggested change

@[simp] lemma linearMap_apply (i : ι) (x : ⨁ i, α i) : (linearMap f) x i = f i (x i) := by

@[simp] lemma linearMap_apply (i : ι) (x : ⨁ i, α i) : linearMap f x i = f i (x i) := by

(optional)

alreadydone · 2026-02-10T10:08:26Z

Mathlib/Algebra/DirectSum/Module.lean

+  | add _ _ hx hy => simp [hx, hy]
+
+@[simp] lemma linearMap_id :
+    (linearMap (fun i ↦ LinearMap.id (R := R) (M := α i))) = LinearMap.id := by


Suggested change

(linearMap (fun i ↦ LinearMap.id (R := R) (M := α i))) = LinearMap.id := by

linearMap (fun i ↦ .id (R := R) (M := α i)) = .id := by

alreadydone · 2026-02-10T10:09:57Z

Mathlib/Algebra/DirectSum/Module.lean

+variable [∀ i, AddCommMonoid (α i)] [∀ i, AddCommMonoid (β i)]
+variable [∀ i, Module R (α i)] [∀ i, Module R (β i)]
+
+variable (f : ∀ (i : ι), α i →ₗ[R] β i)


Suggested change

variable (f : ∀ (i : ι), α i →ₗ[R] β i)

variable (f : ∀ i : ι, α i →ₗ[R] β i)

(optional, you might also omit : ι)

alreadydone · 2026-02-10T10:10:23Z

Mathlib/Algebra/DirectSum/Module.lean

+
+@[simp] lemma linearMap_comp {γ : ι → Type*} [∀ i, AddCommMonoid (γ i)] [∀ i, Module R (γ i)]
+    (g : ∀ (i : ι), β i →ₗ[R] γ i) :
+    (linearMap (fun i ↦ (g i).comp (f i))) = (linearMap g).comp (linearMap f) := by


Suggested change

(linearMap (fun i ↦ (g i).comp (f i))) = (linearMap g).comp (linearMap f) := by

linearMap (fun i ↦ (g i).comp (f i)) = (linearMap g).comp (linearMap f) := by

alreadydone · 2026-02-10T10:52:37Z

Mathlib/Algebra/Algebra/Equiv.lean

+    (h : f.comp e.toAlgHom = g.comp e.toAlgHom) : f = g := AlgHom.ext
+  fun x ↦ (by simpa using congr($h (e.symm x)))


Suggested change

(h : f.comp e.toAlgHom = g.comp e.toAlgHom) : f = g := AlgHom.ext

fun x ↦ (by simpa using congr($h (e.symm x)))

(h : f.comp e.toAlgHom = g.comp e.toAlgHom) : f = g :=

AlgHom.ext fun x ↦ by simpa using congr($h (e.symm x))

alreadydone · 2026-02-10T10:52:49Z

Mathlib/Algebra/DirectSum/Basic.lean

    map f x = map f y ↔ ∀ i, f i (x i) = f i (y i) := by
  simp_rw [DirectSum.ext_iff, map_apply]

+lemma map_eq_toAddMonoid [DecidableEq ι] : map f = toAddMonoid (fun i ↦ (of β i).comp (f i)) := by


Suggested change

lemma map_eq_toAddMonoid [DecidableEq ι] : map f = toAddMonoid (fun i ↦ (of β i).comp (f i)) := by

lemma map_eq_toAddMonoid [DecidableEq ι] : map f = toAddMonoid fun i ↦ (of β i).comp (f i) := by

alreadydone · 2026-02-10T10:53:08Z

Mathlib/Algebra/DirectSum/Module.lean


 theorem lof_eq_of (i : ι) (b : M i) : lof R ι M i b = of M i b := rfl

+@[simp] theorem lof_toAddMonoidHom_eq_of (i : ι) : (lof R ι M i).toAddMonoidHom = of M i := rfl


Suggested change

@[simp] theorem lof_toAddMonoidHom_eq_of (i : ι) : (lof R ι M i).toAddMonoidHom = of M i := rfl

@[simp] theorem toAddMonoidHom_lof_eq_of (i : ι) : (lof R ι M i).toAddMonoidHom = of M i := rfl

alreadydone · 2026-02-10T10:53:47Z

Mathlib/Algebra/DirectSum/Module.lean

+    obtain ⟨v, rfl⟩ := hy
+    exact ⟨u + v, by simp⟩
+
+lemma linearMap_eq_iff (x y : ⨁ i, α i) :


Suggested change

lemma linearMap_eq_iff (x y : ⨁ i, α i) :

lemma linearMap_eq_iff {x y : ⨁ i, α i} :

alreadydone · 2026-02-10T10:59:36Z

Mathlib/Algebra/Algebra/Equiv.lean


 end Semiring

+lemma comp_inj {R A B C : Type*} [CommSemiring R] [Semiring A] [Semiring B] [Semiring C]


You call the RingEquiv version comp_injective so this should probably be named the same.
And why not state this using Function.Injective? The statements are already defeq.

xyzw12345 · 2026-02-10T11:01:35Z

Have you proven that the Submodule.quotientRel associated to a HomogeneousIdeal is a homogeneous relation?

Thanks for the reminder! I will add that proof to this PR when I am available.

alreadydone · 2026-02-11T17:01:54Z

Thanks!
I think for rings it would be more convenient to use the quotient by Submodule/Ideal instead of RingQuot. Hopefully it's not hard to transport the GradedAlgebra instance across the isomorphism? ~~I think I'll also need that the ideal generated by a homogeneous polynomial is homogeneous (IsDomain condition may be required).~~ We should also show that any submodule generated by homogeneous elements is homogeneous. Of course these should be separate PRs ...

AntoineChambert-Loir · 2026-03-27T12:38:52Z

In #36501 , we have unfortunately duplicated (by anticipation, the file had a Lean3 version in 2023) some of your efforts. It seems worthwhile to have the versions for modules and submodules (though we only treated homogeneous submodules for the moment, because we had missed docs#ModuleCon).

Thmoas-Guan and others added 30 commits January 20, 2025 19:45

Create FilteredAlgebra.Basic

9e9b131

Update Mathlib.lean

5b06dee

update import

14ffc6c

Add inducedmaps

c7f978d

fix imports

c553de1

Revert "fix imports"

8eca9e6

This reverts commit c553de1.

Revert "Add inducedmaps"

faf1b4c

This reverts commit c7f978d.

Merge branch 'master' into filtered-ring-basic

1e2e00a

define the associated graded ring

9755a61

fix import

a239ebd

fix variable design

9495d23

Merge branch 'filtered-ring-basic' into associated-graded-ring-to-fil…

dd31559

…tered-ring

fix variable

b71e1e6

initial commit

c7806d2

Merge branch 'master' into filtered-ring-basic

aabea2f

Merge branch 'master' into associated-graded-ring-to-filtered-ring

ffd6ee9

updated missing instance

655826a

add coersion

6d57c93

use new definition

2092c49

fix import

a8a3147

move instance

5f81fe5

shorten lines

c9d7c2d

add end

15356ab

fix docstring

06d26e7

and fix proof style for variable

Merge branch 'filtered-ring-basic' into associated-graded-ring-to-fil…

4f2bf44

…tered-ring

fix import

bc098a0

fix using Monotone

e2a351c

Merge branch 'filtered-ring-basic' into associated-graded-ring-to-fil…

4094da9

…tered-ring

fix monotone

141b1a9

Merge branch 'associated-graded-ring-to-filtered-ring' into xyzw12345…

3a740af

…_HomogeneousRelation

leanprover-community-bot-assistant assigned mattrobball Sep 25, 2025

pelicanhere requested a review from chrisflav October 22, 2025 08:00

erdOne reviewed Nov 15, 2025

View reviewed changes

Mathlib/Algebra/DirectSum/Module.lean Outdated Show resolved Hide resolved

erdOne reviewed Nov 15, 2025

View reviewed changes

erdOne added the awaiting-author A reviewer has asked the author a question or requested changes. label Nov 15, 2025

mathlib4-merge-conflict-bot added the merge-conflict The PR has a merge conflict with master, and needs manual merging. (this label is managed by a bot) label Nov 19, 2025

Update Mathlib/Algebra/DirectSum/Module.lean

fc8a719

Co-authored-by: Andrew Yang <36414270+erdOne@users.noreply.github.com>

xyzw12345 and others added 6 commits February 9, 2026 23:14

Update Mathlib/Algebra/Ring/Equiv.lean

9ad4684

Co-authored-by: Andrew Yang <36414270+erdOne@users.noreply.github.com>

Update Mathlib/Algebra/RingQuot.lean

81e85da

Co-authored-by: Andrew Yang <36414270+erdOne@users.noreply.github.com>

Update Mathlib/RingTheory/GradedAlgebra/Basic.lean

8445f9b

Co-authored-by: Andrew Yang <36414270+erdOne@users.noreply.github.com>

Merge branch 'master' into xyzw12345_HomogeneousRelation

dc2e3df

Update Mathlib/RingTheory/GradedAlgebra/Basic.lean

8d12c7d

Co-authored-by: Andrew Yang <36414270+erdOne@users.noreply.github.com>

Merge branch 'xyzw12345_HomogeneousRelation' of github.com:xyzw12345/…

c038876

…mathlib4 into xyzw12345_HomogeneousRelation

github-actions bot removed the merge-conflict The PR has a merge conflict with master, and needs manual merging. (this label is managed by a bot) label Feb 9, 2026

Raph-DG and others added 8 commits February 9, 2026 17:21

Made the code compile

fa23288

Fixed more things that weren't compiling

100f86a

update to module system and fix some warnings

066dfe8

delete min_imports

3214041

remove unnecessary DecidableEq

150ae52

minor changes

2b63c5b

Update Mathlib/RingTheory/GradedAlgebra/HomogeneousRelation.lean

6f2aa00

Co-authored-by: Junyan Xu <junyanxu.math@gmail.com>

remove some parentheses

0127706

alreadydone reviewed Feb 10, 2026

View reviewed changes

chrisflav mentioned this pull request Mar 27, 2026

feat(RingTheory/GradedAlgebra/Homogeneous/RingQuot): graded structure on the quotient of a graded ring by a homogeneous ideal #36501

Open

	(DirectSum ι fun i => ↥(M i)) ≃+* A := RingEquiv.ofBijective (DirectSum.coeRingHom M) hM
	(DirectSum ι (M ·)) ≃+* A := RingEquiv.ofBijective (DirectSum.coeRingHom M) hM

	(linearMap f) (of α i x) = of β i (f i x) := by
	linearMap f (of α i x) = of β i (f i x) := by

	@[simp] lemma linearMap_apply (i : ι) (x : ⨁ i, α i) : (linearMap f) x i = f i (x i) := by
	@[simp] lemma linearMap_apply (i : ι) (x : ⨁ i, α i) : linearMap f x i = f i (x i) := by

	(linearMap (fun i ↦ LinearMap.id (R := R) (M := α i))) = LinearMap.id := by
	linearMap (fun i ↦ .id (R := R) (M := α i)) = .id := by

	variable (f : ∀ (i : ι), α i →ₗ[R] β i)
	variable (f : ∀ i : ι, α i →ₗ[R] β i)

	(linearMap (fun i ↦ (g i).comp (f i))) = (linearMap g).comp (linearMap f) := by
	linearMap (fun i ↦ (g i).comp (f i)) = (linearMap g).comp (linearMap f) := by

		(h : f.comp e.toAlgHom = g.comp e.toAlgHom) : f = g := AlgHom.ext
		fun x ↦ (by simpa using congr($h (e.symm x)))

	lemma map_eq_toAddMonoid [DecidableEq ι] : map f = toAddMonoid (fun i ↦ (of β i).comp (f i)) := by
	lemma map_eq_toAddMonoid [DecidableEq ι] : map f = toAddMonoid fun i ↦ (of β i).comp (f i) := by


		theorem lof_eq_of (i : ι) (b : M i) : lof R ι M i b = of M i b := rfl

		@[simp] theorem lof_toAddMonoidHom_eq_of (i : ι) : (lof R ι M i).toAddMonoidHom = of M i := rfl

	@[simp] theorem lof_toAddMonoidHom_eq_of (i : ι) : (lof R ι M i).toAddMonoidHom = of M i := rfl
	@[simp] theorem toAddMonoidHom_lof_eq_of (i : ι) : (lof R ι M i).toAddMonoidHom = of M i := rfl

	lemma linearMap_eq_iff (x y : ⨁ i, α i) :
	lemma linearMap_eq_iff {x y : ⨁ i, α i} :


		end Semiring

		lemma comp_inj {R A B C : Type*} [CommSemiring R] [Semiring A] [Semiring B] [Semiring C]

Conversation

xyzw12345 commented Jul 20, 2025 • edited by alreadydone Loading Uh oh! There was an error while loading. Please reload this page.

Uh oh!

Uh oh!

xyzw12345 commented Sep 23, 2025 • edited Loading Uh oh! There was an error while loading. Please reload this page.

Uh oh!

Uh oh!

Uh oh!

erdOne left a comment

Choose a reason for hiding this comment

Uh oh!

Uh oh!

Uh oh!

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Uh oh!

Uh oh!

mathlib4-merge-conflict-bot commented Nov 19, 2025

Uh oh!

xyzw12345 commented Feb 9, 2026

Uh oh!

alreadydone left a comment

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

xyzw12345 commented Feb 10, 2026

Uh oh!

alreadydone commented Feb 11, 2026 • edited Loading Uh oh! There was an error while loading. Please reload this page.

Uh oh!

Uh oh!

AntoineChambert-Loir commented Mar 27, 2026

Uh oh!

Reviewers

Assignees

Labels

Projects

Milestone

Development

Uh oh!

14 participants

xyzw12345 commented Jul 20, 2025 •

edited by alreadydone

Loading

xyzw12345 commented Sep 23, 2025 •

edited

Loading

alreadydone commented Feb 11, 2026 •

edited

Loading