feat(group_theory/group_action/units): group actions on and by units (#…

…7438)

This removes all the lemmas about `(u : α) • x` and `(↑u⁻¹ : α) • x` in favor of granting `units α` its very own `has_scalar` structure, along with providing the stronger variants to make it usable elsewhere.

This means that downstream code need only reason about `[group G] [mul_action G M]` instead of needing to handle groups and `units` separately.

The (multiplicative versions of the) removed and moved lemmas are:
* `units.inv_smul_smul` → `inv_smul_smul`
* `units.smul_inv_smul` → `smul_inv_smul`
* `units.smul_perm_hom`, `mul_action.to_perm` → `mul_action.to_perm_hom`
* `units.smul_perm` → `mul_action.to_perm`
* `units.smul_left_cancel` → `smul_left_cancel`
* `units.smul_eq_iff_eq_inv_smul` → `smul_eq_iff_eq_inv_smul`
* `units.smul_eq_zero` → `smul_eq_zero_iff_eq` (to avoid clashing with `smul_eq_zero`)
* `units.smul_ne_zero` → `smul_ne_zero_iff_ne`
* `homeomorph.smul_of_unit` → `homeomorph.smul` (the latter already existed, and the former was a special case)
* `units.measurable_const_smul_iff` → `measurable_const_smul_iff`
* `units.ae_measurable_const_smul_iff` → `ae_measurable_const_smul_iff`

The new lemmas are:

* `smul_eq_zero_iff_eq'`, a `group_with_zero` version of `smul_eq_zero_iff_eq`
* `smul_ne_zero_iff_ne'`, a `group_with_zero` version of `smul_ne_zero_iff_ne`
* `units.neg_smul`, a version of `neg_smul` for units. We don't currently have typeclasses about `neg` on objects without `+`.

We also end up needing some new typeclass instances downstream

* `units.measurable_space`
* `units.has_measurable_smul`
* `units.has_continuous_smul`

This goes on to remove lots of coercions from `alternating_map`, `matrix.det`, and some lie algebra stuff.
This makes the theorem statement cleaner, but occasionally requires rewriting through `units.smul_def` to add or remove the coercion.



Co-authored-by: Floris van Doorn <fpvdoorn@gmail.com>
Co-authored-by: Floris van Doorn <fpv@andrew.cmu.edu>

src/algebra/group_ring_action.lean

@@ -69,7 +69,7 @@ def distrib_mul_action.to_add_monoid_hom [distrib_mul_action M A] (x : M) : A 
 /-- Each element of the group defines an additive monoid isomorphism. -/
 def distrib_mul_action.to_add_equiv [distrib_mul_action G A] (x : G) : A ≃+ A :=
 { .. distrib_mul_action.to_add_monoid_hom G A x,
-  .. mul_action.to_perm G A x }
+  .. mul_action.to_perm_hom G A x }
 
 /-- Each element of the group defines an additive monoid homomorphism. -/
 def distrib_mul_action.hom_add_monoid_hom [distrib_mul_action M A] : M →* add_monoid.End A :=

src/algebra/lie/classical.lean

@@ -281,7 +281,7 @@ begin
   apply (skew_adjoint_matrices_lie_subalgebra_equiv (JD l R) (PD l R) (is_unit_PD l R)).trans,
   apply lie_equiv.of_eq,
   ext A,
-  rw [JD_transform, ← unit_of_invertible_val (2 : R), lie_subalgebra.mem_coe,
+  rw [JD_transform, ← unit_of_invertible_val (2 : R), ←units.smul_def, lie_subalgebra.mem_coe,
       mem_skew_adjoint_matrices_lie_subalgebra_unit_smul],
   refl,
 end
@@ -362,7 +362,7 @@ begin
     (matrix.reindex_alg_equiv (equiv.sum_assoc punit l l)) (matrix.transpose_reindex _ _)).trans,
   apply lie_equiv.of_eq,
   ext A,
