Documentation

Coxeter.Opposite

Opposite Coxeter group #

This file proves properties of the opposite of a Coxeter group.

def Coxeter.cs_op {W : Type u_1} [CoxeterGroup W] :

CoxeterSystem CoxeterGroup.M Wᵐᵒᵖ

Equations

Coxeter.cs_op = { mulEquiv := (MulEquiv.inv' W).symm.trans Coxeter.CoxeterGroup.cs.mulEquiv }

Instances For

@[implicit_reducible]

instance Coxeter.instCoxeterGroupMulOpposite {W : Type u_1} [CoxeterGroup W] :

CoxeterGroup Wᵐᵒᵖ

Equations

Coxeter.instCoxeterGroupMulOpposite = { toGroup := MulOpposite.instGroup, B := Coxeter.CoxeterGroup.B W, M := Coxeter.CoxeterGroup.M, cs := Coxeter.cs_op }

theorem Coxeter.simple_op {W : Type u_1} [CoxeterGroup W] (i : CoxeterGroup.B W) :

CoxeterGroup.cs.simple i = MulOpposite.op (CoxeterGroup.cs.simple i)

theorem Coxeter.wordProd_op {W : Type u_1} [CoxeterGroup W] (ω : List (CoxeterGroup.B W)) :

CoxeterGroup.cs.wordProd ω = MulOpposite.op (CoxeterGroup.cs.wordProd ω.reverse)

theorem Coxeter.length_op {W : Type u_1} [CoxeterGroup W] (w : W) :

CoxeterGroup.cs.length (MulOpposite.op w) = CoxeterGroup.cs.length w

theorem Coxeter.isLeftDescent_op_iff {W : Type u_1} [CoxeterGroup W] (w : W) (i : CoxeterGroup.B W) :

CoxeterGroup.cs.IsLeftDescent (MulOpposite.op w) i ↔ CoxeterGroup.cs.IsRightDescent w i

theorem Coxeter.isReflection_op_iff {W : Type u_1} [CoxeterGroup W] (t : W) :

CoxeterGroup.cs.IsReflection (MulOpposite.op t) ↔ CoxeterGroup.cs.IsReflection t

theorem Coxeter.isLeftInversion_op_iff {W : Type u_1} [CoxeterGroup W] (w t : W) :

CoxeterGroup.cs.IsLeftInversion (MulOpposite.op w) (MulOpposite.op t) ↔ CoxeterGroup.cs.IsRightInversion w t

theorem Coxeter.leftInvSeq_op {W : Type u_1} [CoxeterGroup W] (ω : List (CoxeterGroup.B W)) :

CoxeterGroup.cs.leftInvSeq ω = List.map MulOpposite.op (CoxeterGroup.cs.leftInvSeq ω)