From 2f29e090f1dddb1a1c7a0f21b88d5e07d4bf8082 Mon Sep 17 00:00:00 2001 From: Eric Wieser Date: Fri, 6 Aug 2021 21:15:20 +0000 Subject: [PATCH] feat(group_action/defs): generalize faithful actions (#8555) MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit This generalizes the `faithful_mul_semiring_action` typeclass to a mixin typeclass `has_faithful_scalar`, and provides instances for some simple actions: * `has_faithful_scalar α α` (on cancellative monoids and monoids with zero) * `has_faithful_scalar (opposite α) α` * `has_faithful_scalar α (Π i, f i)` * `has_faithful_scalar (units A) B` * `has_faithful_scalar (equiv.perm α) α` * `has_faithful_scalar M (α × β)` * `has_faithful_scalar R (α →₀ M)` * `has_faithful_scalar S (polynomial R)` (generalized from an existing instance) * `has_faithful_scalar R (mv_polynomial σ S₁)` * `has_faithful_scalar R (monoid_algebra k G)` * `has_faithful_scalar R (add_monoid_algebra k G)` As well as retaining the one other existing instance * `faithful_mul_semiring_action ↥H E` where `H : subgroup (E ≃ₐ[F] E)` The lemmas taking `faithful_mul_semiring_action` as a typeclass argument have been converted to use the new typeclass, but no attempt has been made to weaken their other hypotheses. --- src/algebra/group_ring_action.lean | 14 ++--------- src/algebra/module/pi.lean | 16 +++++++++++++ src/algebra/monoid_algebra.lean | 8 +++++++ src/algebra/opposites.lean | 24 ++++++++++++++++++- src/algebra/polynomial/group_ring_action.lean | 9 ------- src/data/finsupp/basic.lean | 5 ++++ src/data/mv_polynomial/basic.lean | 3 +++ src/data/polynomial/basic.lean | 4 ++++ src/field_theory/fixed.lean | 11 +++++---- src/field_theory/galois.lean | 8 ++++--- src/group_theory/group_action/defs.lean | 16 +++++++++++++ src/group_theory/group_action/group.lean | 15 ++++++++++++ src/group_theory/group_action/prod.lean | 10 ++++++++ src/group_theory/group_action/units.lean | 4 ++++ 14 files changed, 117 insertions(+), 30 deletions(-) diff --git a/src/algebra/group_ring_action.lean b/src/algebra/group_ring_action.lean index 17fc0bda39f5e..744ee2eaa6945 100644 --- a/src/algebra/group_ring_action.lean +++ b/src/algebra/group_ring_action.lean @@ -38,11 +38,6 @@ class mul_semiring_action (M : Type u) [monoid M] (R : Type v) [semiring R] export mul_semiring_action (smul_one) -/-- Typeclass for faithful multiplicative actions by monoids on semirings. -/ -class faithful_mul_semiring_action (M : Type u) [monoid M] (R : Type v) [semiring R] - extends mul_semiring_action M R := -(eq_of_smul_eq_smul' : ∀ {m₁ m₂ : M}, (∀ r : R, m₁ • r = m₂ • r) → m₁ = m₂) - section semiring variables (M G : Type u) [monoid M] [group G] @@ -53,11 +48,6 @@ lemma smul_mul' [mul_semiring_action M R] (g : M) (x y : R) : g • (x * y) = (g • x) * (g • y) := mul_semiring_action.smul_mul g x y -variables {M} (R) -theorem eq_of_smul_eq_smul [faithful_mul_semiring_action M R] {m₁ m₂ : M} : - (∀ r : R, m₁ • r = m₂ • r) → m₁ = m₂ := -faithful_mul_semiring_action.eq_of_smul_eq_smul' - variables (M R) /-- Each element of the monoid defines a additive monoid homomorphism. -/ @@ -83,9 +73,9 @@ def mul_semiring_action.to_ring_hom [mul_semiring_action M R] (x : M) : R →+* map_mul' := smul_mul' x, .. distrib_mul_action.to_add_monoid_hom M R x } -theorem to_ring_hom_injective [faithful_mul_semiring_action M R] : +theorem to_ring_hom_injective [mul_semiring_action M R] [has_faithful_scalar M R] : function.injective (mul_semiring_action.to_ring_hom M R) := -λ m₁ m₂ h, eq_of_smul_eq_smul R $ λ r, ring_hom.ext_iff.1 h r +λ m₁ m₂ h, eq_of_smul_eq_smul $ λ r, ring_hom.ext_iff.1 h r /-- Each element of the group defines a semiring isomorphism. -/ def mul_semiring_action.to_semiring_equiv [mul_semiring_action G R] (x : G) : R ≃+* R := diff --git a/src/algebra/module/pi.lean b/src/algebra/module/pi.lean index aadeb77b47ef9..ed108f22d3d78 100644 --- a/src/algebra/module/pi.lean +++ b/src/algebra/module/pi.lean @@ -64,6 +64,22 @@ instance smul_comm_class'' {g : I → Type*} {h : I → Type*} [∀ i, smul_comm_class (f i) (g i) (h i)] : smul_comm_class (Π i, f i) (Π i, g i) (Π i, h i) := ⟨λ x y z, funext $ λ i, smul_comm (x i) (y i) (z i)⟩ +/-- If `f i` has a faithful scalar action for a given `i`, then so does `Π i, f i`. This is +not an instance as `i` cannot be inferred. -/ +lemma has_faithful_scalar_at {α : Type*} + [Π i, has_scalar α $ f i] [Π i, nonempty (f i)] (i : I) [has_faithful_scalar α (f i)] : + has_faithful_scalar α (Π i, f i) := +⟨λ x y h, eq_of_smul_eq_smul $ λ a : f i, begin + classical, + have := congr_fun (h $ function.update (λ j, classical.choice (‹Π i, nonempty (f i)› j)) i a) i, + simpa using this, +end⟩ + +instance has_faithful_scalar {α : Type*} + [nonempty I] [Π i, has_scalar α $ f i] [Π i, nonempty (f i)] [Π i, has_faithful_scalar α (f i)] : + has_faithful_scalar α (Π i, f i) := +let ⟨i⟩ := ‹nonempty I› in has_faithful_scalar_at i + instance mul_action (α) {m : monoid α} [Π i, mul_action α $ f i] : @mul_action α (Π i : I, f i) m := { smul := (•), diff --git a/src/algebra/monoid_algebra.lean b/src/algebra/monoid_algebra.lean index ee5fae320e9cf..fdeb59dbcb258 100644 --- a/src/algebra/monoid_algebra.lean +++ b/src/algebra/monoid_algebra.lean @@ -241,6 +241,10 @@ instance [semiring R] [semiring k] [module R k] : module R (monoid_algebra k G) := finsupp.module G k +instance [monoid R] [semiring k] [distrib_mul_action R k] [has_faithful_scalar R k] [nonempty G] : + has_faithful_scalar R (monoid_algebra k G) := +finsupp.has_faithful_scalar + instance [monoid R] [monoid S] [semiring k] [distrib_mul_action R k] [distrib_mul_action S k] [has_scalar R S] [is_scalar_tower R S k] : is_scalar_tower R S (monoid_algebra k G) := @@ -902,6 +906,10 @@ instance [monoid R] [semiring k] [distrib_mul_action R k] : distrib_mul_action R (add_monoid_algebra k G) := finsupp.distrib_mul_action G k +instance [monoid R] [semiring k] [distrib_mul_action R k] [has_faithful_scalar R k] [nonempty G] : + has_faithful_scalar R (add_monoid_algebra k G) := +finsupp.has_faithful_scalar + instance [semiring R] [semiring k] [module R k] : module R (add_monoid_algebra k G) := finsupp.module G k diff --git a/src/algebra/opposites.lean b/src/algebra/opposites.lean index d72fe5c9c8436..83a8536cce9d3 100644 --- a/src/algebra/opposites.lean +++ b/src/algebra/opposites.lean @@ -126,9 +126,21 @@ instance [mul_one_class α] : mul_one_class (opposite α) := instance [monoid α] : monoid (opposite α) := { .. opposite.semigroup α, .. opposite.mul_one_class α } +instance [right_cancel_monoid α] : left_cancel_monoid (opposite α) := +{ .. opposite.left_cancel_semigroup α, ..opposite.monoid α } + +instance [left_cancel_monoid α] : right_cancel_monoid (opposite α) := +{ .. opposite.right_cancel_semigroup α, ..opposite.monoid α } + +instance [cancel_monoid α] : cancel_monoid (opposite α) := +{ .. opposite.right_cancel_monoid α, ..opposite.left_cancel_monoid α } + instance [comm_monoid α] : comm_monoid (opposite α) := { .. opposite.monoid α, .. opposite.comm_semigroup α } +instance [cancel_comm_monoid α] : cancel_comm_monoid (opposite α) := +{ .. opposite.cancel_monoid α, ..opposite.comm_monoid α } + instance [has_inv α] : has_inv (opposite α) := { inv := λ x, op $ (unop x)⁻¹ } @@ -211,7 +223,7 @@ instance (R : Type*) [monoid R] [add_monoid α] [distrib_mul_action R α] : ..opposite.mul_action α R } /-- Like `monoid.to_mul_action`, but multiplies on the right. -/ -instance monoid.to_opposite_mul_action [monoid α] : mul_action (opposite α) α := +instance _root_.monoid.to_opposite_mul_action [monoid α] : mul_action (opposite α) α := { smul := λ c x, x * c.unop, one_smul := mul_one, mul_smul := λ x y r, (mul_assoc _ _ _).symm } @@ -222,6 +234,16 @@ example [monoid α] : monoid.to_mul_action (opposite α) = opposite.mul_action lemma op_smul_eq_mul [monoid α] {a a' : α} : op a • a' = a' * a := rfl +/-- `monoid.to_opposite_mul_action` is faithful on cancellative monoids. -/ +instance left_cancel_monoid.to_has_faithful_scalar [left_cancel_monoid α] : + has_faithful_scalar (opposite α) α := +⟨λ x y h, unop_injective $ mul_left_cancel (h 1)⟩ + +/-- `monoid.to_opposite_mul_action` is faithful on nontrivial cancellative monoids with zero. -/ +instance cancel_monoid_with_zero.to_has_faithful_opposite_scalar + [cancel_monoid_with_zero α] [nontrivial α] : has_faithful_scalar (opposite α) α := +⟨λ x y h, unop_injective $ mul_left_cancel' one_ne_zero (h 1)⟩ + @[simp] lemma op_zero [has_zero α] : op (0 : α) = 0 := rfl @[simp] lemma unop_zero [has_zero α] : unop (0 : αᵒᵖ) = 0 := rfl diff --git a/src/algebra/polynomial/group_ring_action.lean b/src/algebra/polynomial/group_ring_action.lean index b1d42107295c7..b952ae5e1c587 100644 --- a/src/algebra/polynomial/group_ring_action.lean +++ b/src/algebra/polynomial/group_ring_action.lean @@ -43,15 +43,6 @@ noncomputable instance [mul_semiring_action M R] : mul_semiring_action M (polyno smul_mul := λ m p q, (smul_eq_map R m).symm ▸ map_mul (mul_semiring_action.to_ring_hom M R m), ..polynomial.distrib_mul_action } -noncomputable instance [faithful_mul_semiring_action M R] : - faithful_mul_semiring_action M (polynomial R) := -{ eq_of_smul_eq_smul' := λ m₁ m₂ h, eq_of_smul_eq_smul R $ λ s, C_inj.1 $ - calc C (m₁ • s) - = m₁ • C s : (smul_C _ _).symm - ... = m₂ • C s : h (C s) - ... = C (m₂ • s) : smul_C _ _, - .. polynomial.mul_semiring_action M R } - variables {M R} variables [mul_semiring_action M R] diff --git a/src/data/finsupp/basic.lean b/src/data/finsupp/basic.lean index d410cb1815855..69eb132d3a489 100644 --- a/src/data/finsupp/basic.lean +++ b/src/data/finsupp/basic.lean @@ -2082,6 +2082,11 @@ Throughout this section, some `monoid` and `semiring` arguments are specified wi lemma smul_apply {_ : monoid R} [add_monoid M] [distrib_mul_action R M] (b : R) (v : α →₀ M) (a : α) : (b • v) a = b • (v a) := rfl +instance [monoid R] [nonempty α] [add_monoid M] [distrib_mul_action R M] [has_faithful_scalar R M] : + has_faithful_scalar R (α →₀ M) := +{ eq_of_smul_eq_smul := λ r₁ r₂ h, let ⟨a⟩ := ‹nonempty α› in eq_of_smul_eq_smul $ λ m : M, + by simpa using congr_fun (h (single a m)) a } + variables (α M) instance [monoid R] [add_monoid M] [distrib_mul_action R M] : distrib_mul_action R (α →₀ M) := diff --git a/src/data/mv_polynomial/basic.lean b/src/data/mv_polynomial/basic.lean index 605228dcf655e..c1864e2678a05 100644 --- a/src/data/mv_polynomial/basic.lean +++ b/src/data/mv_polynomial/basic.lean @@ -104,6 +104,9 @@ instance [comm_semiring R] : inhabited (mv_polynomial σ R) := ⟨0⟩ instance [monoid R] [comm_semiring S₁] [distrib_mul_action R S₁] : distrib_mul_action R (mv_polynomial σ S₁) := add_monoid_algebra.distrib_mul_action +instance [monoid R] [comm_semiring S₁] [distrib_mul_action R S₁] [has_faithful_scalar R S₁] : + has_faithful_scalar R (mv_polynomial σ S₁) := +add_monoid_algebra.has_faithful_scalar instance [semiring R] [comm_semiring S₁] [module R S₁] : module R (mv_polynomial σ S₁) := add_monoid_algebra.module instance [monoid R] [monoid S₁] [comm_semiring S₂] diff --git a/src/data/polynomial/basic.lean b/src/data/polynomial/basic.lean index d7d2c1932d089..492222974f757 100644 --- a/src/data/polynomial/basic.lean +++ b/src/data/polynomial/basic.lean @@ -132,6 +132,10 @@ instance {S} [monoid S] [distrib_mul_action S R] : distrib_mul_action S (polynom smul_add := by { rintros _ ⟨⟩ ⟨⟩, simp [smul_to_finsupp, add_to_finsupp] }, smul_zero := by { rintros _, simp [← zero_to_finsupp, smul_to_finsupp] } } +instance {S} [monoid S] [distrib_mul_action S R] [has_faithful_scalar S R] : + has_faithful_scalar S (polynomial R) := +{ eq_of_smul_eq_smul := λ s₁ s₂ h, eq_of_smul_eq_smul $ λ a : ℕ →₀ R, congr_arg to_finsupp (h ⟨a⟩) } + instance {S} [semiring S] [module S R] : module S (polynomial R) := { smul := (•), add_smul := by { rintros _ _ ⟨⟩, simp [smul_to_finsupp, add_to_finsupp, add_smul] }, diff --git a/src/field_theory/fixed.lean b/src/field_theory/fixed.lean index 21113bec8cc94..99724b2dfa091 100644 --- a/src/field_theory/fixed.lean +++ b/src/field_theory/fixed.lean @@ -295,18 +295,18 @@ namespace fixed_points /-- Embedding produced from a faithful action. -/ @[simps apply {fully_applied := ff}] def to_alg_hom (G : Type u) (F : Type v) [group G] [field F] - [faithful_mul_semiring_action G F] : G ↪ (F →ₐ[fixed_points.subfield G F] F) := + [mul_semiring_action G F] [has_faithful_scalar G F] : G ↪ (F →ₐ[fixed_points.subfield G F] F) := { to_fun := λ g, { commutes' := λ x, x.2 g, .. mul_semiring_action.to_ring_hom G F g }, inj' := λ g₁ g₂ hg, to_ring_hom_injective G F $ ring_hom.ext $ λ x, alg_hom.ext_iff.1 hg x, } lemma to_alg_hom_apply_apply {G : Type u} {F : Type v} [group G] [field F] - [faithful_mul_semiring_action G F] (g : G) (x : F) : + [mul_semiring_action G F] [has_faithful_scalar G F] (g : G) (x : F) : to_alg_hom G F g x = g • x := rfl theorem finrank_eq_card (G : Type u) (F : Type v) [group G] [field F] - [fintype G] [faithful_mul_semiring_action G F] : + [fintype G] [mul_semiring_action G F] [has_faithful_scalar G F] : finrank (fixed_points.subfield G F) F = fintype.card G := le_antisymm (fixed_points.finrank_le_card G F) $ calc fintype.card G @@ -316,7 +316,7 @@ calc fintype.card G ... = finrank (fixed_points.subfield G F) F : finrank_linear_map' _ _ _ theorem to_alg_hom_bijective (G : Type u) (F : Type v) [group G] [field F] - [fintype G] [faithful_mul_semiring_action G F] : + [fintype G] [mul_semiring_action G F] [has_faithful_scalar G F] : function.bijective (to_alg_hom G F) := begin rw fintype.bijective_iff_injective_and_card, @@ -330,7 +330,8 @@ end /-- Bijection between G and algebra homomorphisms that fix the fixed points -/ def to_alg_hom_equiv (G : Type u) (F : Type v) [group G] [field F] - [fintype G] [faithful_mul_semiring_action G F] : G ≃ (F →ₐ[fixed_points.subfield G F] F) := + [fintype G] [mul_semiring_action G F] [has_faithful_scalar G F] : + G ≃ (F →ₐ[fixed_points.subfield G F] F) := function.embedding.equiv_of_surjective (to_alg_hom G F) (to_alg_hom_bijective G F).2 end fixed_points diff --git a/src/field_theory/galois.lean b/src/field_theory/galois.lean index 6fbb6430b6d0f..06432892a5e07 100644 --- a/src/field_theory/galois.lean +++ b/src/field_theory/galois.lean @@ -170,15 +170,17 @@ variables (H : subgroup (E ≃ₐ[F] E)) (K : intermediate_field F E) namespace intermediate_field -instance subgroup_action : faithful_mul_semiring_action H E := +instance subgroup_action : mul_semiring_action H E := { smul := λ h x, h x, smul_zero := λ _, map_zero _, smul_add := λ _, map_add _, one_smul := λ _, rfl, smul_one := λ _, map_one _, mul_smul := λ _ _ _, rfl, - smul_mul := λ _, map_mul _, - eq_of_smul_eq_smul' := λ x y z, subtype.ext (alg_equiv.ext z) } + smul_mul := λ _, map_mul _ } + +instance : has_faithful_scalar H E := +{ eq_of_smul_eq_smul := λ x y z, subtype.ext (alg_equiv.ext z) } /-- The intermediate_field fixed by a subgroup -/ def fixed_field : intermediate_field F E := diff --git a/src/group_theory/group_action/defs.lean b/src/group_theory/group_action/defs.lean index 0fda7a16b15a8..9fd0788eae9d3 100644 --- a/src/group_theory/group_action/defs.lean +++ b/src/group_theory/group_action/defs.lean @@ -56,6 +56,22 @@ class has_scalar (M : Type*) (α : Type*) := (smul : M → α → α) infix ` +ᵥ `:65 := has_vadd.vadd infixr ` • `:73 := has_scalar.smul +/-- Typeclass for faithful actions. -/ +class has_faithful_vadd (G : Type*) (P : Type*) [has_vadd G P] : Prop := +(eq_of_vadd_eq_vadd : ∀ {g₁ g₂ : G}, (∀ p : P, g₁ +ᵥ p = g₂ +ᵥ p) → g₁ = g₂) + +/-- Typeclass for faithful actions. -/ +@[to_additive has_faithful_vadd] +class has_faithful_scalar (M : Type*) (α : Type*) [has_scalar M α] : Prop := +(eq_of_smul_eq_smul : ∀ {m₁ m₂ : M}, (∀ a : α, m₁ • a = m₂ • a) → m₁ = m₂) + +export has_faithful_scalar (eq_of_smul_eq_smul) has_faithful_vadd (eq_of_vadd_eq_vadd) + +@[to_additive] +lemma smul_left_injective' [has_scalar M α] [has_faithful_scalar M α] : + function.injective ((•) : M → α → α) := +λ m₁ m₂ h, has_faithful_scalar.eq_of_smul_eq_smul (congr_fun h) + /-- See also `monoid.to_mul_action` and `mul_zero_class.to_smul_with_zero`. -/ @[priority 910, to_additive] -- see Note [lower instance priority] instance has_mul.to_has_scalar (α : Type*) [has_mul α] : has_scalar α α := ⟨(*)⟩ diff --git a/src/group_theory/group_action/group.lean b/src/group_theory/group_action/group.lean index a60a4eb1bde5b..9dad4644d45f6 100644 --- a/src/group_theory/group_action/group.lean +++ b/src/group_theory/group_action/group.lean @@ -22,6 +22,12 @@ variables {α : Type u} {β : Type v} {γ : Type w} section mul_action +/-- `monoid.to_mul_action` is faithful on cancellative monoids. -/ +@[to_additive /-" `add_monoid.to_add_action` is faithful on additive cancellative monoids. "-/] +instance right_cancel_monoid.to_has_faithful_scalar [right_cancel_monoid α] : + has_faithful_scalar α α := +⟨λ x y h, mul_right_cancel (h 1)⟩ + section group variables [group α] [mul_action α β] @@ -62,6 +68,10 @@ instance mul_action.perm (α : Type*) : mul_action (equiv.perm α) α := @[simp] lemma equiv.perm.smul_def {α : Type*} (f : equiv.perm α) (a : α) : f • a = f a := rfl +/-- `mul_action.perm` is faithful. -/ +instance equiv.perm.has_faithful_scalar (α : Type*) : has_faithful_scalar (equiv.perm α) α := +⟨λ x y, equiv.ext⟩ + variables {α} {β} @[to_additive] lemma inv_smul_eq_iff {a : α} {x y : β} : a⁻¹ • x = y ↔ x = a • y := @@ -92,6 +102,11 @@ mul_action.injective g h end group +/-- `monoid.to_mul_action` is faithful on nontrivial cancellative monoids with zero. -/ +instance cancel_monoid_with_zero.to_has_faithful_scalar [cancel_monoid_with_zero α] [nontrivial α] : + has_faithful_scalar α α := +⟨λ x y h, mul_left_injective' one_ne_zero (h 1)⟩ + section gwz variables [group_with_zero α] [mul_action α β] diff --git a/src/group_theory/group_action/prod.lean b/src/group_theory/group_action/prod.lean index 6554ec81331aa..6a0d6ae833807 100644 --- a/src/group_theory/group_action/prod.lean +++ b/src/group_theory/group_action/prod.lean @@ -34,6 +34,16 @@ instance [has_scalar M N] [is_scalar_tower M N α] [is_scalar_tower M N β] : smul_comm_class M N (α × β) := { smul_comm := λ r s x, mk.inj_iff.mpr ⟨smul_comm _ _ _, smul_comm _ _ _⟩ } +@[to_additive has_faithful_vadd_left] +instance has_faithful_scalar_left [has_faithful_scalar M α] [nonempty β] : + has_faithful_scalar M (α × β) := +⟨λ x y h, let ⟨b⟩ := ‹nonempty β› in eq_of_smul_eq_smul $ λ a : α, by injection h (a, b)⟩ + +@[to_additive has_faithful_vadd_right] +instance has_faithful_scalar_right [nonempty α] [has_faithful_scalar M β] : + has_faithful_scalar M (α × β) := +⟨λ x y h, let ⟨a⟩ := ‹nonempty α› in eq_of_smul_eq_smul $ λ b : β, by injection h (a, b)⟩ + end @[to_additive] instance {m : monoid M} [mul_action M α] [mul_action M β] : mul_action M (α × β) := diff --git a/src/group_theory/group_action/units.lean b/src/group_theory/group_action/units.lean index 6f2510b3c19bc..f7c8e55e961c0 100644 --- a/src/group_theory/group_action/units.lean +++ b/src/group_theory/group_action/units.lean @@ -32,6 +32,10 @@ instance [monoid M] [has_scalar M α] : has_scalar (units M) α := lemma smul_def [monoid M] [has_scalar M α] (m : units M) (a : α) : m • a = (m : M) • a := rfl +@[to_additive] +instance [monoid M] [has_scalar M α] [has_faithful_scalar M α] : has_faithful_scalar (units M) α := +{ eq_of_smul_eq_smul := λ u₁ u₂ h, units.ext $ eq_of_smul_eq_smul h, } + @[to_additive] instance [monoid M] [mul_action M α] : mul_action (units M) α := { one_smul := (one_smul M : _),