Skip to content

Commit 22765e8

Browse files
kckennylaukckennylau
committed
chore: move SModEq to a new folder (#30990)
Split off from #30989. I only move it to a new folder and do nothing else.
1 parent f4acd3b commit 22765e8

File tree

5 files changed

+160
-156
lines changed

5 files changed

+160
-156
lines changed

‎Mathlib.lean‎

Lines changed: 1 addition & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -4499,6 +4499,7 @@ import Mathlib.LinearAlgebra.RootSystem.RootPairingCat
44994499
import Mathlib.LinearAlgebra.RootSystem.RootPositive
45004500
import Mathlib.LinearAlgebra.RootSystem.WeylGroup
45014501
import Mathlib.LinearAlgebra.SModEq
4502+
import Mathlib.LinearAlgebra.SModEq.Basic
45024503
import Mathlib.LinearAlgebra.Semisimple
45034504
import Mathlib.LinearAlgebra.SesquilinearForm
45044505
import Mathlib.LinearAlgebra.SesquilinearForm.Basic

‎Mathlib/LinearAlgebra/SModEq.lean‎

Lines changed: 2 additions & 154 deletions
Original file line numberDiff line numberDiff line change
@@ -1,155 +1,3 @@
1-
/-
2-
Copyright (c) 2020 Kenny Lau. All rights reserved.
3-
Released under Apache 2.0 license as described in the file LICENSE.
4-
Authors: Kenny Lau
5-
-/
6-
import Mathlib.Algebra.Module.Submodule.Map
7-
import Mathlib.Algebra.Polynomial.Eval.Defs
8-
import Mathlib.RingTheory.Ideal.Quotient.Defs
1+
import Mathlib.LinearAlgebra.SModEq.Basic
92

10-
/-!
11-
# modular equivalence for submodule
12-
-/
13-
14-
15-
open Submodule
16-
17-
open Polynomial
18-
19-
variable {R : Type*} [Ring R]
20-
variable {A : Type*} [CommRing A]
21-
variable {M : Type*} [AddCommGroup M] [Module R M] (U U₁ U₂ : Submodule R M)
22-
variable {x x₁ x₂ y y₁ y₂ z z₁ z₂ : M}
23-
variable {N : Type*} [AddCommGroup N] [Module R N] (V V₁ V₂ : Submodule R N)
24-
25-
/-- A predicate saying two elements of a module are equivalent modulo a submodule. -/
26-
def SModEq (x y : M) : Prop :=
27-
(Submodule.Quotient.mk x : M ⧸ U) = Submodule.Quotient.mk y
28-
29-
@[inherit_doc] notation:50 x " ≡ " y " [SMOD " N "]" => SModEq N x y
30-
31-
variable {U U₁ U₂}
32-
33-
protected theorem SModEq.def :
34-
x ≡ y [SMOD U] ↔ (Submodule.Quotient.mk x : M ⧸ U) = Submodule.Quotient.mk y :=
35-
Iff.rfl
36-
37-
namespace SModEq
38-
39-
theorem sub_mem : x ≡ y [SMOD U] ↔ x - y ∈ U := by rw [SModEq.def, Submodule.Quotient.eq]
40-
41-
@[simp]
42-
theorem top : x ≡ y [SMOD (⊤ : Submodule R M)] :=
43-
(Submodule.Quotient.eq ⊤).2 mem_top
44-
45-
@[simp]
46-
theorem bot : x ≡ y [SMOD (⊥ : Submodule R M)] ↔ x = y := by
47-
rw [SModEq.def, Submodule.Quotient.eq, mem_bot, sub_eq_zero]
48-
49-
@[mono]
50-
theorem mono (HU : U₁ ≤ U₂) (hxy : x ≡ y [SMOD U₁]) : x ≡ y [SMOD U₂] :=
51-
(Submodule.Quotient.eq U₂).2 <| HU <| (Submodule.Quotient.eq U₁).1 hxy
52-
53-
@[refl]
54-
protected theorem refl (x : M) : x ≡ x [SMOD U] :=
55-
@rfl _ _
56-
57-
protected theorem rfl : x ≡ x [SMOD U] :=
58-
SModEq.refl _
59-
60-
instance : IsRefl _ (SModEq U) :=
61-
⟨SModEq.refl⟩
62-
63-
@[symm]
64-
nonrec theorem symm (hxy : x ≡ y [SMOD U]) : y ≡ x [SMOD U] :=
65-
hxy.symm
66-
67-
theorem comm : x ≡ y [SMOD U] ↔ y ≡ x [SMOD U] := ⟨symm, symm⟩
68-
69-
@[trans]
70-
nonrec theorem trans (hxy : x ≡ y [SMOD U]) (hyz : y ≡ z [SMOD U]) : x ≡ z [SMOD U] :=
71-
hxy.trans hyz
72-
73-
instance instTrans : Trans (SModEq U) (SModEq U) (SModEq U) where
74-
trans := trans
75-
76-
@[gcongr]
77-
theorem add (hxy₁ : x₁ ≡ y₁ [SMOD U]) (hxy₂ : x₂ ≡ y₂ [SMOD U]) : x₁ + x₂ ≡ y₁ + y₂ [SMOD U] := by
78-
rw [SModEq.def] at hxy₁ hxy₂ ⊢
79-
simp_rw [Quotient.mk_add, hxy₁, hxy₂]
80-
81-
@[gcongr]
82-
theorem sum {ι} {s : Finset ι} {x y : ι → M}
83-
(hxy : ∀ i ∈ s, x i ≡ y i [SMOD U]) : ∑ i ∈ s, x i ≡ ∑ i ∈ s, y i [SMOD U] := by
84-
classical
85-
induction s using Finset.cons_induction with
86-
| empty => simp [SModEq.rfl]
87-
| cons i s _ ih =>
88-
grw [Finset.sum_cons, Finset.sum_cons, hxy i (Finset.mem_cons_self i s),
89-
ih (fun j hj ↦ hxy j (Finset.mem_cons_of_mem hj))]
90-
91-
@[gcongr]
92-
theorem smul (hxy : x ≡ y [SMOD U]) (c : R) : c • x ≡ c • y [SMOD U] := by
93-
rw [SModEq.def] at hxy ⊢
94-
simp_rw [Quotient.mk_smul, hxy]
95-
96-
@[gcongr]
97-
lemma nsmul (hxy : x ≡ y [SMOD U]) (n : ℕ) : n • x ≡ n • y [SMOD U] := by
98-
rw [SModEq.def] at hxy ⊢
99-
simp_rw [Quotient.mk_smul, hxy]
100-
101-
@[gcongr]
102-
lemma zsmul (hxy : x ≡ y [SMOD U]) (n : ℤ) : n • x ≡ n • y [SMOD U] := by
103-
rw [SModEq.def] at hxy ⊢
104-
simp_rw [Quotient.mk_smul, hxy]
105-
106-
@[gcongr]
107-
theorem mul {I : Ideal A} {x₁ x₂ y₁ y₂ : A} (hxy₁ : x₁ ≡ y₁ [SMOD I])
108-
(hxy₂ : x₂ ≡ y₂ [SMOD I]) : x₁ * x₂ ≡ y₁ * y₂ [SMOD I] := by
109-
simp only [SModEq.def, Ideal.Quotient.mk_eq_mk, map_mul] at hxy₁ hxy₂ ⊢
110-
rw [hxy₁, hxy₂]
111-
112-
@[gcongr]
113-
theorem prod {I : Ideal A} {ι} {s : Finset ι} {x y : ι → A}
114-
(hxy : ∀ i ∈ s, x i ≡ y i [SMOD I]) : ∏ i ∈ s, x i ≡ ∏ i ∈ s, y i [SMOD I] := by
115-
classical
116-
induction s using Finset.cons_induction with
117-
| empty => simp [SModEq.rfl]
118-
| cons i s _ ih =>
119-
grw [Finset.prod_cons, Finset.prod_cons, hxy i (Finset.mem_cons_self i s),
120-
ih (fun j hj ↦ hxy j (Finset.mem_cons_of_mem hj))]
121-
122-
@[gcongr]
123-
lemma pow {I : Ideal A} {x y : A} (n : ℕ) (hxy : x ≡ y [SMOD I]) :
124-
x ^ n ≡ y ^ n [SMOD I] := by
125-
simp only [SModEq.def, Ideal.Quotient.mk_eq_mk, map_pow] at hxy ⊢
126-
rw [hxy]
127-
128-
@[gcongr]
129-
lemma neg (hxy : x ≡ y [SMOD U]) : - x ≡ - y [SMOD U] := by
130-
simpa only [SModEq.def, Quotient.mk_neg, neg_inj]
131-
132-
@[gcongr]
133-
lemma sub (hxy₁ : x₁ ≡ y₁ [SMOD U]) (hxy₂ : x₂ ≡ y₂ [SMOD U]) : x₁ - x₂ ≡ y₁ - y₂ [SMOD U] := by
134-
rw [SModEq.def] at hxy₁ hxy₂ ⊢
135-
simp_rw [Quotient.mk_sub, hxy₁, hxy₂]
136-
137-
theorem zero : x ≡ 0 [SMOD U] ↔ x ∈ U := by rw [SModEq.def, Submodule.Quotient.eq, sub_zero]
138-
139-
theorem _root_.sub_smodEq_zero : x - y ≡ 0 [SMOD U] ↔ x ≡ y [SMOD U] := by
140-
simp only [SModEq.sub_mem, sub_zero]
141-
142-
theorem map (hxy : x ≡ y [SMOD U]) (f : M →ₗ[R] N) : f x ≡ f y [SMOD U.map f] :=
143-
(Submodule.Quotient.eq _).2 <| f.map_sub x y ▸ mem_map_of_mem <| (Submodule.Quotient.eq _).1 hxy
144-
145-
theorem comap {f : M →ₗ[R] N} (hxy : f x ≡ f y [SMOD V]) : x ≡ y [SMOD V.comap f] :=
146-
(Submodule.Quotient.eq _).2 <|
147-
show f (x - y) ∈ V from (f.map_sub x y).symm ▸ (Submodule.Quotient.eq _).1 hxy
148-
149-
@[gcongr]
150-
theorem eval {R : Type*} [CommRing R] {I : Ideal R} {x y : R} (h : x ≡ y [SMOD I]) (f : R[X]) :
151-
f.eval x ≡ f.eval y [SMOD I] := by
152-
simp_rw [Polynomial.eval_eq_sum, Polynomial.sum]
153-
gcongr
154-
155-
end SModEq
3+
deprecated_module (since := "2025-10-28")

‎Mathlib/LinearAlgebra/SModEq/Basic.lean‎

Lines changed: 155 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,155 @@
1+
/-
2+
Copyright (c) 2020 Kenny Lau. All rights reserved.
3+
Released under Apache 2.0 license as described in the file LICENSE.
4+
Authors: Kenny Lau
5+
-/
6+
import Mathlib.Algebra.Module.Submodule.Map
7+
import Mathlib.Algebra.Polynomial.Eval.Defs
8+
import Mathlib.RingTheory.Ideal.Quotient.Defs
9+
10+
/-!
11+
# modular equivalence for submodule
12+
-/
13+
14+
15+
open Submodule
16+
17+
open Polynomial
18+
19+
variable {R : Type*} [Ring R]
20+
variable {A : Type*} [CommRing A]
21+
variable {M : Type*} [AddCommGroup M] [Module R M] (U U₁ U₂ : Submodule R M)
22+
variable {x x₁ x₂ y y₁ y₂ z z₁ z₂ : M}
23+
variable {N : Type*} [AddCommGroup N] [Module R N] (V V₁ V₂ : Submodule R N)
24+
25+
/-- A predicate saying two elements of a module are equivalent modulo a submodule. -/
26+
def SModEq (x y : M) : Prop :=
27+
(Submodule.Quotient.mk x : M ⧸ U) = Submodule.Quotient.mk y
28+
29+
@[inherit_doc] notation:50 x " ≡ " y " [SMOD " N "]" => SModEq N x y
30+
31+
variable {U U₁ U₂}
32+
33+
protected theorem SModEq.def :
34+
x ≡ y [SMOD U] ↔ (Submodule.Quotient.mk x : M ⧸ U) = Submodule.Quotient.mk y :=
35+
Iff.rfl
36+
37+
namespace SModEq
38+
39+
theorem sub_mem : x ≡ y [SMOD U] ↔ x - y ∈ U := by rw [SModEq.def, Submodule.Quotient.eq]
40+
41+
@[simp]
42+
theorem top : x ≡ y [SMOD (⊤ : Submodule R M)] :=
43+
(Submodule.Quotient.eq ⊤).2 mem_top
44+
45+
@[simp]
46+
theorem bot : x ≡ y [SMOD (⊥ : Submodule R M)] ↔ x = y := by
47+
rw [SModEq.def, Submodule.Quotient.eq, mem_bot, sub_eq_zero]
48+
49+
@[mono]
50+
theorem mono (HU : U₁ ≤ U₂) (hxy : x ≡ y [SMOD U₁]) : x ≡ y [SMOD U₂] :=
51+
(Submodule.Quotient.eq U₂).2 <| HU <| (Submodule.Quotient.eq U₁).1 hxy
52+
53+
@[refl]
54+
protected theorem refl (x : M) : x ≡ x [SMOD U] :=
55+
@rfl _ _
56+
57+
protected theorem rfl : x ≡ x [SMOD U] :=
58+
SModEq.refl _
59+
60+
instance : IsRefl _ (SModEq U) :=
61+
⟨SModEq.refl⟩
62+
63+
@[symm]
64+
nonrec theorem symm (hxy : x ≡ y [SMOD U]) : y ≡ x [SMOD U] :=
65+
hxy.symm
66+
67+
theorem comm : x ≡ y [SMOD U] ↔ y ≡ x [SMOD U] := ⟨symm, symm⟩
68+
69+
@[trans]
70+
nonrec theorem trans (hxy : x ≡ y [SMOD U]) (hyz : y ≡ z [SMOD U]) : x ≡ z [SMOD U] :=
71+
hxy.trans hyz
72+
73+
instance instTrans : Trans (SModEq U) (SModEq U) (SModEq U) where
74+
trans := trans
75+
76+
@[gcongr]
77+
theorem add (hxy₁ : x₁ ≡ y₁ [SMOD U]) (hxy₂ : x₂ ≡ y₂ [SMOD U]) : x₁ + x₂ ≡ y₁ + y₂ [SMOD U] := by
78+
rw [SModEq.def] at hxy₁ hxy₂ ⊢
79+
simp_rw [Quotient.mk_add, hxy₁, hxy₂]
80+
81+
@[gcongr]
82+
theorem sum {ι} {s : Finset ι} {x y : ι → M}
83+
(hxy : ∀ i ∈ s, x i ≡ y i [SMOD U]) : ∑ i ∈ s, x i ≡ ∑ i ∈ s, y i [SMOD U] := by
84+
classical
85+
induction s using Finset.cons_induction with
86+
| empty => simp [SModEq.rfl]
87+
| cons i s _ ih =>
88+
grw [Finset.sum_cons, Finset.sum_cons, hxy i (Finset.mem_cons_self i s),
89+
ih (fun j hj ↦ hxy j (Finset.mem_cons_of_mem hj))]
90+
91+
@[gcongr]
92+
theorem smul (hxy : x ≡ y [SMOD U]) (c : R) : c • x ≡ c • y [SMOD U] := by
93+
rw [SModEq.def] at hxy ⊢
94+
simp_rw [Quotient.mk_smul, hxy]
95+
96+
@[gcongr]
97+
lemma nsmul (hxy : x ≡ y [SMOD U]) (n : ℕ) : n • x ≡ n • y [SMOD U] := by
98+
rw [SModEq.def] at hxy ⊢
99+
simp_rw [Quotient.mk_smul, hxy]
100+
101+
@[gcongr]
102+
lemma zsmul (hxy : x ≡ y [SMOD U]) (n : ℤ) : n • x ≡ n • y [SMOD U] := by
103+
rw [SModEq.def] at hxy ⊢
104+
simp_rw [Quotient.mk_smul, hxy]
105+
106+
@[gcongr]
107+
theorem mul {I : Ideal A} {x₁ x₂ y₁ y₂ : A} (hxy₁ : x₁ ≡ y₁ [SMOD I])
108+
(hxy₂ : x₂ ≡ y₂ [SMOD I]) : x₁ * x₂ ≡ y₁ * y₂ [SMOD I] := by
109+
simp only [SModEq.def, Ideal.Quotient.mk_eq_mk, map_mul] at hxy₁ hxy₂ ⊢
110+
rw [hxy₁, hxy₂]
111+
112+
@[gcongr]
113+
theorem prod {I : Ideal A} {ι} {s : Finset ι} {x y : ι → A}
114+
(hxy : ∀ i ∈ s, x i ≡ y i [SMOD I]) : ∏ i ∈ s, x i ≡ ∏ i ∈ s, y i [SMOD I] := by
115+
classical
116+
induction s using Finset.cons_induction with
117+
| empty => simp [SModEq.rfl]
118+
| cons i s _ ih =>
119+
grw [Finset.prod_cons, Finset.prod_cons, hxy i (Finset.mem_cons_self i s),
120+
ih (fun j hj ↦ hxy j (Finset.mem_cons_of_mem hj))]
121+
122+
@[gcongr]
123+
lemma pow {I : Ideal A} {x y : A} (n : ℕ) (hxy : x ≡ y [SMOD I]) :
124+
x ^ n ≡ y ^ n [SMOD I] := by
125+
simp only [SModEq.def, Ideal.Quotient.mk_eq_mk, map_pow] at hxy ⊢
126+
rw [hxy]
127+
128+
@[gcongr]
129+
lemma neg (hxy : x ≡ y [SMOD U]) : - x ≡ - y [SMOD U] := by
130+
simpa only [SModEq.def, Quotient.mk_neg, neg_inj]
131+
132+
@[gcongr]
133+
lemma sub (hxy₁ : x₁ ≡ y₁ [SMOD U]) (hxy₂ : x₂ ≡ y₂ [SMOD U]) : x₁ - x₂ ≡ y₁ - y₂ [SMOD U] := by
134+
rw [SModEq.def] at hxy₁ hxy₂ ⊢
135+
simp_rw [Quotient.mk_sub, hxy₁, hxy₂]
136+
137+
theorem zero : x ≡ 0 [SMOD U] ↔ x ∈ U := by rw [SModEq.def, Submodule.Quotient.eq, sub_zero]
138+
139+
theorem _root_.sub_smodEq_zero : x - y ≡ 0 [SMOD U] ↔ x ≡ y [SMOD U] := by
140+
simp only [SModEq.sub_mem, sub_zero]
141+
142+
theorem map (hxy : x ≡ y [SMOD U]) (f : M →ₗ[R] N) : f x ≡ f y [SMOD U.map f] :=
143+
(Submodule.Quotient.eq _).2 <| f.map_sub x y ▸ mem_map_of_mem <| (Submodule.Quotient.eq _).1 hxy
144+
145+
theorem comap {f : M →ₗ[R] N} (hxy : f x ≡ f y [SMOD V]) : x ≡ y [SMOD V.comap f] :=
146+
(Submodule.Quotient.eq _).2 <|
147+
show f (x - y) ∈ V from (f.map_sub x y).symm ▸ (Submodule.Quotient.eq _).1 hxy
148+
149+
@[gcongr]
150+
theorem eval {R : Type*} [CommRing R] {I : Ideal R} {x y : R} (h : x ≡ y [SMOD I]) (f : R[X]) :
151+
f.eval x ≡ f.eval y [SMOD I] := by
152+
simp_rw [Polynomial.eval_eq_sum, Polynomial.sum]
153+
gcongr
154+
155+
end SModEq

‎Mathlib/RingTheory/AdicCompletion/Basic.lean‎

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -4,7 +4,7 @@ Released under Apache 2.0 license as described in the file LICENSE.
44
Authors: Kenny Lau, Judith Ludwig, Christian Merten
55
-/
66
import Mathlib.Algebra.Ring.GeomSum
7-
import Mathlib.LinearAlgebra.SModEq
7+
import Mathlib.LinearAlgebra.SModEq.Basic
88
import Mathlib.RingTheory.Jacobson.Ideal
99
import Mathlib.RingTheory.Ideal.Quotient.PowTransition
1010

‎Mathlib/RingTheory/PowerBasis.lean‎

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -4,7 +4,7 @@ Released under Apache 2.0 license as described in the file LICENSE.
44
Authors: Anne Baanen
55
-/
66
import Mathlib.FieldTheory.Minpoly.Field
7-
import Mathlib.LinearAlgebra.SModEq
7+
import Mathlib.LinearAlgebra.SModEq.Basic
88
import Mathlib.RingTheory.Ideal.BigOperators
99

1010
/-!

0 commit comments

Comments
 (0)