Root pairings made from bilinear forms

A common construction of root systems is given by taking the set of all vectors in an integral lattice for which reflection yields an automorphism of the lattice. In this file, we generalize this construction, replacing the ring of integers with an arbitrary commutative ring and the integral lattice with an arbitrary reflexive module equipped with a bilinear form.

Main definitions:

• LinearMap.IsReflective: Length is a regular value of R, and reflection is definable.
• LinearMap.IsReflective.coroot: The coroot corresponding to a reflective vector.
• RootPairing.of_Bilinear: The root pairing whose roots are reflective vectors.

TODO

• properties

structure LinearMap.IsReflective {R : Type u_1} {M : Type u_2} [CommRing R] [AddCommGroup M] [Module R M] (B : M →ₗ[R] M →ₗ[R] R) (x : M) : Prop

A vector x is reflective with respect to a bilinear form if multiplication by its norm is injective, and for any vector y, the norm of x divides twice the inner product of x and y. These conditions are what we need when describing reflection as a map taking y to y - 2 • (B x y) / (B x x) • x.

• regular : IsRegular ((B x) x)
• dvd_two_mul : ∀ (y : M), (B x) x ∣ 2 * (B x) y

theorem LinearMap.IsReflective.regular {R : Type u_1} {M : Type u_2} [CommRing R] [AddCommGroup M] [Module R M] {B : M →ₗ[R] M →ₗ[R] R} {x : M} (self : B.IsReflective x) : IsRegular ((B x) x)

theorem LinearMap.IsReflective.dvd_two_mul {R : Type u_1} {M : Type u_2} [CommRing R] [AddCommGroup M] [Module R M] {B : M →ₗ[R] M →ₗ[R] R} {x : M} (self : B.IsReflective x) (y : M) : (B x) x ∣ 2 * (B x) y

theorem LinearMap.IsReflective.of_dvd_two {R : Type u_1} {M : Type u_2} [CommRing R] [AddCommGroup M] [Module R M] (B : M →ₗ[R] M →ₗ[R] R) {x : M} [IsDomain R] [NeZero 2] (hx : (B x) x ∣ 2) : B.IsReflective x

def LinearMap.IsReflective.coroot {R : Type u_1} {M : Type u_2} [CommRing R] [AddCommGroup M] [Module R M] (B : M →ₗ[R] M →ₗ[R] R) {x : M} (hx : B.IsReflective x) : M →ₗ[R] R

The coroot attached to a reflective vector.

Equations

• LinearMap.IsReflective.coroot B hx = { toFun := fun (y : M) => Exists.choose ⋯, map_add' := ⋯, map_smul' := ⋯ }

@[simp]

theorem LinearMap.IsReflective.apply_self_mul_coroot_apply {R : Type u_1} {M : Type u_2} [CommRing R] [AddCommGroup M] [Module R M] (B : M →ₗ[R] M →ₗ[R] R) {x : M} (hx : B.IsReflective x) {y : M} : (B x) x * (LinearMap.IsReflective.coroot B hx) y = 2 * (B x) y

@[simp]

theorem LinearMap.IsReflective.smul_coroot {R : Type u_1} {M : Type u_2} [CommRing R] [AddCommGroup M] [Module R M] (B : M →ₗ[R] M →ₗ[R] R) {x : M} (hx : B.IsReflective x) : (B x) x • LinearMap.IsReflective.coroot B hx = 2 • B x

@[simp]

theorem LinearMap.IsReflective.coroot_apply_self {R : Type u_1} {M : Type u_2} [CommRing R] [AddCommGroup M] [Module R M] (B : M →ₗ[R] M →ₗ[R] R) {x : M} (hx : B.IsReflective x) : (LinearMap.IsReflective.coroot B hx) x = 2

theorem LinearMap.IsReflective.isOrthogonal_reflection {R : Type u_1} {M : Type u_2} [CommRing R] [AddCommGroup M] [Module R M] (B : M →ₗ[R] M →ₗ[R] R) {x : M} (hx : B.IsReflective x) (hSB : B.IsSymm) : B.IsOrthogonal ↑(Module.reflection ⋯)

theorem LinearMap.IsReflective.reflective_reflection {R : Type u_1} {M : Type u_2} [CommRing R] [AddCommGroup M] [Module R M] (B : M →ₗ[R] M →ₗ[R] R) {x : M} (hSB : B.IsSymm) {y : M} (hx : B.IsReflective x) (hy : B.IsReflective y) : B.IsReflective ((Module.reflection ⋯) y)

def RootPairing.ofBilinear {R : Type u_1} {M : Type u_2} [CommRing R] [AddCommGroup M] [Module R M] [Module.IsReflexive R M] (B : M →ₗ[R] M →ₗ[R] R) (hNB : B.Nondegenerate) (hSB : B.IsSymm) (h2 : IsRegular 2) : RootPairing (↑{x : M | B.IsReflective x}) R M (Module.Dual R M)

The root pairing given by all reflective vectors for a bilinear form.

Equations

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