refactor(module_action): bundle and introduce notation

src/algebra/module.lean

@@ -6,16 +6,16 @@ Authors: Nathaniel Thomas, Jeremy Avigad, Johannes Hölzl, Mario Carneiro
 Modules over a ring.
 -/
 
-import algebra.ring algebra.big_operators group_theory.subgroup
+import algebra.ring algebra.big_operators group_theory.subgroup group_theory.group_action
 open function
 
 universes u v w x
 variables {α : Type u} {β : Type v} {γ : Type w} {δ : Type x}
 
-/-- Typeclass for types with a scalar multiplication operation, denoted `•` (`\bu`) -/
-class has_scalar (α : Type u) (γ : Type v) := (smul : α → γ → γ)
+-- /-- Typeclass for types with a scalar multiplication operation, denoted `•` (`\bu`) -/
+-- class has_scalar (α : Type u) (γ : Type v) := (smul : α → γ → γ)
 
-infixr ` • `:73 := has_scalar.smul
+-- infixr ` • `:73 := has_scalar.smul
 
 /-- A semimodule is a generalization of vector spaces to a scalar semiring.
   It consists of a scalar semiring `α` and an additive monoid of "vectors" `β`,

src/group_theory/group_action.lean

@@ -8,137 +8,158 @@ import data.set.finite group_theory.coset
 universes u v w
 variables {α : Type u} {β : Type v} {γ : Type w}
 
-class is_monoid_action [monoid α] (f : α → β → β) : Prop :=
-(one : ∀ a : β, f (1 : α) a = a)
-(mul : ∀ (x y : α) (a : β), f (x * y) a = f x (f y a))
+/-- Typeclass for types with a scalar multiplication operation, denoted `•` (`\bu`) -/
+class has_scalar (α : Type u) (γ : Type v) := (smul : α → γ → γ)
 
-namespace is_monoid_action
+infixr ` • `:73 := has_scalar.smul
 
-variables [monoid α] (f : α → β → β) [is_monoid_action f]
+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)
 
-def orbit (a : β) := set.range (λ x : α, f x a)
+namespace monoid_action
 
-@[simp] lemma mem_orbit_iff {f : α → β → β} [is_monoid_action f] {a b : β} :
-  b ∈ orbit f a ↔ ∃ x : α, f x a = b :=
+variables (α) [monoid α] [monoid_action α β]
+
+def orbit (b : β) := set.range (λ x : α, x • b)
+
+variable {α}
+
+@[simp] lemma mem_orbit_iff {b₁ b₂ : β} : b₂ ∈ orbit α b₁ ↔ ∃ x : α, x • b₁ = b₂ :=
 iff.rfl
 
-@[simp] lemma mem_orbit (a : β) (x : α) :
-  f x a ∈ orbit f a :=
+@[simp] lemma mem_orbit (b : β) (x : α) : x • b ∈ orbit α b :=
 ⟨x, rfl⟩
 
-@[simp] lemma mem_orbit_self (a : β) :
-  a ∈ orbit f a :=
-⟨1, show f 1 a = a, by simp [is_monoid_action.one f]⟩
+@[simp] lemma mem_orbit_self (b : β) : b ∈ orbit α b :=
+⟨1, by simp [monoid_action.one]⟩
 
-instance orbit_fintype (a : β) [fintype α] [decidable_eq β] :
-  fintype (orbit f a) := set.fintype_range _
+instance orbit_fintype (b : β) [fintype α] [decidable_eq β] :
+  fintype (orbit α b) := set.fintype_range _
 
-def stabilizer (a : β) : set α :=
-{x : α | f x a = a}
+variable (α)
 
-@[simp] lemma mem_stabilizer_iff {f : α → β → β} [is_monoid_action f] {a : β} {x : α} :
-  x ∈ stabilizer f a ↔ f x a = a :=
-iff.rfl
+def stabilizer (b : β) : set α :=
+{x : α | x • b = b}
+
+variable {α}
+
+@[simp] lemma mem_stabilizer_iff {b : β} {x : α} :
+  x ∈ stabilizer α b ↔ x • b = b := iff.rfl
 
