diff --git a/src/algebra/module.lean b/src/algebra/module.lean index cabf1bcdc2d2e..2881335e13ae1 100644 --- a/src/algebra/module.lean +++ b/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" `β`, diff --git a/src/group_theory/group_action.lean b/src/group_theory/group_action.lean index f806fc8c86810..5fe4bb2811aa5 100644 --- a/src/group_theory/group_action.lean +++ b/src/group_theory/group_action.lean @@ -8,122 +8,142 @@ 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 := @@ -131,14 +151,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] : 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 diff --git a/src/group_theory/sylow.lean b/src/group_theory/sylow.lean index 2c3a18dc2ba1b..59f6eaef61c13 100644 --- a/src/group_theory/sylow.lean +++ b/src/group_theory/sylow.lean @@ -3,47 +3,49 @@ Copyright (c) 2018 Chris Hughes. All rights reserved. Released under Apache 2.0 license as described in the file LICENSE. Authors: Chris Hughes -/ -import group_theory.order_of_element data.zmod.basic algebra.pi_instances group_theory.group_action group_theory.quotient_group +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 is_group_action is_monoid_action function equiv.perm is_subgroup list quotient_group +open equiv fintype finset group_action monoid_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 is_group_action -variables (f : G → α → α) [is_group_action f] +namespace group_action +variables [group_action G α] -lemma mem_fixed_points_iff_card_orbit_eq_one {f : G → α → α} [is_group_action f] {a : α} - [fintype (orbit f a)] : a ∈ fixed_points f ↔ card (orbit f a) = 1 := +lemma mem_fixed_points_iff_card_orbit_eq_one {a : α} + [fintype (orbit G a)] : a ∈ fixed_points G α ↔ card (orbit G a) = 1 := begin rw [fintype.card_eq_one_iff, mem_fixed_points], split, - { exact λ h, ⟨⟨a, mem_orbit_self _ _⟩, λ ⟨b, ⟨x, hx⟩⟩, subtype.eq $ by simp [h x, hx.symm]⟩ }, + { exact λ h, ⟨⟨a, mem_orbit_self _⟩, λ ⟨b, ⟨x, hx⟩⟩, subtype.eq $ by simp [h x, hx.symm]⟩ }, { assume h x, rcases h with ⟨⟨z, hz⟩, hz₁⟩, - exact calc f x a = z : subtype.mk.inj (hz₁ ⟨f x a, mem_orbit _ _ _⟩) - ... = a : (subtype.mk.inj (hz₁ ⟨a, mem_orbit_self _ _⟩)).symm } + exact calc x • a = z : subtype.mk.inj (hz₁ ⟨x • a, mem_orbit _ _⟩) + ... = a : (subtype.mk.inj (hz₁ ⟨a, mem_orbit_self _⟩)).symm } end -lemma card_modeq_card_fixed_points [fintype α] [fintype G] [fintype (fixed_points f)] - {p n : ℕ} (hp : nat.prime p) (h : card G = p ^ n) : card α ≡ card (fixed_points f) [MOD p] := -calc card α = card (Σ y : quotient (orbit_rel f), {x // quotient.mk' x = y}) : - card_congr (equiv_fib (@quotient.mk' _ (orbit_rel f))) -... = univ.sum (λ a : quotient (orbit_rel f), card {x // quotient.mk' x = a}) : card_sigma _ -... ≡ (@univ (fixed_points f) _).sum (λ _, 1) [MOD p] : +lemma card_modeq_card_fixed_points [fintype α] [fintype G] [fintype (fixed_points G α)] + {p n : ℕ} (hp : nat.prime p) (h : card G = p ^ n) : card α ≡ card (fixed_points G α) [MOD p] := +calc card α = card (Σ y : quotient (orbit_rel G α), {x // quotient.mk' x = y}) : + card_congr (equiv_fib (@quotient.mk' _ (orbit_rel G α))) +... = univ.sum (λ a : quotient (orbit_rel G α), card {x // quotient.mk' x = a}) : card_sigma _ +... ≡ (@univ (fixed_points G α) _).sum (λ _, 1) [MOD p] : begin rw [← zmodp.eq_iff_modeq_nat hp, sum_nat_cast, sum_nat_cast], refine eq.symm (sum_bij_ne_zero (λ a _ _, quotient.mk' a.1) (λ _ _ _, mem_univ _) (λ a₁ a₂ _ _ _ _ h, - subtype.eq (mem_fixed_points'.1 a₂.2 a₁.1 (quotient.exact' h))) + subtype.eq ((mem_fixed_points' α).1 a₂.2 a₁.1 (quotient.exact' h))) (λ b, _) (λ a ha _, by rw [← mem_fixed_points_iff_card_orbit_eq_one.1 a.2]; simp only [quotient.eq']; congr)), { refine quotient.induction_on' b (λ b _ hb, _), - have : card (orbit f b) ∣ p ^ n, - { rw [← h, fintype.card_congr (orbit_equiv_quotient_stabilizer f b)]; + have : card (orbit G b) ∣ p ^ n, + { rw [← h, fintype.card_congr (orbit_equiv_quotient_stabilizer G b)]; exact card_quotient_dvd_card _ }, rcases (nat.dvd_prime_pow hp).1 this with ⟨k, _, hk⟩, have hb' :¬ p ^ 1 ∣ p ^ k, @@ -56,7 +58,7 @@ begin end ... = _ : by simp; refl -end is_group_action +end group_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) = @@ -97,18 +99,19 @@ def rotate_vectors_prod_eq_one (G : Type*) [group G] (n : ℕ+) (m : multiplicat ⟨⟨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 : ℕ+) : - is_group_action (rotate_vectors_prod_eq_one G n) := -{to_is_monoid_action := ⟨λ v, subtype.eq $ vector.eq _ _ $ rotate_zero v.1.to_list, - λ a b ⟨⟨v, hv₁⟩, hv₂⟩, subtype.eq $ vector.eq _ _ $ + group_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 _ _ $ 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₁]⟩} + by rw [zmod.add_val, rotate_rotate, ← rotate_mod _ (b.1 + a.1), add_comm, hv₁] } lemma one_mem_vectors_prod_eq_one (n : ℕ) : vector.repeat (1 : G) n ∈ vectors_prod_eq_one G n := by simp [vector.repeat, vectors_prod_eq_one] lemma one_mem_fixed_points_rotate (n : ℕ+) : (⟨vector.repeat (1 : G) n, one_mem_vectors_prod_eq_one n⟩ : vectors_prod_eq_one G n) ∈ - fixed_points (rotate_vectors_prod_eq_one G n) := + fixed_points (multiplicative (zmod n)) (vectors_prod_eq_one G n) := λ m, subtype.eq $ vector.eq _ _ $ by haveI : nonempty G := ⟨1⟩; exact rotate_eq_self_iff_eq_repeat.2 ⟨(1 : G), @@ -125,18 +128,18 @@ 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 : _ = _ := @is_group_action.card_modeq_card_fixed_points _ _ _ - (rotate_vectors_prod_eq_one G p') _ _ _ _ _ 1 hp hzmod, +have hmodeq : _ = _ := @group_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 ... ∣ card G ^ (n : ℕ) : nat.pow_dvd_pow _ n.2 ... = card (vectors_prod_eq_one G (n + 1)) : hcard.symm, -have hdvdcard₂ : p ∣ card (fixed_points (rotate_vectors_prod_eq_one G p')) := +have hdvdcard₂ : p ∣ card (fixed_points (multiplicative (zmod p')) (vectors_prod_eq_one G p')) := nat.dvd_of_mod_eq_zero (hmodeq ▸ hn.symm ▸ nat.mod_eq_zero_of_dvd hdvdcard), -have hcard_pos : 0 < card (fixed_points (rotate_vectors_prod_eq_one G p')) := +have hcard_pos : 0 < card (fixed_points (multiplicative (zmod p')) (vectors_prod_eq_one G p')) := fintype.card_pos_iff.2 ⟨⟨⟨vector.repeat 1 p', one_mem_vectors_prod_eq_one _⟩, one_mem_fixed_points_rotate _⟩⟩, -have hlt : 1 < card (fixed_points (rotate_vectors_prod_eq_one G p')) := +have hlt : 1 < card (fixed_points (multiplicative (zmod p')) (vectors_prod_eq_one G p')) := calc (1 : ℕ) < p' : hp.gt_one ... ≤ _ : nat.le_of_dvd hcard_pos hdvdcard₂, let ⟨⟨⟨⟨x, hx₁⟩, hx₂⟩, hx₃⟩, hx₄⟩ := fintype.exists_ne_of_card_gt_one hlt @@ -154,18 +157,17 @@ 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 is_group_action +open is_subgroup is_submonoid is_group_hom group_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 (mul_left_cosets H ∘ (subtype.val : H → G)) ↔ x ∈ normalizer H := -⟨λ hx, have ha : ∀ {y : quotient H}, y ∈ orbit (mul_left_cosets H ∘ (subtype.val : H → G)) x → y = x, - from λ _, (mem_fixed_points'.1 hx _), + {x : G} : (x : quotient H) ∈ fixed_points H (quotient H) ↔ x ∈ normalizer H := +⟨λ hx, have ha : ∀ {y : quotient H}, y ∈ orbit H (x : quotient H) → y = x, + from λ _, ((mem_fixed_points' _).1 hx _), (inv_mem_iff _).1 (mem_normalizer_fintype (λ n hn, - have (n⁻¹ * x)⁻¹ * x ∈ H := quotient_group.eq.1 (ha (mem_orbit (mul_left_cosets H ∘ (subtype.val : H → G)) _ - ⟨n⁻¹, inv_mem hn⟩)), + have (n⁻¹ * x)⁻¹ * x ∈ H := quotient_group.eq.1 (ha (mem_orbit _ ⟨n⁻¹, inv_mem hn⟩)), by simpa only [mul_inv_rev, inv_inv] using this)), λ (hx : ∀ (n : G), n ∈ H ↔ x * n * x⁻¹ ∈ H), -mem_fixed_points'.2 $ λ y, quotient.induction_on' y $ λ y hy, quotient_group.eq.2 +(mem_fixed_points' _).2 $ λ y, quotient.induction_on' y $ λ y hy, quotient_group.eq.2 (let ⟨⟨b, hb₁⟩, hb₂⟩ := hy in have hb₂ : (b * x)⁻¹ * y ∈ H := quotient_group.eq.1 hb₂, (inv_mem_iff H).1 $ (hx _).2 $ (mul_mem_cancel_right H (inv_mem hb₁)).1 @@ -173,8 +175,8 @@ mem_fixed_points'.2 $ λ y, quotient.induction_on' y $ λ y hy, quotient_group.e simpa [mul_inv_rev, mul_assoc] using hb₂)⟩ lemma fixed_points_mul_left_cosets_equiv_quotient (H : set G) [is_subgroup H] [fintype H] : - fixed_points (mul_left_cosets H ∘ (subtype.val : H → G)) ≃ quotient (subtype.val ⁻¹' H : set (normalizer H)) := -@subtype_quotient_equiv_quotient_subtype G (normalizer H) (id _) (id _) (fixed_points _) + fixed_points H (quotient H) ≃ quotient (subtype.val ⁻¹' H : set (normalizer H)) := +@subtype_quotient_equiv_quotient_subtype G (normalizer H) (id _) (id _) (fixed_points _ _) (λ a, mem_fixed_points_mul_left_cosets_iff_mem_normalizer.symm) (by intros; refl) local attribute [instance] set_fintype @@ -194,7 +196,7 @@ have hcard : card (quotient H) = s * p := nat.pow_succ, mul_assoc, mul_comm p]), have hm : s * p % p = card (quotient (subtype.val ⁻¹' H : set (normalizer H))) % p := card_congr (fixed_points_mul_left_cosets_equiv_quotient H) ▸ hcard ▸ - card_modeq_card_fixed_points _ hp hH2, + card_modeq_card_fixed_points hp hH2, have hm' : p ∣ card (quotient (subtype.val ⁻¹' H : set (normalizer H))) := nat.dvd_of_mod_eq_zero (by rwa [nat.mod_eq_zero_of_dvd (dvd_mul_left _ _), eq_comm] at hm),