From 0d17cfb64a04ded3972434625fa74505ea1780f0 Mon Sep 17 00:00:00 2001 From: "Yury G. Kudryashov" Date: Tue, 6 Dec 2022 20:53:43 +0000 Subject: [PATCH] chore(group_theory/quotient_group): drop unneeded names in `to_additive` (#17821) This only changes the names of `group` and `comm_group` instances. --- src/group_theory/quotient_group.lean | 121 +++++++++++---------------- src/linear_algebra/quotient.lean | 2 +- 2 files changed, 50 insertions(+), 73 deletions(-) diff --git a/src/group_theory/quotient_group.lean b/src/group_theory/quotient_group.lean index 5bc5378d87bdc..18c1f5b0d9250 100644 --- a/src/group_theory/quotient_group.lean +++ b/src/group_theory/quotient_group.lean @@ -56,12 +56,10 @@ protected def con : con G := ... ∈ N : N.mul_mem (nN.conj_mem _ hab _) hcd end } -@[to_additive quotient_add_group.add_group] -instance quotient.group : group (G ⧸ N) := -(quotient_group.con N).group +@[to_additive] instance quotient.group : group (G ⧸ N) := (quotient_group.con N).group /-- The group homomorphism from `G` to `G/N`. -/ -@[to_additive quotient_add_group.mk' "The additive group homomorphism from `G` to `G/N`."] +@[to_additive "The additive group homomorphism from `G` to `G/N`."] def mk' : G →* G ⧸ N := monoid_hom.mk' (quotient_group.mk) (λ _ _, rfl) @[simp, to_additive] @@ -89,19 +87,18 @@ See note [partially-applied ext lemmas]. "-/] lemma monoid_hom_ext ⦃f g : G ⧸ N →* H⦄ (h : f.comp (mk' N) = g.comp (mk' N)) : f = g := monoid_hom.ext $ λ x, quotient_group.induction_on x $ (monoid_hom.congr_fun h : _) -@[simp, to_additive quotient_add_group.eq_zero_iff] +@[simp, to_additive] lemma eq_one_iff {N : subgroup G} [nN : N.normal] (x : G) : (x : G ⧸ N) = 1 ↔ x ∈ N := begin refine quotient_group.eq.trans _, rw [mul_one, subgroup.inv_mem_iff], end -@[simp, to_additive quotient_add_group.ker_mk] -lemma ker_mk : - monoid_hom.ker (quotient_group.mk' N : G →* G ⧸ N) = N := +@[simp, to_additive] +lemma ker_mk : monoid_hom.ker (quotient_group.mk' N : G →* G ⧸ N) = N := subgroup.ext eq_one_iff -@[to_additive quotient_add_group.eq_iff_sub_mem] +@[to_additive] lemma eq_iff_div_mem {N : subgroup G} [nN : N.normal] {x y : G} : (x : G ⧸ N) = y ↔ x / y ∈ N := begin @@ -112,8 +109,8 @@ end -- for commutative groups we don't need normality assumption omit nN -@[to_additive quotient_add_group.add_comm_group] -instance {G : Type*} [comm_group G] (N : subgroup G) : comm_group (G ⧸ N) := +@[to_additive] +instance quotient.comm_group {G : Type*} [comm_group G] (N : subgroup G) : comm_group (G ⧸ N) := { mul_comm := λ a b, quotient.induction_on₂' a b (λ a b, congr_arg mk (mul_comm a b)), .. @quotient_group.quotient.group _ _ N N.normal_of_comm } @@ -122,28 +119,17 @@ include nN local notation ` Q ` := G ⧸ N -@[simp, to_additive quotient_add_group.coe_zero] -lemma coe_one : ((1 : G) : Q) = 1 := rfl - -@[simp, to_additive quotient_add_group.coe_add] -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 - -@[simp, to_additive quotient_add_group.coe_sub] -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 := rfl - -@[simp, to_additive quotient_add_group.coe_zsmul] -lemma coe_zpow (a : G) (n : ℤ) : ((a ^ n : G) : Q) = a ^ n := rfl +@[simp, to_additive] lemma coe_one : ((1 : G) : Q) = 1 := rfl +@[simp, to_additive] lemma coe_mul (a b : G) : ((a * b : G) : Q) = a * b := rfl +@[simp, to_additive] lemma coe_inv (a : G) : ((a⁻¹ : G) : Q) = a⁻¹ := rfl +@[simp, to_additive] lemma coe_div (a b : G) : ((a / b : G) : Q) = a / b := rfl +@[simp, to_additive] lemma coe_pow (a : G) (n : ℕ) : ((a ^ n : G) : Q) = a ^ n := rfl +@[simp, to_additive] 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`. -/ -@[to_additive quotient_add_group.lift "An `add_group` homomorphism `φ : G →+ H` with `N ⊆ ker(φ)` -descends (i.e. `lift`s) to a group homomorphism `G/N →* H`."] +@[to_additive "An `add_group` homomorphism `φ : G →+ H` with `N ⊆ ker(φ)` descends (i.e. `lift`s) +to a group homomorphism `G/N →* H`."] def lift (φ : G →* H) (HN : ∀x∈N, φ x = 1) : Q →* H := (quotient_group.con N).lift φ $ λ x y h, begin simp only [quotient_group.con, left_rel_apply, con.rel_mk] at h, @@ -151,21 +137,19 @@ def lift (φ : G →* H) (HN : ∀x∈N, φ x = 1) : Q →* H := ... = φ y : by rw [φ.map_mul, HN _ (N.inv_mem h), mul_one] end -@[simp, to_additive quotient_add_group.lift_mk] -lemma lift_mk {φ : G →* H} (HN : ∀x∈N, φ x = 1) (g : G) : - lift N φ HN (g : Q) = φ g := rfl +@[simp, to_additive] +lemma lift_mk {φ : G →* H} (HN : ∀x∈N, φ x = 1) (g : G) : lift N φ HN (g : Q) = φ g := rfl -@[simp, to_additive quotient_add_group.lift_mk'] -lemma lift_mk' {φ : G →* H} (HN : ∀x∈N, φ x = 1) (g : G) : - lift N φ HN (mk g : Q) = φ g := rfl +@[simp, to_additive] +lemma lift_mk' {φ : G →* H} (HN : ∀x∈N, φ x = 1) (g : G) : lift N φ HN (mk g : Q) = φ g := rfl -@[simp, to_additive quotient_add_group.lift_quot_mk] +@[simp, to_additive] lemma lift_quot_mk {φ : G →* H} (HN : ∀x∈N, φ x = 1) (g : G) : lift N φ HN (quot.mk _ g : Q) = φ g := rfl /-- A group homomorphism `f : G →* H` induces a map `G/N →* H/M` if `N ⊆ f⁻¹(M)`. -/ -@[to_additive quotient_add_group.map "An `add_group` homomorphism `f : G →+ H` induces a map -`G/N →+ H/M` if `N ⊆ f⁻¹(M)`."] +@[to_additive "An `add_group` homomorphism `f : G →+ H` induces a map `G/N →+ H/M` if +`N ⊆ f⁻¹(M)`."] def map (M : subgroup H) [M.normal] (f : G →* H) (h : N ≤ M.comap f) : G ⧸ N →* H ⧸ M := begin @@ -176,13 +160,12 @@ begin exact h hx, end -@[simp, to_additive quotient_add_group.map_coe] lemma map_coe - (M : subgroup H) [M.normal] (f : G →* H) (h : N ≤ M.comap f) (x : G) : +@[simp, to_additive] lemma map_coe (M : subgroup H) [M.normal] (f : G →* H) (h : N ≤ M.comap f) + (x : G) : map N M f h ↑x = ↑(f x) := lift_mk' _ _ x -@[to_additive quotient_add_group.map_mk'] lemma map_mk' - (M : subgroup H) [M.normal] (f : G →* H) (h : N ≤ M.comap f) (x : G) : +@[to_additive] lemma map_mk' (M : subgroup H) [M.normal] (f : G →* H) (h : N ≤ M.comap f) (x : G) : map N M f h (mk' _ x) = ↑(f x) := quotient_group.lift_mk' _ _ x @@ -268,20 +251,17 @@ variables (φ : G →* H) open function monoid_hom /-- The induced map from the quotient by the kernel to the codomain. -/ -@[to_additive quotient_add_group.ker_lift "The induced map from the quotient by the kernel to the -codomain."] +@[to_additive "The induced map from the quotient by the kernel to the codomain."] def ker_lift : G ⧸ ker φ →* H := lift _ φ $ λ g, φ.mem_ker.mp -@[simp, to_additive quotient_add_group.ker_lift_mk] -lemma ker_lift_mk (g : G) : (ker_lift φ) g = φ g := -lift_mk _ _ _ +@[simp, to_additive] +lemma ker_lift_mk (g : G) : (ker_lift φ) g = φ g := lift_mk _ _ _ -@[simp, to_additive quotient_add_group.ker_lift_mk'] -lemma ker_lift_mk' (g : G) : (ker_lift φ) (mk g) = φ g := -lift_mk' _ _ _ +@[simp, to_additive] +lemma ker_lift_mk' (g : G) : (ker_lift φ) (mk g) = φ g := lift_mk' _ _ _ -@[to_additive quotient_add_group.ker_lift_injective] +@[to_additive] lemma ker_lift_injective : injective (ker_lift φ) := assume a b, quotient.induction_on₂' a b $ assume a b (h : φ a = φ b), quotient.sound' $ @@ -291,19 +271,18 @@ assume a b, quotient.induction_on₂' a b $ -- so there is a bit of annoying code duplication here /-- The induced map from the quotient by the kernel to the range. -/ -@[to_additive quotient_add_group.range_ker_lift "The induced map from the quotient by the kernel to -the range."] +@[to_additive "The induced map from the quotient by the kernel to the range."] def range_ker_lift : G ⧸ ker φ →* φ.range := lift _ φ.range_restrict $ λ g hg, (mem_ker _).mp $ by rwa ker_range_restrict -@[to_additive quotient_add_group.range_ker_lift_injective] +@[to_additive] lemma range_ker_lift_injective : injective (range_ker_lift φ) := assume a b, quotient.induction_on₂' a b $ assume a b (h : φ.range_restrict a = φ.range_restrict b), quotient.sound' $ by rw [left_rel_apply, ←ker_range_restrict, mem_ker, φ.range_restrict.map_mul, ← h, φ.range_restrict.map_inv, inv_mul_self] -@[to_additive quotient_add_group.range_ker_lift_surjective] +@[to_additive] lemma range_ker_lift_surjective : surjective (range_ker_lift φ) := begin rintro ⟨_, g, rfl⟩, @@ -313,16 +292,15 @@ end /-- **Noether's first isomorphism theorem** (a definition): the canonical isomorphism between `G/(ker φ)` to `range φ`. -/ -@[to_additive quotient_add_group.quotient_ker_equiv_range "The first isomorphism theorem -(a definition): the canonical isomorphism between `G/(ker φ)` to `range φ`."] +@[to_additive "The first isomorphism theorem (a definition): the canonical isomorphism between +`G/(ker φ)` to `range φ`."] noncomputable def quotient_ker_equiv_range : G ⧸ ker φ ≃* range φ := mul_equiv.of_bijective (range_ker_lift φ) ⟨range_ker_lift_injective φ, range_ker_lift_surjective φ⟩ /-- The canonical isomorphism `G/(ker φ) ≃* H` induced by a homomorphism `φ : G →* H` with a right inverse `ψ : H → G`. -/ -@[to_additive quotient_add_group.quotient_ker_equiv_of_right_inverse "The canonical isomorphism -`G/(ker φ) ≃+ H` induced by a homomorphism `φ : G →+ H` with a right inverse `ψ : H → G`.", - simps] +@[to_additive "The canonical isomorphism `G/(ker φ) ≃+ H` induced by a homomorphism `φ : G →+ H` +with a right inverse `ψ : H → G`.", simps] def quotient_ker_equiv_of_right_inverse (ψ : H → G) (hφ : function.right_inverse ψ φ) : G ⧸ ker φ ≃* H := { to_fun := ker_lift φ, @@ -332,7 +310,7 @@ def quotient_ker_equiv_of_right_inverse (ψ : H → G) (hφ : function.right_inv .. ker_lift φ } /-- The canonical isomorphism `G/⊥ ≃* G`. -/ -@[to_additive quotient_add_group.quotient_bot "The canonical isomorphism `G/⊥ ≃+ G`.", simps] +@[to_additive "The canonical isomorphism `G/⊥ ≃+ G`.", simps] def quotient_bot : G ⧸ (⊥ : subgroup G) ≃* G := quotient_ker_equiv_of_right_inverse (monoid_hom.id G) id (λ x, rfl) @@ -340,8 +318,7 @@ quotient_ker_equiv_of_right_inverse (monoid_hom.id G) id (λ x, rfl) For a `computable` version, see `quotient_group.quotient_ker_equiv_of_right_inverse`. -/ -@[to_additive quotient_add_group.quotient_ker_equiv_of_surjective "The canonical isomorphism -`G/(ker φ) ≃+ H` induced by a surjection `φ : G →+ H`. +@[to_additive "The canonical isomorphism `G/(ker φ) ≃+ H` induced by a surjection `φ : G →+ H`. For a `computable` version, see `quotient_add_group.quotient_ker_equiv_of_right_inverse`."] noncomputable def quotient_ker_equiv_of_surjective (hφ : function.surjective φ) : @@ -495,8 +472,8 @@ nM.map _ mk_surjective variables (h : N ≤ M) /-- The map from the third isomorphism theorem for groups: `(G / N) / (M / N) → G / M`. -/ -@[to_additive quotient_add_group.quotient_quotient_equiv_quotient_aux -"The map from the third isomorphism theorem for additive groups: `(A / N) / (M / N) → A / M`."] +@[to_additive "The map from the third isomorphism theorem for additive groups: +`(A / N) / (M / N) → A / M`."] def quotient_quotient_equiv_quotient_aux : (G ⧸ N) ⧸ (M.map (mk' N)) →* G ⧸ M := lift (M.map (mk' N)) @@ -504,20 +481,20 @@ lift (M.map (mk' N)) (by { rintro _ ⟨x, hx, rfl⟩, rw map_mk' N M _ _ x, exact (quotient_group.eq_one_iff _).mpr hx }) -@[simp, to_additive quotient_add_group.quotient_quotient_equiv_quotient_aux_coe] +@[simp, to_additive] lemma quotient_quotient_equiv_quotient_aux_coe (x : G ⧸ N) : quotient_quotient_equiv_quotient_aux N M h x = quotient_group.map N M (monoid_hom.id G) h x := quotient_group.lift_mk' _ _ x -@[to_additive quotient_add_group.quotient_quotient_equiv_quotient_aux_coe_coe] +@[to_additive] lemma quotient_quotient_equiv_quotient_aux_coe_coe (x : G) : quotient_quotient_equiv_quotient_aux N M h (x : G ⧸ N) = x := quotient_group.lift_mk' _ _ x -/-- **Noether's third isomorphism theorem** for groups: `(G / N) / (M / N) ≃ G / M`. -/ -@[to_additive quotient_add_group.quotient_quotient_equiv_quotient -"**Noether's third isomorphism theorem** for additive groups: `(A / N) / (M / N) ≃ A / M`."] +/-- **Noether's third isomorphism theorem** for groups: `(G / N) / (M / N) ≃* G / M`. -/ +@[to_additive "**Noether's third isomorphism theorem** for additive groups: +`(A / N) / (M / N) ≃+ A / M`."] def quotient_quotient_equiv_quotient : (G ⧸ N) ⧸ (M.map (quotient_group.mk' N)) ≃* G ⧸ M := monoid_hom.to_mul_equiv @@ -548,7 +525,7 @@ top_unique $ λ x _, end trivial -@[to_additive quotient_add_group.comap_comap_center] +@[to_additive] lemma comap_comap_center {H₁ : subgroup G} [H₁.normal] {H₂ : subgroup (G ⧸ H₁)} [H₂.normal] : (((subgroup.center ((G ⧸ H₁) ⧸ H₂))).comap (mk' H₂)).comap (mk' H₁) = (subgroup.center (G ⧸ H₂.comap (mk' H₁))).comap (mk' (H₂.comap (mk' H₁))) := diff --git a/src/linear_algebra/quotient.lean b/src/linear_algebra/quotient.lean index 514cef1e60686..2e91ca51d780d 100644 --- a/src/linear_algebra/quotient.lean +++ b/src/linear_algebra/quotient.lean @@ -62,7 +62,7 @@ instance : inhabited (M ⧸ p) := ⟨0⟩ by simpa using (quotient.eq p : mk x = 0 ↔ _) instance add_comm_group : add_comm_group (M ⧸ p) := -quotient_add_group.add_comm_group p.to_add_subgroup +quotient_add_group.quotient.add_comm_group p.to_add_subgroup @[simp] theorem mk_add : (mk (x + y) : M ⧸ p) = mk x + mk y := rfl