-
Notifications
You must be signed in to change notification settings - Fork 307
/
Support.lean
150 lines (116 loc) · 6.64 KB
/
Support.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
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
104
105
106
107
108
109
110
111
112
113
114
115
116
117
118
119
120
121
122
123
124
125
126
127
128
129
130
131
132
133
134
135
136
137
138
139
140
141
142
143
144
145
146
147
148
149
150
/-
Copyright (c) 2022 Damiano Testa. All rights reserved.
Released under Apache 2.0 license as described in the file LICENSE.
Authors: Damiano Testa
-/
import Mathlib.Algebra.MonoidAlgebra.Basic
import Mathlib.Data.Finset.Pointwise
#align_import algebra.monoid_algebra.support from "leanprover-community/mathlib"@"16749fc4661828cba18cd0f4e3c5eb66a8e80598"
/-!
# Lemmas about the support of a finitely supported function
-/
open scoped Pointwise
universe u₁ u₂ u₃
namespace MonoidAlgebra
open Finset Finsupp
variable {k : Type u₁} {G : Type u₂} [Semiring k]
theorem support_mul [Mul G] [DecidableEq G] (a b : MonoidAlgebra k G) :
(a * b).support ⊆ a.support * b.support :=
support_sum.trans <| biUnion_subset.2 fun _x hx ↦
support_sum.trans <| biUnion_subset.2 fun _y hy ↦
support_single_subset.trans <| singleton_subset_iff.2 <| mem_image₂_of_mem hx hy
#align monoid_algebra.support_mul MonoidAlgebra.support_mul
theorem support_single_mul_subset [DecidableEq G] [Mul G] (f : MonoidAlgebra k G) (r : k) (a : G) :
(single a r * f : MonoidAlgebra k G).support ⊆ Finset.image (a * ·) f.support :=
(support_mul _ _).trans <| (Finset.image₂_subset_right support_single_subset).trans <| by
rw [Finset.image₂_singleton_left]
#align monoid_algebra.support_single_mul_subset MonoidAlgebra.support_single_mul_subset
theorem support_mul_single_subset [DecidableEq G] [Mul G] (f : MonoidAlgebra k G) (r : k) (a : G) :
(f * single a r).support ⊆ Finset.image (· * a) f.support :=
(support_mul _ _).trans <| (Finset.image₂_subset_left support_single_subset).trans <| by
rw [Finset.image₂_singleton_right]
#align monoid_algebra.support_mul_single_subset MonoidAlgebra.support_mul_single_subset
theorem support_single_mul_eq_image [DecidableEq G] [Mul G] (f : MonoidAlgebra k G) {r : k}
(hr : ∀ y, r * y = 0 ↔ y = 0) {x : G} (lx : IsLeftRegular x) :
(single x r * f : MonoidAlgebra k G).support = Finset.image (x * ·) f.support := by
refine' subset_antisymm (support_single_mul_subset f _ _) fun y hy => _
obtain ⟨y, yf, rfl⟩ : ∃ a : G, a ∈ f.support ∧ x * a = y := by
simpa only [Finset.mem_image, exists_prop] using hy
simp only [mul_apply, mem_support_iff.mp yf, hr, mem_support_iff, sum_single_index,
Finsupp.sum_ite_eq', Ne.def, not_false_iff, if_true, zero_mul, ite_self, sum_zero, lx.eq_iff]
#align monoid_algebra.support_single_mul_eq_image MonoidAlgebra.support_single_mul_eq_image
theorem support_mul_single_eq_image [DecidableEq G] [Mul G] (f : MonoidAlgebra k G) {r : k}
(hr : ∀ y, y * r = 0 ↔ y = 0) {x : G} (rx : IsRightRegular x) :
(f * single x r).support = Finset.image (· * x) f.support := by
refine' subset_antisymm (support_mul_single_subset f _ _) fun y hy => _
obtain ⟨y, yf, rfl⟩ : ∃ a : G, a ∈ f.support ∧ a * x = y := by
simpa only [Finset.mem_image, exists_prop] using hy
simp only [mul_apply, mem_support_iff.mp yf, hr, mem_support_iff, sum_single_index,
Finsupp.sum_ite_eq', Ne.def, not_false_iff, if_true, mul_zero, ite_self, sum_zero, rx.eq_iff]
#align monoid_algebra.support_mul_single_eq_image MonoidAlgebra.support_mul_single_eq_image
theorem support_mul_single [Mul G] [IsRightCancelMul G] (f : MonoidAlgebra k G) (r : k)
(hr : ∀ y, y * r = 0 ↔ y = 0) (x : G) :
(f * single x r).support = f.support.map (mulRightEmbedding x) := by
classical
ext
simp only [support_mul_single_eq_image f hr (IsRightRegular.all x),
mem_image, mem_map, mulRightEmbedding_apply]
#align monoid_algebra.support_mul_single MonoidAlgebra.support_mul_single
theorem support_single_mul [Mul G] [IsLeftCancelMul G] (f : MonoidAlgebra k G) (r : k)
(hr : ∀ y, r * y = 0 ↔ y = 0) (x : G) :
(single x r * f : MonoidAlgebra k G).support = f.support.map (mulLeftEmbedding x) := by
classical
ext
simp only [support_single_mul_eq_image f hr (IsLeftRegular.all x), mem_image,
mem_map, mulLeftEmbedding_apply]
#align monoid_algebra.support_single_mul MonoidAlgebra.support_single_mul
lemma support_one_subset [One G] : (1 : MonoidAlgebra k G).support ⊆ 1 :=
Finsupp.support_single_subset
@[simp]
lemma support_one [One G] [NeZero (1 : k)] : (1 : MonoidAlgebra k G).support = 1 :=
Finsupp.support_single_ne_zero _ one_ne_zero
section Span
variable [MulOneClass G]
/-- An element of `MonoidAlgebra k G` is in the subalgebra generated by its support. -/
theorem mem_span_support (f : MonoidAlgebra k G) :
f ∈ Submodule.span k (of k G '' (f.support : Set G)) := by
erw [of, MonoidHom.coe_mk, ← supported_eq_span_single, Finsupp.mem_supported]
#align monoid_algebra.mem_span_support MonoidAlgebra.mem_span_support
end Span
end MonoidAlgebra
namespace AddMonoidAlgebra
open Finset Finsupp MulOpposite
variable {k : Type u₁} {G : Type u₂} [Semiring k]
theorem support_mul [DecidableEq G] [Add G] (a b : k[G]) :
(a * b).support ⊆ a.support + b.support :=
@MonoidAlgebra.support_mul k (Multiplicative G) _ _ _ _ _
#align add_monoid_algebra.support_mul AddMonoidAlgebra.support_mul
theorem support_mul_single [Add G] [IsRightCancelAdd G] (f : k[G]) (r : k)
(hr : ∀ y, y * r = 0 ↔ y = 0) (x : G) :
(f * single x r : k[G]).support = f.support.map (addRightEmbedding x) :=
MonoidAlgebra.support_mul_single (G := Multiplicative G) _ _ hr _
#align add_monoid_algebra.support_mul_single AddMonoidAlgebra.support_mul_single
theorem support_single_mul [Add G] [IsLeftCancelAdd G] (f : k[G]) (r : k)
(hr : ∀ y, r * y = 0 ↔ y = 0) (x : G) :
(single x r * f : k[G]).support = f.support.map (addLeftEmbedding x) :=
MonoidAlgebra.support_single_mul (G := Multiplicative G) _ _ hr _
#align add_monoid_algebra.support_single_mul AddMonoidAlgebra.support_single_mul
lemma support_one_subset [Zero G] : (1 : k[G]).support ⊆ 0 := Finsupp.support_single_subset
@[simp]
lemma support_one [Zero G] [NeZero (1 : k)] : (1 : k[G]).support = 0 :=
Finsupp.support_single_ne_zero _ one_ne_zero
section Span
/-- An element of `k[G]` is in the submodule generated by its support. -/
theorem mem_span_support [AddZeroClass G] (f : k[G]) :
f ∈ Submodule.span k (of k G '' (f.support : Set G)) := by
erw [of, MonoidHom.coe_mk, ← Finsupp.supported_eq_span_single, Finsupp.mem_supported]
#align add_monoid_algebra.mem_span_support AddMonoidAlgebra.mem_span_support
/-- An element of `k[G]` is in the subalgebra generated by its support, using
unbundled inclusion. -/
theorem mem_span_support' (f : k[G]) :
f ∈ Submodule.span k (of' k G '' (f.support : Set G)) := by
delta of'
rw [← Finsupp.supported_eq_span_single, Finsupp.mem_supported]
#align add_monoid_algebra.mem_span_support' AddMonoidAlgebra.mem_span_support'
end Span
end AddMonoidAlgebra