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

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 P.corootSpan

instance RootPairing.instIsBalanced {ι : 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 : RootSystem ι R M N) : P.IsBalanced

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] (hP : ∀ (i j : ι), P.pairing i j ∈ (algebraMap K L).range) : RootSystem ι 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.

Note that we obtain a root system (not just a root pairing). See also RootPairing.restrictScalars.

Equations

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

@[simp]

theorem RootPairing.restrictScalars_toPerfectPairing_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] (hP : ∀ (i j : ι), P.pairing i j ∈ (algebraMap K L).range) (x : ↥(Submodule.span K (Set.range ⇑P.root))) (y : ↥(Submodule.span K (Set.range ⇑P.coroot))) : (algebraMap K L) (((P.restrictScalars' K hP).toPerfectPairing x) y) = (P.toPerfectPairing ↑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] (hP : ∀ (i j : ι), P.pairing i j ∈ (algebraMap K L).range) (i : ι) : ↑((P.restrictScalars' K hP).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] (hP : ∀ (i j : ι), P.pairing i j ∈ (algebraMap K L).range) (i : ι) : ↑((P.restrictScalars' K hP).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] (hP : ∀ (i j : ι), P.pairing i j ∈ (algebraMap K L).range) (i j : ι) : (algebraMap K L) ((P.restrictScalars' K hP).pairing i j) = P.pairing i j

@[reducible, inline]

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] : RootSystem ι 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]

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] : RootSystem ι ℚ ↥(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 ℚ