From 2d26cc191b101f171248245eaca6552d8a5cfee2 Mon Sep 17 00:00:00 2001 From: Johan Commelin Date: Tue, 26 Mar 2019 11:48:07 +0100 Subject: [PATCH] refactor(*): unify group/monoid_action, use standard names, make semimodule extend action --- src/algebra/module.lean | 8 ++-- src/group_theory/group_action.lean | 74 ++++++++++++++---------------- src/group_theory/sylow.lean | 20 ++++---- src/ring_theory/algebra.lean | 8 ++-- 4 files changed, 52 insertions(+), 58 deletions(-) diff --git a/src/algebra/module.lean b/src/algebra/module.lean index e550b4e72a105..d863b8f703b11 100644 --- a/src/algebra/module.lean +++ b/src/algebra/module.lean @@ -23,11 +23,9 @@ variables {α : Type u} {β : Type v} {γ : Type w} {δ : Type x} (where `r : α` and `x : β`) with some natural associativity and distributivity axioms similar to those on a ring. -/ class semimodule (α : Type u) (β : Type v) [semiring α] - [add_comm_monoid β] extends has_scalar α β := + [add_comm_monoid β] extends action α β := (smul_add : ∀(r : α) (x y : β), r • (x + y) = r • x + r • y) (add_smul : ∀(r s : α) (x : β), (r + s) • x = r • x + s • x) -(mul_smul : ∀(r s : α) (x : β), (r * s) • x = r • s • x) -(one_smul : ∀x : β, (1 : α) • x = x) (zero_smul : ∀x : β, (0 : α) • x = 0) (smul_zero {} : ∀(r : α), r • (0 : β) = 0) @@ -37,10 +35,10 @@ include R theorem smul_add : r • (x + y) = r • x + r • y := semimodule.smul_add r x y theorem add_smul : (r + s) • x = r • x + s • x := semimodule.add_smul r s x -theorem mul_smul : (r * s) • x = r • s • x := semimodule.mul_smul r s x +theorem mul_smul : (r * s) • x = r • s • x := action.mul_smul r s x @[simp] theorem smul_zero : r • (0 : β) = 0 := semimodule.smul_zero r variables (α) -@[simp] theorem one_smul : (1 : α) • x = x := semimodule.one_smul α x +@[simp] theorem one_smul : (1 : α) • x = x := action.one_smul α x @[simp] theorem zero_smul : (0 : α) • x = 0 := semimodule.zero_smul α x lemma smul_smul : r • s • x = (r * s) • x := (mul_smul _ _ _).symm diff --git a/src/group_theory/group_action.lean b/src/group_theory/group_action.lean index 5fe4bb2811aa5..8e7910513dfec 100644 --- a/src/group_theory/group_action.lean +++ b/src/group_theory/group_action.lean @@ -13,13 +13,15 @@ class has_scalar (α : Type u) (γ : Type v) := (smul : α → γ → γ) infixr ` • `:73 := has_scalar.smul -class monoid_action (α : Type u) (β : Type v) [monoid α] extends has_scalar α β := -(one : ∀ b : β, (1 : α) • b = b) -(mul : ∀ (x y : α) (b : β), (x * y) • b = x • y • b) +class action (α : Type u) (β : Type v) [monoid α] extends has_scalar α β := +(one_smul : ∀ b : β, (1 : α) • b = b) +(mul_smul : ∀ (x y : α) (b : β), (x * y) • b = x • y • b) -namespace monoid_action +namespace action -variables (α) [monoid α] [monoid_action α β] +variables (α) [monoid α] [action α β] + +attribute [simp] one_smul def orbit (b : β) := set.range (λ x : α, x • b) @@ -32,7 +34,7 @@ iff.rfl ⟨x, rfl⟩ @[simp] lemma mem_orbit_self (b : β) : b ∈ orbit α b := -⟨1, by simp [monoid_action.one]⟩ +⟨1, by simp [action.one_smul]⟩ instance orbit_fintype (b : β) [fintype α] [decidable_eq β] : fintype (orbit α b) := set.fintype_range _ @@ -62,33 +64,31 @@ lemma mem_fixed_points' {b : β} : b ∈ fixed_points α β ↔ λ h b, mem_stabilizer_iff.2 (h _ (mem_orbit _ _))⟩ def comp_hom [monoid γ] (g : γ → α) [is_monoid_hom g] : - monoid_action γ β := + action γ β := { smul := λ x b, (g x) • b, - one := by simp [is_monoid_hom.map_one g, monoid_action.one], - mul := by simp [is_monoid_hom.map_mul g, monoid_action.mul] } - -end monoid_action + one_smul := by simp [is_monoid_hom.map_one g, action.one_smul], + mul_smul := by simp [is_monoid_hom.map_mul g, action.mul_smul] } -class group_action (α : Type u) (β : Type v) [group α] extends monoid_action α β +end action -namespace group_action -variables [group α] [group_action α β] +namespace action +variables [group α] [action α β] section -open monoid_action quotient_group +open action quotient_group variables (α) (β) def to_perm (g : α) : equiv.perm β := { to_fun := (•) g, inv_fun := (•) g⁻¹, - left_inv := λ a, by rw [← monoid_action.mul, inv_mul_self, monoid_action.one], - right_inv := λ a, by rw [← monoid_action.mul, mul_inv_self, monoid_action.one] } + left_inv := λ a, by rw [← action.mul_smul, inv_mul_self, action.one_smul], + right_inv := λ a, by rw [← action.mul_smul, mul_inv_self, action.one_smul] } variables {α} {β} instance : is_group_hom (to_perm α β) := -{ mul := λ x y, equiv.ext _ _ (λ a, monoid_action.mul x y a) } +{ mul := λ x y, equiv.ext _ _ (λ a, action.mul_smul x y a) } lemma bijective (g : α) : function.bijective (λ b : β, g • b) := (to_perm α β g).bijective @@ -97,25 +97,21 @@ lemma orbit_eq_iff {a b : β} : orbit α a = orbit α b ↔ a ∈ orbit α b:= ⟨λ h, h ▸ mem_orbit_self _, λ ⟨x, (hx : x • b = a)⟩, set.ext (λ c, ⟨λ ⟨y, (hy : y • a = c)⟩, ⟨y * x, - show (y * x) • b = c, by rwa [monoid_action.mul, hx]⟩, + show (y * x) • b = c, by rwa [action.mul_smul, hx]⟩, λ ⟨y, (hy : y • b = c)⟩, ⟨y * x⁻¹, show (y * x⁻¹) • a = c, by conv {to_rhs, rw [← hy, ← mul_one y, ← inv_mul_self x, ← mul_assoc, - monoid_action.mul, hx]}⟩⟩)⟩ + action.mul_smul, hx]}⟩⟩)⟩ instance (b : β) : is_subgroup (stabilizer α b) := -{ one_mem := monoid_action.one _ _, +{ one_mem := action.one_smul _ _, mul_mem := λ x y (hx : x • b = b) (hy : y • b = b), - show (x * y) • b = b, by rw monoid_action.mul; simp *, + show (x * y) • b = b, by rw action.mul_smul; simp *, inv_mem := λ x (hx : x • b = b), show x⁻¹ • b = b, - by rw [← hx, ← monoid_action.mul, inv_mul_self, monoid_action.one, hx] } + by rw [← hx, ← action.mul_smul, inv_mul_self, action.one_smul, hx] } -variables (β) -def comp_hom [group γ] (g : γ → α) [is_group_hom g] : - group_action γ β := { ..monoid_action.comp_hom β g } - -variables (α) +variables (α) (β) def orbit_rel : setoid β := { r := λ a b, a ∈ orbit α b, @@ -131,19 +127,19 @@ noncomputable def orbit_equiv_quotient_stabilizer (b : β) : equiv.symm (@equiv.of_bijective _ _ (λ x : quotient (stabilizer α b), quotient.lift_on' x (λ x, (⟨x • b, mem_orbit _ _⟩ : orbit α b)) - (λ g h (H : _ = _), subtype.eq $ (group_action.bijective (g⁻¹)).1 + (λ g h (H : _ = _), subtype.eq $ (action.bijective (g⁻¹)).1 $ show g⁻¹ • (g • b) = g⁻¹ • (h • b), - by rw [← monoid_action.mul, ← monoid_action.mul, - H, inv_mul_self, monoid_action.one])) + by rw [← action.mul_smul, ← action.mul_smul, + H, inv_mul_self, action.one_smul])) ⟨λ g h, quotient.induction_on₂' g h (λ g h H, quotient.sound' $ have H : g • b = h • b := subtype.mk.inj H, show (g⁻¹ * h) • b = b, - by rw [monoid_action.mul, ← H, ← monoid_action.mul, inv_mul_self, monoid_action.one]), + by rw [action.mul_smul, ← H, ← action.mul_smul, inv_mul_self, action.one_smul]), λ ⟨b, ⟨g, hgb⟩⟩, ⟨g, subtype.eq hgb⟩⟩) end -open quotient_group monoid_action is_subgroup +open quotient_group action is_subgroup def mul_left_cosets (H : set α) [is_subgroup H] (x : α) (y : quotient H) : quotient H := @@ -151,15 +147,15 @@ quotient.lift_on' y (λ y, quotient_group.mk ((x : α) * y)) (λ a b (hab : _ ∈ H), quotient_group.eq.2 (by rwa [mul_inv_rev, ← mul_assoc, mul_assoc (a⁻¹), inv_mul_self, mul_one])) -instance (H : set α) [is_subgroup H] : group_action α (quotient H) := +instance (H : set α) [is_subgroup H] : action α (quotient H) := { smul := mul_left_cosets H, - one := λ a, quotient.induction_on' a (λ a, quotient_group.eq.2 + one_smul := λ a, quotient.induction_on' a (λ a, quotient_group.eq.2 (by simp [is_submonoid.one_mem])), - mul := λ x y a, quotient.induction_on' a (λ a, quotient_group.eq.2 + mul_smul := λ x y a, quotient.induction_on' a (λ a, quotient_group.eq.2 (by simp [mul_inv_rev, is_submonoid.one_mem, mul_assoc])) } instance mul_left_cosets_comp_subtype_val (H I : set α) [is_subgroup H] [is_subgroup I] : - group_action I (quotient H) := -group_action.comp_hom (quotient H) (subtype.val : I → α) + action I (quotient H) := +action.comp_hom (quotient H) (subtype.val : I → α) -end group_action +end action diff --git a/src/group_theory/sylow.lean b/src/group_theory/sylow.lean index 59f6eaef61c13..53823acab3dea 100644 --- a/src/group_theory/sylow.lean +++ b/src/group_theory/sylow.lean @@ -6,15 +6,15 @@ Authors: Chris Hughes import group_theory.group_action group_theory.quotient_group import group_theory.order_of_element data.zmod.basic algebra.pi_instances -open equiv fintype finset group_action monoid_action function +open equiv fintype finset action function open equiv.perm is_subgroup list quotient_group universes u v w variables {G : Type u} {α : Type v} {β : Type w} [group G] local attribute [instance, priority 0] subtype.fintype set_fintype classical.prop_decidable -namespace group_action -variables [group_action G α] +namespace action +variables [action G α] lemma mem_fixed_points_iff_card_orbit_eq_one {a : α} [fintype (orbit G a)] : a ∈ fixed_points G α ↔ card (orbit G a) = 1 := @@ -58,7 +58,7 @@ begin end ... = _ : by simp; refl -end group_action +end action lemma quotient_group.card_preimage_mk [fintype G] (s : set G) [is_subgroup s] (t : set (quotient s)) : fintype.card (quotient_group.mk ⁻¹' t) = @@ -98,11 +98,11 @@ def rotate_vectors_prod_eq_one (G : Type*) [group G] (n : ℕ+) (m : multiplicat (v : vectors_prod_eq_one G n) : vectors_prod_eq_one G n := ⟨⟨v.1.to_list.rotate m.1, by simp⟩, prod_rotate_eq_one_of_prod_eq_one v.2 _⟩ -instance rotate_vectors_prod_eq_one.is_group_action (n : ℕ+) : - group_action (multiplicative (zmod n)) (vectors_prod_eq_one G n) := +instance rotate_vectors_prod_eq_one.action (n : ℕ+) : + action (multiplicative (zmod n)) (vectors_prod_eq_one G n) := { smul := (rotate_vectors_prod_eq_one G n), - one := λ v, subtype.eq $ vector.eq _ _ $ rotate_zero v.1.to_list, - mul := λ a b ⟨⟨v, hv₁⟩, hv₂⟩, subtype.eq $ vector.eq _ _ $ + one_smul := λ v, subtype.eq $ vector.eq _ _ $ rotate_zero v.1.to_list, + mul_smul := λ a b ⟨⟨v, hv₁⟩, hv₂⟩, subtype.eq $ vector.eq _ _ $ show v.rotate ((a + b : zmod n).val) = list.rotate (list.rotate v (b.val)) (a.val), by rw [zmod.add_val, rotate_rotate, ← rotate_mod _ (b.1 + a.1), add_comm, hv₁] } @@ -128,7 +128,7 @@ have hcard : card (vectors_prod_eq_one G (n + 1)) = card G ^ (n : ℕ), set.card_range_of_injective (mk_vector_prod_eq_one_inj _), card_vector], have hzmod : fintype.card (multiplicative (zmod p')) = (p' : ℕ) ^ 1 := (nat.pow_one p').symm ▸ card_fin _, -have hmodeq : _ = _ := @group_action.card_modeq_card_fixed_points +have hmodeq : _ = _ := @action.card_modeq_card_fixed_points (multiplicative (zmod p')) (vectors_prod_eq_one G p') _ _ _ _ _ _ 1 hp hzmod, have hdvdcard : p ∣ fintype.card (vectors_prod_eq_one G (n + 1)) := calc p ∣ card G ^ 1 : by rwa nat.pow_one @@ -157,7 +157,7 @@ let ⟨a, ha⟩ := this in (hp.2 _ (order_of_dvd_of_pow_eq_one this)).resolve_left (λ h, ha1 (order_of_eq_one_iff.1 h))⟩ -open is_subgroup is_submonoid is_group_hom group_action +open is_subgroup is_submonoid is_group_hom action lemma mem_fixed_points_mul_left_cosets_iff_mem_normalizer {H : set G} [is_subgroup H] [fintype H] {x : G} : (x : quotient H) ∈ fixed_points H (quotient H) ↔ x ∈ normalizer H := diff --git a/src/ring_theory/algebra.lean b/src/ring_theory/algebra.lean index 232c77ff93388..a3e5e48601f6d 100644 --- a/src/ring_theory/algebra.lean +++ b/src/ring_theory/algebra.lean @@ -381,10 +381,10 @@ instance algebra : algebra R S := by rw algebra.smul_def; exact @@is_submonoid.mul_mem _ S.2.2 (S.3 ⟨c, rfl⟩) x.2⟩, smul_add := λ c x y, subtype.eq $ by apply _inst_3.1.1.2, add_smul := λ c x y, subtype.eq $ by apply _inst_3.1.1.3, - mul_smul := λ c x y, subtype.eq $ by apply _inst_3.1.1.4, - one_smul := λ x, subtype.eq $ by apply _inst_3.1.1.5, - zero_smul := λ x, subtype.eq $ by apply _inst_3.1.1.6, - smul_zero := λ x, subtype.eq $ by apply _inst_3.1.1.7, + mul_smul := λ c x y, subtype.eq $ by simp [mul_smul], + one_smul := λ x, subtype.eq $ by simp [one_smul], + zero_smul := λ x, subtype.eq $ by apply _inst_3.1.1.4, + smul_zero := λ x, subtype.eq $ by apply _inst_3.1.1.5, to_fun := λ r, ⟨algebra_map A r, S.range_le ⟨r, rfl⟩⟩, hom := ⟨subtype.eq $ algebra.map_one R A, λ x y, subtype.eq $ algebra.map_mul A x y, λ x y, subtype.eq $ algebra.map_add A x y⟩,