Flipping a root pairing transposes its Cartan matrix

Mathlib's RootPairing.flip interchanges the roots and the coroots of a root pairing, and RootPairing.Base.flip records that a base of P is a base of P.flip supported on the same simple indices. Interchanging the two sides transposes every pairing ⟨αᵢ, αⱼ^∨⟩ (RootPairing.pairing_flip); this file carries that transposition across the integral structure and the Cartan matrix of a base, which is where flipping is used.

Main definitions

• RootPairing.Base.flipSupportEquiv: the identification of the support of a base with the support of its flip, which the two Cartan matrices are indexed by.

Main results

• RootPairing.pairingIn_flip: flipping transposes the chosen preimage of a pairing in the coefficient ring S, not only the pairing itself.
• RootPairing.Base.cartanMatrix_flip: the Cartan matrix of the flipped base is the transpose of the Cartan matrix of the base.

References

This file supplies the root-pairing half of the duality item of Layer 5 of TauCetiRoadmap/RepresentationTheory/RootSystems/README.md, which records that DynkinType.cartanMatrix (.B n) is the transpose of DynkinType.cartanMatrix (.C n) and that the two types are "identified only after flip (duality)"; the classification side of that item is TauCeti.LinearAlgebra.RootSystem.Duality.

@[simp]

theorem RootPairing.pairingIn_flip {ι : Type u_1} {R : Type u_2} {M : Type u_3} {N : Type u_4} [CommRing R] [AddCommGroup M] [Module R M] [AddCommGroup N] [Module R N] (S : Type u_5) [CommRing S] [Algebra S R] [FaithfulSMul S R] (P : RootPairing ι R M N) [P.IsValuedIn S] (i j : ι) : P.flip.pairingIn S i j = P.pairingIn S j i

Flipping a root pairing transposes its integral pairing. The pairing of the flipped pairing is transposed by definition (RootPairing.pairing_flip); the content here is that the chosen preimage in S is transposed too, which needs algebraMap S R to be injective.

def RootPairing.Base.flipSupportEquiv {ι : Type u_1} {R : Type u_2} {M : Type u_3} {N : Type u_4} [CommRing R] [AddCommGroup M] [Module R M] [AddCommGroup N] [Module R N] {P : RootPairing ι R M N} (b : P.Base) : ↥b.flip.support ≃ ↥b.support

A base of P is a base of P.flip supported on the same simple indices (RootPairing.Base.flip); this is the resulting identification of the two index types, which the Cartan matrices of the base and of its flip are indexed by.

Equations

• b.flipSupportEquiv = Equiv.subtypeEquivRight ⋯

@[simp]

theorem RootPairing.Base.coe_flipSupportEquiv_apply {ι : Type u_1} {R : Type u_2} {M : Type u_3} {N : Type u_4} [CommRing R] [AddCommGroup M] [Module R M] [AddCommGroup N] [Module R N] {P : RootPairing ι R M N} (b : P.Base) (i : ↥b.flip.support) : ↑(b.flipSupportEquiv i) = ↑i

@[simp]

theorem RootPairing.Base.cartanMatrix_flip {ι : Type u_1} {R : Type u_2} {M : Type u_3} {N : Type u_4} [CommRing R] [AddCommGroup M] [Module R M] [AddCommGroup N] [Module R N] [CharZero R] {P : RootPairing ι R M N} [P.IsCrystallographic] (b : P.Base) (i j : ↥b.flip.support) : b.flip.cartanMatrix i j = b.cartanMatrix (b.flipSupportEquiv j) (b.flipSupportEquiv i)

The Cartan matrix of the flipped base is the transpose of the Cartan matrix of the base.

@[simp]

theorem RootPairing.Base.flip_flip {ι : Type u_1} {R : Type u_2} {M : Type u_3} {N : Type u_4} [CommRing R] [AddCommGroup M] [Module R M] [AddCommGroup N] [Module R N] {P : RootPairing ι R M N} (b : P.Base) : b.flip.flip = b

Flipping a base twice returns the original base.