-def fixed_points : set β := {a : β | ∀ x, x ∈ stabilizer f a}
+variables (α) (β)
 
-@[simp] lemma mem_fixed_points {f : α → β → β} [is_monoid_action f] {a : β} :
-  a ∈ fixed_points f ↔ ∀ x : α, f x a = a := iff.rfl
+def fixed_points : set β := {b : β | ∀ x, x ∈ stabilizer α b}
 
-lemma mem_fixed_points' {f : α → β → β} [is_monoid_action f] {a : β} : a ∈ fixed_points f ↔
-  (∀ b, b ∈ orbit f a → b = a) :=
+variables {α} (β)
+
+@[simp] lemma mem_fixed_points {b : β} :
+  b ∈ fixed_points α β ↔ ∀ x : α, x • b = b := iff.rfl
+
+lemma mem_fixed_points' {b : β} : b ∈ fixed_points α β ↔
+  (∀ b', b' ∈ orbit α b → b' = b) :=
 ⟨λ h b h₁, let ⟨x, hx⟩ := mem_orbit_iff.1 h₁ in hx ▸ h x,
-λ h b, mem_stabilizer_iff.2 (h _ (mem_orbit _ _ _))⟩
+λ h b, mem_stabilizer_iff.2 (h _ (mem_orbit _ _))⟩
 
-lemma comp_hom [group γ] (f : α → β → β) [is_monoid_action f] (g : γ → α) [is_monoid_hom g] :
-  is_monoid_action (f ∘ g) :=
-{ one := by simp [is_monoid_hom.map_one g, is_monoid_action.one f],
-  mul := by simp [is_monoid_hom.map_mul g, is_monoid_action.mul f] }
+def comp_hom [monoid γ] (g : γ → α) [is_monoid_hom g] :
+  monoid_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 is_monoid_action
+end monoid_action
 
-class is_group_action [group α] (f : α → β → β) extends is_monoid_action f : Prop
+class group_action (α : Type u) (β : Type v) [group α] extends monoid_action α β
 
-namespace is_group_action
-variables [group α]
+namespace group_action
+variables [group α] [group_action α β]
 
 section
-variables (f : α → β → β) [is_group_action f]
-open is_monoid_action quotient_group
+open monoid_action quotient_group
+
+variables (α) (β)
 
 def to_perm (g : α) : equiv.perm β :=
-{ to_fun := f g,
-  inv_fun := f g⁻¹,
-  left_inv := λ a, by rw [← is_monoid_action.mul f, inv_mul_self, is_monoid_action.one f],
-  right_inv := λ a, by rw [← is_monoid_action.mul f, mul_inv_self, is_monoid_action.one f] }
-
-instance : is_group_hom (to_perm f) :=
-{ mul := λ x y, equiv.ext _ _ (λ a, is_monoid_action.mul f x y a) }
-
-lemma bijective (g : α) : function.bijective (f g) :=
-(to_perm f g).bijective
-
-lemma orbit_eq_iff {f : α → β → β} [is_monoid_action f] {a b : β} :
-   orbit f a = orbit f b ↔ a ∈ orbit f b:=
-⟨λ h, h ▸ mem_orbit_self _ _,
-λ ⟨x, (hx : f x b = a)⟩, set.ext (λ c, ⟨λ ⟨y, (hy : f y a = c)⟩, ⟨y * x,
-  show f (y * x) b = c, by rwa [is_monoid_action.mul f, hx]⟩,
-  λ ⟨y, (hy : f y b = c)⟩, ⟨y * x⁻¹,
-    show f (y * x⁻¹) a = c, by
+{ 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] }
+
+variables {α} {β}
+
+instance : is_group_hom (to_perm α β) :=
+{ mul := λ x y, equiv.ext _ _ (λ a, monoid_action.mul x y a) }
+
+lemma bijective (g : α) : function.bijective (λ b : β, g • b) :=
+(to_perm α β g).bijective
+
+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]⟩,
+  λ ⟨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,
-        is_monoid_action.mul f, hx]}⟩⟩)⟩
+        monoid_action.mul, hx]}⟩⟩)⟩
 
