Base change for root pairings

When the coefficients are a field, root pairings behave well with respect to restriction and extension of scalars.

Main results:

• RootPairing.restrict: if RootPairing.pairing takes values in a subfield, we may restrict to get a root system with coefficients in the subfield. Of particular interest is the case when the pairing takes values in its prime subfield (which happens for crystallographic pairings).

TODO

• Extension of scalars
• Crystallographic root systems are isomorphic to base changes of root systems over ℤ: Take M₀ and N₀ to be the ℤ-span of roots and coroots.

class RootPairing.IsBalanced {ι : Type u_1} {R : Type u_2} {M : Type u_3} {N : Type u_4} [AddCommGroup M] [AddCommGroup N] [CommRing R] [Module R M] [Module R N] (P : RootPairing ι R M N) : Prop

We say a root pairing is balanced if the root span and coroot span are perfectly complementary.

All root systems are balanced and all finite root pairings over a field are balanced.

• isPerfectCompl : P.IsPerfectCompl (P.rootSpan R) (P.corootSpan R)

instance RootPairing.instIsBalancedOfIsRootSystem {ι : Type u_1} {R : Type u_2} {M : Type u_3} {N : Type u_4} [AddCommGroup M] [AddCommGroup N] [CommRing R] [Module R M] [Module R N] (P : RootPairing ι R M N) [P.IsRootSystem] : P.IsBalanced

noncomputable def RootPairing.restrictScalars' {ι : Type u_1} {L : Type u_2} {M : Type u_3} {N : Type u_4} [Field L] [AddCommGroup M] [AddCommGroup N] [Module L M] [Module L N] (P : RootPairing ι L M N) (K : Type u_5) [Field K] [Algebra K L] [Module K M] [Module K N] [IsScalarTower K L M] [IsScalarTower K L N] [P.IsBalanced] [P.IsValuedIn K] : RootPairing ι K ↥(Submodule.span K (Set.range ⇑P.root)) ↥(Submodule.span K (Set.range ⇑P.coroot))

Restriction of scalars for a root pairing taking values in a subfield.

See also RootPairing.restrictScalars.

Equations

• One or more equations did not get rendered due to their size.

instance RootPairing.instIsRootSystemSubtypeMemSubmoduleSpanRangeCoeEmbeddingRootCorootRestrictScalars' {ι : Type u_1} {L : Type u_2} {M : Type u_3} {N : Type u_4} [Field L] [AddCommGroup M] [AddCommGroup N] [Module L M] [Module L N] (P : RootPairing ι L M N) (K : Type u_5) [Field K] [Algebra K L] [Module K M] [Module K N] [IsScalarTower K L M] [IsScalarTower K L N] [P.IsBalanced] [P.IsValuedIn K] : (P.restrictScalars' K).IsRootSystem

@[simp]

theorem RootPairing.restrictScalars_toLinearMap_apply_apply {ι : Type u_1} {L : Type u_2} {M : Type u_3} {N : Type u_4} [Field L] [AddCommGroup M] [AddCommGroup N] [Module L M] [Module L N] (P : RootPairing ι L M N) (K : Type u_5) [Field K] [Algebra K L] [Module K M] [Module K N] [IsScalarTower K L M] [IsScalarTower K L N] [P.IsBalanced] [P.IsValuedIn K] (x : ↥(Submodule.span K (Set.range ⇑P.root))) (y : ↥(Submodule.span K (Set.range ⇑P.coroot))) : (algebraMap K L) (((P.restrictScalars' K).toLinearMap x) y) = (P.toLinearMap ↑x) ↑y

@[simp]

theorem RootPairing.restrictScalars_coe_root {ι : Type u_1} {L : Type u_2} {M : Type u_3} {N : Type u_4} [Field L] [AddCommGroup M] [AddCommGroup N] [Module L M] [Module L N] (P : RootPairing ι L M N) (K : Type u_5) [Field K] [Algebra K L] [Module K M] [Module K N] [IsScalarTower K L M] [IsScalarTower K L N] [P.IsBalanced] [P.IsValuedIn K] (i : ι) : ↑((P.restrictScalars' K).root i) = P.root i

@[simp]

theorem RootPairing.restrictScalars_coe_coroot {ι : Type u_1} {L : Type u_2} {M : Type u_3} {N : Type u_4} [Field L] [AddCommGroup M] [AddCommGroup N] [Module L M] [Module L N] (P : RootPairing ι L M N) (K : Type u_5) [Field K] [Algebra K L] [Module K M] [Module K N] [IsScalarTower K L M] [IsScalarTower K L N] [P.IsBalanced] [P.IsValuedIn K] (i : ι) : ↑((P.restrictScalars' K).coroot i) = P.coroot i

@[simp]

theorem RootPairing.restrictScalars_pairing {ι : Type u_1} {L : Type u_2} {M : Type u_3} {N : Type u_4} [Field L] [AddCommGroup M] [AddCommGroup N] [Module L M] [Module L N] (P : RootPairing ι L M N) (K : Type u_5) [Field K] [Algebra K L] [Module K M] [Module K N] [IsScalarTower K L M] [IsScalarTower K L N] [P.IsBalanced] [P.IsValuedIn K] (i j : ι) : (algebraMap K L) ((P.restrictScalars' K).pairing i j) = P.pairing i j

@[reducible, inline]

noncomputable abbrev RootPairing.restrictScalars {ι : Type u_1} {L : Type u_2} {M : Type u_3} {N : Type u_4} [Field L] [AddCommGroup M] [AddCommGroup N] [Module L M] [Module L N] (P : RootPairing ι L M N) (K : Type u_5) [Field K] [Algebra K L] [Module K M] [Module K N] [IsScalarTower K L M] [IsScalarTower K L N] [P.IsBalanced] [P.IsCrystallographic] : RootPairing ι K ↥(Submodule.span K (Set.range ⇑P.root)) ↥(Submodule.span K (Set.range ⇑P.coroot))

Restriction of scalars for a crystallographic root pairing.

Equations

• P.restrictScalars K = P.restrictScalars' K

@[reducible, inline]

noncomputable abbrev RootPairing.restrictScalarsRat {ι : Type u_1} {L : Type u_2} {M : Type u_3} {N : Type u_4} [Field L] [AddCommGroup M] [AddCommGroup N] [Module L M] [Module L N] (P : RootPairing ι L M N) [P.IsBalanced] [CharZero L] [P.IsCrystallographic] : RootPairing ι ℚ ↥(Submodule.span ℚ (Set.range ⇑P.root)) ↥(Submodule.span ℚ (Set.range ⇑P.coroot))

Restriction of scalars to ℚ for a crystallographic root pairing in characteristic zero.

Equations

• P.restrictScalarsRat = P.restrictScalars ℚ