Composing, inverting and conjugating equivalences of root pairings

Equivalences of root pairings form a groupoid: RootPairing.Equiv.comp composes them, RootPairing.Equiv.id is the identity and RootPairing.Equiv.symm inverts. This file records the laws of that groupoid which relate composition and inversion, together with the weight- and coweight-space linear equivalences of a composite.

Conjugation by an equivalence e : P.Equiv Q is then built out of those laws: it carries an automorphism g of P to e ∘ g ∘ e⁻¹, an automorphism of Q, and does so compatibly with the group structures, with the weight-space, coweight-space and index-set data of an automorphism, and with the actions of the automorphism groups on weight vectors and on root indices.

The statements are about two or three root pairings with unrelated index sets, weight spaces and coweight spaces; nothing here needs any finiteness, reducedness or crystallographic hypothesis. Laws about a single pairing are already available from the Group (RootPairing.Equiv P P) instance, so they are not restated here.

Main definitions

• RootPairing.Equiv.autCongr: conjugation by an equivalence, as a group isomorphism P.Aut ≃* Q.Aut.

Main results

• RootPairing.Equiv.self_comp_symm and RootPairing.Equiv.symm_comp_self: an equivalence composes with its inverse to the identity, in both orders.
• RootPairing.Equiv.symm_comp: the inverse of a composite is the composite of the inverses in the reverse order.
• RootPairing.Equiv.weightEquiv_comp and RootPairing.Equiv.coweightEquiv_comp: the weight- and coweight-space equivalences of a composite.
• RootPairing.Equiv.weightEquiv_autCongr_apply, RootPairing.Equiv.coweightEquiv_autCongr_apply and RootPairing.Equiv.indexEquiv_autCongr_apply: the weight-space map, the coweight-space map and the index permutation of a conjugated automorphism are the conjugates of the originals.
• RootPairing.Equiv.smul_index_eq_indexEquiv: an automorphism acts on root indices through its index permutation.
• RootPairing.Equiv.autCongr_smul and RootPairing.Equiv.autCongr_smul_index: conjugation transports the actions on weight vectors and on root indices.
• RootPairing.Equiv.autCongr_id and RootPairing.Equiv.autCongr_comp: conjugation is functorial.

References

• N. Bourbaki, Lie Groups and Lie Algebras, Chapters 4--6, Ch. VI, §1.

@[simp]

theorem RootPairing.Equiv.self_comp_symm {ι : Type u_1} {ι₂ : Type u_2} {R : Type u_4} {M : Type u_5} {N : Type u_6} {M₂ : Type u_7} {N₂ : Type u_8} [CommRing R] [AddCommGroup M] [Module R M] [AddCommGroup N] [Module R N] [AddCommGroup M₂] [Module R M₂] [AddCommGroup N₂] [Module R N₂] {P : RootPairing ι R M N} {Q : RootPairing ι₂ R M₂ N₂} (e : P.Equiv Q) : e.comp (symm P Q e) = id Q

An equivalence of root pairings composed with its inverse is the identity of the target.

@[simp]

theorem RootPairing.Equiv.symm_comp_self {ι : Type u_1} {ι₂ : Type u_2} {R : Type u_4} {M : Type u_5} {N : Type u_6} {M₂ : Type u_7} {N₂ : Type u_8} [CommRing R] [AddCommGroup M] [Module R M] [AddCommGroup N] [Module R N] [AddCommGroup M₂] [Module R M₂] [AddCommGroup N₂] [Module R N₂] {P : RootPairing ι R M N} {Q : RootPairing ι₂ R M₂ N₂} (e : P.Equiv Q) : (symm P Q e).comp e = id P

The inverse of an equivalence of root pairings composed with it is the identity of the source.

@[simp]

