From 0d2f0621968fef0faf5ab5bd6aebb8edd6f9ba51 Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?David=20W=C3=A4rn?= Date: Sat, 26 Nov 2022 16:48:13 +0000 Subject: [PATCH] feat: port algebra.group.semiconj (#717) mathlib SHA e50b8c261b0a000b806ec0e1356b41945eda61f7 This completes an earlier partial port of the file. ~~I added a workaround for the issue explained by Floris at https://github.com/leanprover-community/mathlib4/pull/707#issuecomment-1326669750.~~ Co-authored-by: Ruben Van de Velde <65514131+Ruben-VandeVelde@users.noreply.github.com> --- Mathlib/Algebra/Group/Semiconj.lean | 190 +++++++++++++++++++++++++--- Mathlib/Logic/Function/Basic.lean | 3 + 2 files changed, 172 insertions(+), 21 deletions(-) diff --git a/Mathlib/Algebra/Group/Semiconj.lean b/Mathlib/Algebra/Group/Semiconj.lean index 0b362a709a832..0f8c2d3b57f2d 100644 --- a/Mathlib/Algebra/Group/Semiconj.lean +++ b/Mathlib/Algebra/Group/Semiconj.lean @@ -12,12 +12,12 @@ import Mathlib.Algebra.Group.Units ## Main definitions -We say that `x` is semiconjugate to `y` by `a` (`semiconj_by a x y`), if `a * x = y * a`. -In this file we provide operations on `semiconj_by _ _ _`. +We say that `x` is semiconjugate to `y` by `a` (`SemiconjBy a x y`), if `a * x = y * a`. +In this file we provide operations on `SemiconjBy _ _ _`. In the names of these operations, we treat `a` as the “left” argument, and both `x` and `y` as “right” arguments. This way most names in this file agree with the names of the corresponding lemmas -for `commute a b = semiconj_by a b b`. As a side effect, some lemmas have only `_right` version. +for `Commute a b = SemiconjBy a b b`. As a side effect, some lemmas have only `_right` version. Lean does not immediately recognise these terms as equations, so for rewriting we need syntax like `rw [(h.pow_right 5).eq]` rather than just `rw [h.pow_right 5]`. @@ -26,26 +26,23 @@ This file provides only basic operations (`mul_left`, `mul_right`, `inv_right` e operations (`pow_right`, field inverse etc) are in the files that define corresponding notions. -/ - -universe u v - -variable {G : Type _} - /-- `x` is semiconjugate to `y` by `a`, if `a * x = y * a`. -/ @[to_additive AddSemiconjBy "`x` is additive semiconjugate to `y` by `a` if `a + x = y + a`"] -def SemiconjBy {M : Type u} [Mul M] (a x y : M) : Prop := +def SemiconjBy [Mul M] (a x y : M) : Prop := a * x = y * a +#align semiconj_by SemiconjBy namespace SemiconjBy -/-- Equality behind `semiconj_by a x y`; useful for rewriting. -/ -@[to_additive "Equality behind `add_semiconj_by a x y`; useful for rewriting."] -protected theorem eq {S : Type u} [Mul S] {a x y : S} (h : SemiconjBy a x y) : a * x = y * a := +/-- Equality behind `SemiconjBy a x y`; useful for rewriting. -/ +@[to_additive "Equality behind `AddSemiconjBy a x y`; useful for rewriting."] +protected theorem eq [Mul S] {a x y : S} (h : SemiconjBy a x y) : a * x = y * a := h +#align semiconj_by.eq SemiconjBy.eq section Semigroup -variable {S : Type u} [Semigroup S] {a b x y z x' y' : S} +variable [Semigroup S] {a b x y z x' y' : S} /-- If `a` semiconjugates `x` to `y` and `x'` to `y'`, then it semiconjugates `x * x'` to `y * y'`. -/ @@ -56,40 +53,191 @@ theorem mul_right (h : SemiconjBy a x y) (h' : SemiconjBy a x' y') : unfold SemiconjBy -- TODO this could be done using `assoc_rw` if/when this is ported to mathlib4 rw [←mul_assoc, h.eq, mul_assoc, h'.eq, ←mul_assoc] +#align semiconj_by.mul_right SemiconjBy.mul_right -/-- If both `a` and `b` semiconjugate `x` to `y`, then so does `a * b`. -/ -@[to_additive "If both `a` and `b` semiconjugate `x` to `y`, then so does `a + b`."] +/-- If `b` semiconjugates `x` to `y` and `a` semiconjugates `y` to `z`, then `a * b` +semiconjugates `x` to `z`. -/ +@[to_additive "If `b` semiconjugates `x` to `y` and `a` semiconjugates `y` to `z`, then `a + b` +semiconjugates `x` to `z`."] theorem mul_left (ha : SemiconjBy a y z) (hb : SemiconjBy b x y) : SemiconjBy (a * b) x z := by unfold SemiconjBy rw [mul_assoc, hb.eq, ←mul_assoc, ha.eq, mul_assoc] +#align semiconj_by.mul_left SemiconjBy.mul_left +#align add_semiconj_by.add_left AddSemiconjBy.add_left + +/-- The relation “there exists an element that semiconjugates `a` to `b`” on a semigroup +is transitive. -/ +@[to_additive "The relation “there exists an element that semiconjugates `a` to `b`” on an additive +semigroup is transitive."] +protected theorem transitive : Transitive fun a b : S ↦ ∃ c, SemiconjBy c a b + | _, _, _, ⟨x, hx⟩, ⟨y, hy⟩ => ⟨y * x, hy.mul_left hx⟩ +#align semiconj_by.transitive SemiconjBy.transitive +#align add_semiconj_by.transitive SemiconjBy.transitive end Semigroup section MulOneClass -variable {M : Type u} [MulOneClass M] +variable [MulOneClass M] /-- Any element semiconjugates `1` to `1`. -/ -@[simp] +@[simp, to_additive "Any element semiconjugates `0` to `0`."] theorem one_right (a : M) : SemiconjBy a 1 1 := by rw [SemiconjBy, mul_one, one_mul] +#align semiconj_by.one_right SemiconjBy.one_right +#align add_semiconj_by.zero_right AddSemiconjBy.zero_right /-- One semiconjugates any element to itself. -/ -@[simp] +@[simp, to_additive "Zero semiconjugates any element to itself."] theorem one_left (x : M) : SemiconjBy 1 x x := Eq.symm <| one_right x +#align semiconj_by.one_left SemiconjBy.one_left +#align add_semiconj_by.zero_left AddSemiconjBy.zero_left + +/-- The relation “there exists an element that semiconjugates `a` to `b`” on a monoid (or, more +generally, on `MulOneClass` type) is reflexive. -/ +@[to_additive "The relation “there exists an element that semiconjugates `a` to `b`” on an additive +monoid (or, more generally, on a `add_zero_class` type) is reflexive."] +protected theorem reflexive : Reflexive fun a b : M ↦ ∃ c, SemiconjBy c a b + | a => ⟨1, one_left a⟩ +#align semiconj_by.reflexive SemiconjBy.reflexive +#align add_semiconj_by.reflexive AddSemiconjBy.reflexive end MulOneClass section Monoid -variable {M : Type u} [Monoid M] - -@[simp] +variable [Monoid M] + +/-- If `a` semiconjugates a unit `x` to a unit `y`, then it semiconjugates `x⁻¹` to `y⁻¹`. -/ +@[to_additive "If `a` semiconjugates an additive unit `x` to an additive unit `y`, then it +semiconjugates `-x` to `-y`."] +theorem units_inv_right {a : M} {x y : Mˣ} (h : SemiconjBy a x y) : SemiconjBy a ↑x⁻¹ ↑y⁻¹ := + calc + a * ↑x⁻¹ = ↑y⁻¹ * (y * a) * ↑x⁻¹ := by rw [Units.inv_mul_cancel_left] + _ = ↑y⁻¹ * a := by rw [← h.eq, mul_assoc, Units.mul_inv_cancel_right] +#align semiconj_by.units_inv_right SemiconjBy.units_inv_right +#align add_semiconj_by.add_units_neg_right AddSemiconjBy.addUnits_neg_right + +@[simp, to_additive] +theorem units_inv_right_iff {a : M} {x y : Mˣ} : SemiconjBy a ↑x⁻¹ ↑y⁻¹ ↔ SemiconjBy a x y := + ⟨units_inv_right, units_inv_right⟩ +#align semiconj_by.units_inv_right_iff SemiconjBy.units_inv_right_iff +#align add_semiconj_by.add_units_neg_right_iff AddSemiconjBy.addUnits_neg_right_iff + +/-- If a unit `a` semiconjugates `x` to `y`, then `a⁻¹` semiconjugates `y` to `x`. -/ +@[to_additive "If an additive unit `a` semiconjugates `x` to `y`, then `-a` semiconjugates `y` to +`x`."] +theorem units_inv_symm_left {a : Mˣ} {x y : M} (h : SemiconjBy (↑a) x y) : SemiconjBy (↑a⁻¹) y x := + calc + ↑a⁻¹ * y = ↑a⁻¹ * (y * a * ↑a⁻¹) := by rw [Units.mul_inv_cancel_right] + _ = x * ↑a⁻¹ := by rw [← h.eq, ← mul_assoc, Units.inv_mul_cancel_left] +#align semiconj_by.units_inv_symm_left SemiconjBy.units_inv_symm_left +#align add_semiconj_by.add_units_neg_symm_left AddSemiconjBy.addUnits_neg_symm_left + +@[simp, to_additive] +theorem units_inv_symm_left_iff {a : Mˣ} {x y : M} : SemiconjBy (↑a⁻¹) y x ↔ SemiconjBy (↑a) x y := + ⟨units_inv_symm_left, units_inv_symm_left⟩ +#align semiconj_by.units_inv_symm_left_iff SemiconjBy.units_inv_symm_left_iff +#align add_semiconj_by.add_units_neg_symm_left_iff AddSemiconjBy.addUnits_neg_symm_left_iff + +@[to_additive] +theorem units_coe {a x y : Mˣ} (h : SemiconjBy a x y) : SemiconjBy (a : M) x y := + congr_arg Units.val h +#align semiconj_by.units_coe SemiconjBy.units_coe +#align add_semiconj_by.add_units_coe AddSemiconjBy.addUnits_coe + +@[to_additive] +theorem units_of_coe {a x y : Mˣ} (h : SemiconjBy (a : M) x y) : SemiconjBy a x y := + Units.ext h +#align semiconj_by.units_of_coe SemiconjBy.units_of_coe +#align add_semiconj_by.addUnits_of_coe AddSemiconjBy.addUnits_of_coe + +@[simp, to_additive] +theorem units_coe_iff {a x y : Mˣ} : SemiconjBy (a : M) x y ↔ SemiconjBy a x y := + ⟨units_of_coe, units_coe⟩ +#align semiconj_by.units_coe_iff SemiconjBy.units_coe_iff +#align add_semiconj_by.add_units_coe_iff AddSemiconjBy.addUnits_coe_iff + +@[simp, to_additive] theorem pow_right {a x y : M} (h : SemiconjBy a x y) (n : ℕ) : SemiconjBy a (x ^ n) (y ^ n) := by induction' n with n ih · rw [pow_zero, pow_zero] exact SemiconjBy.one_right _ · rw [pow_succ, pow_succ] exact h.mul_right ih +#align semiconj_by.pow_right SemiconjBy.pow_right +#align add_semiconj_by.smul_right AddSemiconjBy.smul_right end Monoid + +section DivisionMonoid + +variable [DivisionMonoid G] {a x y : G} + +@[simp, to_additive] +theorem inv_inv_symm_iff : SemiconjBy a⁻¹ x⁻¹ y⁻¹ ↔ SemiconjBy a y x := + inv_involutive.injective.eq_iff.symm.trans <| by + rw [mul_inv_rev, mul_inv_rev, inv_inv, inv_inv, inv_inv, eq_comm, SemiconjBy] +#align semiconj_by.inv_inv_symm_iff SemiconjBy.inv_inv_symm_iff +#align add_semiconj_by.neg_neg_symm_iff AddSemiconjBy.neg_neg_symm_iff + +@[to_additive] +theorem inv_inv_symm : SemiconjBy a x y → SemiconjBy a⁻¹ y⁻¹ x⁻¹ := + inv_inv_symm_iff.2 +#align semiconj_by.inv_inv_symm SemiconjBy.inv_inv_symm +#align add_semiconj_by.neg_neg_symm AddSemiconjBy.neg_neg_symm + +end DivisionMonoid + +section Group + +variable [Group G] {a x y : G} + +@[simp, to_additive] +theorem inv_right_iff : SemiconjBy a x⁻¹ y⁻¹ ↔ SemiconjBy a x y := + @units_inv_right_iff G _ a ⟨x, x⁻¹, mul_inv_self x, inv_mul_self x⟩ + ⟨y, y⁻¹, mul_inv_self y, inv_mul_self y⟩ +#align semiconj_by.inv_right_iff SemiconjBy.inv_right_iff +#align add_semiconj_by.neg_right_iff AddSemiconjBy.neg_right_iff + +@[to_additive] +theorem inv_right : SemiconjBy a x y → SemiconjBy a x⁻¹ y⁻¹ := + inv_right_iff.2 +#align semiconj_by.inv_right SemiconjBy.inv_right +#align add_semiconj_by.neg_right AddSemiconjBy.neg_right + +@[simp, to_additive] +theorem inv_symm_left_iff : SemiconjBy a⁻¹ y x ↔ SemiconjBy a x y := + @units_inv_symm_left_iff G _ ⟨a, a⁻¹, mul_inv_self a, inv_mul_self a⟩ _ _ +#align semiconj_by.inv_symm_left_iff SemiconjBy.inv_symm_left_iff +#align add_semiconj_by.neg_symm_left_iff AddSemiconjBy.neg_symm_left_iff + +@[to_additive] +theorem inv_symm_left : SemiconjBy a x y → SemiconjBy a⁻¹ y x := + inv_symm_left_iff.2 +#align semiconj_by.inv_symm_left SemiconjBy.inv_symm_left +#align add_semiconj_by.neg_symm_left AddSemiconjBy.neg_symm_left + +/-- `a` semiconjugates `x` to `a * x * a⁻¹`. -/ +@[to_additive "`a` semiconjugates `x` to `a + x + -a`."] +theorem conj_mk (a x : G) : SemiconjBy a x (a * x * a⁻¹) := by + unfold SemiconjBy; rw [mul_assoc, inv_mul_self, mul_one] +#align semiconj_by.conj_mk SemiconjBy.conj_mk +#align add_semiconj_by.conj_mk AddSemiconjBy.conj_mk + +end Group + +end SemiconjBy + +@[simp, to_additive addSemiconjBy_iff_eq] +theorem semiconjBy_iff_eq [CancelCommMonoid M] {a x y : M} : SemiconjBy a x y ↔ x = y := + ⟨fun h => mul_left_cancel (h.trans (mul_comm _ _)), fun h => by rw [h, SemiconjBy, mul_comm]⟩ +#align semiconj_by_iff_eq semiconjBy_iff_eq +#align add_semiconj_by_iff_eq addSemiconjBy_iff_eq + +/-- `a` semiconjugates `x` to `a * x * a⁻¹`. -/ +@[to_additive AddUnits.mk_addSemiconjBy "`a` semiconjugates `x` to `a + x + -a`."] +theorem Units.mk_semiconjBy [Monoid M] (u : Mˣ) (x : M) : SemiconjBy (↑u) x (u * x * ↑u⁻¹) := by + unfold SemiconjBy; rw [Units.inv_mul_cancel_right] +#align units.mk_semiconj_by Units.mk_semiconjBy +#align add_units.mk_semiconj_by AddUnits.mk_addSemiconjBy diff --git a/Mathlib/Logic/Function/Basic.lean b/Mathlib/Logic/Function/Basic.lean index a629beee39c3b..aebc0a28632d6 100644 --- a/Mathlib/Logic/Function/Basic.lean +++ b/Mathlib/Logic/Function/Basic.lean @@ -783,10 +783,13 @@ protected theorem rightInverse : RightInverse f f := h #align involutive.right_inverse Function.Involutive.rightInverse protected theorem injective : Injective f := h.leftInverse.injective +#align function.involutive.injective Function.Involutive.injective protected theorem surjective : Surjective f := fun x ↦ ⟨f x, h x⟩ +#align function.involutive.surjective Function.Involutive.surjective protected theorem bijective : Bijective f := ⟨h.injective, h.surjective⟩ +#align function.involutive.bijective Function.Involutive.bijective /-- Involuting an `ite` of an involuted value `x : α` negates the `Prop` condition in the `ite`. -/ protected theorem ite_not (P : Prop) [Decidable P] (x : α) : f (ite P x (f x)) = ite (¬P) x (f x) :=