Skip to content

Commit ad4f601

Browse files
kckennylaukckennylau
committed
feat(RingTheory): define graded ring homomorphisms (leanprover-community#30312)
This PR defines graded ring homomorphisms, which are ring homomorphisms that preserve the grading. We also provide the basic properties (aka the "API"). Zulip discussion: [#mathlib4 > Graded Ring Hom](https://leanprover.zulipchat.com/#narrow/channel/287929-mathlib4/topic/Graded.20Ring.20Hom/with/543601500)
1 parent 4ae5631 commit ad4f601

2 files changed

Lines changed: 301 additions & 0 deletions

File tree

β€ŽMathlib.leanβ€Ž

Lines changed: 1 addition & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -6179,6 +6179,7 @@ public import Mathlib.RingTheory.GradedAlgebra.Homogeneous.Subsemiring
61796179
public import Mathlib.RingTheory.GradedAlgebra.HomogeneousLocalization
61806180
public import Mathlib.RingTheory.GradedAlgebra.Noetherian
61816181
public import Mathlib.RingTheory.GradedAlgebra.Radical
6182+
public import Mathlib.RingTheory.GradedAlgebra.RingHom
61826183
public import Mathlib.RingTheory.Grassmannian
61836184
public import Mathlib.RingTheory.HahnSeries.Addition
61846185
public import Mathlib.RingTheory.HahnSeries.Basic

β€ŽMathlib/RingTheory/GradedAlgebra/RingHom.leanβ€Ž

Lines changed: 300 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,300 @@
1+
/-
2+
Copyright (c) 2025 Kenny Lau. All rights reserved.
3+
Released under Apache 2.0 license as described in the file LICENSE.
4+
Authors: Kenny Lau
5+
-/
6+
module
7+
8+
public import Mathlib.Data.FunLike.Graded
9+
public import Mathlib.RingTheory.GradedAlgebra.Basic
10+
11+
/-!
12+
# Homomorphisms of graded (semi)rings
13+
14+
This file defines bundled homomorphisms of graded (semi)rings. We use the same structure
15+
`GradedRingHom π’œ ℬ`, a.k.a. `π’œ β†’+*ᡍ ℬ`, for both types of homomorphisms.
16+
17+
We do **not** define a separate class of graded ring homomorphisms; instead, we use
18+
`[FunLike F A B] [GradedFunLike F π’œ ℬ] [RingHomClass F A B]`.
19+
20+
## Main definitions
21+
22+
* `GradedRingHom`: Graded (semi)ring homomorphisms. Ring homomorphism which preserves the grading.
23+
24+
## Notation
25+
26+
* `β†’+*ᡍ`: Graded (semi)ring hom.
27+
28+
## Implementation notes
29+
30+
* We don't really need the fact that they are graded rings until the theorem
31+
`DirectSum.decompose_map` which describes how the decomposition interacts with the map.
32+
-/
33+
34+
@[expose] public section
35+
36+
variable {ΞΉ A B C D Οƒ Ο„ ψ Ο‰ : Type*}
37+
[Semiring A] [Semiring B] [Semiring C] [Semiring D]
38+
[SetLike Οƒ A] [SetLike Ο„ B] [SetLike ψ C] [SetLike Ο‰ D]
39+
40+
section SetLike
41+
42+
/-- Bundled graded (semi)ring homomorphisms. Use `GradedRingHom` for the namespace and other
43+
identifiers, and `π’œ β†’+*ᡍ ℬ` for the notation. -/
44+
structure GradedRingHom (π’œ : ΞΉ β†’ Οƒ) (ℬ : ΞΉ β†’ Ο„) extends A β†’+* B where
45+
protected map_mem {i : ΞΉ} {x : A} : x ∈ π’œ i β†’ toRingHom x ∈ ℬ i
46+
47+
variable {π’œ : ΞΉ β†’ Οƒ} {ℬ : ΞΉ β†’ Ο„} {π’ž : ΞΉ β†’ ψ} {π’Ÿ : ΞΉ β†’ Ο‰}
48+
49+
@[inherit_doc]
50+
notation:25 π’œ " β†’+*ᡍ " ℬ => GradedRingHom π’œ ℬ
51+
52+
namespace GradedRingHom
53+
54+
section ofClass
55+
variable {F : Type*} [FunLike F A B] [GradedFunLike F π’œ ℬ] [RingHomClass F A B]
56+
57+
/-- Turn an element of a type `F` satisfying
58+
`[FunLike F A B] [GradedFunLike F π’œ ℬ] [RingHomClass F A B]` into an actual `GradedRingHom`.
59+
60+
This should not be used directly. In the future, Mathlib will prefer structural projections over
61+
these general constructions from hom classes. -/
62+
@[coe]
63+
def ofClass (f : F) : π’œ β†’+*ᡍ ℬ where
64+
__ := (f : A β†’+* B)
65+
map_mem := map_mem f
66+
67+
end ofClass
68+
69+
section coe
70+
71+
instance : FunLike (π’œ β†’+*ᡍ ℬ) A B where
72+
coe f := f.toFun
73+
coe_injective' f g h := by
74+
cases f
75+
cases g
76+
congr
77+
apply DFunLike.coe_injective'
78+
exact h
79+
80+
instance : GradedFunLike (π’œ β†’+*ᡍ ℬ) π’œ ℬ where
81+
map_mem f := f.map_mem
82+
83+
instance : RingHomClass (π’œ β†’+*ᡍ ℬ) A B where
84+
map_add f := f.map_add'
85+
map_zero f := f.map_zero'
86+
map_mul f := f.map_mul'
87+
map_one f := f.map_one'
88+
89+
initialize_simps_projections GradedRingHom (toFun β†’ apply)
90+
91+
attribute [coe] GradedRingHom.toRingHom
92+
93+
@[simp]
94+
theorem toRingHom_eq_toRingHom (f : π’œ β†’+*ᡍ ℬ) : RingHomClass.toRingHom f = f.toRingHom := rfl
95+
96+
@[simp]
97+
theorem coe_toRingHom (f : π’œ β†’+*ᡍ ℬ) : ⇑f.toRingHom = f := rfl
98+
99+
@[simp]
100+
theorem coe_mk (f : A β†’+* B) (h) : ((⟨f, h⟩ : π’œ β†’+*ᡍ ℬ) : A β†’ B) = f := rfl
101+
102+
@[simp]
103+
theorem coe_ofClass {F : Type*} [FunLike F A B] [GradedFunLike F π’œ ℬ] [RingHomClass F A B]
104+
(f : F) : ((.ofClass f : π’œ β†’+*ᡍ ℬ) : A β†’ B) = f := rfl
105+
106+
instance coeToRingHom : CoeOut (π’œ β†’+*ᡍ ℬ) (A β†’+* B) :=
107+
⟨GradedRingHom.toRingHom⟩
108+
109+
/-- Copy of a `GradedRingHom` with a new `toFun` equal to the old one. Useful to fix definitional
110+
equalities. -/
111+
def copy (f : π’œ β†’+*ᡍ ℬ) (f' : A β†’ B) (h : f' = f) : π’œ β†’+*ᡍ ℬ where
112+
__ := f.toRingHom.copy f' h
113+
map_mem hx := congr($h _ ∈ ℬ _).to_iff.mpr <| map_mem f hx
114+
115+
@[simp]
116+
theorem coe_copy (f : π’œ β†’+*ᡍ ℬ) (f' : A β†’ B) (h : f' = f) : ⇑(f.copy f' h) = f' :=
117+
rfl
118+
119+
theorem copy_eq (f : π’œ β†’+*ᡍ ℬ) (f' : A β†’ B) (h : f' = f) : f.copy f' h = f :=
120+
DFunLike.ext' h
121+
122+
end coe
123+
124+
section
125+
126+
variable (f : π’œ β†’+*ᡍ ℬ)
127+
128+
protected theorem congr_fun {f g : π’œ β†’+*ᡍ ℬ} (h : f = g) (x : A) : f x = g x :=
129+
DFunLike.congr_fun h x
130+
131+
protected theorem congr_arg (f : π’œ β†’+*ᡍ ℬ) {x y : A} (h : x = y) : f x = f y :=
132+
DFunLike.congr_arg f h
133+
134+
theorem coe_inj ⦃f g : π’œ β†’+*ᡍ ℬ⦄ (h : (f : A β†’ B) = g) : f = g :=
135+
DFunLike.coe_injective h
136+
137+
@[ext]
138+
theorem ext ⦃f g : π’œ β†’+*ᡍ ℬ⦄ : (βˆ€ x, f x = g x) β†’ f = g :=
139+
DFunLike.ext _ _
140+
141+
@[simp]
142+
theorem mk_coe (f : π’œ β†’+*ᡍ ℬ) (h₁ hβ‚‚ h₃ hβ‚„ hβ‚…) : .mk ⟨⟨⟨f, hβ‚βŸ©, hβ‚‚βŸ©, h₃, hβ‚„βŸ© hβ‚… = f :=
143+
ext fun _ => rfl
144+
145+
theorem coe_ringHom_injective : (fun f : π’œ β†’+*ᡍ ℬ => (f : A β†’+* B)).Injective := fun _ _ h =>
146+
ext <| DFunLike.congr_fun (F := A β†’+* B) h
147+
148+
/-- Graded ring homomorphisms map zero to zero. -/
149+
protected theorem map_zero (f : π’œ β†’+*ᡍ ℬ) : f 0 = 0 :=
150+
map_zero f
151+
152+
/-- Graded ring homomorphisms map one to one. -/
153+
protected theorem map_one (f : π’œ β†’+*ᡍ ℬ) : f 1 = 1 :=
154+
map_one f
155+
156+
/-- Graded ring homomorphisms preserve addition. -/
157+
protected theorem map_add (f : π’œ β†’+*ᡍ ℬ) (a b : A) : f (a + b) = f a + f b :=
158+
map_add ..
159+
160+
/-- Graded ring homomorphisms preserve multiplication. -/
161+
protected theorem map_mul (f : π’œ β†’+*ᡍ ℬ) (a b : A) : f (a * b) = f a * f b :=
162+
map_mul ..
163+
164+
end
165+
166+
section Ring
167+
variable {A B Οƒ Ο„ : Type*}
168+
variable [Ring A] [Ring B] [SetLike Οƒ A] [SetLike Ο„ B]
169+
variable (π’œ : ΞΉ β†’ Οƒ) (ℬ : ΞΉ β†’ Ο„)
170+
171+
/-- Graded ring homomorphisms preserve additive inverse. -/
172+
protected theorem map_neg (f : π’œ β†’+*ᡍ ℬ) (x : A) : f (-x) = -f x :=
173+
map_neg f x
174+
175+
/-- Graded ring homomorphisms preserve subtraction. -/
176+
protected theorem map_sub (f : π’œ β†’+*ᡍ ℬ) (x y : A) :
177+
f (x - y) = f x - f y :=
178+
map_sub f x y
179+
180+
end Ring
181+
182+
variable (π’œ) in
183+
/-- The identity graded ring homomorphism from a graded ring to itself. -/
184+
def id : π’œ β†’+*ᡍ π’œ where
185+
__ := RingHom.id _
186+
map_mem h := h
187+
188+
@[simp, norm_cast]
189+
theorem coe_id : ⇑(GradedRingHom.id π’œ) = _root_.id := rfl
190+
191+
@[simp]
192+
theorem id_apply (x : A) : GradedRingHom.id π’œ x = x :=
193+
rfl
194+
195+
@[simp]
196+
theorem toRingHom_id : (id π’œ).toRingHom = RingHom.id A :=
197+
rfl
198+
199+
/-- Composition of graded ring homomorphisms is a graded ring homomorphism. -/
200+
def comp (g : ℬ β†’+*ᡍ π’ž) (f : π’œ β†’+*ᡍ ℬ) : π’œ β†’+*ᡍ π’ž where
201+
__ := g.toRingHom.comp f
202+
map_mem := g.map_mem ∘ f.map_mem
203+
204+
/-- Composition of graded ring homomorphisms is associative. -/
205+
theorem comp_assoc (h : π’ž β†’+*ᡍ π’Ÿ) (g : ℬ β†’+*ᡍ π’ž) (f : π’œ β†’+*ᡍ ℬ) :
206+
(h.comp g).comp f = h.comp (g.comp f) :=
207+
rfl
208+
209+
@[simp]
210+
theorem coe_comp (hnp : ℬ β†’+*ᡍ π’ž) (hmn : π’œ β†’+*ᡍ ℬ) : (hnp.comp hmn : A β†’ C) = hnp ∘ hmn :=
211+
rfl
212+
213+
theorem comp_apply (hnp : ℬ β†’+*ᡍ π’ž) (hmn : π’œ β†’+*ᡍ ℬ) (x : A) :
214+
(hnp.comp hmn : A β†’ C) x = hnp (hmn x) :=
215+
rfl
216+
217+
@[simp]
218+
theorem comp_id (f : π’œ β†’+*ᡍ ℬ) : f.comp (id π’œ) = f :=
219+
ext fun _ => rfl
220+
221+
@[simp]
222+
theorem id_comp (f : π’œ β†’+*ᡍ ℬ) : (id ℬ).comp f = f :=
223+
ext fun _ => rfl
224+
225+
instance instOne : One (π’œ β†’+*ᡍ π’œ) where one := id _
226+
instance instMul : Mul (π’œ β†’+*ᡍ π’œ) where mul := comp
227+
228+
lemma one_def : (1 : π’œ β†’+*ᡍ π’œ) = id π’œ := rfl
229+
230+
lemma mul_def (f g : π’œ β†’+*ᡍ π’œ) : f * g = f.comp g := rfl
231+
232+
@[simp, norm_cast] lemma coe_one : ⇑(1 : π’œ β†’+*ᡍ π’œ) = _root_.id := rfl
233+
234+
@[simp, norm_cast] lemma coe_mul (f g : π’œ β†’+*ᡍ π’œ) : ⇑(f * g) = f ∘ g := rfl
235+
236+
instance instMonoid : Monoid (π’œ β†’+*ᡍ π’œ) where
237+
mul_one := comp_id
238+
one_mul := id_comp
239+
mul_assoc _ _ _ := comp_assoc _ _ _
240+
npow n f := (npowRec n f).copy f^[n] <| by induction n <;> simp [npowRec, *]
241+
npow_succ _ _ := DFunLike.coe_injective <| Function.iterate_succ _ _
242+
243+
@[simp, norm_cast] lemma coe_pow (f : π’œ β†’+*ᡍ π’œ) (n : β„•) : ⇑(f ^ n) = f^[n] := rfl
244+
245+
@[simp]
246+
theorem cancel_right {g₁ gβ‚‚ : ℬ β†’+*ᡍ π’ž} {f : π’œ β†’+*ᡍ ℬ} (hf : Function.Surjective f) :
247+
g₁.comp f = gβ‚‚.comp f ↔ g₁ = gβ‚‚ :=
248+
⟨fun h => ext <| hf.forall.2 (GradedRingHom.ext_iff.1 h), fun h => h β–Έ rfl⟩
249+
250+
@[simp]
251+
theorem cancel_left {g : ℬ β†’+*ᡍ π’ž} {f₁ fβ‚‚ : π’œ β†’+*ᡍ ℬ} (hg : Function.Injective g) :
252+
g.comp f₁ = g.comp fβ‚‚ ↔ f₁ = fβ‚‚ :=
253+
⟨fun h => ext fun x => hg <| by rw [← comp_apply, h, comp_apply], fun h => h β–Έ rfl⟩
254+
255+
-- Note: if `GradedAddHom` is added later, then the assumptions can be relaxed.
256+
/-- A graded ring homomorphism descends to an additive homomorphism on each indexed component. -/
257+
@[simps!] def gradedAddHom [AddSubmonoidClass Οƒ A] [AddSubmonoidClass Ο„ B]
258+
(f : π’œ β†’+*ᡍ ℬ) (i : ΞΉ) : π’œ i β†’+ ℬ i where
259+
toFun x := ⟨f x, map_mem f x.2⟩
260+
map_zero' := by ext; simp
261+
map_add' x y := by ext; simp
262+
263+
/-- A graded ring homomorphism descends to a ring homomorphism on the zeroth component. -/
264+
@[simps!] def gradedZeroRingHom [AddSubmonoidClass Οƒ A] [AddSubmonoidClass Ο„ B] [AddMonoid ΞΉ]
265+
[SetLike.GradedMonoid π’œ] [SetLike.GradedMonoid ℬ] (f : π’œ β†’+*ᡍ ℬ) : π’œ 0 β†’+* ℬ 0 where
266+
__ := f.gradedAddHom 0
267+
map_one' := Subtype.ext <| map_one _
268+
map_mul' _ _ := Subtype.ext <| map_mul ..
269+
270+
end GradedRingHom
271+
272+
end SetLike
273+
274+
section GradedRing
275+
variable [DecidableEq ΞΉ] [AddMonoid ΞΉ] [AddSubmonoidClass Οƒ A] [AddSubmonoidClass Ο„ B]
276+
variable (π’œ : ΞΉ β†’ Οƒ) (ℬ : ΞΉ β†’ Ο„) [GradedRing π’œ] [GradedRing ℬ]
277+
variable {F : Type*} [FunLike F A B] [GradedFunLike F π’œ ℬ] [RingHomClass F A B]
278+
279+
-- not simp because `π’œ` cannot be inferred
280+
lemma DirectSum.decompose_map (f : F) {x : A} :
281+
DirectSum.decompose ℬ (f x) =
282+
.map (GradedRingHom.gradedAddHom <| .ofClass f) (.decompose π’œ x) := by
283+
classical
284+
rw [← DirectSum.sum_support_decompose π’œ x, map_sum, DirectSum.decompose_sum,
285+
DirectSum.decompose_sum, map_sum]
286+
congr 1
287+
simp [DirectSum.decompose_of_mem _ (map_mem f (Subtype.prop _)),
288+
DirectSum.decompose_of_mem _ (Subtype.prop _), DirectSum.map_of, GradedRingHom.gradedAddHom]
289+
290+
-- not simp because `ℬ` cannot be inferred
291+
-- for every concrete instance of GradedFunLike, we need one simp lemma
292+
lemma map_directSumDecompose (f : F) {x : A} {i : ΞΉ} :
293+
f (DirectSum.decompose π’œ x i) = DirectSum.decompose ℬ (f x) i := by
294+
simp [DirectSum.decompose_map π’œ]
295+
296+
@[simp] lemma GradedRingHom.map_directSumDecompose (f : π’œ β†’+*ᡍ ℬ) {x : A} {i : ΞΉ} :
297+
f (DirectSum.decompose π’œ x i) = DirectSum.decompose ℬ (f x) i :=
298+
_root_.map_directSumDecompose ..
299+
300+
end GradedRing

0 commit comments

Comments
Β (0)