theorem RootPairing.Equiv.weightEquiv_comp {ι : Type u_1} {ι₂ : Type u_2} {ι₃ : Type u_3} {R : Type u_4} {M : Type u_5} {N : Type u_6} {M₂ : Type u_7} {N₂ : Type u_8} {M₃ : Type u_9} {N₃ : Type u_10} [CommRing R] [AddCommGroup M] [Module R M] [AddCommGroup N] [Module R N] [AddCommGroup M₂] [Module R M₂] [AddCommGroup N₂] [Module R N₂] [AddCommGroup M₃] [Module R M₃] [AddCommGroup N₃] [Module R N₃] {P : RootPairing ι R M N} {Q : RootPairing ι₂ R M₂ N₂} {S : RootPairing ι₃ R M₃ N₃} (e : P.Equiv Q) (f : Q.Equiv S) : (f.comp e).weightEquiv = e.weightEquiv ≪≫ₗ f.weightEquiv

The weight-space equivalence of a composite is the composite of the weight-space equivalences.

@[simp]

theorem RootPairing.Equiv.coweightEquiv_comp {ι : Type u_1} {ι₂ : Type u_2} {ι₃ : Type u_3} {R : Type u_4} {M : Type u_5} {N : Type u_6} {M₂ : Type u_7} {N₂ : Type u_8} {M₃ : Type u_9} {N₃ : Type u_10} [CommRing R] [AddCommGroup M] [Module R M] [AddCommGroup N] [Module R N] [AddCommGroup M₂] [Module R M₂] [AddCommGroup N₂] [Module R N₂] [AddCommGroup M₃] [Module R M₃] [AddCommGroup N₃] [Module R N₃] {P : RootPairing ι R M N} {Q : RootPairing ι₂ R M₂ N₂} {S : RootPairing ι₃ R M₃ N₃} (e : P.Equiv Q) (f : Q.Equiv S) : (f.comp e).coweightEquiv = f.coweightEquiv ≪≫ₗ e.coweightEquiv

The coweight-space equivalence of a composite is the composite of the coweight-space equivalences, in the reverse order.

@[simp]

theorem RootPairing.Equiv.symm_comp {ι : Type u_1} {ι₂ : Type u_2} {ι₃ : Type u_3} {R : Type u_4} {M : Type u_5} {N : Type u_6} {M₂ : Type u_7} {N₂ : Type u_8} {M₃ : Type u_9} {N₃ : Type u_10} [CommRing R] [AddCommGroup M] [Module R M] [AddCommGroup N] [Module R N] [AddCommGroup M₂] [Module R M₂] [AddCommGroup N₂] [Module R N₂] [AddCommGroup M₃] [Module R M₃] [AddCommGroup N₃] [Module R N₃] {P : RootPairing ι R M N} {Q : RootPairing ι₂ R M₂ N₂} {S : RootPairing ι₃ R M₃ N₃} (e : P.Equiv Q) (f : Q.Equiv S) : symm P S (f.comp e) = (symm P Q e).comp (symm Q S f)

The inverse of a composite of equivalences is the composite of the inverses, in the reverse order.

theorem RootPairing.Equiv.smul_index_eq_indexEquiv {ι : Type u_1} {R : Type u_4} {M : Type u_5} {N : Type u_6} [CommRing R] [AddCommGroup M] [Module R M] [AddCommGroup N] [Module R N] {P : RootPairing ι R M N} (g : P.Aut) (i : ι) : g • i = (↑g).indexEquiv i

The action of the automorphism group on root indices is through indexEquiv.

Not a simp lemma: it would rewrite the left-hand side of the simp lemma RootPairing.Equiv.autCongr_smul_index, which is stated for the action.

noncomputable def RootPairing.Equiv.autCongr {ι : Type u_1} {ι₂ : Type u_2} {R : Type u_4} {M : Type u_5} {N : Type u_6} {M₂ : Type u_7} {N₂ : Type u_8} [CommRing R] [AddCommGroup M] [Module R M] [AddCommGroup N] [Module R N] [AddCommGroup M₂] [Module R M₂] [AddCommGroup N₂] [Module R N₂] {P : RootPairing ι R M N} {Q : RootPairing ι₂ R M₂ N₂} (e : P.Equiv Q) : P.Aut ≃* Q.Aut

