Skip to content

Commit 31cff6e

Browse files
EgbertRijkeEgbertRijke
committed
Merge branch 'master' of github.com:UniMath/agda-unimath into jhu-seminar
2 parents bd9e529 + 095a6f6 commit 31cff6e

5 files changed

+787
-0
lines changed

‎src/group-theory.lagda.md

Lines changed: 3 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -116,6 +116,9 @@ open import group-theory.large-semigroups public
116116
open import group-theory.loop-groups-sets public
117117
open import group-theory.mere-equivalences-concrete-group-actions public
118118
open import group-theory.mere-equivalences-group-actions public
119+
open import group-theory.minkowski-multiplication-commutative-monoids public
120+
open import group-theory.minkowski-multiplication-monoids public
121+
open import group-theory.minkowski-multiplication-semigroups public
119122
open import group-theory.monoid-actions public
120123
open import group-theory.monoids public
121124
open import group-theory.monomorphisms-concrete-groups public

‎src/group-theory/minkowski-multiplication-commutative-monoids.lagda.md

Lines changed: 290 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,290 @@
1+
# Minkowski multiplication of subsets of a commutative monoid
2+
3+
```agda
4+
module group-theory.minkowski-multiplication-commutative-monoids where
5+
```
6+
7+
<details><summary>Imports</summary>
8+
9+
```agda
10+
open import foundation.cartesian-product-types
11+
open import foundation.dependent-pair-types
12+
open import foundation.existential-quantification
13+
open import foundation.identity-types
14+
open import foundation.inhabited-subtypes
15+
open import foundation.powersets
16+
open import foundation.subtypes
17+
open import foundation.unital-binary-operations
18+
open import foundation.universe-levels
19+
20+
open import group-theory.commutative-monoids
21+
open import group-theory.minkowski-multiplication-monoids
22+
open import group-theory.monoids
23+
open import group-theory.subsets-commutative-monoids
24+
25+
open import logic.functoriality-existential-quantification
26+
```
27+
28+
</details>
29+
30+
## Idea
31+
32+
Given two [subsets](group-theory.subsets-commutative-monoids.md) `A` and `B` of
33+
a [commutative monoid](group-theory.commutative-monoids.md) `M`, the
34+
{{#concept "Minkowski multiplication" Disambiguation="on subsets of a commutative monoid" WD="Minkowski addition" WDID=Q1322294 Agda=minkowski-mul-Commutative-Monoid}}
35+
of `A` and `B` is the [set](foundation-core.sets.md) of elements that can be
36+
formed by multiplying an element of `A` and an element of `B`. This binary
37+
operation defines a commutative monoid structure on the
38+
[powerset](foundation.powersets.md) of `M`.
39+
40+
## Definition
41+
42+
```agda
43+
module _
44+
{l1 l2 l3 : Level}
45+
(M : Commutative-Monoid l1)
46+
(A : subset-Commutative-Monoid l2 M)
47+
(B : subset-Commutative-Monoid l3 M)
48+
where
49+
50+
minkowski-mul-Commutative-Monoid :
51+
subset-Commutative-Monoid (l1 ⊔ l2 ⊔ l3) M
52+
minkowski-mul-Commutative-Monoid =
53+
minkowski-mul-Monoid (monoid-Commutative-Monoid M) A B
54+
```
55+
56+
## Properties
57+
58+
### Minkowski multiplication on subsets of a commutative monoid is associative
59+
60+
```agda
61+
module _
62+
{l1 l2 l3 l4 : Level}
63+
(M : Commutative-Monoid l1)
64+
(A : subset-Commutative-Monoid l2 M)
65+
(B : subset-Commutative-Monoid l3 M)
66+
(C : subset-Commutative-Monoid l4 M)
67+
where
68+
69+
associative-minkowski-mul-Commutative-Monoid :
70+
minkowski-mul-Commutative-Monoid
71+
( M)
72+
( minkowski-mul-Commutative-Monoid M A B)
73+
( C) ＝
74+
minkowski-mul-Commutative-Monoid
75+
( M)
76+
( A)
77+
( minkowski-mul-Commutative-Monoid M B C)
78+
associative-minkowski-mul-Commutative-Monoid =
79+
associative-minkowski-mul-Monoid (monoid-Commutative-Monoid M) A B C
80+
```
81+
82+
### Minkowski multiplication on subsets of a commutative monoid is unital
83+
84+
```agda
85+
module _
86+
{l1 l2 : Level}
87+
(M : Commutative-Monoid l1)
88+
(A : subset-Commutative-Monoid l2 M)
89+
where
90+
91+
left-unit-law-minkowski-mul-Commutative-Monoid :
92+
sim-subtype
93+
( minkowski-mul-Commutative-Monoid
94+
( M)
95+
( is-unit-prop-Commutative-Monoid M)
96+
( A))
97+
( A)
98+
left-unit-law-minkowski-mul-Commutative-Monoid =
99+
left-unit-law-minkowski-mul-Monoid (monoid-Commutative-Monoid M) A
100+
101+
right-unit-law-minkowski-mul-Commutative-Monoid :
102+
sim-subtype
103+
( minkowski-mul-Commutative-Monoid
104+
( M)
105+
( A)
106+
( is-unit-prop-Commutative-Monoid M))
107+
( A)
108+
right-unit-law-minkowski-mul-Commutative-Monoid =
109+
right-unit-law-minkowski-mul-Monoid (monoid-Commutative-Monoid M) A
110+
```
111+
112+
### Minkowski multiplication on a commutative monoid is unital
113+
114+
```agda
115+
module _
116+
{l : Level}
117+
(M : Commutative-Monoid l)
118+
where
119+
120+
is-unital-minkowski-mul-Commutative-Monoid :
121+
is-unital (minkowski-mul-Commutative-Monoid {l} {l} {l} M)
122+
is-unital-minkowski-mul-Commutative-Monoid =
123+
is-unital-minkowski-mul-Monoid (monoid-Commutative-Monoid M)
124+
```
125+
126+
### Minkowski multiplication on subsets of a commutative monoid is commutative
127+
128+
```agda
129+
module _
130+
{l1 l2 l3 : Level}
131+
(M : Commutative-Monoid l1)
132+
(A : subset-Commutative-Monoid l2 M)
133+
(B : subset-Commutative-Monoid l3 M)
134+
where
135+
136+
commutative-minkowski-mul-leq-Commutative-Monoid :
137+
minkowski-mul-Commutative-Monoid M A B ⊆
138+
minkowski-mul-Commutative-Monoid M B A
139+
commutative-minkowski-mul-leq-Commutative-Monoid x =
140+
elim-exists
141+
( minkowski-mul-Commutative-Monoid M B A x)
142+
( λ (a , b) (a∈A , b∈B , x=ab) →
143+
intro-exists
144+
( b , a)
145+
( b∈B , a∈A , x=ab ∙ commutative-mul-Commutative-Monoid M a b))
146+
147+
module _
148+
{l1 l2 l3 : Level}
149+
(M : Commutative-Monoid l1)
150+
(A : subset-Commutative-Monoid l2 M)
151+
(B : subset-Commutative-Monoid l3 M)
152+
where
153+
154+
commutative-minkowski-mul-Commutative-Monoid :
155+
minkowski-mul-Commutative-Monoid M A B ＝
156+
minkowski-mul-Commutative-Monoid M B A
157+
commutative-minkowski-mul-Commutative-Monoid =
158+
antisymmetric-sim-subtype
159+
( minkowski-mul-Commutative-Monoid M A B)
160+
( minkowski-mul-Commutative-Monoid M B A)
161+
( commutative-minkowski-mul-leq-Commutative-Monoid M A B ,
162+
commutative-minkowski-mul-leq-Commutative-Monoid M B A)
163+
```
164+
165+
### Minkowski multiplication on subsets of a commutative monoid is a commutative monoid
166+
167+
```agda
168+
module _
169+
{l : Level}
170+
(M : Commutative-Monoid l)
171+
where
172+
173+
commutative-monoid-minkowski-mul-Commutative-Monoid :
174+
Commutative-Monoid (lsuc l)
175+
pr1 commutative-monoid-minkowski-mul-Commutative-Monoid =
176+
monoid-minkowski-mul-Monoid (monoid-Commutative-Monoid M)
177+
pr2 commutative-monoid-minkowski-mul-Commutative-Monoid =
178+
commutative-minkowski-mul-Commutative-Monoid M
179+
```
180+
181+
### The Minkowski multiplication of two inhabited subsets is inhabited
182+
183+
```agda
184+
module _
185+
{l1 : Level}
186+
(M : Commutative-Monoid l1)
187+
where
188+
189+
minkowski-mul-inhabited-is-inhabited-Commutative-Monoid :
190+
{l2 l3 : Level} →
191+
(A : subset-Commutative-Monoid l2 M) →
192+
(B : subset-Commutative-Monoid l3 M) →
193+
is-inhabited-subtype A →
194+
is-inhabited-subtype B →
195+
is-inhabited-subtype (minkowski-mul-Commutative-Monoid M A B)
196+
minkowski-mul-inhabited-is-inhabited-Commutative-Monoid =
197+
minkowski-mul-inhabited-is-inhabited-Monoid (monoid-Commutative-Monoid M)
198+
```
199+
200+
### Containment of subsets is preserved by Minkowski multiplication
201+
202+
```agda
203+
module _
204+
{l1 l2 l3 l4 : Level}
205+
(M : Commutative-Monoid l1)
206+
(B : subset-Commutative-Monoid l2 M)
207+
(A : subset-Commutative-Monoid l3 M)
208+
(A' : subset-Commutative-Monoid l4 M)
209+
where
210+
211+
preserves-leq-left-minkowski-mul-Commutative-Monoid :
212+
A ⊆ A' →
213+
minkowski-mul-Commutative-Monoid M A B ⊆
214+
minkowski-mul-Commutative-Monoid M A' B
215+
preserves-leq-left-minkowski-mul-Commutative-Monoid =
216+
preserves-leq-left-minkowski-mul-Monoid (monoid-Commutative-Monoid M) B A A'
217+
218+
preserves-leq-right-minkowski-mul-Commutative-Monoid :
219+
A ⊆ A' →
220+
minkowski-mul-Commutative-Monoid M B A ⊆
221+
minkowski-mul-Commutative-Monoid M B A'
222+
preserves-leq-right-minkowski-mul-Commutative-Monoid =
223+
preserves-leq-right-minkowski-mul-Monoid
224+
( monoid-Commutative-Monoid M)
225+
( B)
226+
( A)
227+
( A')
228+
```
229+
230+
### Similarity of subsets is preserved by Minkowski multiplication
231+
232+
```agda
233+
module _
234+
{l1 l2 l3 l4 : Level}
235+
(M : Commutative-Monoid l1)
236+
(B : subset-Commutative-Monoid l2 M)
237+
(A : subset-Commutative-Monoid l3 M)
238+
(A' : subset-Commutative-Monoid l4 M)
239+
where
240+
241+
preserves-sim-left-minkowski-mul-Commutative-Monoid :
242+
sim-subtype A A' →
243+
sim-subtype
244+
( minkowski-mul-Commutative-Monoid M A B)
245+
( minkowski-mul-Commutative-Monoid M A' B)
246+
preserves-sim-left-minkowski-mul-Commutative-Monoid =
247+
preserves-sim-left-minkowski-mul-Monoid (monoid-Commutative-Monoid M) B A A'
248+
249+
preserves-sim-right-minkowski-mul-Commutative-Monoid :
250+
sim-subtype A A' →
251+
sim-subtype
252+
( minkowski-mul-Commutative-Monoid M B A)
253+
( minkowski-mul-Commutative-Monoid M B A')
254+
preserves-sim-right-minkowski-mul-Commutative-Monoid =
255+
preserves-sim-right-minkowski-mul-Monoid
256+
( monoid-Commutative-Monoid M)
257+
( B)
258+
( A)
259+
( A')
260+
261+
module _
262+
{l1 l2 l3 l4 l5 : Level}
263+
(M : Commutative-Monoid l1)
264+
(A : subset-Commutative-Monoid l2 M)
265+
(A' : subset-Commutative-Monoid l3 M)
266+
(B : subset-Commutative-Monoid l4 M)
267+
(B' : subset-Commutative-Monoid l5 M)
268+
where
269+
270+
preserves-sim-minkowski-mul-Commutative-Monoid :
271+
sim-subtype A A' →
272+
sim-subtype B B' →
273+
sim-subtype
274+
( minkowski-mul-Commutative-Monoid M A B)
275+
( minkowski-mul-Commutative-Monoid M A' B')
276+
preserves-sim-minkowski-mul-Commutative-Monoid =
277+
preserves-sim-minkowski-mul-Monoid (monoid-Commutative-Monoid M) A A' B B'
278+
```
279+
280+
## See also
281+
282+
- Minkowski multiplication on semigroups is defined in
283+
[`group-theory.minkowski-multiplication-semigroups`](group-theory.minkowski-multiplication-semigroups.md).
284+
- Minkowski multiplication on monoids is defined in
285+
[`group-theory.minkowski-multiplication-monoids`](group-theory.minkowski-multiplication-monoids.md).
286+
287+
## External links
288+
289+
- [Minkowski addition](https://en.wikipedia.org/wiki/Minkowski_addition) at
290+
Wikipedia

0 commit comments

Comments
 (0)