Documentation

TauCeti.LinearAlgebra.RootSystem.Duality

Duality of Dynkin types #

Interchanging the roots and the coroots of a root pairing (RootPairing.flip) transposes every pairing ⟨αᵢ, αⱼ^∨⟩, hence transposes the Cartan matrix of a base (RootPairing.Base.cartanMatrix_flip, proved in TauCeti.LinearAlgebra.RootSystem.Flip). On the classification side that operation permutes the Dynkin types, and this file pins the permutation: TauCeti.DynkinType.dual exchanges Bₙ with Cₙ and fixes every other type. Duality is what makes the orientation carried by TauCeti.HasCartanType meaningful, since Bₙ and Cₙ are exactly the pair of types that the orientation separates.

The dual type is not read off the transposed matrix on the nose. Transposing a Cartan matrix does not merely relabel the diagram, it reverses every arrow, and for F₄ and G₂ the reversed diagram is the original one read backwards. So duality carries a relabelling of the nodes as well as a change of type, and TauCeti.DynkinType.dualNodeEquiv is that relabelling: the identity for the classical families and the E types, and the reversal Fin.revPerm for F₄ and G₂.

TauCeti.DynkinType.Valid is deliberately not preserved by duality, and the failure is exactly the low-rank coincidence B 2 = C 2: B 2 is valid and its dual C 2 is not, because the two name the same root system and the enumeration keeps only one of the names. Away from that pair validity does transfer (TauCeti.DynkinType.valid_dual_iff). The last section shows that nothing is lost there: at rank at most two a base has a Cartan type exactly when it has the dual type (TauCeti.hasCartanType_dual_iff_of_rank_le_two), because transposing a matrix with constant diagonal and at most two indices is itself a simultaneous relabelling.

Main definitions #

Main results #

References #

This file supplies the duality half of the DynkinType layer of TauCetiRoadmap/RepresentationTheory/RootSystems/README.md: Layer 5 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)", and Layer 6 asks for the adjoint root datum to be RootPairing.flip of the dual type's datum. See Bourbaki, Lie Groups and Lie Algebras, Chapters 4-6, plates I-IX, for the standard Cartan matrices and their duals.

source
def TauCeti.DynkinType.dual :
DynkinType → DynkinType

The dual Dynkin type. Duality reverses the arrows of a diagram, which exchanges the types Bₙ and Cₙ — the one pair whose standard Cartan matrices are transposes of one another without being equal — and fixes all the others. It is realized on root systems by RootPairing.flip; see TauCeti.hasCartanType_flip_iff.

This is @[expose]d because it occurs in the type of TauCeti.DynkinType.dualNodeEquiv below, whose constructor equations do not even elaborate unless (.A n).dual.rank reduces to n.

