From e84f3ce826860e6f38873509b2a003be10f799a2 Mon Sep 17 00:00:00 2001 From: Louis Wasserman Date: Sun, 9 Feb 2025 10:22:00 -0800 Subject: [PATCH 01/23] Define Minkowski multiplication for semigroups --- ...nkowski-multiplication-semigroups.lagda.md | 144 ++++++++++++++++++ 1 file changed, 144 insertions(+) create mode 100644 src/group-theory/minkowski-multiplication-semigroups.lagda.md diff --git a/src/group-theory/minkowski-multiplication-semigroups.lagda.md b/src/group-theory/minkowski-multiplication-semigroups.lagda.md new file mode 100644 index 0000000000..1978d3b786 --- /dev/null +++ b/src/group-theory/minkowski-multiplication-semigroups.lagda.md @@ -0,0 +1,144 @@ +# Minkowski multiplication of semigroup subtypes + +```agda +module group-theory.minkowski-multiplication-semigroups where +``` + +
Imports + +```agda +open import foundation.action-on-identifications-functions +open import foundation.cartesian-product-types +open import foundation.conjunction +open import foundation.dependent-pair-types +open import foundation.existential-quantification +open import foundation.identity-types +open import foundation.propositions +open import foundation.sets +open import foundation.subtypes +open import foundation.universe-levels + +open import group-theory.semigroups +``` + +
+ +## Idea + +For two subtypes `A`, `B` of a semigroup `S`, the Minkowski multiplication of `A` and `B` is the set +of elements that can be formed by multiplying an element of `A` and an element +of `B`. (This is more usually referred to as a Minkowski sum, but as the +operation on semigroups is referred to as `mul`, we use multiplicative +terminology.) + +## Definition + +```agda +module _ + {l1 l2 l3 : Level} + (G : Semigroup l1) + (A : subtype l2 (type-Semigroup G)) + (B : subtype l3 (type-Semigroup G)) + where + + minkowski-mul-Semigroup : subtype (l1 ⊔ l2 ⊔ l3) (type-Semigroup G) + minkowski-mul-Semigroup c = + ∃ + ( type-Semigroup G × type-Semigroup G) + ( λ (a , b) → + A a ∧ B b ∧ Id-Prop (set-Semigroup G) c (mul-Semigroup G a b)) +``` + +## Properties + +### Minkowski multiplication of semigroup subtypes is associative + +```agda +module _ + {l1 l2 l3 l4 : Level} + (G : Semigroup l1) + (A : subtype l2 (type-Semigroup G)) + (B : subtype l3 (type-Semigroup G)) + (C : subtype l4 (type-Semigroup G)) + where + + associative-minkowski-mul-has-same-elements-subtype-Semigroup : + has-same-elements-subtype + ( minkowski-mul-Semigroup G (minkowski-mul-Semigroup G A B) C) + ( minkowski-mul-Semigroup G A (minkowski-mul-Semigroup G B C)) + pr1 (associative-minkowski-mul-has-same-elements-subtype-Semigroup x) = + elim-exists + ( claim) + ( λ (ab , c) (ab∈AB , c∈C , x=ab*c) → + elim-exists + ( claim) + ( λ (a , b) (a∈A , b∈B , ab=a*b) → + intro-exists + ( a , mul-Semigroup G b c) + ( a∈A , + intro-exists (b , c) (b∈B , c∈C , refl) , + ( equational-reasoning + x + ＝ mul-Semigroup G ab c by x=ab*c + ＝ mul-Semigroup G (mul-Semigroup G a b) c + by ap (mul-Semigroup' G c) ab=a*b + ＝ mul-Semigroup G a (mul-Semigroup G b c) + by associative-mul-Semigroup G a b c))) + ( ab∈AB)) + where + claim = + minkowski-mul-Semigroup G A (minkowski-mul-Semigroup G B C) x + pr2 (associative-minkowski-mul-has-same-elements-subtype-Semigroup x) = + elim-exists + ( claim) + ( λ (a , bc) (a∈A , bc∈BC , x=a*bc) → + elim-exists + ( claim) + ( λ (b , c) (b∈B , c∈C , bc=b*c) → + intro-exists + ( mul-Semigroup G a b , c) + ( intro-exists (a , b) (a∈A , b∈B , refl) , + c∈C , + ( equational-reasoning + x + ＝ mul-Semigroup G a bc by x=a*bc + ＝ mul-Semigroup G a (mul-Semigroup G b c) + by ap (mul-Semigroup G a) bc=b*c + ＝ mul-Semigroup G (mul-Semigroup G a b) c + by inv (associative-mul-Semigroup G a b c)))) + ( bc∈BC)) + where + claim = + minkowski-mul-Semigroup G (minkowski-mul-Semigroup G A B) C x + + associative-minkowski-mul-Semigroup : + minkowski-mul-Semigroup G (minkowski-mul-Semigroup G A B) C ＝ + minkowski-mul-Semigroup G A (minkowski-mul-Semigroup G B C) + associative-minkowski-mul-Semigroup = + eq-has-same-elements-subtype + ( minkowski-mul-Semigroup G (minkowski-mul-Semigroup G A B) C) + ( minkowski-mul-Semigroup G A (minkowski-mul-Semigroup G B C)) + ( associative-minkowski-mul-has-same-elements-subtype-Semigroup) +``` + +### Minkowski multiplication of subtypes of a semigroup forms a semigroup + +```agda +module _ + {l1 : Level} + (G : Semigroup l1) + where + + semigroup-minkowski-mul-Semigroup : + (l : Level) → Semigroup (lsuc l1 ⊔ lsuc l) + pr1 (semigroup-minkowski-mul-Semigroup l) = + subtype-Set (l1 ⊔ l) (type-Semigroup G) + pr1 (pr2 (semigroup-minkowski-mul-Semigroup l)) = minkowski-mul-Semigroup G + pr2 (pr2 (semigroup-minkowski-mul-Semigroup l)) = + associative-minkowski-mul-Semigroup G +``` + +## External links + +- [Minkowski addition](https://en.wikipedia.org/wiki/Minkowski_addition) at + Wikipedia From 4f547c83691fc800d61a68d06f0518ac0ad1b514 Mon Sep 17 00:00:00 2001 From: Louis Wasserman Date: Sun, 9 Feb 2025 10:22:39 -0800 Subject: [PATCH 02/23] make pre-commit --- src/group-theory.lagda.md | 1 + .../minkowski-multiplication-semigroups.lagda.md | 10 +++++----- 2 files changed, 6 insertions(+), 5 deletions(-) diff --git a/src/group-theory.lagda.md b/src/group-theory.lagda.md index 962a96a816..1233b0af98 100644 --- a/src/group-theory.lagda.md +++ b/src/group-theory.lagda.md @@ -116,6 +116,7 @@ open import group-theory.large-semigroups public open import group-theory.loop-groups-sets public open import group-theory.mere-equivalences-concrete-group-actions public open import group-theory.mere-equivalences-group-actions public +open import group-theory.minkowski-multiplication-semigroups public open import group-theory.monoid-actions public open import group-theory.monoids public open import group-theory.monomorphisms-concrete-groups public diff --git a/src/group-theory/minkowski-multiplication-semigroups.lagda.md b/src/group-theory/minkowski-multiplication-semigroups.lagda.md index 1978d3b786..e4a81a386c 100644 --- a/src/group-theory/minkowski-multiplication-semigroups.lagda.md +++ b/src/group-theory/minkowski-multiplication-semigroups.lagda.md @@ -25,11 +25,11 @@ open import group-theory.semigroups ## Idea -For two subtypes `A`, `B` of a semigroup `S`, the Minkowski multiplication of `A` and `B` is the set -of elements that can be formed by multiplying an element of `A` and an element -of `B`. (This is more usually referred to as a Minkowski sum, but as the -operation on semigroups is referred to as `mul`, we use multiplicative -terminology.) +For two subtypes `A`, `B` of a semigroup `S`, the Minkowski multiplication of +`A` and `B` is the set of elements that can be formed by multiplying an element +of `A` and an element of `B`. (This is more usually referred to as a Minkowski +sum, but as the operation on semigroups is referred to as `mul`, we use +multiplicative terminology.) ## Definition From ab87dac060d95050de28e5aa81fd4830ceb99c50 Mon Sep 17 00:00:00 2001 From: Louis Wasserman Date: Sun, 9 Feb 2025 11:15:39 -0800 Subject: [PATCH 03/23] Add monoids and commutative monoids --- ...ultiplication-commutative-monoids.lagda.md | 116 +++++++++++++++ .../minkowski-multiplication-monoids.lagda.md | 138 ++++++++++++++++++ ...nkowski-multiplication-semigroups.lagda.md | 17 +-- src/group-theory/monoids.lagda.md | 6 + 4 files changed, 268 insertions(+), 9 deletions(-) create mode 100644 src/group-theory/minkowski-multiplication-commutative-monoids.lagda.md create mode 100644 src/group-theory/minkowski-multiplication-monoids.lagda.md diff --git a/src/group-theory/minkowski-multiplication-commutative-monoids.lagda.md b/src/group-theory/minkowski-multiplication-commutative-monoids.lagda.md new file mode 100644 index 0000000000..f85d234c4a --- /dev/null +++ b/src/group-theory/minkowski-multiplication-commutative-monoids.lagda.md @@ -0,0 +1,116 @@ +# Minkowski multiplication of commutative monoid subtypes + +```agda +module group-theory.minkowski-multiplication-commutative-monoids where +``` + +
Imports + +```agda +open import foundation.dependent-pair-types +open import foundation.existential-quantification +open import foundation.identity-types +open import foundation.powersets +open import foundation.subtypes +open import foundation.universe-levels + +open import group-theory.minkowski-multiplication-monoids +open import group-theory.commutative-monoids +open import group-theory.monoids +``` + +
+ +## Idea + +For two [subtypes](foundation-core.subtypes.md) `A`, `B` of a +[commutative monoid](group-theory.commutative-monoids.md) `M`, the Minkowski multiplication of +`A` and `B` is the set of elements that can be formed by multiplying an element +of `A` and an element of `B`. (This is more usually referred to as a Minkowski +sum, but as the operation on commutative monoids is referred to as `mul`, we use +multiplicative terminology.) + +## Definition + +```agda +module _ + {l1 l2 l3 : Level} + (M : Commutative-Monoid l1) + (A : subtype l2 (type-Commutative-Monoid M)) + (B : subtype l3 (type-Commutative-Monoid M)) + where + + minkowski-mul-Commutative-Monoid : + subtype (l1 ⊔ l2 ⊔ l3) (type-Commutative-Monoid M) + minkowski-mul-Commutative-Monoid = + minkowski-mul-Monoid (monoid-Commutative-Monoid M) A B +``` + +## Properties + +### Minkowski multiplication on a commutative monoid is commutative + +```agda +module _ + {l1 l2 l3 : Level} + (M : Commutative-Monoid l1) + (A : subtype l2 (type-Commutative-Monoid M)) + (B : subtype l3 (type-Commutative-Monoid M)) + where + + commutative-minkowski-mul-leq-Commutative-Monoid : + minkowski-mul-Commutative-Monoid M A B ⊆ + minkowski-mul-Commutative-Monoid M B A + commutative-minkowski-mul-leq-Commutative-Monoid x = + elim-exists + (minkowski-mul-Commutative-Monoid M B A x) + ( λ (a , b) (a∈A , b∈B , x=ab) → + intro-exists + ( b , a) + ( b∈B , a∈A , x=ab ∙ commutative-mul-Commutative-Monoid M a b)) + +module _ + {l1 l2 l3 : Level} + (M : Commutative-Monoid l1) + (A : subtype l2 (type-Commutative-Monoid M)) + (B : subtype l3 (type-Commutative-Monoid M)) + where + + commutative-minkowski-mul-Commutative-Monoid : + minkowski-mul-Commutative-Monoid M A B ＝ + minkowski-mul-Commutative-Monoid M B A + commutative-minkowski-mul-Commutative-Monoid = + antisymmetric-sim-subtype + ( minkowski-mul-Commutative-Monoid M A B) + ( minkowski-mul-Commutative-Monoid M B A) + ( commutative-minkowski-mul-leq-Commutative-Monoid M A B , + commutative-minkowski-mul-leq-Commutative-Monoid M B A) +``` + +### Minkowski multiplication on a commutative monoid is a commutative monoid + +```agda +module _ + {l : Level} + (M : Commutative-Monoid l) + where + + commutative-monoid-minkowski-mul-Commutative-Monoid : + Commutative-Monoid (lsuc l) + pr1 commutative-monoid-minkowski-mul-Commutative-Monoid = + monoid-minkowski-mul-Monoid (monoid-Commutative-Monoid M) + pr2 commutative-monoid-minkowski-mul-Commutative-Monoid = + commutative-minkowski-mul-Commutative-Monoid M +``` + +## See also + +- Minkowski multiplication on semigroups is defined in + [`group-theory.minkowski-multiplication-semigroups`](group-theory.minkowski-multiplication-semigroups.md). +- Minkowski multiplication on monoids is defined in + [`group-theory.minkowski-multiplication-monoids`](group-theory.minkowski-multiplication-monoids.md). + +## External links + +- [Minkowski addition](https://en.wikipedia.org/wiki/Minkowski_addition) at + Wikipedia diff --git a/src/group-theory/minkowski-multiplication-monoids.lagda.md b/src/group-theory/minkowski-multiplication-monoids.lagda.md new file mode 100644 index 0000000000..88de396de6 --- /dev/null +++ b/src/group-theory/minkowski-multiplication-monoids.lagda.md @@ -0,0 +1,138 @@ +# Minkowski multiplication of monoid subtypes + +```agda +module group-theory.minkowski-multiplication-monoids where +``` + +
Imports + +```agda +open import foundation.action-on-identifications-functions +open import foundation.dependent-pair-types +open import foundation.existential-quantification +open import foundation.identity-types +open import foundation.powersets +open import foundation.unital-binary-operations +open import foundation.subtypes +open import foundation.transport-along-identifications +open import foundation.universe-levels + +open import group-theory.minkowski-multiplication-semigroups +open import group-theory.monoids +open import group-theory.semigroups +``` + +
+ +## Idea + +For two [subtypes](foundation-core.subtypes.md) `A`, `B` of a +[monoid](group-theory.monoids.md) `M`, the Minkowski multiplication of +`A` and `B` is the set of elements that can be formed by multiplying an element +of `A` and an element of `B`. (This is more usually referred to as a Minkowski +sum, but as the operation on monoids is referred to as `mul`, we use +multiplicative terminology.) + +## Definition + +```agda +module _ + {l1 l2 l3 : Level} + (M : Monoid l1) + (A : subtype l2 (type-Monoid M)) + (B : subtype l3 (type-Monoid M)) + where + + minkowski-mul-Monoid : subtype (l1 ⊔ l2 ⊔ l3) (type-Monoid M) + minkowski-mul-Monoid = minkowski-mul-Semigroup (semigroup-Monoid M) A B +``` + +## Properties + +### Unit laws for Minkowski multiplication of semigroup subtypes + +```agda +module _ + {l1 l2 : Level} + (M : Monoid l1) + (A : subtype l2 (type-Monoid M)) + where + + left-unit-law-minkowski-mul-Monoid : + sim-subtype (minkowski-mul-Monoid M (is-unit-Monoid-Prop M) A) A + pr1 left-unit-law-minkowski-mul-Monoid a = + elim-exists + ( A a) + ( λ (z , a') (z=1 , a'∈A , a=za') → + tr + ( is-in-subtype A) + ( inv + ( equational-reasoning + a + ＝ mul-Monoid M z a' by a=za' + ＝ mul-Monoid M (unit-Monoid M) a' by ap (mul-Monoid' M a') z=1 + ＝ a' by left-unit-law-mul-Monoid M a')) + ( a'∈A)) + pr2 left-unit-law-minkowski-mul-Monoid a a∈A = + intro-exists + ( unit-Monoid M , a) + ( refl , a∈A , inv (left-unit-law-mul-Monoid M a)) + + right-unit-law-minkowski-mul-Monoid : + sim-subtype (minkowski-mul-Monoid M A (is-unit-Monoid-Prop M)) A + pr1 right-unit-law-minkowski-mul-Monoid a = + elim-exists + ( A a) + ( λ (a' , z) (a'∈A , z=1 , a=a'z) → + tr + ( is-in-subtype A) + ( inv + ( equational-reasoning + a + ＝ mul-Monoid M a' z by a=a'z + ＝ mul-Monoid M a' (unit-Monoid M) by ap (mul-Monoid M a') z=1 + ＝ a' by right-unit-law-mul-Monoid M a')) + ( a'∈A)) + pr2 right-unit-law-minkowski-mul-Monoid a a∈A = + intro-exists + ( a , unit-Monoid M) + ( a∈A , refl , inv (right-unit-law-mul-Monoid M a)) +``` + +### Minkowski multiplication of subtypes of a monoid forms a monoid + +```agda +module _ + {l : Level} + (M : Monoid l) + where + + is-unital-minkowski-mul-Monoid : + is-unital (minkowski-mul-Monoid {l} {l} {l} M) + pr1 is-unital-minkowski-mul-Monoid = is-unit-Monoid-Prop M + pr1 (pr2 is-unital-minkowski-mul-Monoid) A = + antisymmetric-sim-subtype + ( minkowski-mul-Monoid M (is-unit-Monoid-Prop M) A) + ( A) + ( left-unit-law-minkowski-mul-Monoid M A) + pr2 (pr2 is-unital-minkowski-mul-Monoid) A = + antisymmetric-sim-subtype + ( minkowski-mul-Monoid M A (is-unit-Monoid-Prop M)) + ( A) + ( right-unit-law-minkowski-mul-Monoid M A) + + monoid-minkowski-mul-Monoid : Monoid (lsuc l) + pr1 monoid-minkowski-mul-Monoid = + semigroup-minkowski-mul-Semigroup (semigroup-Monoid M) + pr2 monoid-minkowski-mul-Monoid = is-unital-minkowski-mul-Monoid +``` + +## See also + +- Minkowski multiplication on semigroups is defined in + [`group-theory.minkowski-multiplication-semigroups`](group-theory.minkowski-multiplication-semigroups.md). + +## External links + +- [Minkowski addition](https://en.wikipedia.org/wiki/Minkowski_addition) at + Wikipedia diff --git a/src/group-theory/minkowski-multiplication-semigroups.lagda.md b/src/group-theory/minkowski-multiplication-semigroups.lagda.md index e4a81a386c..4fd589d0d2 100644 --- a/src/group-theory/minkowski-multiplication-semigroups.lagda.md +++ b/src/group-theory/minkowski-multiplication-semigroups.lagda.md @@ -25,7 +25,8 @@ open import group-theory.semigroups ## Idea -For two subtypes `A`, `B` of a semigroup `S`, the Minkowski multiplication of +For two [subtypes](foundation-core.subtypes.md) `A`, `B` of a +[semigroup](group-theory.semigroups.md) `S`, the Minkowski multiplication of `A` and `B` is the set of elements that can be formed by multiplying an element of `A` and an element of `B`. (This is more usually referred to as a Minkowski sum, but as the operation on semigroups is referred to as `mul`, we use @@ -125,16 +126,14 @@ module _ ```agda module _ - {l1 : Level} - (G : Semigroup l1) + {l : Level} + (G : Semigroup l) where - semigroup-minkowski-mul-Semigroup : - (l : Level) → Semigroup (lsuc l1 ⊔ lsuc l) - pr1 (semigroup-minkowski-mul-Semigroup l) = - subtype-Set (l1 ⊔ l) (type-Semigroup G) - pr1 (pr2 (semigroup-minkowski-mul-Semigroup l)) = minkowski-mul-Semigroup G - pr2 (pr2 (semigroup-minkowski-mul-Semigroup l)) = + semigroup-minkowski-mul-Semigroup : Semigroup (lsuc l) + pr1 semigroup-minkowski-mul-Semigroup = subtype-Set l (type-Semigroup G) + pr1 (pr2 semigroup-minkowski-mul-Semigroup) = minkowski-mul-Semigroup G + pr2 (pr2 semigroup-minkowski-mul-Semigroup) = associative-minkowski-mul-Semigroup G ``` diff --git a/src/group-theory/monoids.lagda.md b/src/group-theory/monoids.lagda.md index 1e76dbc225..6a0c542cfc 100644 --- a/src/group-theory/monoids.lagda.md +++ b/src/group-theory/monoids.lagda.md @@ -82,6 +82,12 @@ module _ unit-Monoid : type-Monoid unit-Monoid = pr1 has-unit-Monoid + is-unit-Monoid-Prop : type-Monoid → Prop l + is-unit-Monoid-Prop x = Id-Prop set-Monoid x unit-Monoid + + is-unit-Monoid : type-Monoid → UU l + is-unit-Monoid x = x ＝ unit-Monoid + left-unit-law-mul-Monoid : (x : type-Monoid) → mul-Monoid unit-Monoid x ＝ x left-unit-law-mul-Monoid = pr1 (pr2 has-unit-Monoid) From 1f8bb30ec86e99692a98eecfcc9f829029aa45ac Mon Sep 17 00:00:00 2001 From: Louis Wasserman Date: Sun, 9 Feb 2025 11:16:52 -0800 Subject: [PATCH 04/23] make pre-commit --- src/group-theory.lagda.md | 2 ++ ...owski-multiplication-commutative-monoids.lagda.md | 12 ++++++------ .../minkowski-multiplication-monoids.lagda.md | 12 ++++++------ .../minkowski-multiplication-semigroups.lagda.md | 8 ++++---- 4 files changed, 18 insertions(+), 16 deletions(-) diff --git a/src/group-theory.lagda.md b/src/group-theory.lagda.md index 1233b0af98..3c4fb0e591 100644 --- a/src/group-theory.lagda.md +++ b/src/group-theory.lagda.md @@ -116,6 +116,8 @@ open import group-theory.large-semigroups public open import group-theory.loop-groups-sets public open import group-theory.mere-equivalences-concrete-group-actions public open import group-theory.mere-equivalences-group-actions public +open import group-theory.minkowski-multiplication-commutative-monoids public +open import group-theory.minkowski-multiplication-monoids public open import group-theory.minkowski-multiplication-semigroups public open import group-theory.monoid-actions public open import group-theory.monoids public diff --git a/src/group-theory/minkowski-multiplication-commutative-monoids.lagda.md b/src/group-theory/minkowski-multiplication-commutative-monoids.lagda.md index f85d234c4a..90d8c9c2a6 100644 --- a/src/group-theory/minkowski-multiplication-commutative-monoids.lagda.md +++ b/src/group-theory/minkowski-multiplication-commutative-monoids.lagda.md @@ -14,8 +14,8 @@ open import foundation.powersets open import foundation.subtypes open import foundation.universe-levels -open import group-theory.minkowski-multiplication-monoids open import group-theory.commutative-monoids +open import group-theory.minkowski-multiplication-monoids open import group-theory.monoids ``` @@ -24,11 +24,11 @@ open import group-theory.monoids ## Idea For two [subtypes](foundation-core.subtypes.md) `A`, `B` of a -[commutative monoid](group-theory.commutative-monoids.md) `M`, the Minkowski multiplication of -`A` and `B` is the set of elements that can be formed by multiplying an element -of `A` and an element of `B`. (This is more usually referred to as a Minkowski -sum, but as the operation on commutative monoids is referred to as `mul`, we use -multiplicative terminology.) +[commutative monoid](group-theory.commutative-monoids.md) `M`, the Minkowski +multiplication of `A` and `B` is the set of elements that can be formed by +multiplying an element of `A` and an element of `B`. (This is more usually +referred to as a Minkowski sum, but as the operation on commutative monoids is +referred to as `mul`, we use multiplicative terminology.) ## Definition diff --git a/src/group-theory/minkowski-multiplication-monoids.lagda.md b/src/group-theory/minkowski-multiplication-monoids.lagda.md index 88de396de6..34ceb6b961 100644 --- a/src/group-theory/minkowski-multiplication-monoids.lagda.md +++ b/src/group-theory/minkowski-multiplication-monoids.lagda.md @@ -12,9 +12,9 @@ open import foundation.dependent-pair-types open import foundation.existential-quantification open import foundation.identity-types open import foundation.powersets -open import foundation.unital-binary-operations open import foundation.subtypes open import foundation.transport-along-identifications +open import foundation.unital-binary-operations open import foundation.universe-levels open import group-theory.minkowski-multiplication-semigroups @@ -27,11 +27,11 @@ open import group-theory.semigroups ## Idea For two [subtypes](foundation-core.subtypes.md) `A`, `B` of a -[monoid](group-theory.monoids.md) `M`, the Minkowski multiplication of -`A` and `B` is the set of elements that can be formed by multiplying an element -of `A` and an element of `B`. (This is more usually referred to as a Minkowski -sum, but as the operation on monoids is referred to as `mul`, we use -multiplicative terminology.) +[monoid](group-theory.monoids.md) `M`, the Minkowski multiplication of `A` and +`B` is the set of elements that can be formed by multiplying an element of `A` +and an element of `B`. (This is more usually referred to as a Minkowski sum, but +as the operation on monoids is referred to as `mul`, we use multiplicative +terminology.) ## Definition diff --git a/src/group-theory/minkowski-multiplication-semigroups.lagda.md b/src/group-theory/minkowski-multiplication-semigroups.lagda.md index 4fd589d0d2..3c6e307454 100644 --- a/src/group-theory/minkowski-multiplication-semigroups.lagda.md +++ b/src/group-theory/minkowski-multiplication-semigroups.lagda.md @@ -26,10 +26,10 @@ open import group-theory.semigroups ## Idea For two [subtypes](foundation-core.subtypes.md) `A`, `B` of a -[semigroup](group-theory.semigroups.md) `S`, the Minkowski multiplication of -`A` and `B` is the set of elements that can be formed by multiplying an element -of `A` and an element of `B`. (This is more usually referred to as a Minkowski -sum, but as the operation on semigroups is referred to as `mul`, we use +[semigroup](group-theory.semigroups.md) `S`, the Minkowski multiplication of `A` +and `B` is the set of elements that can be formed by multiplying an element of +`A` and an element of `B`. (This is more usually referred to as a Minkowski sum, +but as the operation on semigroups is referred to as `mul`, we use multiplicative terminology.) ## Definition From 4581333c10e4b668df65a2f0a33378d7c1e28e78 Mon Sep 17 00:00:00 2001 From: Louis Wasserman Date: Sun, 9 Feb 2025 11:27:12 -0800 Subject: [PATCH 05/23] Use subset syntax --- ...ultiplication-commutative-monoids.lagda.md | 17 +++++----- .../minkowski-multiplication-monoids.lagda.md | 13 ++++---- ...nkowski-multiplication-semigroups.lagda.md | 32 ++++++++++--------- 3 files changed, 33 insertions(+), 29 deletions(-) diff --git a/src/group-theory/minkowski-multiplication-commutative-monoids.lagda.md b/src/group-theory/minkowski-multiplication-commutative-monoids.lagda.md index 90d8c9c2a6..1d5453d267 100644 --- a/src/group-theory/minkowski-multiplication-commutative-monoids.lagda.md +++ b/src/group-theory/minkowski-multiplication-commutative-monoids.lagda.md @@ -17,13 +17,14 @@ open import foundation.universe-levels open import group-theory.commutative-monoids open import group-theory.minkowski-multiplication-monoids open import group-theory.monoids +open import group-theory.subsets-commutative-monoids ``` ## Idea -For two [subtypes](foundation-core.subtypes.md) `A`, `B` of a +For two [subsets](group-theory.subsets-commutative-monoids.md) `A`, `B` of a [commutative monoid](group-theory.commutative-monoids.md) `M`, the Minkowski multiplication of `A` and `B` is the set of elements that can be formed by multiplying an element of `A` and an element of `B`. (This is more usually @@ -36,12 +37,12 @@ referred to as `mul`, we use multiplicative terminology.) module _ {l1 l2 l3 : Level} (M : Commutative-Monoid l1) - (A : subtype l2 (type-Commutative-Monoid M)) - (B : subtype l3 (type-Commutative-Monoid M)) + (A : subset-Commutative-Monoid l2 M) + (B : subset-Commutative-Monoid l3 M) where minkowski-mul-Commutative-Monoid : - subtype (l1 ⊔ l2 ⊔ l3) (type-Commutative-Monoid M) + subset-Commutative-Monoid (l1 ⊔ l2 ⊔ l3) M minkowski-mul-Commutative-Monoid = minkowski-mul-Monoid (monoid-Commutative-Monoid M) A B ``` @@ -54,8 +55,8 @@ module _ module _ {l1 l2 l3 : Level} (M : Commutative-Monoid l1) - (A : subtype l2 (type-Commutative-Monoid M)) - (B : subtype l3 (type-Commutative-Monoid M)) + (A : subset-Commutative-Monoid l2 M) + (B : subset-Commutative-Monoid l3 M) where commutative-minkowski-mul-leq-Commutative-Monoid : @@ -72,8 +73,8 @@ module _ module _ {l1 l2 l3 : Level} (M : Commutative-Monoid l1) - (A : subtype l2 (type-Commutative-Monoid M)) - (B : subtype l3 (type-Commutative-Monoid M)) + (A : subset-Commutative-Monoid l2 M) + (B : subset-Commutative-Monoid l3 M) where commutative-minkowski-mul-Commutative-Monoid : diff --git a/src/group-theory/minkowski-multiplication-monoids.lagda.md b/src/group-theory/minkowski-multiplication-monoids.lagda.md index 34ceb6b961..6d51224108 100644 --- a/src/group-theory/minkowski-multiplication-monoids.lagda.md +++ b/src/group-theory/minkowski-multiplication-monoids.lagda.md @@ -20,13 +20,14 @@ open import foundation.universe-levels open import group-theory.minkowski-multiplication-semigroups open import group-theory.monoids open import group-theory.semigroups +open import group-theory.subsets-monoids ``` ## Idea -For two [subtypes](foundation-core.subtypes.md) `A`, `B` of a +For two [subsets](group-theory.subsets-monoids.md) `A`, `B` of a [monoid](group-theory.monoids.md) `M`, the Minkowski multiplication of `A` and `B` is the set of elements that can be formed by multiplying an element of `A` and an element of `B`. (This is more usually referred to as a Minkowski sum, but @@ -39,23 +40,23 @@ terminology.) module _ {l1 l2 l3 : Level} (M : Monoid l1) - (A : subtype l2 (type-Monoid M)) - (B : subtype l3 (type-Monoid M)) + (A : subset-Monoid l2 M) + (B : subset-Monoid l3 M) where - minkowski-mul-Monoid : subtype (l1 ⊔ l2 ⊔ l3) (type-Monoid M) + minkowski-mul-Monoid : subset-Monoid (l1 ⊔ l2 ⊔ l3) M minkowski-mul-Monoid = minkowski-mul-Semigroup (semigroup-Monoid M) A B ``` ## Properties -### Unit laws for Minkowski multiplication of semigroup subtypes +### Unit laws for Minkowski multiplication of monoid subsets ```agda module _ {l1 l2 : Level} (M : Monoid l1) - (A : subtype l2 (type-Monoid M)) + (A : subset-Monoid l2 M) where left-unit-law-minkowski-mul-Monoid : diff --git a/src/group-theory/minkowski-multiplication-semigroups.lagda.md b/src/group-theory/minkowski-multiplication-semigroups.lagda.md index 3c6e307454..0587640fe3 100644 --- a/src/group-theory/minkowski-multiplication-semigroups.lagda.md +++ b/src/group-theory/minkowski-multiplication-semigroups.lagda.md @@ -13,19 +13,21 @@ open import foundation.conjunction open import foundation.dependent-pair-types open import foundation.existential-quantification open import foundation.identity-types +open import foundation.powersets open import foundation.propositions open import foundation.sets open import foundation.subtypes open import foundation.universe-levels open import group-theory.semigroups +open import group-theory.subsets-semigroups ``` ## Idea -For two [subtypes](foundation-core.subtypes.md) `A`, `B` of a +For two [subsets](group-theory.subsets-semigroups.md) `A`, `B` of a [semigroup](group-theory.semigroups.md) `S`, the Minkowski multiplication of `A` and `B` is the set of elements that can be formed by multiplying an element of `A` and an element of `B`. (This is more usually referred to as a Minkowski sum, @@ -38,11 +40,11 @@ multiplicative terminology.) module _ {l1 l2 l3 : Level} (G : Semigroup l1) - (A : subtype l2 (type-Semigroup G)) - (B : subtype l3 (type-Semigroup G)) + (A : subset-Semigroup l2 G) + (B : subset-Semigroup l3 G) where - minkowski-mul-Semigroup : subtype (l1 ⊔ l2 ⊔ l3) (type-Semigroup G) + minkowski-mul-Semigroup : subset-Semigroup (l1 ⊔ l2 ⊔ l3) G minkowski-mul-Semigroup c = ∃ ( type-Semigroup G × type-Semigroup G) @@ -52,22 +54,22 @@ module _ ## Properties -### Minkowski multiplication of semigroup subtypes is associative +### Minkowski multiplication of semigroup subsets is associative ```agda module _ {l1 l2 l3 l4 : Level} (G : Semigroup l1) - (A : subtype l2 (type-Semigroup G)) - (B : subtype l3 (type-Semigroup G)) - (C : subtype l4 (type-Semigroup G)) + (A : subset-Semigroup l2 G) + (B : subset-Semigroup l3 G) + (C : subset-Semigroup l4 G) where - associative-minkowski-mul-has-same-elements-subtype-Semigroup : - has-same-elements-subtype + associative-minkowski-mul-sim-Semigroup : + sim-subtype ( minkowski-mul-Semigroup G (minkowski-mul-Semigroup G A B) C) ( minkowski-mul-Semigroup G A (minkowski-mul-Semigroup G B C)) - pr1 (associative-minkowski-mul-has-same-elements-subtype-Semigroup x) = + pr1 associative-minkowski-mul-sim-Semigroup x = elim-exists ( claim) ( λ (ab , c) (ab∈AB , c∈C , x=ab*c) → @@ -89,7 +91,7 @@ module _ where claim = minkowski-mul-Semigroup G A (minkowski-mul-Semigroup G B C) x - pr2 (associative-minkowski-mul-has-same-elements-subtype-Semigroup x) = + pr2 associative-minkowski-mul-sim-Semigroup x = elim-exists ( claim) ( λ (a , bc) (a∈A , bc∈BC , x=a*bc) → @@ -116,13 +118,13 @@ module _ minkowski-mul-Semigroup G (minkowski-mul-Semigroup G A B) C ＝ minkowski-mul-Semigroup G A (minkowski-mul-Semigroup G B C) associative-minkowski-mul-Semigroup = - eq-has-same-elements-subtype + antisymmetric-sim-subtype ( minkowski-mul-Semigroup G (minkowski-mul-Semigroup G A B) C) ( minkowski-mul-Semigroup G A (minkowski-mul-Semigroup G B C)) - ( associative-minkowski-mul-has-same-elements-subtype-Semigroup) + ( associative-minkowski-mul-sim-Semigroup) ``` -### Minkowski multiplication of subtypes of a semigroup forms a semigroup +### Minkowski multiplication of subsets of a semigroup forms a semigroup ```agda module _ From 258ec997f9af6eddb40b6ff3afbe6f53dfb53537 Mon Sep 17 00:00:00 2001 From: Louis Wasserman Date: Sun, 9 Feb 2025 12:19:23 -0800 Subject: [PATCH 06/23] Inhabitedness --- ...ultiplication-commutative-monoids.lagda.md | 20 ++++++++++++++++ .../minkowski-multiplication-monoids.lagda.md | 21 ++++++++++++++++ ...nkowski-multiplication-semigroups.lagda.md | 24 +++++++++++++++++++ 3 files changed, 65 insertions(+) diff --git a/src/group-theory/minkowski-multiplication-commutative-monoids.lagda.md b/src/group-theory/minkowski-multiplication-commutative-monoids.lagda.md index 1d5453d267..1500a3439a 100644 --- a/src/group-theory/minkowski-multiplication-commutative-monoids.lagda.md +++ b/src/group-theory/minkowski-multiplication-commutative-monoids.lagda.md @@ -11,6 +11,7 @@ open import foundation.dependent-pair-types open import foundation.existential-quantification open import foundation.identity-types open import foundation.powersets +open import foundation.inhabited-subtypes open import foundation.subtypes open import foundation.universe-levels @@ -104,6 +105,25 @@ module _ commutative-minkowski-mul-Commutative-Monoid M ``` +### The Minkowski multiplication of two inhabited subsets of a commutative monoid is inhabited + +```agda +module _ + {l1 : Level} + (M : Commutative-Monoid l1) + where + + minkowski-mul-inhabited-is-inhabited-Commutative-Monoid : + {l2 l3 : Level} → + (A : subset-Commutative-Monoid l2 M) → + (B : subset-Commutative-Monoid l3 M) → + is-inhabited-subtype A → + is-inhabited-subtype B → + is-inhabited-subtype (minkowski-mul-Commutative-Monoid M A B) + minkowski-mul-inhabited-is-inhabited-Commutative-Monoid = + minkowski-mul-inhabited-is-inhabited-Monoid (monoid-Commutative-Monoid M) +``` + ## See also - Minkowski multiplication on semigroups is defined in diff --git a/src/group-theory/minkowski-multiplication-monoids.lagda.md b/src/group-theory/minkowski-multiplication-monoids.lagda.md index 6d51224108..5152319062 100644 --- a/src/group-theory/minkowski-multiplication-monoids.lagda.md +++ b/src/group-theory/minkowski-multiplication-monoids.lagda.md @@ -13,6 +13,7 @@ open import foundation.existential-quantification open import foundation.identity-types open import foundation.powersets open import foundation.subtypes +open import foundation.inhabited-subtypes open import foundation.transport-along-identifications open import foundation.unital-binary-operations open import foundation.universe-levels @@ -128,6 +129,26 @@ module _ pr2 monoid-minkowski-mul-Monoid = is-unital-minkowski-mul-Monoid ``` +### The Minkowski multiplication of two inhabited subsets of a monoid is inhabited + +```agda +module _ + {l1 : Level} + (M : Monoid l1) + where + + minkowski-mul-inhabited-is-inhabited-Monoid : + {l2 l3 : Level} → + (A : subset-Monoid l2 M) → + (B : subset-Monoid l3 M) → + is-inhabited-subtype A → + is-inhabited-subtype B → + is-inhabited-subtype (minkowski-mul-Monoid M A B) + minkowski-mul-inhabited-is-inhabited-Monoid = + minkowski-mul-inhabited-is-inhabited-Semigroup (semigroup-Monoid M) +``` + + ## See also - Minkowski multiplication on semigroups is defined in diff --git a/src/group-theory/minkowski-multiplication-semigroups.lagda.md b/src/group-theory/minkowski-multiplication-semigroups.lagda.md index 0587640fe3..ea819dde6b 100644 --- a/src/group-theory/minkowski-multiplication-semigroups.lagda.md +++ b/src/group-theory/minkowski-multiplication-semigroups.lagda.md @@ -13,12 +13,15 @@ open import foundation.conjunction open import foundation.dependent-pair-types open import foundation.existential-quantification open import foundation.identity-types +open import foundation.inhabited-subtypes open import foundation.powersets open import foundation.propositions open import foundation.sets open import foundation.subtypes open import foundation.universe-levels +open import logic.functoriality-existential-quantification + open import group-theory.semigroups open import group-theory.subsets-semigroups ``` @@ -139,6 +142,27 @@ module _ associative-minkowski-mul-Semigroup G ``` +### The Minkowski multiplication of two inhabited subsets of a semigroup is inhabited + +```agda +module _ + {l1 l2 l3 : Level} + (G : Semigroup l1) + (A : subset-Semigroup l2 G) + (B : subset-Semigroup l3 G) + where + + minkowski-mul-inhabited-is-inhabited-Semigroup : + is-inhabited-subtype A → + is-inhabited-subtype B → + is-inhabited-subtype (minkowski-mul-Semigroup G A B) + minkowski-mul-inhabited-is-inhabited-Semigroup = + map-binary-exists + ( is-in-subtype (minkowski-mul-Semigroup G A B)) + ( mul-Semigroup G) + λ a b a∈A b∈B → intro-exists (a , b) (a∈A , b∈B , refl) +``` + ## External links - [Minkowski addition](https://en.wikipedia.org/wiki/Minkowski_addition) at From 40a9e33195feaa76211760edcf9138d3b4d5f192 Mon Sep 17 00:00:00 2001 From: Louis Wasserman Date: Sun, 9 Feb 2025 12:20:00 -0800 Subject: [PATCH 07/23] make pre-commit --- .../minkowski-multiplication-commutative-monoids.lagda.md | 2 +- src/group-theory/minkowski-multiplication-monoids.lagda.md | 3 +-- src/group-theory/minkowski-multiplication-semigroups.lagda.md | 4 ++-- 3 files changed, 4 insertions(+), 5 deletions(-) diff --git a/src/group-theory/minkowski-multiplication-commutative-monoids.lagda.md b/src/group-theory/minkowski-multiplication-commutative-monoids.lagda.md index 1500a3439a..1e0ad307f4 100644 --- a/src/group-theory/minkowski-multiplication-commutative-monoids.lagda.md +++ b/src/group-theory/minkowski-multiplication-commutative-monoids.lagda.md @@ -10,8 +10,8 @@ module group-theory.minkowski-multiplication-commutative-monoids where open import foundation.dependent-pair-types open import foundation.existential-quantification open import foundation.identity-types -open import foundation.powersets open import foundation.inhabited-subtypes +open import foundation.powersets open import foundation.subtypes open import foundation.universe-levels diff --git a/src/group-theory/minkowski-multiplication-monoids.lagda.md b/src/group-theory/minkowski-multiplication-monoids.lagda.md index 5152319062..b2e67b3464 100644 --- a/src/group-theory/minkowski-multiplication-monoids.lagda.md +++ b/src/group-theory/minkowski-multiplication-monoids.lagda.md @@ -11,9 +11,9 @@ open import foundation.action-on-identifications-functions open import foundation.dependent-pair-types open import foundation.existential-quantification open import foundation.identity-types +open import foundation.inhabited-subtypes open import foundation.powersets open import foundation.subtypes -open import foundation.inhabited-subtypes open import foundation.transport-along-identifications open import foundation.unital-binary-operations open import foundation.universe-levels @@ -148,7 +148,6 @@ module _ minkowski-mul-inhabited-is-inhabited-Semigroup (semigroup-Monoid M) ``` - ## See also - Minkowski multiplication on semigroups is defined in diff --git a/src/group-theory/minkowski-multiplication-semigroups.lagda.md b/src/group-theory/minkowski-multiplication-semigroups.lagda.md index ea819dde6b..dae5ef51d5 100644 --- a/src/group-theory/minkowski-multiplication-semigroups.lagda.md +++ b/src/group-theory/minkowski-multiplication-semigroups.lagda.md @@ -20,10 +20,10 @@ open import foundation.sets open import foundation.subtypes open import foundation.universe-levels -open import logic.functoriality-existential-quantification - open import group-theory.semigroups open import group-theory.subsets-semigroups + +open import logic.functoriality-existential-quantification ``` From d7f6e2d518fec56f063419e9c8cefb022ce51c8a Mon Sep 17 00:00:00 2001 From: Louis Wasserman Date: Sun, 9 Feb 2025 14:09:53 -0800 Subject: [PATCH 08/23] Similarity and containment --- ...ultiplication-commutative-monoids.lagda.md | 80 +++++++++++++++++++ .../minkowski-multiplication-monoids.lagda.md | 66 +++++++++++++++ ...nkowski-multiplication-semigroups.lagda.md | 75 +++++++++++++++++ 3 files changed, 221 insertions(+) diff --git a/src/group-theory/minkowski-multiplication-commutative-monoids.lagda.md b/src/group-theory/minkowski-multiplication-commutative-monoids.lagda.md index 1e0ad307f4..8956fa2608 100644 --- a/src/group-theory/minkowski-multiplication-commutative-monoids.lagda.md +++ b/src/group-theory/minkowski-multiplication-commutative-monoids.lagda.md @@ -124,6 +124,86 @@ module _ minkowski-mul-inhabited-is-inhabited-Monoid (monoid-Commutative-Monoid M) ``` +### Containment is preserved by Minkowski multiplication of monoid subsets + +```agda +module _ + {l1 l2 l3 l4 : Level} + (M : Commutative-Monoid l1) + (B : subset-Commutative-Monoid l2 M) + (A : subset-Commutative-Monoid l3 M) + (A' : subset-Commutative-Monoid l4 M) + where + + preserves-leq-left-minkowski-mul-Commutative-Monoid : + A ⊆ A' → + minkowski-mul-Commutative-Monoid M A B ⊆ + minkowski-mul-Commutative-Monoid M A' B + preserves-leq-left-minkowski-mul-Commutative-Monoid = + preserves-leq-left-minkowski-mul-Monoid (monoid-Commutative-Monoid M) B A A' + + preserves-leq-right-minkowski-mul-Commutative-Monoid : + A ⊆ A' → + minkowski-mul-Commutative-Monoid M B A ⊆ + minkowski-mul-Commutative-Monoid M B A' + preserves-leq-right-minkowski-mul-Commutative-Monoid = + preserves-leq-right-minkowski-mul-Monoid + ( monoid-Commutative-Monoid M) + ( B) + ( A) + ( A') +``` + +### Similarity is preserved by Minkowski multiplication of monoid subsets + +```agda +module _ + {l1 l2 l3 l4 : Level} + (M : Commutative-Monoid l1) + (B : subset-Commutative-Monoid l2 M) + (A : subset-Commutative-Monoid l3 M) + (A' : subset-Commutative-Monoid l4 M) + where + + preserves-sim-left-minkowski-mul-Commutative-Monoid : + sim-subtype A A' → + sim-subtype + ( minkowski-mul-Commutative-Monoid M A B) + ( minkowski-mul-Commutative-Monoid M A' B) + preserves-sim-left-minkowski-mul-Commutative-Monoid = + preserves-sim-left-minkowski-mul-Monoid (monoid-Commutative-Monoid M) B A A' + + preserves-sim-right-minkowski-mul-Commutative-Monoid : + sim-subtype A A' → + sim-subtype + ( minkowski-mul-Commutative-Monoid M B A) + ( minkowski-mul-Commutative-Monoid M B A') + preserves-sim-right-minkowski-mul-Commutative-Monoid = + preserves-sim-right-minkowski-mul-Monoid + ( monoid-Commutative-Monoid M) + ( B) + ( A) + ( A') + +module _ + {l1 l2 l3 l4 l5 : Level} + (M : Commutative-Monoid l1) + (A : subset-Commutative-Monoid l2 M) + (A' : subset-Commutative-Monoid l3 M) + (B : subset-Commutative-Monoid l4 M) + (B' : subset-Commutative-Monoid l5 M) + where + + preserves-sim-minkowski-mul-Commutative-Monoid : + sim-subtype A A' → + sim-subtype B B' → + sim-subtype + ( minkowski-mul-Commutative-Monoid M A B) + ( minkowski-mul-Commutative-Monoid M A' B') + preserves-sim-minkowski-mul-Commutative-Monoid = + preserves-sim-minkowski-mul-Monoid (monoid-Commutative-Monoid M) A A' B B' +``` + ## See also - Minkowski multiplication on semigroups is defined in diff --git a/src/group-theory/minkowski-multiplication-monoids.lagda.md b/src/group-theory/minkowski-multiplication-monoids.lagda.md index b2e67b3464..a9302b06e3 100644 --- a/src/group-theory/minkowski-multiplication-monoids.lagda.md +++ b/src/group-theory/minkowski-multiplication-monoids.lagda.md @@ -148,10 +148,76 @@ module _ minkowski-mul-inhabited-is-inhabited-Semigroup (semigroup-Monoid M) ``` +### Containment is preserved by Minkowski multiplication of monoid subsets + +```agda +module _ + {l1 l2 l3 l4 : Level} + (M : Monoid l1) + (B : subset-Monoid l2 M) + (A : subset-Monoid l3 M) + (A' : subset-Monoid l4 M) + where + + preserves-leq-left-minkowski-mul-Monoid : + A ⊆ A' → minkowski-mul-Monoid M A B ⊆ minkowski-mul-Monoid M A' B + preserves-leq-left-minkowski-mul-Monoid = + preserves-leq-left-minkowski-mul-Semigroup (semigroup-Monoid M) B A A' + + preserves-leq-right-minkowski-mul-Monoid : + A ⊆ A' → minkowski-mul-Monoid M B A ⊆ minkowski-mul-Monoid M B A' + preserves-leq-right-minkowski-mul-Monoid = + preserves-leq-right-minkowski-mul-Semigroup (semigroup-Monoid M) B A A' +``` + +### Similarity is preserved by Minkowski multiplication of monoid subsets + +```agda +module _ + {l1 l2 l3 l4 : Level} + (M : Monoid l1) + (B : subset-Monoid l2 M) + (A : subset-Monoid l3 M) + (A' : subset-Monoid l4 M) + where + + preserves-sim-left-minkowski-mul-Monoid : + sim-subtype A A' → + sim-subtype (minkowski-mul-Monoid M A B) (minkowski-mul-Monoid M A' B) + preserves-sim-left-minkowski-mul-Monoid = + preserves-sim-left-minkowski-mul-Semigroup (semigroup-Monoid M) B A A' + + preserves-sim-right-minkowski-mul-Monoid : + sim-subtype A A' → + sim-subtype (minkowski-mul-Monoid M B A) (minkowski-mul-Monoid M B A') + preserves-sim-right-minkowski-mul-Monoid = + preserves-sim-right-minkowski-mul-Semigroup (semigroup-Monoid M) B A A' + +module _ + {l1 l2 l3 l4 l5 : Level} + (M : Monoid l1) + (A : subset-Monoid l2 M) + (A' : subset-Monoid l3 M) + (B : subset-Monoid l4 M) + (B' : subset-Monoid l5 M) + where + + preserves-sim-minkowski-mul-Monoid : + sim-subtype A A' → + sim-subtype B B' → + sim-subtype + ( minkowski-mul-Monoid M A B) + ( minkowski-mul-Monoid M A' B') + preserves-sim-minkowski-mul-Monoid = + preserves-sim-minkowski-mul-Semigroup (semigroup-Monoid M) A A' B B' +``` + ## See also - Minkowski multiplication on semigroups is defined in [`group-theory.minkowski-multiplication-semigroups`](group-theory.minkowski-multiplication-semigroups.md). +- Minkowski multiplication on commutative monoids is defined in + [`group-theory.minkowski-multiplication-commutative-monoids`](group-theory.minkowski-multiplication-commutative-monoids.md). ## External links diff --git a/src/group-theory/minkowski-multiplication-semigroups.lagda.md b/src/group-theory/minkowski-multiplication-semigroups.lagda.md index dae5ef51d5..8b233f4d0e 100644 --- a/src/group-theory/minkowski-multiplication-semigroups.lagda.md +++ b/src/group-theory/minkowski-multiplication-semigroups.lagda.md @@ -12,6 +12,8 @@ open import foundation.cartesian-product-types open import foundation.conjunction open import foundation.dependent-pair-types open import foundation.existential-quantification +open import foundation.function-types +open import foundation.functoriality-cartesian-product-types open import foundation.identity-types open import foundation.inhabited-subtypes open import foundation.powersets @@ -163,6 +165,79 @@ module _ λ a b a∈A b∈B → intro-exists (a , b) (a∈A , b∈B , refl) ``` +### Containment is preserved by Minkowski multiplication of semigroup subtypes + +```agda +module _ + {l1 l2 l3 l4 : Level} + (G : Semigroup l1) + (B : subset-Semigroup l2 G) + (A : subset-Semigroup l3 G) + (A' : subset-Semigroup l4 G) + where + + preserves-leq-left-minkowski-mul-Semigroup : + A ⊆ A' → minkowski-mul-Semigroup G A B ⊆ minkowski-mul-Semigroup G A' B + preserves-leq-left-minkowski-mul-Semigroup A⊆A' x = + map-tot-exists (λ (a , b) → map-product (A⊆A' a) id) + + preserves-leq-right-minkowski-mul-Semigroup : + A ⊆ A' → minkowski-mul-Semigroup G B A ⊆ minkowski-mul-Semigroup G B A' + preserves-leq-right-minkowski-mul-Semigroup A⊆A' x = + map-tot-exists (λ (b , a) → map-product id (map-product (A⊆A' a) id)) +``` + +### Similarity is preserved by Minkowski multiplication of semigroup subtypes + +```agda +module _ + {l1 l2 l3 l4 : Level} + (G : Semigroup l1) + (B : subset-Semigroup l2 G) + (A : subset-Semigroup l3 G) + (A' : subset-Semigroup l4 G) + where + + preserves-sim-left-minkowski-mul-Semigroup : + sim-subtype A A' → + sim-subtype (minkowski-mul-Semigroup G A B) (minkowski-mul-Semigroup G A' B) + pr1 (preserves-sim-left-minkowski-mul-Semigroup (A⊆A' , _)) = + preserves-leq-left-minkowski-mul-Semigroup G B A A' A⊆A' + pr2 (preserves-sim-left-minkowski-mul-Semigroup (_ , A'⊆A)) = + preserves-leq-left-minkowski-mul-Semigroup G B A' A A'⊆A + + preserves-sim-right-minkowski-mul-Semigroup : + sim-subtype A A' → + sim-subtype (minkowski-mul-Semigroup G B A) (minkowski-mul-Semigroup G B A') + pr1 (preserves-sim-right-minkowski-mul-Semigroup (A⊆A' , _)) = + preserves-leq-right-minkowski-mul-Semigroup G B A A' A⊆A' + pr2 (preserves-sim-right-minkowski-mul-Semigroup (_ , A'⊆A)) = + preserves-leq-right-minkowski-mul-Semigroup G B A' A A'⊆A + +module _ + {l1 l2 l3 l4 l5 : Level} + (G : Semigroup l1) + (A : subset-Semigroup l2 G) + (A' : subset-Semigroup l3 G) + (B : subset-Semigroup l4 G) + (B' : subset-Semigroup l5 G) + where + + preserves-sim-minkowski-mul-Semigroup : + sim-subtype A A' → + sim-subtype B B' → + sim-subtype + ( minkowski-mul-Semigroup G A B) + ( minkowski-mul-Semigroup G A' B') + preserves-sim-minkowski-mul-Semigroup A≈A' B≈B' = + transitive-sim-subtype + ( minkowski-mul-Semigroup G A B) + ( minkowski-mul-Semigroup G A B') + ( minkowski-mul-Semigroup G A' B') + ( preserves-sim-left-minkowski-mul-Semigroup G B' A A' A≈A') + ( preserves-sim-right-minkowski-mul-Semigroup G A B B' B≈B') +``` + ## External links - [Minkowski addition](https://en.wikipedia.org/wiki/Minkowski_addition) at From ca7ab8b6abb4e8c2f0273511bf159c92de70ec1e Mon Sep 17 00:00:00 2001 From: Louis Wasserman Date: Sun, 9 Feb 2025 14:30:13 -0800 Subject: [PATCH 09/23] Propagate properties --- ...ultiplication-commutative-monoids.lagda.md | 69 +++++++++++++++++++ .../minkowski-multiplication-monoids.lagda.md | 18 +++++ 2 files changed, 87 insertions(+) diff --git a/src/group-theory/minkowski-multiplication-commutative-monoids.lagda.md b/src/group-theory/minkowski-multiplication-commutative-monoids.lagda.md index 8956fa2608..ad3624e6ed 100644 --- a/src/group-theory/minkowski-multiplication-commutative-monoids.lagda.md +++ b/src/group-theory/minkowski-multiplication-commutative-monoids.lagda.md @@ -13,6 +13,7 @@ open import foundation.identity-types open import foundation.inhabited-subtypes open import foundation.powersets open import foundation.subtypes +open import foundation.unital-binary-operations open import foundation.universe-levels open import group-theory.commutative-monoids @@ -50,6 +51,74 @@ module _ ## Properties +### Minkowski multiplication of commutative monoid subsets is associative + +```agda +module _ + {l1 l2 l3 l4 : Level} + (M : Commutative-Monoid l1) + (A : subset-Commutative-Monoid l2 M) + (B : subset-Commutative-Monoid l3 M) + (C : subset-Commutative-Monoid l4 M) + where + + associative-minkowski-mul-Commutative-Monoid : + minkowski-mul-Commutative-Monoid + ( M) + ( minkowski-mul-Commutative-Monoid M A B) + ( C) ＝ + minkowski-mul-Commutative-Monoid + ( M) + ( A) + ( minkowski-mul-Commutative-Monoid M B C) + associative-minkowski-mul-Commutative-Monoid = + associative-minkowski-mul-Monoid (monoid-Commutative-Monoid M) A B C +``` + +### Minkowski multiplication of commutative monoid subsets is unital + +```agda +module _ + {l1 l2 : Level} + (M : Commutative-Monoid l1) + (A : subset-Commutative-Monoid l2 M) + where + + left-unit-law-minkowski-mul-Commutative-Monoid : + sim-subtype + ( minkowski-mul-Commutative-Monoid + ( M) + ( is-unit-prop-Commutative-Monoid M) + ( A)) + ( A) + left-unit-law-minkowski-mul-Commutative-Monoid = + left-unit-law-minkowski-mul-Monoid (monoid-Commutative-Monoid M) A + + right-unit-law-minkowski-mul-Commutative-Monoid : + sim-subtype + ( minkowski-mul-Commutative-Monoid + ( M) + ( A) + ( is-unit-prop-Commutative-Monoid M)) + ( A) + right-unit-law-minkowski-mul-Commutative-Monoid = + right-unit-law-minkowski-mul-Monoid (monoid-Commutative-Monoid M) A +``` + +### Minkowski multiplication on a commutative monoid is unital + +```agda +module _ + {l : Level} + (M : Commutative-Monoid l) + where + + is-unital-minkowski-mul-Commutative-Monoid : + is-unital (minkowski-mul-Commutative-Monoid {l} {l} {l} M) + is-unital-minkowski-mul-Commutative-Monoid = + is-unital-minkowski-mul-Monoid (monoid-Commutative-Monoid M) +``` + ### Minkowski multiplication on a commutative monoid is commutative ```agda diff --git a/src/group-theory/minkowski-multiplication-monoids.lagda.md b/src/group-theory/minkowski-multiplication-monoids.lagda.md index a9302b06e3..b9f33264cf 100644 --- a/src/group-theory/minkowski-multiplication-monoids.lagda.md +++ b/src/group-theory/minkowski-multiplication-monoids.lagda.md @@ -51,6 +51,24 @@ module _ ## Properties +### Minkowski multiplication of monoid subsets is associative + +```agda +module _ + {l1 l2 l3 l4 : Level} + (M : Monoid l1) + (A : subset-Monoid l2 M) + (B : subset-Monoid l3 M) + (C : subset-Monoid l4 M) + where + + associative-minkowski-mul-Monoid : + minkowski-mul-Monoid M (minkowski-mul-Monoid M A B) C ＝ + minkowski-mul-Monoid M A (minkowski-mul-Monoid M B C) + associative-minkowski-mul-Monoid = + associative-minkowski-mul-Semigroup (semigroup-Monoid M) A B C +``` + ### Unit laws for Minkowski multiplication of monoid subsets ```agda From 93cb3c2e60babedc00927a14fd8aa8932b5ff41f Mon Sep 17 00:00:00 2001 From: Louis Wasserman Date: Mon, 10 Feb 2025 08:34:32 -0800 Subject: [PATCH 10/23] Review suggestions --- ...nkowski-multiplication-semigroups.lagda.md | 19 +++++++++---------- 1 file changed, 9 insertions(+), 10 deletions(-) diff --git a/src/group-theory/minkowski-multiplication-semigroups.lagda.md b/src/group-theory/minkowski-multiplication-semigroups.lagda.md index 8b233f4d0e..9beb16e85b 100644 --- a/src/group-theory/minkowski-multiplication-semigroups.lagda.md +++ b/src/group-theory/minkowski-multiplication-semigroups.lagda.md @@ -50,11 +50,10 @@ module _ where minkowski-mul-Semigroup : subset-Semigroup (l1 ⊔ l2 ⊔ l3) G - minkowski-mul-Semigroup c = - ∃ - ( type-Semigroup G × type-Semigroup G) - ( λ (a , b) → - A a ∧ B b ∧ Id-Prop (set-Semigroup G) c (mul-Semigroup G a b)) + minkowski-mul-Semigroup c = ∃ + ( type-Semigroup G × type-Semigroup G) + ( λ (a , b) → + A a ∧ B b ∧ Id-Prop (set-Semigroup G) c (mul-Semigroup G a b)) ``` ## Properties @@ -70,11 +69,11 @@ module _ (C : subset-Semigroup l4 G) where - associative-minkowski-mul-sim-Semigroup : + sim-associative-minkowski-mul-Semigroup : sim-subtype ( minkowski-mul-Semigroup G (minkowski-mul-Semigroup G A B) C) ( minkowski-mul-Semigroup G A (minkowski-mul-Semigroup G B C)) - pr1 associative-minkowski-mul-sim-Semigroup x = + pr1 sim-associative-minkowski-mul-Semigroup x = elim-exists ( claim) ( λ (ab , c) (ab∈AB , c∈C , x=ab*c) → @@ -96,7 +95,7 @@ module _ where claim = minkowski-mul-Semigroup G A (minkowski-mul-Semigroup G B C) x - pr2 associative-minkowski-mul-sim-Semigroup x = + pr2 sim-associative-minkowski-mul-Semigroup x = elim-exists ( claim) ( λ (a , bc) (a∈A , bc∈BC , x=a*bc) → @@ -126,7 +125,7 @@ module _ antisymmetric-sim-subtype ( minkowski-mul-Semigroup G (minkowski-mul-Semigroup G A B) C) ( minkowski-mul-Semigroup G A (minkowski-mul-Semigroup G B C)) - ( associative-minkowski-mul-sim-Semigroup) + ( sim-associative-minkowski-mul-Semigroup) ``` ### Minkowski multiplication of subsets of a semigroup forms a semigroup @@ -162,7 +161,7 @@ module _ map-binary-exists ( is-in-subtype (minkowski-mul-Semigroup G A B)) ( mul-Semigroup G) - λ a b a∈A b∈B → intro-exists (a , b) (a∈A , b∈B , refl) + ( λ a b a∈A b∈B → intro-exists (a , b) (a∈A , b∈B , refl)) ``` ### Containment is preserved by Minkowski multiplication of semigroup subtypes From 2f376265622b93e071c80fa73c74e219d32ef14e Mon Sep 17 00:00:00 2001 From: Louis Wasserman Date: Mon, 10 Feb 2025 08:35:55 -0800 Subject: [PATCH 11/23] Apply suggestions from code review Co-authored-by: Fredrik Bakke --- ...nkowski-multiplication-semigroups.lagda.md | 20 +++++++++---------- 1 file changed, 9 insertions(+), 11 deletions(-) diff --git a/src/group-theory/minkowski-multiplication-semigroups.lagda.md b/src/group-theory/minkowski-multiplication-semigroups.lagda.md index 9beb16e85b..5f5d8a83d0 100644 --- a/src/group-theory/minkowski-multiplication-semigroups.lagda.md +++ b/src/group-theory/minkowski-multiplication-semigroups.lagda.md @@ -1,4 +1,4 @@ -# Minkowski multiplication of semigroup subtypes +# Minkowski multiplication on subsets of a semigroup ```agda module group-theory.minkowski-multiplication-semigroups where @@ -32,12 +32,10 @@ open import logic.functoriality-existential-quantification ## Idea -For two [subsets](group-theory.subsets-semigroups.md) `A`, `B` of a -[semigroup](group-theory.semigroups.md) `S`, the Minkowski multiplication of `A` -and `B` is the set of elements that can be formed by multiplying an element of -`A` and an element of `B`. (This is more usually referred to as a Minkowski sum, -but as the operation on semigroups is referred to as `mul`, we use -multiplicative terminology.) +Given two [subsets](group-theory.subsets-semigroups.md) `A` and `B` of a +[semigroup](group-theory.semigroups.md) `S`, the {{#concept "Minkowski multiplication" Disambiguation="on subsets of a semigroup" WD="Minkowski addition" WDID=Q1322294 Agda=minkowski-mul-Semigroup}} of `A` +and `B` is the [set](foundation-core.sets.md) of elements that can be formed by multiplying an element of +`A` and an element of `B`. This binary operation defines a semigroup structure on the [powerset](foundation.powersets.md) of `S`. ## Definition @@ -58,7 +56,7 @@ module _ ## Properties -### Minkowski multiplication of semigroup subsets is associative +### Minkowski multiplication on subsets of a semigroup is associative ```agda module _ @@ -128,7 +126,7 @@ module _ ( sim-associative-minkowski-mul-Semigroup) ``` -### Minkowski multiplication of subsets of a semigroup forms a semigroup +### Minkowski multiplication on subsets of a semigroup forms a semigroup ```agda module _ @@ -164,7 +162,7 @@ module _ ( λ a b a∈A b∈B → intro-exists (a , b) (a∈A , b∈B , refl)) ``` -### Containment is preserved by Minkowski multiplication of semigroup subtypes +### Containment of subsets is preserved by Minkowski multiplication ```agda module _ @@ -186,7 +184,7 @@ module _ map-tot-exists (λ (b , a) → map-product id (map-product (A⊆A' a) id)) ``` -### Similarity is preserved by Minkowski multiplication of semigroup subtypes +### Similarity of subsets is preserved by Minkowski multiplication ```agda module _ From 32a09515fc778a7901fc8849d54627a385c7f992 Mon Sep 17 00:00:00 2001 From: Louis Wasserman Date: Mon, 10 Feb 2025 08:39:07 -0800 Subject: [PATCH 12/23] More progress --- ...kowski-multiplication-commutative-monoids.lagda.md | 11 +++++------ 1 file changed, 5 insertions(+), 6 deletions(-) diff --git a/src/group-theory/minkowski-multiplication-commutative-monoids.lagda.md b/src/group-theory/minkowski-multiplication-commutative-monoids.lagda.md index ad3624e6ed..abffb529c6 100644 --- a/src/group-theory/minkowski-multiplication-commutative-monoids.lagda.md +++ b/src/group-theory/minkowski-multiplication-commutative-monoids.lagda.md @@ -133,12 +133,11 @@ module _ minkowski-mul-Commutative-Monoid M A B ⊆ minkowski-mul-Commutative-Monoid M B A commutative-minkowski-mul-leq-Commutative-Monoid x = - elim-exists - (minkowski-mul-Commutative-Monoid M B A x) - ( λ (a , b) (a∈A , b∈B , x=ab) → - intro-exists - ( b , a) - ( b∈B , a∈A , x=ab ∙ commutative-mul-Commutative-Monoid M a b)) + map-exists + ( minkowski-mul-Commutative-Monoid M B A x) + ( λ (a, b) → (b , a)) + ( λ (b , a) (a∈A , b∈B , x=ab) → + ( b∈B , a∈A , x=ab ∙ commutative-mul-Commutative-Monoid M a b)) module _ {l1 l2 l3 : Level} From cc06569cceb5df3384d2c987134179d10f67b440 Mon Sep 17 00:00:00 2001 From: Louis Wasserman Date: Mon, 10 Feb 2025 08:40:13 -0800 Subject: [PATCH 13/23] Apply suggestions from code review Co-authored-by: Fredrik Bakke --- ...owski-multiplication-commutative-monoids.lagda.md | 8 ++++---- .../minkowski-multiplication-monoids.lagda.md | 12 ++++++------ 2 files changed, 10 insertions(+), 10 deletions(-) diff --git a/src/group-theory/minkowski-multiplication-commutative-monoids.lagda.md b/src/group-theory/minkowski-multiplication-commutative-monoids.lagda.md index ad3624e6ed..a64bc6232d 100644 --- a/src/group-theory/minkowski-multiplication-commutative-monoids.lagda.md +++ b/src/group-theory/minkowski-multiplication-commutative-monoids.lagda.md @@ -158,7 +158,7 @@ module _ commutative-minkowski-mul-leq-Commutative-Monoid M B A) ``` -### Minkowski multiplication on a commutative monoid is a commutative monoid +### Minkowski multiplication on subsets of a commutative monoid is a commutative monoid ```agda module _ @@ -174,7 +174,7 @@ module _ commutative-minkowski-mul-Commutative-Monoid M ``` -### The Minkowski multiplication of two inhabited subsets of a commutative monoid is inhabited +### The Minkowski multiplication of two inhabited subsets is inhabited ```agda module _ @@ -193,7 +193,7 @@ module _ minkowski-mul-inhabited-is-inhabited-Monoid (monoid-Commutative-Monoid M) ``` -### Containment is preserved by Minkowski multiplication of monoid subsets +### Containment of subsets is preserved by Minkowski multiplication ```agda module _ @@ -223,7 +223,7 @@ module _ ( A') ``` -### Similarity is preserved by Minkowski multiplication of monoid subsets +### Similarity of subsets is preserved by Minkowski multiplication ```agda module _ diff --git a/src/group-theory/minkowski-multiplication-monoids.lagda.md b/src/group-theory/minkowski-multiplication-monoids.lagda.md index b9f33264cf..1e8a6b7847 100644 --- a/src/group-theory/minkowski-multiplication-monoids.lagda.md +++ b/src/group-theory/minkowski-multiplication-monoids.lagda.md @@ -1,4 +1,4 @@ -# Minkowski multiplication of monoid subtypes +# Minkowski multiplication on subsets of a monoid ```agda module group-theory.minkowski-multiplication-monoids where @@ -51,7 +51,7 @@ module _ ## Properties -### Minkowski multiplication of monoid subsets is associative +### Minkowski multiplication on subsets of a monoid is associative ```agda module _ @@ -69,7 +69,7 @@ module _ associative-minkowski-mul-Semigroup (semigroup-Monoid M) A B C ``` -### Unit laws for Minkowski multiplication of monoid subsets +### Unit laws for Minkowski multiplication on subsets of a monoid ```agda module _ @@ -119,7 +119,7 @@ module _ ( a∈A , refl , inv (right-unit-law-mul-Monoid M a)) ``` -### Minkowski multiplication of subtypes of a monoid forms a monoid +### Minkowski multiplication on subsets of a monoid forms a monoid ```agda module _ @@ -166,7 +166,7 @@ module _ minkowski-mul-inhabited-is-inhabited-Semigroup (semigroup-Monoid M) ``` -### Containment is preserved by Minkowski multiplication of monoid subsets +### Containment of subsets is preserved by Minkowski multiplication ```agda module _ @@ -188,7 +188,7 @@ module _ preserves-leq-right-minkowski-mul-Semigroup (semigroup-Monoid M) B A A' ``` -### Similarity is preserved by Minkowski multiplication of monoid subsets +### Similarity of subsets is preserved by Minkowski multiplication ```agda module _ From ba39406d3290e9bc196420965f8a3fad40e529e1 Mon Sep 17 00:00:00 2001 From: Louis Wasserman Date: Mon, 10 Feb 2025 08:47:23 -0800 Subject: [PATCH 14/23] Review comments --- ...owski-multiplication-commutative-monoids.lagda.md | 12 +++++++++--- 1 file changed, 9 insertions(+), 3 deletions(-) diff --git a/src/group-theory/minkowski-multiplication-commutative-monoids.lagda.md b/src/group-theory/minkowski-multiplication-commutative-monoids.lagda.md index ca63f6d65c..72d45fbbd4 100644 --- a/src/group-theory/minkowski-multiplication-commutative-monoids.lagda.md +++ b/src/group-theory/minkowski-multiplication-commutative-monoids.lagda.md @@ -7,6 +7,7 @@ module group-theory.minkowski-multiplication-commutative-monoids where
Imports ```agda +open import foundation.cartesian-product-types open import foundation.dependent-pair-types open import foundation.existential-quantification open import foundation.identity-types @@ -20,6 +21,8 @@ open import group-theory.commutative-monoids open import group-theory.minkowski-multiplication-monoids open import group-theory.monoids open import group-theory.subsets-commutative-monoids + +open import logic.functoriality-existential-quantification ```
@@ -134,10 +137,13 @@ module _ minkowski-mul-Commutative-Monoid M B A commutative-minkowski-mul-leq-Commutative-Monoid x = map-exists - ( minkowski-mul-Commutative-Monoid M B A x) - ( λ (a, b) → (b , a)) + ( λ (b , a) → + is-in-subtype B b × + is-in-subtype A a × + (x ＝ mul-Commutative-Monoid M b a)) + ( λ (a , b) → (b , a)) ( λ (b , a) (a∈A , b∈B , x=ab) → - ( b∈B , a∈A , x=ab ∙ commutative-mul-Commutative-Monoid M a b)) + ( b∈B , a∈A , x=ab ∙ commutative-mul-Commutative-Monoid M b a)) module _ {l1 l2 l3 : Level} From 38d7af2e9a8727a1dfb48b2035466a7c855f05fe Mon Sep 17 00:00:00 2001 From: Louis Wasserman Date: Mon, 10 Feb 2025 08:47:53 -0800 Subject: [PATCH 15/23] Apply suggestions from code review Co-authored-by: Fredrik Bakke --- .../minkowski-multiplication-commutative-monoids.lagda.md | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/src/group-theory/minkowski-multiplication-commutative-monoids.lagda.md b/src/group-theory/minkowski-multiplication-commutative-monoids.lagda.md index 72d45fbbd4..c8f16402e0 100644 --- a/src/group-theory/minkowski-multiplication-commutative-monoids.lagda.md +++ b/src/group-theory/minkowski-multiplication-commutative-monoids.lagda.md @@ -122,7 +122,7 @@ module _ is-unital-minkowski-mul-Monoid (monoid-Commutative-Monoid M) ``` -### Minkowski multiplication on a commutative monoid is commutative +### Minkowski multiplication on subsets of a commutative monoid is commutative ```agda module _ From 667bea25772d5bb1c024f0152f903125fe0f2c03 Mon Sep 17 00:00:00 2001 From: Louis Wasserman Date: Mon, 10 Feb 2025 08:48:52 -0800 Subject: [PATCH 16/23] make pre-commit --- .../minkowski-multiplication-semigroups.lagda.md | 9 ++++++--- 1 file changed, 6 insertions(+), 3 deletions(-) diff --git a/src/group-theory/minkowski-multiplication-semigroups.lagda.md b/src/group-theory/minkowski-multiplication-semigroups.lagda.md index 5f5d8a83d0..4fd75c3fff 100644 --- a/src/group-theory/minkowski-multiplication-semigroups.lagda.md +++ b/src/group-theory/minkowski-multiplication-semigroups.lagda.md @@ -33,9 +33,12 @@ open import logic.functoriality-existential-quantification ## Idea Given two [subsets](group-theory.subsets-semigroups.md) `A` and `B` of a -[semigroup](group-theory.semigroups.md) `S`, the {{#concept "Minkowski multiplication" Disambiguation="on subsets of a semigroup" WD="Minkowski addition" WDID=Q1322294 Agda=minkowski-mul-Semigroup}} of `A` -and `B` is the [set](foundation-core.sets.md) of elements that can be formed by multiplying an element of -`A` and an element of `B`. This binary operation defines a semigroup structure on the [powerset](foundation.powersets.md) of `S`. +[semigroup](group-theory.semigroups.md) `S`, the +{{#concept "Minkowski multiplication" Disambiguation="on subsets of a semigroup" WD="Minkowski addition" WDID=Q1322294 Agda=minkowski-mul-Semigroup}} +of `A` and `B` is the [set](foundation-core.sets.md) of elements that can be +formed by multiplying an element of `A` and an element of `B`. This binary +operation defines a semigroup structure on the +[powerset](foundation.powersets.md) of `S`. ## Definition From 30c6fa755ebf2554b72c14e5a8e6a9c85e7be295 Mon Sep 17 00:00:00 2001 From: Louis Wasserman Date: Mon, 10 Feb 2025 08:51:59 -0800 Subject: [PATCH 17/23] More fixes --- .../minkowski-multiplication-commutative-monoids.lagda.md | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/src/group-theory/minkowski-multiplication-commutative-monoids.lagda.md b/src/group-theory/minkowski-multiplication-commutative-monoids.lagda.md index c8f16402e0..6e5219ff82 100644 --- a/src/group-theory/minkowski-multiplication-commutative-monoids.lagda.md +++ b/src/group-theory/minkowski-multiplication-commutative-monoids.lagda.md @@ -1,4 +1,4 @@ -# Minkowski multiplication of commutative monoid subtypes +# Minkowski multiplication of subsets of a commutative monoid ```agda module group-theory.minkowski-multiplication-commutative-monoids where From a9db0165f8ab555dec94f0bc22a8541606f52e50 Mon Sep 17 00:00:00 2001 From: Louis Wasserman Date: Mon, 10 Feb 2025 10:48:21 -0800 Subject: [PATCH 18/23] Apply suggestions from code review Co-authored-by: Fredrik Bakke --- ...minkowski-multiplication-commutative-monoids.lagda.md | 9 +++------ 1 file changed, 3 insertions(+), 6 deletions(-) diff --git a/src/group-theory/minkowski-multiplication-commutative-monoids.lagda.md b/src/group-theory/minkowski-multiplication-commutative-monoids.lagda.md index 6e5219ff82..b9798fdbb3 100644 --- a/src/group-theory/minkowski-multiplication-commutative-monoids.lagda.md +++ b/src/group-theory/minkowski-multiplication-commutative-monoids.lagda.md @@ -29,12 +29,9 @@ open import logic.functoriality-existential-quantification ## Idea -For two [subsets](group-theory.subsets-commutative-monoids.md) `A`, `B` of a -[commutative monoid](group-theory.commutative-monoids.md) `M`, the Minkowski -multiplication of `A` and `B` is the set of elements that can be formed by -multiplying an element of `A` and an element of `B`. (This is more usually -referred to as a Minkowski sum, but as the operation on commutative monoids is -referred to as `mul`, we use multiplicative terminology.) +Given two [subsets](group-theory.subsets-commutative-monoids.md) `A` and `B` of a +[commutative monoid](group-theory.commutative-monoids.md) `M`, the {{#concept "Minkowski multiplication" Disambiguation="on subsets of a commutative monoid" WD="Minkowski addition" WDID=Q1322294 Agda=minkowski-mul-Commutative-Monoid}} of `A` and `B` is the [set](foundation-core.sets.md) of elements that can be formed by +multiplying an element of `A` and an element of `B`. This binary operation defines a commutative monoid structure on the [powerset](foundation.powersets.md) of `M`. ## Definition From eb03e6c55aa3f52411677a3a97016f3edcb2e1fe Mon Sep 17 00:00:00 2001 From: Louis Wasserman Date: Mon, 10 Feb 2025 10:50:17 -0800 Subject: [PATCH 19/23] Revert change --- ...ski-multiplication-commutative-monoids.lagda.md | 14 ++++++-------- 1 file changed, 6 insertions(+), 8 deletions(-) diff --git a/src/group-theory/minkowski-multiplication-commutative-monoids.lagda.md b/src/group-theory/minkowski-multiplication-commutative-monoids.lagda.md index b9798fdbb3..180afb0266 100644 --- a/src/group-theory/minkowski-multiplication-commutative-monoids.lagda.md +++ b/src/group-theory/minkowski-multiplication-commutative-monoids.lagda.md @@ -133,14 +133,12 @@ module _ minkowski-mul-Commutative-Monoid M A B ⊆ minkowski-mul-Commutative-Monoid M B A commutative-minkowski-mul-leq-Commutative-Monoid x = - map-exists - ( λ (b , a) → - is-in-subtype B b × - is-in-subtype A a × - (x ＝ mul-Commutative-Monoid M b a)) - ( λ (a , b) → (b , a)) - ( λ (b , a) (a∈A , b∈B , x=ab) → - ( b∈B , a∈A , x=ab ∙ commutative-mul-Commutative-Monoid M b a)) + elim-exists + ( minkowski-mul-Commutative-Monoid M B A x) + ( λ (a , b) (a∈A , b∈B , x=ab) → + intro-exists + ( b , a) + ( b∈B , a∈A , x=ab ∙ commutative-mul-Commutative-Monoid M a b)) module _ {l1 l2 l3 : Level} From 18af8014015654a39f72f84fb02df6bca91fad1f Mon Sep 17 00:00:00 2001 From: Louis Wasserman Date: Mon, 10 Feb 2025 10:52:39 -0800 Subject: [PATCH 20/23] make pre-commit formatting --- ...nkowski-multiplication-commutative-monoids.lagda.md | 10 +++++++--- 1 file changed, 7 insertions(+), 3 deletions(-) diff --git a/src/group-theory/minkowski-multiplication-commutative-monoids.lagda.md b/src/group-theory/minkowski-multiplication-commutative-monoids.lagda.md index 180afb0266..cddeb139ef 100644 --- a/src/group-theory/minkowski-multiplication-commutative-monoids.lagda.md +++ b/src/group-theory/minkowski-multiplication-commutative-monoids.lagda.md @@ -29,9 +29,13 @@ open import logic.functoriality-existential-quantification ## Idea -Given two [subsets](group-theory.subsets-commutative-monoids.md) `A` and `B` of a -[commutative monoid](group-theory.commutative-monoids.md) `M`, the {{#concept "Minkowski multiplication" Disambiguation="on subsets of a commutative monoid" WD="Minkowski addition" WDID=Q1322294 Agda=minkowski-mul-Commutative-Monoid}} of `A` and `B` is the [set](foundation-core.sets.md) of elements that can be formed by -multiplying an element of `A` and an element of `B`. This binary operation defines a commutative monoid structure on the [powerset](foundation.powersets.md) of `M`. +Given two [subsets](group-theory.subsets-commutative-monoids.md) `A` and `B` of +a [commutative monoid](group-theory.commutative-monoids.md) `M`, the +{{#concept "Minkowski multiplication" Disambiguation="on subsets of a commutative monoid" WD="Minkowski addition" WDID=Q1322294 Agda=minkowski-mul-Commutative-Monoid}} +of `A` and `B` is the [set](foundation-core.sets.md) of elements that can be +formed by multiplying an element of `A` and an element of `B`. This binary +operation defines a commutative monoid structure on the +[powerset](foundation.powersets.md) of `M`. ## Definition From e057c55d7304c47499e70c841fc0beaf6b9ee7f6 Mon Sep 17 00:00:00 2001 From: Louis Wasserman Date: Mon, 10 Feb 2025 10:57:15 -0800 Subject: [PATCH 21/23] Update src/group-theory/minkowski-multiplication-commutative-monoids.lagda.md Co-authored-by: Fredrik Bakke --- .../minkowski-multiplication-commutative-monoids.lagda.md | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/src/group-theory/minkowski-multiplication-commutative-monoids.lagda.md b/src/group-theory/minkowski-multiplication-commutative-monoids.lagda.md index cddeb139ef..d010db10ae 100644 --- a/src/group-theory/minkowski-multiplication-commutative-monoids.lagda.md +++ b/src/group-theory/minkowski-multiplication-commutative-monoids.lagda.md @@ -55,7 +55,7 @@ module _ ## Properties -### Minkowski multiplication of commutative monoid subsets is associative +### Minkowski multiplication on subsets of a commutative monoid is associative ```agda module _ From 31ed0f35ee26e8e9da3594bc8b696a3ccbe25306 Mon Sep 17 00:00:00 2001 From: Louis Wasserman Date: Mon, 10 Feb 2025 10:57:33 -0800 Subject: [PATCH 22/23] Update src/group-theory/minkowski-multiplication-commutative-monoids.lagda.md Co-authored-by: Fredrik Bakke --- .../minkowski-multiplication-commutative-monoids.lagda.md | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/src/group-theory/minkowski-multiplication-commutative-monoids.lagda.md b/src/group-theory/minkowski-multiplication-commutative-monoids.lagda.md index d010db10ae..5ad656d151 100644 --- a/src/group-theory/minkowski-multiplication-commutative-monoids.lagda.md +++ b/src/group-theory/minkowski-multiplication-commutative-monoids.lagda.md @@ -79,7 +79,7 @@ module _ associative-minkowski-mul-Monoid (monoid-Commutative-Monoid M) A B C ``` -### Minkowski multiplication of commutative monoid subsets is unital +### Minkowski multiplication on subsets of a commutative monoid is unital ```agda module _ From 9a9b288088ec17a08a1d67b440546fe7bc6e91c4 Mon Sep 17 00:00:00 2001 From: Louis Wasserman Date: Mon, 10 Feb 2025 11:22:45 -0800 Subject: [PATCH 23/23] Update src/group-theory/minkowski-multiplication-monoids.lagda.md Co-authored-by: Fredrik Bakke --- .../minkowski-multiplication-monoids.lagda.md | 13 +++++++------ 1 file changed, 7 insertions(+), 6 deletions(-) diff --git a/src/group-theory/minkowski-multiplication-monoids.lagda.md b/src/group-theory/minkowski-multiplication-monoids.lagda.md index 1e8a6b7847..185f47cbda 100644 --- a/src/group-theory/minkowski-multiplication-monoids.lagda.md +++ b/src/group-theory/minkowski-multiplication-monoids.lagda.md @@ -28,12 +28,13 @@ open import group-theory.subsets-monoids ## Idea -For two [subsets](group-theory.subsets-monoids.md) `A`, `B` of a -[monoid](group-theory.monoids.md) `M`, the Minkowski multiplication of `A` and -`B` is the set of elements that can be formed by multiplying an element of `A` -and an element of `B`. (This is more usually referred to as a Minkowski sum, but -as the operation on monoids is referred to as `mul`, we use multiplicative -terminology.) +Given two [subsets](group-theory.subsets-monoids.md) `A` and `B` of a +[monoid](group-theory.monoids.md) `M`, the +{{#concept "Minkowski multiplication" Disambiguation="on subsets of a monoid" WD="Minkowski addition" WDID=Q1322294 Agda=minkowski-mul-Monoid}} +of `A` and `B` is the [set](foundation-core.sets.md) of elements that can be +formed by multiplying an element of `A` and an element of `B`. This binary +operation defines a monoid structure on the [powerset](foundation.powersets.md) +of `M`. ## Definition