-  rw [JB_transform, ← unit_of_invertible_val (2 : R), lie_subalgebra.mem_coe,
+  rw [JB_transform, ← unit_of_invertible_val (2 : R), ←units.smul_def, lie_subalgebra.mem_coe,
       lie_subalgebra.mem_coe, mem_skew_adjoint_matrices_lie_subalgebra_unit_smul],
   simpa [indefinite_diagonal_assoc],
 end

src/algebra/lie/skew_adjoint.lean

@@ -148,13 +148,13 @@ end
 rfl
 
 lemma mem_skew_adjoint_matrices_lie_subalgebra_unit_smul (u : units R) (J A : matrix n n R) :
-  A ∈ skew_adjoint_matrices_lie_subalgebra ((u : R) • J) ↔
+  A ∈ skew_adjoint_matrices_lie_subalgebra (u • J) ↔
   A ∈ skew_adjoint_matrices_lie_subalgebra J :=
 begin
-  change A ∈ skew_adjoint_matrices_submodule ((u : R) • J) ↔  A ∈ skew_adjoint_matrices_submodule J,
+  change A ∈ skew_adjoint_matrices_submodule (u • J) ↔ A ∈ skew_adjoint_matrices_submodule J,
   simp only [mem_skew_adjoint_matrices_submodule, matrix.is_skew_adjoint, matrix.is_adjoint_pair],
   split; intros h,
-  { simpa using congr_arg (λ B, (↑u⁻¹ : R) • B) h, },
+  { simpa using congr_arg (λ B, u⁻¹ • B) h, },
   { simp [h], },
 end
 

src/algebra/module/basic.lean

@@ -210,6 +210,9 @@ variables [ring R] [add_comm_group M] [module R M] (r s : R) (x y : M)
 @[simp] theorem neg_smul : -r • x = - (r • x) :=
 eq_neg_of_add_eq_zero (by rw [← add_smul, add_left_neg, zero_smul])
 
+@[simp] theorem units.neg_smul (u : units R) (x : M) : -u • x = - (u • x) :=
+by rw [units.smul_def, units.coe_neg, neg_smul, units.smul_def]
+
 variables (R)
 theorem neg_one_smul (x : M) : (-1 : R) • x = -x := by simp
 variables {R}
@@ -502,7 +505,7 @@ variables [division_ring R] [add_comm_group M] [module R M]
 
 @[priority 100] -- see note [lower instance priority]
 instance no_zero_smul_divisors.of_division_ring : no_zero_smul_divisors R M :=
-⟨λ c x h, or_iff_not_imp_left.2 $ λ hc, (units.mk0 c hc).smul_eq_zero.1 h⟩
+⟨λ c x h, or_iff_not_imp_left.2 $ λ hc, (smul_eq_zero_iff_eq' hc).1 h⟩
 
 end division_ring
 

src/algebra/module/linear_map.lean

@@ -261,6 +261,12 @@ instance compatible_smul.int_module
   case hn : n ih { simp [sub_smul, ih] }
 end⟩
 
+instance compatible_smul.units {R S : Type*}
+  [monoid R] [mul_action R M] [mul_action R M₂] [semiring S] [module S M] [module S M₂]
+  [compatible_smul M M₂ R S] :
+  compatible_smul M M₂ (units R) S :=
+⟨λ f c x, (compatible_smul.map_smul f (c : R) x : _)⟩
+
 end add_comm_group
 
 end linear_map

src/algebra/module/ordered.lean

@@ -98,7 +98,7 @@ begin
   refine { smul_lt_smul_of_pos := hlt', .. },
   intros a b c h hc,
   rcases (hR hc.ne') with ⟨c, rfl⟩,
-  rw [← c.inv_smul_smul a, ← c.inv_smul_smul b],
+  rw [← inv_smul_smul c a, ← inv_smul_smul c b],
   refine hlt' h (pos_of_mul_pos_left _ hc.le),
   simp only [c.mul_inv, zero_lt_one]
 end

src/group_theory/group_action/group.lean

@@ -9,139 +9,125 @@ import algebra.group_with_zero
 import data.equiv.mul_add
 import data.equiv.mul_add_aut
 import group_theory.perm.basic
+import group_theory.group_action.units
 
 /-!
 # Group actions applied to various types of group
 
-This file contains lemmas about `smul` on `units`, `group_with_zero`, and `group`.
+This file contains lemmas about `smul` on `group_with_zero`, and `group`.
 -/
 
 universes u v w
 variables {α : Type u} {β : Type v} {γ : Type w}
 
 section mul_action
 
-section units
-variables [monoid α] [mul_action α β]
+section group
+variables [group α] [mul_action α β]
+
+@[simp, to_additive] lemma inv_smul_smul (c : α) (x : β) : c⁻¹ • c • x = x :=
+by rw [smul_smul, mul_left_inv, one_smul]
 
-@[simp, to_additive] lemma units.inv_smul_smul (u : units α) (x : β) :
-  (↑u⁻¹:α) • (u:α) • x = x :=
-by rw [smul_smul, u.inv_mul, one_smul]
+@[simp, to_additive] lemma smul_inv_smul (c : α) (x : β) : c • c⁻¹ • x = x :=
+by rw [smul_smul, mul_right_inv, one_smul]
 
-@[simp, to_additive] lemma units.smul_inv_smul (u : units α) (x : β) :
-  (u:α) • (↑u⁻¹:α) • x = x :=
-by rw [smul_smul, u.mul_inv, one_smul]
+/-- Given an action of a group `α` on `β`, each `g : α` defines a permutation of `β`. -/
+@[to_additive] def mul_action.to_perm (a : α) : equiv.perm β :=
+⟨λ x, a • x, λ x, a⁻¹ • x, inv_smul_smul a, smul_inv_smul a⟩
 
-/-- If a monoid `α` acts on `β`, then each `u : units α` defines a permutation of `β`. -/
-@[to_additive] def units.smul_perm (u : units α) : equiv.perm β :=
-⟨λ x, (u:α) • x, λ x, (↑u⁻¹:α) • x, u.inv_smul_smul, u.smul_inv_smul⟩
+/-- Given an action of an additive group `α` on `β`, each `g : α` defines a permutation of `β`. -/
+add_decl_doc add_action.to_perm
 
-/-- If an additive monoid `α` acts on `β`, then each `u : add_units α` defines a permutation
-of `β`. -/
-add_decl_doc add_units.vadd_perm
+variables (α) (β)
 
-/-- If a monoid `α` acts on `β`, then each `u : units α` defines a permutation of `β`. -/
-def units.smul_perm_hom : units α →* equiv.perm β :=
-{ to_fun := units.smul_perm,
+/-- Given an action of a group `α` on a set `β`, each `g : α` defines a permutation of `β`. -/
+def mul_action.to_perm_hom : α →* equiv.perm β :=
+{ to_fun := mul_action.to_perm,
   map_one' := equiv.ext $ one_smul α,
   map_mul' := λ u₁ u₂, equiv.ext $ mul_smul (u₁:α) u₂ }
 
-/-- If an additive monoid `α` acts on `β`, then each `u : add_units α` defines a permutation
-of `β`. -/
-def add_units.vadd_perm_hom {M : Type*} [add_monoid M] [add_action M β] :
-  add_units M →+ additive (equiv.perm β) :=
-{ to_fun := λ u, additive.of_mul u.vadd_perm,
-  map_zero' := equiv.ext $ zero_vadd M,
-  map_add' := λ u₁ u₂, equiv.ext $ add_vadd (u₁:M) u₂ }
+/-- Given an action of a additive group `α` on a set `β`, each `g : α` defines a permutation of
+`β`. -/
+def add_action.to_perm_hom (α : Type*) [add_group α] [add_action α β] :
+  α →+ additive (equiv.perm β) :=
+{ to_fun := λ a, additive.of_mul $ add_action.to_perm a,
+  map_zero' := equiv.ext $ zero_vadd α,
+  map_add' := λ a₁ a₂, equiv.ext $ add_vadd a₁ a₂ }
+
+variables {α} {β}
+
+@[to_additive] lemma inv_smul_eq_iff {a : α} {x y : β} : a⁻¹ • x = y ↔ x = a • y :=
+(mul_action.to_perm a).symm_apply_eq
 
-@[simp, to_additive] lemma units.smul_left_cancel (u : units α) {x y : β} :
-  (u:α) • x = (u:α) • y ↔ x = y :=
-u.smul_perm.apply_eq_iff_eq
+@[to_additive] lemma eq_inv_smul_iff {a : α} {x y : β} : x = a⁻¹ • y ↔ a • x = y :=
+(mul_action.to_perm a).eq_symm_apply
+
+lemma smul_inv [group β] [smul_comm_class α β β] [is_scalar_tower α β β] (c : α) (x : β) :
+  (c • x)⁻¹ = c⁻¹ • x⁻¹  :=
+by rw [inv_eq_iff_mul_eq_one, smul_mul_smul, mul_right_inv, mul_right_inv, one_smul]
 
-@[to_additive] lemma units.smul_eq_iff_eq_inv_smul (u : units α) {x y : β} :
-  (u:α) • x = y ↔ x = (↑u⁻¹:α) • y :=
-u.smul_perm.apply_eq_iff_eq_symm_apply
+@[to_additive] protected lemma mul_action.bijective (g : α) : function.bijective (λ b : β, g • b) :=
+(mul_action.to_perm g).bijective
 
-@[to_additive] lemma is_unit.smul_left_cancel {a : α} (ha : is_unit a) {x y : β} :
-  a • x = a • y ↔ x = y :=
-let ⟨u, hu⟩ := ha in hu ▸ u.smul_left_cancel
+@[to_additive] protected lemma mul_action.injective (g : α) : function.injective (λ b : β, g • b) :=
+(mul_action.bijective g).injective
 
-end units
+@[to_additive] lemma smul_left_cancel (g : α) {x y : β} (h : g • x = g • y) : x = y :=
+mul_action.injective g h
+
+@[simp, to_additive] lemma smul_left_cancel_iff (g : α) {x y : β} : g • x = g • y ↔ x = y :=
+(mul_action.injective g).eq_iff
+
+@[to_additive] lemma smul_eq_iff_eq_inv_smul (g : α) {x y : β} :
+  g • x = y ↔ x = g⁻¹ • y :=
+(mul_action.to_perm g).apply_eq_iff_eq_symm_apply
+
+end group
 
 section gwz
 variables [group_with_zero α] [mul_action α β]
 
 @[simp]
 lemma inv_smul_smul' {c : α} (hc : c ≠ 0) (x : β) : c⁻¹ • c • x = x :=
-(units.mk0 c hc).inv_smul_smul x
+inv_smul_smul (units.mk0 c hc) x
 
 @[simp]
 lemma smul_inv_smul' {c : α} (hc : c ≠ 0) (x : β) : c • c⁻¹ • x = x :=
-(units.mk0 c hc).smul_inv_smul x
+smul_inv_smul (units.mk0 c hc) x
 
 lemma inv_smul_eq_iff' {a : α} (ha : a ≠ 0) {x y : β} : a⁻¹ • x = y ↔ x = a • y :=
-(units.mk0 a ha).smul_perm.symm_apply_eq
+(mul_action.to_perm (units.mk0 a ha)).symm_apply_eq
 
 lemma eq_inv_smul_iff' {a : α} (ha : a ≠ 0) {x y : β} : x = a⁻¹ • y ↔ a • x = y :=
-(units.mk0 a ha).smul_perm.eq_symm_apply
+(mul_action.to_perm (units.mk0 a ha)).eq_symm_apply
 
 end gwz
 
-section group
-variables [group α] [mul_action α β]
-
-@[simp, to_additive] lemma inv_smul_smul (c : α) (x : β) : c⁻¹ • c • x = x :=
-(to_units c).inv_smul_smul x
-
-@[simp, to_additive] lemma smul_inv_smul (c : α) (x : β) : c • c⁻¹ • x = x :=
-(to_units c).smul_inv_smul x
-
-@[to_additive] lemma inv_smul_eq_iff {a : α} {x y : β} : a⁻¹ • x = y ↔ x = a • y :=
-(to_units a).smul_perm.symm_apply_eq
-
-@[to_additive] lemma eq_inv_smul_iff {a : α} {x y : β} : x = a⁻¹ • y ↔ a • x = y :=
-(to_units a).smul_perm.eq_symm_apply
-
-lemma smul_inv [group β] [smul_comm_class α β β] [is_scalar_tower α β β] (c : α) (x : β) :
-  (c • x)⁻¹ = c⁻¹ • x⁻¹ :=
-by rw [inv_eq_iff_mul_eq_one, smul_mul_smul, mul_right_inv, mul_right_inv, one_smul]
-
-variables (α) (β)
-
-/-- Given an action of a group `α` on a set `β`, each `g : α` defines a permutation of `β`. -/
-def mul_action.to_perm : α →* equiv.perm β :=
-units.smul_perm_hom.comp to_units.to_monoid_hom
-
-variables {α} {β}
+end mul_action
 
-@[to_additive] protected lemma mul_action.bijective (g : α) : function.bijective (λ b : β, g • b) :=
-(to_units g).smul_perm.bijective
+section distrib_mul_action
 
-@[to_additive] protected lemma mul_action.injective (g : α) : function.injective (λ b : β, g • b) :=
-(mul_action.bijective g).injective
+section group
+variables [group α] [add_monoid β] [distrib_mul_action α β]
 
-@[to_additive] lemma smul_left_cancel (g : α) {x y : β} (h : g • x = g • y) : x = y :=
-mul_action.injective g h
+theorem smul_eq_zero_iff_eq (a : α) {x : β} : a • x = 0 ↔ x = 0 :=
+⟨λ h, by rw [← inv_smul_smul a x, h, smul_zero], λ h, h.symm ▸ smul_zero _⟩
 
-@[simp, to_additive] lemma smul_left_cancel_iff (g : α) {x y : β} : g • x = g • y ↔ x = y :=
-(mul_action.injective g).eq_iff
+theorem smul_ne_zero_iff_ne (a : α) {x : β} : a • x ≠ 0 ↔ x ≠ 0 :=
+not_congr $ smul_eq_zero_iff_eq a
 
 end group
 
-end mul_action
-
-section distrib_mul_action
-variables [monoid α] [add_monoid β] [distrib_mul_action α β]
+section gwz
+variables [group_with_zero α] [add_monoid β] [distrib_mul_action α β]
 
-theorem units.smul_eq_zero (u : units α) {x : β} : (u : α) • x = 0 ↔ x = 0 :=
-⟨λ h, by rw [← u.inv_smul_smul x, h, smul_zero], λ h, h.symm ▸ smul_zero _⟩
+theorem smul_eq_zero_iff_eq' {a : α} (ha : a ≠ 0) {x : β} : a • x = 0 ↔ x = 0 :=
+smul_eq_zero_iff_eq (units.mk0 a ha)
 
-theorem units.smul_ne_zero (u : units α) {x : β} : (u : α) • x ≠ 0 ↔ x ≠ 0 :=
-not_congr u.smul_eq_zero
+theorem smul_ne_zero_iff_ne' {a : α} (ha : a ≠ 0) {x : β} : a • x ≠ 0 ↔ x ≠ 0 :=
+smul_ne_zero_iff_ne (units.mk0 a ha)
 
-@[simp] theorem is_unit.smul_eq_zero {u : α} (hu : is_unit u) {x : β} :
-  u • x = 0 ↔ x = 0 :=
-exists.elim hu $ λ u hu, hu ▸ u.smul_eq_zero
+end gwz
 
 end distrib_mul_action
 
@@ -168,3 +154,25 @@ local attribute [instance] arrow_action
   map_mul' := by { intros, ext, simp only [mul_smul, mul_equiv.coe_mk, mul_aut.mul_apply] } }
 
 end arrow
+
+namespace is_unit
+
+section mul_action
+variables [monoid α] [mul_action α β]
+
+@[to_additive] lemma smul_left_cancel {a : α} (ha : is_unit a) {x y : β} :
+  a • x = a • y ↔ x = y :=
+let ⟨u, hu⟩ := ha in hu ▸ smul_left_cancel_iff u
+
+end mul_action
+
+section distrib_mul_action
+variables [monoid α] [add_monoid β] [distrib_mul_action α β]
+
+@[simp] theorem smul_eq_zero {u : α} (hu : is_unit u) {x : β} :
+  u • x = 0 ↔ x = 0 :=
+exists.elim hu $ λ u hu, hu ▸ smul_eq_zero_iff_eq u
+
+end distrib_mul_action
+
+end is_unit