Conjugation by an equivalence of root pairings, as a group isomorphism of automorphism groups: an automorphism g of P is carried to e ∘ g ∘ e⁻¹.

theorem RootPairing.Equiv.autCongr_apply {ι : Type u_1} {ι₂ : Type u_2} {R : Type u_4} {M : Type u_5} {N : Type u_6} {M₂ : Type u_7} {N₂ : Type u_8} [CommRing R] [AddCommGroup M] [Module R M] [AddCommGroup N] [Module R N] [AddCommGroup M₂] [Module R M₂] [AddCommGroup N₂] [Module R N₂] {P : RootPairing ι R M N} {Q : RootPairing ι₂ R M₂ N₂} (e : P.Equiv Q) (g : P.Aut) : e.autCongr g = e.comp (comp g (symm P Q e))

theorem RootPairing.Equiv.autCongr_symm_apply {ι : Type u_1} {ι₂ : Type u_2} {R : Type u_4} {M : Type u_5} {N : Type u_6} {M₂ : Type u_7} {N₂ : Type u_8} [CommRing R] [AddCommGroup M] [Module R M] [AddCommGroup N] [Module R N] [AddCommGroup M₂] [Module R M₂] [AddCommGroup N₂] [Module R N₂] {P : RootPairing ι R M N} {Q : RootPairing ι₂ R M₂ N₂} (e : P.Equiv Q) (h : Q.Aut) : e.autCongr.symm h = (symm P Q e).comp (comp h e)

theorem RootPairing.Equiv.weightEquiv_autCongr_apply {ι : Type u_1} {ι₂ : Type u_2} {R : Type u_4} {M : Type u_5} {N : Type u_6} {M₂ : Type u_7} {N₂ : Type u_8} [CommRing R] [AddCommGroup M] [Module R M] [AddCommGroup N] [Module R N] [AddCommGroup M₂] [Module R M₂] [AddCommGroup N₂] [Module R N₂] {P : RootPairing ι R M N} {Q : RootPairing ι₂ R M₂ N₂} (e : P.Equiv Q) (g : P.Aut) (x : M₂) : (weightEquiv (e.autCongr g)) x = e.weightEquiv ((weightEquiv g) (e.weightEquiv.symm x))

The weight-space map of a conjugated automorphism is the conjugated weight-space map.

Not a simp lemma: RootPairing.Equiv.weightEquiv_apply rewrites the left-hand side to the underlying weightMap, so the statement is not in simp-normal form. The intended interface is RootPairing.Equiv.autCongr_smul, which is stated for the weight-space action.

theorem RootPairing.Equiv.coweightEquiv_autCongr_apply {ι : Type u_1} {ι₂ : Type u_2} {R : Type u_4} {M : Type u_5} {N : Type u_6} {M₂ : Type u_7} {N₂ : Type u_8} [CommRing R] [AddCommGroup M] [Module R M] [AddCommGroup N] [Module R N] [AddCommGroup M₂] [Module R M₂] [AddCommGroup N₂] [Module R N₂] {P : RootPairing ι R M N} {Q : RootPairing ι₂ R M₂ N₂} (e : P.Equiv Q) (g : P.Aut) (y : N₂) : (coweightEquiv (e.autCongr g)) y = e.coweightEquiv.symm ((coweightEquiv g) (e.coweightEquiv y))

The coweight-space map of a conjugated automorphism is the conjugated coweight-space map. Note that RootPairing.Equiv.coweightEquiv is contravariant, so the conjugation runs the other way round than for weight spaces; applying e.coweightEquiv to both sides turns this into e.coweightEquiv ((e.autCongr g).coweightEquiv y) = g.coweightEquiv (e.coweightEquiv y).

Not a simp lemma, for the same reason as RootPairing.Equiv.weightEquiv_autCongr_apply: RootPairing.Equiv.coweightEquiv_apply rewrites the left-hand side to the underlying coweightMap.

