Documentation

TauCeti.Algebra.Group.CommuteOrNeg

Commutation up to a central sign #

The relation CommuteOrNeg a x records that a commutes with x or that it anticommutes with x. Its closure laws are useful when a group is generated by elements that pairwise commute or anticommute.

source
def TauCeti.CommuteOrNeg {M : Type u_1} [Mul M] [HasDistribNeg M] (a x : M) :
Prop

Two elements commute or anticommute.

Instances For
    source
    theorem TauCeti.CommuteOrNeg.of_commute {M : Type u_1} [Mul M] [HasDistribNeg M] {a x : M} (h : Commute a x) :
    CommuteOrNeg a x

    Construct commutation up to a sign from ordinary commutation.

    source
    theorem TauCeti.CommuteOrNeg.of_semiconjBy {M : Type u_1} [Mul M] [HasDistribNeg M] {a x : M} (h : SemiconjBy a x (-x)) :
    CommuteOrNeg a x

    Construct commutation up to a sign from anticommutation.

    source
    theorem TauCeti.CommuteOrNeg.out {M : Type u_1} [Mul M] [HasDistribNeg M] {a x : M} :
    CommuteOrNeg a x → Commute a x ∨ SemiconjBy a x (-x)

    Eliminate commutation up to a sign into its two alternatives.

    source
    theorem TauCeti.CommuteOrNeg.symm {M : Type u_1} [Mul M] [HasDistribNeg M] {a x : M} :
    CommuteOrNeg a x → CommuteOrNeg x a

    Commutation up to a sign is symmetric.

    source
    theorem TauCeti.CommuteOrNeg.mul_right {M : Type u_1} [Semigroup M] [HasDistribNeg M] {a x y : M} (hx : CommuteOrNeg a x) (hy : CommuteOrNeg a y) :
    CommuteOrNeg a (x * y)

    Commutation up to a sign is preserved by multiplication on the right.

    source
    theorem TauCeti.CommuteOrNeg.inv_right {M : Type u_1} [Group M] [HasDistribNeg M] {a x : M} (hx : CommuteOrNeg a x) :
    CommuteOrNeg a x⁻¹

    Commutation up to a sign is preserved by inversion on the right.

    source
    theorem TauCeti.CommuteOrNeg.mul_left {M : Type u_1} [Semigroup M] [HasDistribNeg M] {a x y : M} (hx : CommuteOrNeg x a) (hy : CommuteOrNeg y a) :
    CommuteOrNeg (x * y) a

    Commutation up to a sign is preserved by multiplication on the left.

    source
    theorem TauCeti.CommuteOrNeg.inv_left {M : Type u_1} [Group M] [HasDistribNeg M] {a x : M} (hx : CommuteOrNeg x a) :
    CommuteOrNeg x⁻¹ a

    Commutation up to a sign is preserved by inversion on the left.

    source
    @[simp]
    theorem TauCeti.CommuteOrNeg.refl {M : Type u_1} [Mul M] [HasDistribNeg M] (a : M) :
    CommuteOrNeg a a

    Every element commutes or anticommutes with itself.

    source
    @[simp]
    theorem TauCeti.CommuteOrNeg.one_left {M : Type u_1} [MulOneClass M] [HasDistribNeg M] (x : M) :
    CommuteOrNeg 1 x

    The identity commutes or anticommutes with every element.

    source
    @[simp]
    theorem TauCeti.CommuteOrNeg.one_right {M : Type u_1} [MulOneClass M] [HasDistribNeg M] (x : M) :
    CommuteOrNeg x 1

    Every element commutes or anticommutes with the identity.

    source
    theorem TauCeti.CommuteOrNeg.of_mem_closure {G : Type u_1} [Group G] [HasDistribNeg G] {S : Set G} (h : ∀ x ∈ S, ∀ y ∈ S, CommuteOrNeg x y) {x y : G} (hx : x ∈ Subgroup.closure S) (hy : y ∈ Subgroup.closure S) :
    CommuteOrNeg x y

    Pairwise commutation up to a sign extends from a set to its subgroup closure.