-instance (a : β) : is_subgroup (stabilizer f a) :=
-{ one_mem := is_monoid_action.one _ _,
-  mul_mem := λ x y (hx : f x a = a) (hy : f y a = a),
-    show f (x * y) a = a, by rw is_monoid_action.mul f; simp *,
-  inv_mem := λ x (hx : f x a = a), show f x⁻¹ a = a,
-    by rw [← hx, ← is_monoid_action.mul f, inv_mul_self, is_monoid_action.one f, hx] }
+instance (b : β) : is_subgroup (stabilizer α b) :=
+{ one_mem := monoid_action.one _ _,
+  mul_mem := λ x y (hx : x • b = b) (hy : y • b = b),
+    show (x * y) • b = b, by rw monoid_action.mul; 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] }
 
-lemma comp_hom [group γ] (f : α → β → β) [is_group_action f] (g : γ → α) [is_group_hom g] :
-  is_group_action (f ∘ g) := { ..is_monoid_action.comp_hom f g }
+variables (β)
+
+def comp_hom [group γ] (g : γ → α) [is_group_hom g] :
+  group_action γ β := { ..monoid_action.comp_hom β g }
+
+variables (α)
 
 def orbit_rel : setoid β :=
-{ r := λ a b, a ∈ orbit f b,
-  iseqv := ⟨mem_orbit_self f, λ a b, by simp [orbit_eq_iff.symm, eq_comm],
+{ r := λ a b, a ∈ orbit α b,
+  iseqv := ⟨mem_orbit_self, λ a b, by simp [orbit_eq_iff.symm, eq_comm],
     λ a b, by simp [orbit_eq_iff.symm, eq_comm] {contextual := tt}⟩ }
 
+variables {β}
+
 open quotient_group
 
-noncomputable def orbit_equiv_quotient_stabilizer (a : β) :
-  orbit f a ≃ quotient (stabilizer f a) :=
+noncomputable def orbit_equiv_quotient_stabilizer (b : β) :
+  orbit α b ≃ quotient (stabilizer α b) :=
 equiv.symm (@equiv.of_bijective _ _
-  (λ x : quotient (stabilizer f a), quotient.lift_on' x
-    (λ x, (⟨f x a, mem_orbit _ _ _⟩ : orbit f a))
-    (λ g h (H : _ = _), subtype.eq $ (is_group_action.bijective f (g⁻¹)).1
-      $ show f g⁻¹ (f g a) = f g⁻¹ (f h a),
-      by rw [← is_monoid_action.mul f, ← is_monoid_action.mul f,
-        H, inv_mul_self, is_monoid_action.one f]))
+  (λ 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
+      $ show g⁻¹ • (g • b) = g⁻¹ • (h • b),
+      by rw [← monoid_action.mul, ← monoid_action.mul,
+        H, inv_mul_self, monoid_action.one]))
 ⟨λ g h, quotient.induction_on₂' g h (λ g h H, quotient.sound' $
-  have H : f g a = f h a := subtype.mk.inj H,
-  show f (g⁻¹ * h) a = a,
-  by rw [is_monoid_action.mul f, ← H, ← is_monoid_action.mul f, inv_mul_self,
-    is_monoid_action.one f]),
+  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]),
   λ ⟨b, ⟨g, hgb⟩⟩, ⟨g, subtype.eq hgb⟩⟩)
 
 end
 
-open quotient_group  is_monoid_action is_subgroup
+open quotient_group  monoid_action is_subgroup
 
 def mul_left_cosets (H : set α) [is_subgroup H]
   (x : α) (y : quotient H) : quotient H :=
 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] : is_group_action (mul_left_cosets H) :=
-{ one := λ a, quotient.induction_on' a (λ a, quotient_group.eq.2
+instance (H : set α) [is_subgroup H] : group_action α (quotient H) :=
+{ smul := mul_left_cosets H,
+  one := λ 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
     (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] :
-  is_group_action (mul_left_cosets H ∘ (subtype.val : I → α)) :=
-is_group_action.comp_hom _ _
+  group_action I (quotient H) :=
+group_action.comp_hom (quotient H) (subtype.val : I → α)
 
-end is_group_action
+end group_action