@[simp]

theorem RootPairing.Equiv.indexEquiv_autCongr_apply {ι : Type u_1} {ι₂ : Type u_2} {R : Type u_4} {M : Type u_5} {N : Type u_6} {M₂ : Type u_7} {N₂ : Type u_8} [CommRing R] [AddCommGroup M] [Module R M] [AddCommGroup N] [Module R N] [AddCommGroup M₂] [Module R M₂] [AddCommGroup N₂] [Module R N₂] {P : RootPairing ι R M N} {Q : RootPairing ι₂ R M₂ N₂} (e : P.Equiv Q) (g : P.Aut) (i : ι₂) : (↑(e.autCongr g)).indexEquiv i = (↑e).indexEquiv ((↑g).indexEquiv ((↑e).indexEquiv.symm i))

The index permutation of a conjugated automorphism is the conjugated index permutation.

theorem RootPairing.Equiv.autCongr_smul {ι : Type u_1} {ι₂ : Type u_2} {R : Type u_4} {M : Type u_5} {N : Type u_6} {M₂ : Type u_7} {N₂ : Type u_8} [CommRing R] [AddCommGroup M] [Module R M] [AddCommGroup N] [Module R N] [AddCommGroup M₂] [Module R M₂] [AddCommGroup N₂] [Module R N₂] {P : RootPairing ι R M N} {Q : RootPairing ι₂ R M₂ N₂} (e : P.Equiv Q) (g : P.Aut) (x : M) : e.autCongr g • e.weightEquiv x = e.weightEquiv (g • x)

Conjugation transports the action on weight vectors along e.weightEquiv.

Not a simp lemma: RootPairing.Equiv.weightEquiv_apply rewrites e.weightEquiv x in the left-hand side to (↑e).weightMap x, so the statement is not in simp-normal form.

@[simp]

theorem RootPairing.Equiv.autCongr_smul_index {ι : Type u_1} {ι₂ : Type u_2} {R : Type u_4} {M : Type u_5} {N : Type u_6} {M₂ : Type u_7} {N₂ : Type u_8} [CommRing R] [AddCommGroup M] [Module R M] [AddCommGroup N] [Module R N] [AddCommGroup M₂] [Module R M₂] [AddCommGroup N₂] [Module R N₂] {P : RootPairing ι R M N} {Q : RootPairing ι₂ R M₂ N₂} (e : P.Equiv Q) (g : P.Aut) (i : ι) : e.autCongr g • (↑e).indexEquiv i = (↑e).indexEquiv (g • i)

Conjugation transports the action on root indices along e.indexEquiv.

@[simp]

theorem RootPairing.Equiv.autCongr_id {ι : Type u_1} {R : Type u_4} {M : Type u_5} {N : Type u_6} [CommRing R] [AddCommGroup M] [Module R M] [AddCommGroup N] [Module R N] {P : RootPairing ι R M N} : (id P).autCongr = MulEquiv.refl P.Aut

Conjugation by the identity equivalence is the identity.

@[simp]

theorem RootPairing.Equiv.autCongr_comp {ι : Type u_1} {ι₂ : Type u_2} {ι₃ : Type u_3} {R : Type u_4} {M : Type u_5} {N : Type u_6} {M₂ : Type u_7} {N₂ : Type u_8} {M₃ : Type u_9} {N₃ : Type u_10} [CommRing R] [AddCommGroup M] [Module R M] [AddCommGroup N] [Module R N] [AddCommGroup M₂] [Module R M₂] [AddCommGroup N₂] [Module R N₂] [AddCommGroup M₃] [Module R M₃] [AddCommGroup N₃] [Module R N₃] {P : RootPairing ι R M N} {Q : RootPairing ι₂ R M₂ N₂} {S : RootPairing ι₃ R M₃ N₃} (e : P.Equiv Q) (f : Q.Equiv S) : (f.comp e).autCongr = e.autCongr.trans f.autCongr

Conjugation by a composite is the composite of the conjugations.