From ca554bee0b1dc5349e9e55f9b5fcee48e1d4c6fa Mon Sep 17 00:00:00 2001 From: Eric Wieser Date: Tue, 21 Dec 2021 16:21:11 +0000 Subject: [PATCH] chore(group_theory/quotient_group): make pow definitionally equal (#10833) Motivated by a TODO comment. --- src/group_theory/congruence.lean | 83 ++++++++++++++++++++++++---- src/group_theory/quotient_group.lean | 9 +-- 2 files changed, 74 insertions(+), 18 deletions(-) diff --git a/src/group_theory/congruence.lean b/src/group_theory/congruence.lean index 0c6f74ab15961..a51dd3e4f571a 100644 --- a/src/group_theory/congruence.lean +++ b/src/group_theory/congruence.lean @@ -870,23 +870,51 @@ end mul_one_class section monoids +/-- Multiplicative congruence relations preserve natural powers. -/ +@[to_additive add_con.nsmul "Additive congruence relations preserve natural scaling."] +protected lemma pow {M : Type*} [monoid M] (c : con M) : + ∀ (n : ℕ) {w x}, c w x → c (w ^ n) (x ^ n) +| 0 w x h := by simpa using c.refl _ +| (nat.succ n) w x h := by simpa [pow_succ] using c.mul h (pow n h) + +@[to_additive] +instance {M : Type*} [mul_one_class M] (c : con M) : has_one c.quotient := +{ one := ((1 : M) : c.quotient) } + +instance _root_.add_con.quotient.has_nsmul + {M : Type*} [add_monoid M] (c : add_con M) : has_scalar ℕ c.quotient := +{ smul := λ n x, quotient.lift_on' x (λ w, ((n • w : M) : c.quotient)) + $ λ x y h, c.eq.2 $ c.nsmul n h} + +@[to_additive add_con.quotient.has_nsmul] +instance {M : Type*} [monoid M] (c : con M) : has_pow c.quotient ℕ := +{ pow := λ x n, quotient.lift_on' x (λ w, ((w ^ n : M) : c.quotient)) + $ λ x y h, c.eq.2 $ c.pow n h} + +/-- The quotient of a semigroup by a congruence relation is a semigroup. -/ +@[to_additive "The quotient of an `add_semigroup` by an additive congruence relation is +an `add_semigroup`."] +instance semigroup {M : Type*} [semigroup M] (c : con M) : semigroup c.quotient := +function.surjective.semigroup _ quotient.surjective_quotient_mk' (λ _ _, rfl) + +/-- The quotient of a commutative semigroup by a congruence relation is a semigroup. -/ +@[to_additive "The quotient of an `add_comm_semigroup` by an additive congruence relation is +an `add_semigroup`."] +instance comm_semigroup {M : Type*} [comm_semigroup M] (c : con M) : comm_semigroup c.quotient := +function.surjective.comm_semigroup _ quotient.surjective_quotient_mk' (λ _ _, rfl) + /-- The quotient of a monoid by a congruence relation is a monoid. -/ @[to_additive "The quotient of an `add_monoid` by an additive congruence relation is an `add_monoid`."] -instance monoid {M : Type*} [monoid M] (c : con M): monoid c.quotient := -{ one := ((1 : M) : c.quotient), - mul := (*), - mul_assoc := λ x y z, quotient.induction_on₃' x y z - $ λ _ _ _, congr_arg coe $ mul_assoc _ _ _, - .. c.mul_one_class } +instance monoid {M : Type*} [monoid M] (c : con M) : monoid c.quotient := +function.surjective.monoid_pow _ quotient.surjective_quotient_mk' rfl (λ _ _, rfl) (λ _ _, rfl) /-- The quotient of a `comm_monoid` by a congruence relation is a `comm_monoid`. -/ @[to_additive "The quotient of an `add_comm_monoid` by an additive congruence relation is an `add_comm_monoid`."] instance comm_monoid {M : Type*} [comm_monoid M] (c : con M) : comm_monoid c.quotient := -{ mul_comm := λ x y, con.induction_on₂ x y $ λ w z, by rw [←coe_mul, ←coe_mul, mul_comm], - ..c.monoid} +{ ..c.comm_semigroup, ..c.monoid} end monoids @@ -899,6 +927,17 @@ variables {M} [group M] [group N] [group P] (c : con M) protected lemma inv : ∀ {w x}, c w x → c w⁻¹ x⁻¹ := λ x y h, by simpa using c.symm (c.mul (c.mul (c.refl x⁻¹) h) (c.refl y⁻¹)) +/-- Multiplicative congruence relations preserve division. -/ +@[to_additive "Additive congruence relations preserve subtraction."] +protected lemma div : ∀ {w x y z}, c w x → c y z → c (w / y) (x / z) := +λ w x y z h1 h2, by simpa only [div_eq_mul_inv] using c.mul h1 (c.inv h2) + +/-- Multiplicative congruence relations preserve integer powers. -/ +@[to_additive add_con.zsmul "Additive congruence relations preserve integer scaling."] +protected lemma zpow : ∀ (n : ℤ) {w x}, c w x → c (w ^ n) (x ^ n) +| (int.of_nat n) w x h := by simpa only [zpow_of_nat] using c.pow _ h +| -[1+ n] w x h := by simpa only [zpow_neg_succ_of_nat] using c.inv (c.pow _ h) + /-- The inversion induced on the quotient by a congruence relation on a type with a inversion. -/ @[to_additive "The negation induced on the quotient by an additive congruence relation on a type @@ -907,14 +946,34 @@ instance has_inv : has_inv c.quotient := ⟨λ x, quotient.lift_on' x (λ w, ((w⁻¹ : M) : c.quotient)) $ λ x y h, c.eq.2 $ c.inv h⟩ +/-- The division induced on the quotient by a congruence relation on a type with a + division. -/ +@[to_additive "The subtraction induced on the quotient by an additive congruence relation on a type +with a subtraction."] +instance has_div : has_div c.quotient := +⟨λ x y, quotient.lift_on₂' x y (λ w z, ((w / z : M) : c.quotient)) + $ λ _ _ _ _ h1 h2, c.eq.2 $ c.div h1 h2⟩ + +/-- The integer scaling induced on the quotient by a congruence relation on a type with a + subtraction. -/ +instance _root_.add_con.quotient.has_zsmul + {M : Type*} [add_group M] (c : add_con M) : has_scalar ℤ c.quotient := +⟨λ z x, quotient.lift_on' x (λ w, ((z • w : M) : c.quotient)) + $ λ x y h, c.eq.2 $ c.zsmul z h⟩ + +/-- The integer power induced on the quotient by a congruence relation on a type with a + division. -/ +@[to_additive add_con.quotient.has_zsmul] +instance has_zpow : has_pow c.quotient ℤ := +⟨λ x z, quotient.lift_on' x (λ w, ((w ^ z : M) : c.quotient)) + $ λ x y h, c.eq.2 $ c.zpow z h⟩ + /-- The quotient of a group by a congruence relation is a group. -/ @[to_additive "The quotient of an `add_group` by an additive congruence relation is an `add_group`."] instance group : group c.quotient := -{ inv := λ x, x⁻¹, - mul_left_inv := λ x, show x⁻¹ * x = 1, - from quotient.induction_on' x $ λ _, congr_arg coe $ mul_left_inv _, - .. con.monoid c} +function.surjective.group_pow _ quotient.surjective_quotient_mk' rfl + (λ _ _, rfl) (λ _, rfl) (λ _ _, rfl) (λ _ _, rfl) (λ _ _, rfl) end groups diff --git a/src/group_theory/quotient_group.lean b/src/group_theory/quotient_group.lean index 2ef654eff4ed5..5313a1950c10d 100644 --- a/src/group_theory/quotient_group.lean +++ b/src/group_theory/quotient_group.lean @@ -120,17 +120,14 @@ lemma coe_mul (a b : G) : ((a * b : G) : Q) = a * b := rfl @[simp, to_additive quotient_add_group.coe_neg] lemma coe_inv (a : G) : ((a⁻¹ : G) : Q) = a⁻¹ := rfl --- TODO: make it `rfl` @[simp, to_additive quotient_add_group.coe_sub] -lemma coe_div (a b : G) : ((a / b : G) : Q) = a / b := by simp [div_eq_mul_inv] +lemma coe_div (a b : G) : ((a / b : G) : Q) = a / b := rfl @[simp, to_additive quotient_add_group.coe_nsmul] -lemma coe_pow (a : G) (n : ℕ) : ((a ^ n : G) : Q) = a ^ n := -(mk' N).map_pow a n +lemma coe_pow (a : G) (n : ℕ) : ((a ^ n : G) : Q) = a ^ n := rfl @[simp, to_additive quotient_add_group.coe_zsmul] -lemma coe_zpow (a : G) (n : ℤ) : ((a ^ n : G) : Q) = a ^ n := -(mk' N).map_zpow a n +lemma coe_zpow (a : G) (n : ℤ) : ((a ^ n : G) : Q) = a ^ n := rfl /-- A group homomorphism `φ : G →* H` with `N ⊆ ker(φ)` descends (i.e. `lift`s) to a group homomorphism `G/N →* H`. -/