Built with
doc-gen4 , running Lean4.
Bubbles (
) indicate interactive fragments: hover for details, tap to reveal contents.
Use
Ctrl+β Ctrl+β to navigate,
Ctrl+π±οΈ to focus.
On Mac, use
Cmd instead of
Ctrl .
/-
Copyright (c) 2019 Yury Kudryashov. All rights reserved.
Released under Apache 2.0 license as described in the file LICENSE.
Authors: Yury Kudryashov
Some proofs and docs came from `algebra/commute` (c) Neil Strickland
! This file was ported from Lean 3 source module algebra.group.semiconj
! leanprover-community/mathlib commit a148d797a1094ab554ad4183a4ad6f130358ef64
! Please do not edit these lines, except to modify the commit id
! if you have ported upstream changes.
-/
import Mathlib.Algebra.Group.Units
/-!
# Semiconjugate elements of a semigroup
## Main definitions
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 = 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]`.
This file provides only basic operations (`mul_left`, `mul_right`, `inv_right` etc). Other
operations (`pow_right`, field inverse etc) are in the files that define corresponding notions.
-/
/-- `x` is semiconjugate to `y` by `a`, if `a * x = y * a`. -/
@[ to_additive AddSemiconjBy : {M : Type u_1} β [inst : Add M M β M β M β Prop "`x` is additive semiconjugate to `y` by `a` if `a + x = y + a`"]
def SemiconjBy : {M : Type u_1} β [inst : Mul M M β M β M β Prop SemiconjBy [ Mul M ] ( a x y : M ) : Prop :=
a * x = y * a
#align semiconj_by SemiconjBy : {M : Type u_1} β [inst : Mul M M β M β M β Prop
#align add_semiconj_by AddSemiconjBy : {M : Type u_1} β [inst : Add M M β M β M β Prop
namespace SemiconjBy
/-- 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 : {M : Type ?u.140} β [inst : Mul M M β M β M β Prop a x y ) : a * x = y * a :=
h
#align semiconj_by.eq SemiconjBy.eq
#align add_semiconj_by.eq AddSemiconjBy.eq
section Semigroup
variable [ Semigroup : Type ?u.1081 β Type ?u.1081 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'`. -/
@[ to_additive ( attr := simp ) "If `a` semiconjugates `x` to `y` and `x'` to `y'`,
then it semiconjugates `x + x'` to `y + y'`."]
theorem mul_right ( h : SemiconjBy : {M : Type ?u.297} β [inst : Mul M M β M β M β Prop a x y ) ( h' : SemiconjBy : {M : Type ?u.411} β [inst : Mul M M β M β M β Prop a x' y' ) :
SemiconjBy : {M : Type ?u.420} β [inst : Mul M M β M β M β Prop a ( x * x' ) ( y * y' ) := by
unfold SemiconjBy : {M : Type u_1} β [inst : Mul M M β M β M β Prop a * (x * x' = y * y' * a
-- TODO this could be done using `assoc_rw` if/when this is ported to mathlib4
rw [ a * (x * x' = y * y' * a β mul_assoc : β {G : Type ?u.716} [inst : Semigroup G a b c : G ), a * b * c = a * (b * c , a * (x * x' = y * y' * a h . eq , a * (x * x' = y * y' * a mul_assoc : β {G : Type ?u.877} [inst : Semigroup G a b c : G ), a * b * c = a * (b * c , y * (a * x' = y * y' * a a * (x * x' = y * y' * a h' . eq , y * (y' * a = y * y' * a a * (x * x' = y * y' * a β mul_assoc : β {G : Type ?u.915} [inst : Semigroup G a b c : G ), a * b * c = a * (b * c ]
#align semiconj_by.mul_right SemiconjBy.mul_right
#align add_semiconj_by.add_right AddSemiconjBy.add_right
/-- 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 : {M : Type ?u.1098} β [inst : Mul M M β M β M β Prop a y z ) ( hb : SemiconjBy : {M : Type ?u.1212} β [inst : Mul M M β M β M β Prop b x y ) : SemiconjBy : {M : Type ?u.1221} β [inst : Mul M M β M β M β Prop ( a * b ) x z := by
unfold SemiconjBy : {M : Type u_1} β [inst : Mul M M β M β M β Prop
rw [ mul_assoc : β {G : Type ?u.1420} [inst : Semigroup G a b c : G ), a * b * c = a * (b * c , a * (b * x = z * (a * b hb . eq , a * (y * b = z * (a * b β mul_assoc : β {G : Type ?u.1581} [inst : Semigroup G a b c : G ), a * b * c = a * (b * c , ha . eq , mul_assoc : β {G : Type ?u.1619} [inst : Semigroup G a b c : G ), a * b * c = a * (b * c z * (a * b = z * (a * b ]
#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 : {Ξ² : Sort ?u.1724} β (Ξ² β Ξ² β Prop Prop fun a b : S β¦ β c , SemiconjBy : {M : Type ?u.1735} β [inst : Mul M M β M β M β Prop 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 [ MulOneClass : Type ?u.2905 β Type ?u.2905 M ]
/-- Any element semiconjugates `1` to `1`. -/
@[ to_additive ( attr := simp ) "Any element semiconjugates `0` to `0`."]
theorem one_right ( a : M ) : SemiconjBy : {M : Type ?u.2613} β [inst : Mul M M β M β M β Prop a 1 1 := by rw [ SemiconjBy : {M : Type ?u.2792} β [inst : Mul M M β M β M β Prop , 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. -/
@[ to_additive ( attr := simp ) "Zero semiconjugates any element to itself."]
theorem one_left ( x : M ) : SemiconjBy : {M : Type ?u.2910} β [inst : Mul M M β M β M β Prop 1 x x :=
Eq.symm : β {Ξ± : Sort ?u.3056} {a b : Ξ± }, a = b b = a <| 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 `AddZeroClass` type) is reflexive."]
protected theorem reflexive : Reflexive : {Ξ² : Sort ?u.3130} β (Ξ² β Ξ² β Prop Prop fun a b : M β¦ β c , SemiconjBy : {M : Type ?u.3141} β [inst : Mul M M β M β M β Prop 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 [ 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 : {M : Type ?u.3371} β [inst : Mul M M β M β M β Prop a x y ) : SemiconjBy : {M : Type ?u.3626} β [inst : Mul M M β M β M β Prop a β x β»ΒΉ β y β»ΒΉ :=
calc
a * β x β»ΒΉ = β y β»ΒΉ * ( y * a ) * β x β»ΒΉ := by rw [ Units.inv_mul_cancel_left : β {Ξ± : Type ?u.4589} [inst : Monoid Ξ± a : Ξ± Λ£ b : Ξ± ), βa β»ΒΉ * (βa * b = b ]
_ = β y β»ΒΉ * a := by rw [ β h . eq , mul_assoc : β {G : Type ?u.4676} [inst : Semigroup G a b c : G ), a * b * c = a * (b * c , Units.mul_inv_cancel_right : β {Ξ± : Type ?u.4724} [inst : Monoid Ξ± a : Ξ± ) (b : Ξ± Λ£ a * βb * βb β»ΒΉ = a ]
#align semiconj_by.units_inv_right SemiconjBy.units_inv_right
#align add_semiconj_by.add_units_neg_right AddSemiconjBy.addUnits_neg_right
@[ to_additive ( attr := simp )]
theorem units_inv_right_iff { a : M } { x y : M Λ£} : SemiconjBy : {M : Type ?u.4824} β [inst : Mul M M β M β M β Prop a β x β»ΒΉ β y β»ΒΉ β SemiconjBy : {M : Type ?u.5088} β [inst : Mul M M β M β M β Prop 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 : {M : Type ?u.5462} β [inst : Mul M M β M β M β Prop (β a ) x y ) : SemiconjBy : {M : Type ?u.5489} β [inst : Mul M M β M β M β Prop (β a β»ΒΉ) y x :=
calc
β a β»ΒΉ * y = β a β»ΒΉ * ( y * a * β a β»ΒΉ) := by rw [ Units.mul_inv_cancel_right : β {Ξ± : Type ?u.6376} [inst : Monoid Ξ± a : Ξ± ) (b : Ξ± Λ£ a * βb * βb β»ΒΉ = a ]
_ = x * β a β»ΒΉ := by rw [ β h . eq , β mul_assoc : β {G : Type ?u.6463} [inst : Semigroup G a b c : G ), a * b * c = a * (b * c , Units.inv_mul_cancel_left : β {Ξ± : Type ?u.6511} [inst : Monoid Ξ± a : Ξ± Λ£ b : Ξ± ), βa β»ΒΉ * (βa * b = b ]
#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
@[ to_additive ( attr := simp )]
theorem units_inv_symm_left_iff { a : M Λ£} { x y : M } : SemiconjBy : {M : Type ?u.6609} β [inst : Mul M M β M β M β Prop (β a β»ΒΉ) y x β SemiconjBy : {M : Type ?u.6630} β [inst : Mul M M β M β M β Prop (β 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_val { a x y : M Λ£} ( h : SemiconjBy : {M : Type ?u.7048} β [inst : Mul M M β M β M β Prop a x y ) : SemiconjBy : {M : Type ?u.7074} β [inst : Mul M M β M β M β Prop ( a : M ) x y :=
congr_arg : β {Ξ± : Sort ?u.7431} {Ξ² : Sort ?u.7430} {aβ aβ : Ξ± } (f : Ξ± β Ξ² aβ = aβ f aβ = f aβ Units.val : {Ξ± : Type ?u.7436} β [inst : Monoid Ξ± Ξ± Λ£ Ξ± h
#align semiconj_by.units_coe SemiconjBy.units_val
#align add_semiconj_by.add_units_coe AddSemiconjBy.addUnits_val
@[ to_additive ]
theorem units_of_val { a x y : M Λ£} ( h : SemiconjBy : {M : Type ?u.7525} β [inst : Mul M M β M β M β Prop ( a : M ) x y ) : SemiconjBy : {M : Type ?u.7882} β [inst : Mul M M β M β M β Prop a x y :=
Units.ext h
#align semiconj_by.units_of_coe SemiconjBy.units_of_val
#align add_semiconj_by.add_units_of_coe AddSemiconjBy.addUnits_of_val
@[ to_additive ( attr := simp )]
theorem units_val_iff { a x y : M Λ£} : SemiconjBy : {M : Type ?u.7987} β [inst : Mul M M β M β M β Prop ( a : M ) x y β SemiconjBy : {M : Type ?u.8338} β [inst : Mul M M β M β M β Prop a x y :=
β¨ units_of_val , units_val β©
#align semiconj_by.units_coe_iff SemiconjBy.units_val_iff
#align add_semiconj_by.add_units_coe_iff AddSemiconjBy.addUnits_val_iff
@[ to_additive ( attr := simp )]
theorem pow_right { a x y : M } ( h : SemiconjBy : {M : Type ?u.8503} β [inst : Mul M M β M β M β Prop a x y ) ( n : β ) : SemiconjBy : {M : Type ?u.8532} β [inst : Mul M M β M β M β Prop a ( x ^ n ) ( y ^ n ) := by
induction' n with n ih
Β· rw [ pow_zero : β {M : Type ?u.9106} [inst : Monoid M a : M ), a ^ 0 = 1 , pow_zero : β {M : Type ?u.9142} [inst : Monoid M a : M ), a ^ 0 = 1 ]
exact SemiconjBy.one_right _
Β· rw [ pow_succ : β {M : Type ?u.9197} [inst : Monoid M a : M ) (n : β ), a ^ (n + 1 = a * a ^ n , pow_succ : β {M : Type ?u.9218} [inst : Monoid M a : M ) (n : β ), a ^ (n + 1 = a * a ^ n ]
exact h . mul_right ih
#align semiconj_by.pow_right SemiconjBy.pow_right
#align add_semiconj_by.nsmul_right AddSemiconjBy.nsmul_right
end Monoid
section DivisionMonoid
variable [ DivisionMonoid : Type ?u.9431 β Type ?u.9431 G ] { a x y : G }
@[ to_additive ( attr := simp )]
theorem inv_inv_symm_iff : SemiconjBy : {M : Type ?u.9440} β [inst : Mul M M β M β M β Prop a β»ΒΉ x β»ΒΉ y β»ΒΉ β SemiconjBy : {M : Type ?u.9534} β [inst : Mul M M β M β M β Prop 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 : β {Ξ± : Sort ?u.9761} {a b : Ξ± }, a = b β b = a , SemiconjBy : {M : Type ?u.9831} β [inst : Mul M M β M β M β Prop ]
#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 : {M : Type ?u.9947} β [inst : Mul M M β M β M β Prop a x y β SemiconjBy : {M : Type ?u.9993} β [inst : Mul M M β M β M β Prop a β»ΒΉ y β»ΒΉ x β»ΒΉ :=
inv_inv_symm_iff . 2 : β {a b : Prop }, (a β b b β a
#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 }
@[ to_additive ( attr := simp )]
theorem inv_right_iff : SemiconjBy : {M : Type ?u.10144} β [inst : Mul M M β M β M β Prop a x β»ΒΉ y β»ΒΉ β SemiconjBy : {M : Type ?u.10231} β [inst : Mul M M β M β M β Prop 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 : {M : Type ?u.10505} β [inst : Mul M M β M β M β Prop a x y β SemiconjBy : {M : Type ?u.10543} β [inst : Mul M M β M β M β Prop a x β»ΒΉ y β»ΒΉ :=
inv_right_iff . 2 : β {a b : Prop }, (a β b b β a
#align semiconj_by.inv_right SemiconjBy.inv_right
#align add_semiconj_by.neg_right AddSemiconjBy.neg_right
@[ to_additive ( attr := simp )]
theorem inv_symm_left_iff : SemiconjBy : {M : Type ?u.10680} β [inst : Mul M M β M β M β Prop a β»ΒΉ y x β SemiconjBy : {M : Type ?u.10756} β [inst : Mul M M β M β M β Prop 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 : {M : Type ?u.10988} β [inst : Mul M M β M β M β Prop a x y β SemiconjBy : {M : Type ?u.11026} β [inst : Mul M M β M β M β Prop a β»ΒΉ y x :=
inv_symm_left_iff . 2 : β {a b : Prop }, (a β b b β a
#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 : {M : Type ?u.11156} β [inst : Mul M M β M β M β Prop a x ( a * x * a β»ΒΉ) := by
G : Type u_1instβ : Group G aβ, xβ, y, a, x : G unfold SemiconjBy : {M : Type u_1} β [inst : Mul M M β M β M β Prop G : Type u_1instβ : Group G aβ, xβ, y, a, x : G ; G : Type u_1instβ : Group G aβ, xβ, y, a, x : G G : Type u_1instβ : Group G aβ, xβ, y, a, x : G rw [ G : Type u_1instβ : Group G aβ, xβ, y, a, x : G mul_assoc : β {G : Type ?u.11346} [inst : Semigroup G a b c : G ), a * b * c = a * (b * c , G : Type u_1instβ : Group G aβ, xβ, y, a, x : G G : Type u_1instβ : Group G aβ, xβ, y, a, x : G inv_mul_self , G : Type u_1instβ : Group G aβ, xβ, y, a, x : G G : Type u_1instβ : Group G aβ, xβ, y, a, x : G mul_one G : Type u_1instβ : Group G aβ, xβ, y, a, x : G ]
#align semiconj_by.conj_mk SemiconjBy.conj_mk
#align add_semiconj_by.conj_mk AddSemiconjBy.conj_mk
end Group
end SemiconjBy
@[ to_additive ( attr := simp ) addSemiconjBy_iff_eq ]
theorem semiconjBy_iff_eq [ CancelCommMonoid : Type ?u.11593 β Type ?u.11593 M ] { a x y : M } : SemiconjBy : {M : Type ?u.11602} β [inst : Mul M M β M β M β Prop a x y β x = y :=
β¨ fun h => mul_left_cancel ( h . trans : β {Ξ± : Sort ?u.11729} {a b c : Ξ± }, a = b b = c a = c ( mul_comm _ _ )), fun h => by rw [ h , SemiconjBy : {M : Type ?u.11929} β [inst : Mul M M β M β M β Prop , 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 : {M : Type ?u.12082} β [inst : Mul M M β M β M β Prop (β u ) x ( u * x * β u β»ΒΉ) := by
unfold SemiconjBy : {M : Type u_1} β [inst : Mul M M β M β M β Prop ; rw [ Units.inv_mul_cancel_right : β {Ξ± : Type ?u.12551} [inst : Monoid Ξ± a : Ξ± ) (b : Ξ± Λ£ a * βb β»ΒΉ * βb = a ]
#align units.mk_semiconj_by Units.mk_semiconjBy
#align add_units.mk_semiconj_by AddUnits.mk_addSemiconjBy