Skip to content
This repository was archived by the owner on Jul 24, 2024. It is now read-only.

Commit ca56c5a

Browse files
committed
feat(measure_theory/group): define a few measurable_equivs (#10299)
1 parent 3578403 commit ca56c5a

File tree

2 files changed

+181
-4
lines changed

2 files changed

+181
-4
lines changed

src/data/equiv/mul_add.lean

Lines changed: 8 additions & 4 deletions
Original file line numberDiff line numberDiff line change
@@ -512,16 +512,20 @@ variable (G)
512512
@[to_additive "Negation on an `add_group` is a permutation of the underlying type.",
513513
simps apply {fully_applied := ff}]
514514
protected def inv : perm G :=
515-
{ to_fun := λa, a⁻¹,
516-
inv_fun := λa, a⁻¹,
517-
left_inv := assume a, inv_inv a,
518-
right_inv := assume a, inv_inv a }
515+
function.involutive.to_equiv has_inv.inv inv_inv
516+
517+
/-- Inversion on a `group_with_zero` is a permutation of the underlying type. -/
518+
@[simps apply {fully_applied := ff}]
519+
protected def inv₀ (G : Type*) [group_with_zero G] : perm G :=
520+
function.involutive.to_equiv has_inv.inv inv_inv₀
519521

520522
variable {G}
521523

522524
@[simp, to_additive]
523525
lemma inv_symm : (equiv.inv G).symm = equiv.inv G := rfl
524526

527+
@[simp] lemma inv_symm₀ {G : Type*} [group_with_zero G] : (equiv.inv₀ G).symm = equiv.inv₀ G := rfl
528+
525529
/-- A version of `equiv.mul_left a b⁻¹` that is defeq to `a / b`. -/
526530
@[to_additive /-" A version of `equiv.add_left a (-b)` that is defeq to `a - b`. "-/, simps]
527531
protected def div_left (a : G) : G ≃ G :=
Lines changed: 173 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,173 @@
1+
/-
2+
Copyright (c) 2021 Yury G. Kudryashov. All rights reserved.
3+
Released under Apache 2.0 license as described in the file LICENSE.
4+
Authors: Yury G. Kudryashov
5+
-/
6+
import measure_theory.group.arithmetic
7+
8+
/-!
9+
# (Scalar) multiplication and (vector) addition as measurable equivalences
10+
11+
In this file we define the following measurable equivalences:
12+
13+
* `measurable_equiv.smul`: if a group `G` acts on `α` by measurable maps, then each element `c : G`
14+
defines a measurable automorphism of `α`;
15+
* `measurable_equiv.vadd`: additive version of `measurable_equiv.smul`;
16+
* `measurable_equiv.smul₀`: if a group with zero `G` acts on `α` by measurable maps, then each
17+
nonzero element `c : G` defines a measurable automorphism of `α`;
18+
* `measurable_equiv.mul_left`: if `G` is a group with measurable multiplication, then left
19+
multiplication by `g : G` is a measurable automorphism of `G`;
20+
* `measurable_equiv.add_left`: additive version of `measurable_equiv.mul_left`;
21+
* `measurable_equiv.mul_right`: if `G` is a group with measurable multiplication, then right
22+
multiplication by `g : G` is a measurable automorphism of `G`;
23+
* `measurable_equiv.add_right`: additive version of `measurable_equiv.mul_right`;
24+
* `measurable_equiv.mul_left₀`, `measurable_equiv.mul_right₀`: versions of
25+
`measurable_equiv.mul_left` and `measurable_equiv.mul_right` for groups with zero;
26+
* `measurable_equiv.inv`, `measurable_equiv.inv₀`: `has_inv.inv` as a measurable automorphism
27+
of a group (or a group with zero);
28+
* `measurable_equiv.neg`: negation as a measurable automorphism of an additive group.
29+
30+
We also deduce that the corresponding maps are measurable embeddings.
31+
32+
## Tags
33+
34+
measurable, equivalence, group action
35+
-/
36+
37+
namespace measurable_equiv
38+
39+
variables {G G₀ α : Type*} [measurable_space G] [measurable_space G₀] [measurable_space α]
40+
[group G] [group_with_zero G₀] [mul_action G α] [mul_action G₀ α]
41+
[has_measurable_smul G α] [has_measurable_smul G₀ α]
42+
43+
/-- If a group `G` acts on `α` by measurable maps, then each element `c : G` defines a measurable
44+
automorphism of `α`. -/
45+
@[to_additive "If an additive group `G` acts on `α` by measurable maps, then each element `c : G`
46+
defines a measurable automorphism of `α`.", simps to_equiv apply { fully_applied := ff }]
47+
def smul (c : G) : α ≃ᵐ α :=
48+
{ to_equiv := mul_action.to_perm c,
49+
measurable_to_fun := measurable_const_smul c,
50+
measurable_inv_fun := measurable_const_smul c⁻¹ }
51+
52+
@[to_additive]
53+
lemma _root_.measurable_embedding_const_smul (c : G) : measurable_embedding ((•) c : α → α) :=
54+
(smul c).measurable_embedding
55+
56+
@[simp, to_additive]
57+
lemma symm_smul (c : G) : (smul c : α ≃ᵐ α).symm = smul c⁻¹ := ext rfl
58+
59+
/-- If a group with zero `G₀` acts on `α` by measurable maps, then each nonzero element `c : G₀`
60+
defines a measurable automorphism of `α` -/
61+
def smul₀ (c : G₀) (hc : c ≠ 0) : α ≃ᵐ α :=
62+
measurable_equiv.smul (units.mk0 c hc)
63+
64+
@[simp] lemma coe_smul₀ {c : G₀} (hc : c ≠ 0) : ⇑(smul₀ c hc : α ≃ᵐ α) = (•) c := rfl
65+
66+
@[simp] lemma symm_smul₀ {c : G₀} (hc : c ≠ 0) :
67+
(smul₀ c hc : α ≃ᵐ α).symm = smul₀ c⁻¹ (inv_ne_zero hc) :=
68+
ext rfl
69+
70+
lemma _root_.measurable_embedding_const_smul₀ {c : G₀} (hc : c ≠ 0) :
71+
measurable_embedding ((•) c : α → α) :=
72+
(smul₀ c hc).measurable_embedding
73+
74+
section mul
75+
76+
variables [has_measurable_mul G] [has_measurable_mul G₀]
77+
78+
/-- If `G` is a group with measurable multiplication, then left multiplication by `g : G` is a
79+
measurable automorphism of `G`. -/
80+
@[to_additive "If `G` is an additive group with measurable addition, then addition of `g : G`
81+
on the left is a measurable automorphism of `G`."]
82+
def mul_left (g : G) : G ≃ᵐ G := smul g
83+
84+
@[simp, to_additive] lemma coe_mul_left (g : G) : ⇑(mul_left g) = (*) g := rfl
85+
86+
@[simp, to_additive] lemma symm_mul_left (g : G) : (mul_left g).symm = mul_left g⁻¹ := ext rfl
87+
88+
@[simp, to_additive] lemma to_equiv_mul_left (g : G) :
89+
(mul_left g).to_equiv = equiv.mul_left g := rfl
90+
91+
@[to_additive]
92+
lemma _root_.measurable_embedding_mul_left (g : G) : measurable_embedding ((*) g) :=
93+
(mul_left g).measurable_embedding
94+
95+
/-- If `G` is a group with measurable multiplication, then right multiplication by `g : G` is a
96+
measurable automorphism of `G`. -/
97+
@[to_additive "If `G` is an additive group with measurable addition, then addition of `g : G`
98+
on the right is a measurable automorphism of `G`."]
99+
def mul_right (g : G) : G ≃ᵐ G :=
100+
{ to_equiv := equiv.mul_right g,
101+
measurable_to_fun := measurable_mul_const g,
102+
measurable_inv_fun := measurable_mul_const g⁻¹ }
103+
104+
@[to_additive]
105+
lemma _root_.measurable_embedding_mul_right (g : G) : measurable_embedding (λ x, x * g) :=
106+
(mul_right g).measurable_embedding
107+
108+
@[simp, to_additive] lemma coe_mul_right (g : G) : ⇑(mul_right g) = (λ x, x * g) := rfl
109+
110+
@[simp, to_additive] lemma symm_mul_right (g : G) : (mul_right g).symm = mul_right g⁻¹ := ext rfl
111+
112+
@[simp, to_additive] lemma to_equiv_mul_right (g : G) :
113+
(mul_right g).to_equiv = equiv.mul_right g := rfl
114+
115+
/-- If `G₀` is a group with zero with measurable multiplication, then left multiplication by a
116+
nonzero element `g : G₀` is a measurable automorphism of `G₀`. -/
117+
def mul_left₀ (g : G₀) (hg : g ≠ 0) : G₀ ≃ᵐ G₀ := smul₀ g hg
118+
119+
lemma _root_.measurable_embedding_mul_left₀ {g : G₀} (hg : g ≠ 0) : measurable_embedding ((*) g) :=
120+
(mul_left₀ g hg).measurable_embedding
121+
122+
@[simp] lemma coe_mul_left₀ {g : G₀} (hg : g ≠ 0) : ⇑(mul_left₀ g hg) = (*) g := rfl
123+
124+
@[simp] lemma symm_mul_left₀ {g : G₀} (hg : g ≠ 0) :
125+
(mul_left₀ g hg).symm = mul_left₀ g⁻¹ (inv_ne_zero hg) := ext rfl
126+
127+
@[simp] lemma to_equiv_mul_left₀ {g : G₀} (hg : g ≠ 0) :
128+
(mul_left₀ g hg).to_equiv = equiv.mul_left₀ g hg := rfl
129+
130+
/-- If `G₀` is a group with zero with measurable multiplication, then right multiplication by a
131+
nonzero element `g : G₀` is a measurable automorphism of `G₀`. -/
132+
def mul_right₀ (g : G₀) (hg : g ≠ 0) : G₀ ≃ᵐ G₀ :=
133+
{ to_equiv := equiv.mul_right₀ g hg,
134+
measurable_to_fun := measurable_mul_const g,
135+
measurable_inv_fun := measurable_mul_const g⁻¹ }
136+
137+
lemma _root_.measurable_embedding_mul_right₀ {g : G₀} (hg : g ≠ 0) :
138+
measurable_embedding (λ x, x * g) :=
139+
(mul_right₀ g hg).measurable_embedding
140+
141+
@[simp] lemma coe_mul_right₀ {g : G₀} (hg : g ≠ 0) : ⇑(mul_right₀ g hg) = λ x, x * g := rfl
142+
143+
@[simp] lemma symm_mul_right₀ {g : G₀} (hg : g ≠ 0) :
144+
(mul_right₀ g hg).symm = mul_right₀ g⁻¹ (inv_ne_zero hg) := ext rfl
145+
146+
@[simp] lemma to_equiv_mul_right₀ {g : G₀} (hg : g ≠ 0) :
147+
(mul_right₀ g hg).to_equiv = equiv.mul_right₀ g hg := rfl
148+
149+
end mul
150+
151+
variables (G G₀)
152+
153+
/-- Inversion as a measurable automorphism of a group. -/
154+
@[to_additive "Negation as a measurable automorphism of an additive group.",
155+
simps to_equiv apply { fully_applied := ff }]
156+
def inv [has_measurable_inv G] : G ≃ᵐ G :=
157+
{ to_equiv := equiv.inv G,
158+
measurable_to_fun := measurable_inv,
159+
measurable_inv_fun := measurable_inv }
160+
161+
/-- Inversion as a measurable automorphism of a group with zero. -/
162+
@[simps to_equiv apply { fully_applied := ff }]
163+
def inv₀ [has_measurable_inv G₀] : G₀ ≃ᵐ G₀ :=
164+
{ to_equiv := equiv.inv₀ G₀,
165+
measurable_to_fun := measurable_inv,
166+
measurable_inv_fun := measurable_inv }
167+
168+
variables {G G₀}
169+
170+
@[simp] lemma symm_inv [has_measurable_inv G] : (inv G).symm = inv G := rfl
171+
@[simp] lemma symm_inv₀ [has_measurable_inv G₀] : (inv₀ G₀).symm = inv₀ G₀ := rfl
172+
173+
end measurable_equiv

0 commit comments

Comments
 (0)