Equations
Instances For
    source
    @[simp]
    theorem TauCeti.DynkinType.dual_A (n : ℕ) :
    (A n).dual = A n
    source
    @[simp]
    theorem TauCeti.DynkinType.dual_B (n : ℕ) :
    (B n).dual = C n
    source
    @[simp]
    theorem TauCeti.DynkinType.dual_C (n : ℕ) :
    (C n).dual = B n
    source
    @[simp]
    theorem TauCeti.DynkinType.dual_D (n : ℕ) :
    (D n).dual = D n
    source
    @[simp]
    theorem TauCeti.DynkinType.dual_E6 :
    E6.dual = E6
    source
    @[simp]
    theorem TauCeti.DynkinType.dual_E7 :
    E7.dual = E7
    source
    @[simp]
    theorem TauCeti.DynkinType.dual_E8 :
    E8.dual = E8
    source
    @[simp]
    theorem TauCeti.DynkinType.dual_F4 :
    F4.dual = F4
    source
    @[simp]
    theorem TauCeti.DynkinType.dual_G2 :
    G2.dual = G2
    source
    @[simp]
    theorem TauCeti.DynkinType.dual_dual (t : DynkinType) :
    t.dual.dual = t

    Duality is an involution.

    source
    theorem TauCeti.DynkinType.dual_injective :
    Function.Injective dual

    Duality is injective, being an involution; so distinct types stay distinct after dualizing.

    source
    @[simp]
    theorem TauCeti.DynkinType.rank_dual (t : DynkinType) :
    t.dual.rank = t.rank

    Duality preserves the rank: it reverses arrows without adding or removing nodes.

    source
    @[simp]
    theorem TauCeti.DynkinType.isSimplyLaced_dual (t : DynkinType) :
    t.dual.IsSimplyLaced ↔ t.IsSimplyLaced

    Duality preserves simple-lacedness: a diagram has an arrow to reverse exactly when its dual does.

    source
    theorem TauCeti.DynkinType.valid_dual_iff {t : DynkinType} (hB : t ≠ B 2) (hC : t ≠ C 2) :
    t.dual.Valid ↔ t.Valid

    Validity transfers along duality away from the pair B 2, C 2. The excluded pair is the low-rank coincidence B 2 = C 2: both names describe the same root system, and the enumeration keeps only B 2 valid. So both orientations of that pair genuinely fail — B 2 is valid while its dual C 2 is not, and C 2 is not valid while its dual B 2 is (simp proves either from TauCeti.DynkinType.valid_B, TauCeti.DynkinType.valid_C and dual_B, dual_C). No base is lost by keeping only the first name; see TauCeti.hasCartanType_dual_iff_of_rank_le_two.

    source
    def TauCeti.DynkinType.dualNodeEquiv (t : DynkinType) :
    Fin t.rank ≃ Fin t.dual.rank

    The relabelling of nodes carried by duality. Transposing a Cartan matrix reverses the arrows of its diagram, and for the classical families and the E types the result is the standard matrix of the dual type already in the Bourbaki numbering. For F₄ and G₂ — the two types that are self-dual without being simply laced — the reversed diagram is the original one read backwards, so the relabelling there is Fin.revPerm.

    Equations
    Instances For
      source
      @[simp]
      theorem TauCeti.DynkinType.dualNodeEquiv_A (n : ℕ) :
      (A n).dualNodeEquiv = Equiv.refl (Fin n)
      source
      @[simp]
      theorem TauCeti.DynkinType.dualNodeEquiv_B (n : ℕ) :
      (B n).dualNodeEquiv = Equiv.refl (Fin n)
      source
      @[simp]
      theorem TauCeti.DynkinType.dualNodeEquiv_C (n : ℕ) :
      (C n).dualNodeEquiv = Equiv.refl (Fin n)
      source
      @[simp]
      theorem TauCeti.DynkinType.dualNodeEquiv_D (n : ℕ) :
      (D n).dualNodeEquiv = Equiv.refl (Fin n)
      source
      @[simp]
      theorem TauCeti.DynkinType.dualNodeEquiv_E6 :
      E6.dualNodeEquiv = Equiv.refl (Fin 6)
      source
      @[simp]
      theorem TauCeti.DynkinType.dualNodeEquiv_E7 :
      E7.dualNodeEquiv = Equiv.refl (Fin 7)
      source
      @[simp]
      theorem TauCeti.DynkinType.dualNodeEquiv_E8 :
      E8.dualNodeEquiv = Equiv.refl (Fin 8)
      source
      @[simp]
      theorem TauCeti.DynkinType.dualNodeEquiv_F4 :
      F4.dualNodeEquiv = Fin.revPerm
      source
      @[simp]
      theorem TauCeti.DynkinType.dualNodeEquiv_G2 :
      G2.dualNodeEquiv = Fin.revPerm
      source
      @[simp]
      theorem TauCeti.DynkinType.cartanMatrix_dual (t : DynkinType) (i j : Fin t.rank) :
      t.dual.cartanMatrix (t.dualNodeEquiv i) (t.dualNodeEquiv j) = t.cartanMatrix j i

      The standard Cartan matrix of the dual type is the transpose, read through the node relabelling TauCeti.DynkinType.dualNodeEquiv. For the simply-laced types the standard matrices are symmetric and there is nothing to move; for Bₙ and Cₙ the transposition is CartanMatrix.B_transpose; and for F₄ and G₂ the transpose is the matrix itself with its nodes reversed.

      source
      theorem TauCeti.DynkinType.cartanMatrix_dual_eq_reindex (t : DynkinType) :
      t.dual.cartanMatrix = (Matrix.reindex t.dualNodeEquiv t.dualNodeEquiv) t.cartanMatrix.transpose

      TauCeti.DynkinType.cartanMatrix_dual as an identity of matrices rather than of entries.

      source
      theorem TauCeti.DynkinType.cartanMatrix_rev_of_rank_le_two {t : DynkinType} (ht : t.rank ≤ 2) (i j : Fin t.rank) :
      t.cartanMatrix j.rev i.rev = t.cartanMatrix i j

      Reversing the nodes of a standard Cartan matrix of rank at most two transposes it. With at most two indices the only off-diagonal entries form a single transposed pair, which the reversal swaps, while the diagonal is constant. This is why the orientation built into TauCeti.HasCartanType carries no information at rank at most two.

      source
      theorem TauCeti.HasCartanType.flip {ι : Type u_1} {R : Type u_2} {M : Type u_3} {N : Type u_4} [CommRing R] [CharZero R] [AddCommGroup M] [Module R M] [AddCommGroup N] [Module R N] {P : RootPairing ι R M N} [P.IsCrystallographic] {b : P.Base} {t : DynkinType} (h : HasCartanType P b t) :
      HasCartanType P.flip b.flip t.dual

      The Cartan type of a flipped base is the dual type. Flipping transposes the Cartan matrix (RootPairing.Base.cartanMatrix_flip), and transposing a standard Cartan matrix is passing to the dual type up to the node relabelling TauCeti.DynkinType.dualNodeEquiv.

      source
      @[simp]
      theorem TauCeti.hasCartanType_flip_iff {ι : Type u_1} {R : Type u_2} {M : Type u_3} {N : Type u_4} [CommRing R] [CharZero R] [AddCommGroup M] [Module R M] [AddCommGroup N] [Module R N] {P : RootPairing ι R M N} [P.IsCrystallographic] {b : P.Base} {t : DynkinType} :
      HasCartanType P.flip b.flip t.dual ↔ HasCartanType P b t

      A base has Cartan type t exactly when the flipped base has the dual type. This is what gives TauCeti.DynkinType.dual its meaning: passing from a root system to its dual is passing from a Dynkin type to its dual.

      source
      @[simp]
      theorem TauCeti.hasCartanType_flip_C_iff {ι : Type u_1} {R : Type u_2} {M : Type u_3} {N : Type u_4} [CommRing R] [CharZero R] [AddCommGroup M] [Module R M] [AddCommGroup N] [Module R N] {P : RootPairing ι R M N} [P.IsCrystallographic] {b : P.Base} {n : ℕ} :
      HasCartanType P.flip b.flip (DynkinType.C n) ↔ HasCartanType P b (DynkinType.B n)

      A base is of type Bₙ exactly when the flipped base is of type Cₙ. This is the worked instance of TauCeti.hasCartanType_flip_iff: Bₙ and Cₙ are the pair of types that the oriented matching of TauCeti.HasCartanType keeps apart, and duality is what identifies them.

      It is stated separately from TauCeti.hasCartanType_flip_iff because that lemma matches a flipped type t.dual syntactically, so neither simp nor rw recovers this instance from it: doing so would mean solving .C n = ?t.dual for ?t.

      source
      @[simp]
      theorem TauCeti.hasCartanType_flip_B_iff {ι : Type u_1} {R : Type u_2} {M : Type u_3} {N : Type u_4} [CommRing R] [CharZero R] [AddCommGroup M] [Module R M] [AddCommGroup N] [Module R N] {P : RootPairing ι R M N} [P.IsCrystallographic] {b : P.Base} {n : ℕ} :
      HasCartanType P.flip b.flip (DynkinType.B n) ↔ HasCartanType P b (DynkinType.C n)

      The other orientation of TauCeti.hasCartanType_flip_C_iff: a base is of type Cₙ exactly when the flipped base is of type Bₙ.

      source
      theorem TauCeti.hasCartanType_dual_iff_of_rank_le_two {ι : 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} [P.IsCrystallographic] {b : P.Base} {t : DynkinType} (ht : t.rank ≤ 2) :
      HasCartanType P b t.dual ↔ HasCartanType P b t

      At rank at most two a base has a Cartan type exactly when it has the dual type. The enumeration keeps B 2 valid and drops C 2, and this is what makes that choice harmless: the two names match exactly the same bases. From rank three on the statement fails, since Bₙ and Cₙ are then genuinely different root systems.

      source
      @[simp]
      theorem TauCeti.hasCartanType_C_two_iff_B_two {ι : 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} [P.IsCrystallographic] {b : P.Base} :
      HasCartanType P b (DynkinType.C 2) ↔ HasCartanType P b (DynkinType.B 2)

      Types B 2 and C 2 match exactly the same bases, the low-rank coincidence that TauCeti.DynkinType.Valid resolves by keeping only B 2.