/
smodeq.lean
65 lines (44 loc) · 2.36 KB
/
smodeq.lean
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
/-
Copyright (c) 2020 Kenny Lau. All rights reserved.
Released under Apache 2.0 license as described in the file LICENSE.
Authors: Kenny Lau
-/
import linear_algebra.basic
/-!
# modular equivalence for submodule
-/
open submodule
variables {R : Type*} [ring R]
variables {M : Type*} [add_comm_group M] [module R M] (U U₁ U₂ : submodule R M)
variables {x x₁ x₂ y y₁ y₂ z z₁ z₂ : M}
variables {N : Type*} [add_comm_group N] [module R N] (V V₁ V₂ : submodule R N)
/-- A predicate saying two elements of a module are equivalent modulo a submodule. -/
def smodeq (x y : M) : Prop :=
(submodule.quotient.mk x : U.quotient) = submodule.quotient.mk y
notation x ` ≡ `:50 y ` [SMOD `:50 N `]`:0 := smodeq N x y
variables {U U₁ U₂}
protected lemma smodeq.def : x ≡ y [SMOD U] ↔
(submodule.quotient.mk x : U.quotient) = submodule.quotient.mk y := iff.rfl
namespace smodeq
@[simp] theorem top : x ≡ y [SMOD (⊤ : submodule R M)] :=
(submodule.quotient.eq ⊤).2 mem_top
@[simp] theorem bot : x ≡ y [SMOD (⊥ : submodule R M)] ↔ x = y :=
by rw [smodeq.def, submodule.quotient.eq, mem_bot, sub_eq_zero]
@[mono] theorem mono (HU : U₁ ≤ U₂) (hxy : x ≡ y [SMOD U₁]) : x ≡ y [SMOD U₂] :=
(submodule.quotient.eq U₂).2 $ HU $ (submodule.quotient.eq U₁).1 hxy
@[refl] theorem refl : x ≡ x [SMOD U] := eq.refl _
@[symm] theorem symm (hxy : x ≡ y [SMOD U]) : y ≡ x [SMOD U] := hxy.symm
@[trans] theorem trans (hxy : x ≡ y [SMOD U]) (hyz : y ≡ z [SMOD U]) : x ≡ z [SMOD U] :=
hxy.trans hyz
theorem add (hxy₁ : x₁ ≡ y₁ [SMOD U]) (hxy₂ : x₂ ≡ y₂ [SMOD U]) : x₁ + x₂ ≡ y₁ + y₂ [SMOD U] :=
by { rw smodeq.def at hxy₁ hxy₂ ⊢, simp_rw [quotient.mk_add, hxy₁, hxy₂] }
theorem smul (hxy : x ≡ y [SMOD U]) (c : R) : c • x ≡ c • y [SMOD U] :=
by { rw smodeq.def at hxy ⊢, simp_rw [quotient.mk_smul, hxy] }
theorem zero : x ≡ 0 [SMOD U] ↔ x ∈ U :=
by rw [smodeq.def, submodule.quotient.eq, sub_zero]
theorem map (hxy : x ≡ y [SMOD U]) (f : M →ₗ[R] N) : f x ≡ f y [SMOD U.map f] :=
(submodule.quotient.eq _).2 $ f.map_sub x y ▸ mem_map_of_mem $ (submodule.quotient.eq _).1 hxy
theorem comap {f : M →ₗ[R] N} (hxy : f x ≡ f y [SMOD V]) : x ≡ y [SMOD V.comap f] :=
(submodule.quotient.eq _).2 $ show f (x - y) ∈ V,
from (f.map_sub x y).symm ▸ (submodule.quotient.eq _).1 hxy
end smodeq