Numerical quotients of a bilinear map

For a possibly nonsymmetric bilinear map b : L →ₗ[R] M →ₗ[R] P, its left radical and right radical need not agree—indeed, its two arguments need not even have the same type. This file defines the two radicals separately, quotients each argument by the appropriate radical, and descends b to a nondegenerate pairing between the resulting quotients. An ordinary biadditive pairing of additive groups is reinterpreted over ℤ by TauCeti.biadditiveToIntBilinear.

The intermediate pairings with only one argument quotiented are also provided. Quotienting the left argument makes the pairing left-separating, while quotienting the right argument makes it right-separating; no assertion is made about the other side until both quotients are taken.

Main definitions

• TauCeti.biadditiveToIntBilinear: a biadditive pairing viewed as a ℤ-bilinear map.
• TauCeti.leftRadical and TauCeti.rightRadical: the two radicals of a bilinear map.
• TauCeti.LeftNumericalQuotient and TauCeti.RightNumericalQuotient: the corresponding quotient modules.
• TauCeti.leftNumericalPairing and TauCeti.rightNumericalPairing: the one-sided quotient pairings.
• TauCeti.numericalPairing: the pairing between both numerical quotients.

Main results

• TauCeti.leftNumericalPairing_separatingLeft and TauCeti.rightNumericalPairing_separatingRight: the precise one-sided nondegeneracy results.
• TauCeti.numericalPairing_nondegenerate: the pairing between both quotients has zero left and right radicals.

The quotient construction uses Mathlib's asymmetric LinearMap.liftQ₂. The terminology and the warning that the two radicals remain distinct follow Dancso–Licata, Koszul algebras and flow lattices, Section 3.1, and the Grothendieck-groups, Cartan-maps, and Euler-forms roadmap, Layer 7.

def TauCeti.biadditiveToIntBilinear {A : Type u_2} {B : Type u_3} {D : Type u_4} [AddCommGroup A] [AddCommGroup B] [AddCommGroup D] (b : A →+ B →+ D) : A →ₗ[ℤ] B →ₗ[ℤ] D

A biadditive pairing of additive groups, reinterpreted as a bilinear map over ℤ.

This is the bridge from pairings such as an Euler pairing, naturally constructed as A →+ B →+ D, to the bilinear numerical-quotient API in this file.

Equations

• TauCeti.biadditiveToIntBilinear b = { toFun := fun (a : A) => (addMonoidHomLequivInt ℤ) (b a), map_add' := ⋯, map_smul' := ⋯ }

@[simp]

theorem TauCeti.biadditiveToIntBilinear_apply {A : Type u_2} {B : Type u_3} {D : Type u_4} [AddCommGroup A] [AddCommGroup B] [AddCommGroup D] (b : A →+ B →+ D) (a : A) (x : B) : ((biadditiveToIntBilinear b) a) x = (b a) x

Reinterpreting a biadditive pairing over ℤ does not change its values.

def TauCeti.leftRadical {R : Type u_1} [CommRing R] {L : Type u₁} {M : Type u₂} {P : Type u₃} [AddCommGroup L] [Module R L] [AddCommGroup M] [Module R M] [AddCommGroup P] [Module R P] (b : L →ₗ[R] M →ₗ[R] P) : Submodule R L

The left radical of a bilinear map: the elements in the first argument which pair to zero with every element of the second argument.

Equations

• TauCeti.leftRadical b = b.ker

def TauCeti.rightRadical {R : Type u_1} [CommRing R] {L : Type u₁} {M : Type u₂} {P : Type u₃} [AddCommGroup L] [Module R L] [AddCommGroup M] [Module R M] [AddCommGroup P] [Module R P] (b : L →ₗ[R] M →ₗ[R] P) : Submodule R M

The right radical of a bilinear map: the elements in the second argument which pair to zero with every element of the first argument.

Equations

• TauCeti.rightRadical b = b.flip.ker

@[simp]

theorem TauCeti.mem_leftRadical_iff {R : Type u_1} [CommRing R] {L : Type u₁} {M : Type u₂} {P : Type u₃} [AddCommGroup L] [Module R L] [AddCommGroup M] [Module R M] [AddCommGroup P] [Module R P] (b : L →ₗ[R] M →ₗ[R] P) (x : L) : x ∈ leftRadical b ↔ ∀ (y : M), (b x) y = 0

Membership in the left radical means pairing to zero against every second argument.

@[simp]

theorem TauCeti.mem_rightRadical_iff {R : Type u_1} [CommRing R] {L : Type u₁} {M : Type u₂} {P : Type u₃} [AddCommGroup L] [Module R L] [AddCommGroup M] [Module R M] [AddCommGroup P] [Module R P] (b : L →ₗ[R] M →ₗ[R] P) (y : M) : y ∈ rightRadical b ↔ ∀ (x : L), (b x) y = 0

Membership in the right radical means pairing to zero against every first argument.

theorem TauCeti.separatingLeft_iff_leftRadical_eq_bot {R : Type u_1} [CommRing R] {L : Type u₁} {M : Type u₂} {P : Type u₃} [AddCommGroup L] [Module R L] [AddCommGroup M] [Module R M] [AddCommGroup P] [Module R P] (b : L →ₗ[R] M →ₗ[R] P) : b.SeparatingLeft ↔ leftRadical b = ⊥

A bilinear map is left-separating exactly when its left radical is trivial.

theorem TauCeti.separatingRight_iff_rightRadical_eq_bot {R : Type u_1} [CommRing R] {L : Type u₁} {M : Type u₂} {P : Type u₃} [AddCommGroup L] [Module R L] [AddCommGroup M] [Module R M] [AddCommGroup P] [Module R P] (b : L →ₗ[R] M →ₗ[R] P) : b.SeparatingRight ↔ rightRadical b = ⊥

A bilinear map is right-separating exactly when its right radical is trivial.

@[reducible, inline]

abbrev TauCeti.LeftNumericalQuotient {R : Type u_1} [CommRing R] {L : Type u₁} {M : Type u₂} {P : Type u₃} [AddCommGroup L] [Module R L] [AddCommGroup M] [Module R M] [AddCommGroup P] [Module R P] (b : L →ₗ[R] M →ₗ[R] P) : Type u₁

The quotient of the first argument by the left radical.

Equations

• TauCeti.LeftNumericalQuotient b = (L ⧸ TauCeti.leftRadical b)

@[reducible, inline]

abbrev TauCeti.RightNumericalQuotient {R : Type u_1} [CommRing R] {L : Type u₁} {M : Type u₂} {P : Type u₃} [AddCommGroup L] [Module R L] [AddCommGroup M] [Module R M] [AddCommGroup P] [Module R P] (b : L →ₗ[R] M →ₗ[R] P) : Type u₂

The quotient of the second argument by the right radical.

Equations

• TauCeti.RightNumericalQuotient b = (M ⧸ TauCeti.rightRadical b)

def TauCeti.leftNumericalQuotientMk {R : Type u_1} [CommRing R] {L : Type u₁} {M : Type u₂} {P : Type u₃} [AddCommGroup L] [Module R L] [AddCommGroup M] [Module R M] [AddCommGroup P] [Module R P] (b : L →ₗ[R] M →ₗ[R] P) : L →ₗ[R] LeftNumericalQuotient b

The quotient map from the first argument to its left numerical quotient.

Equations

• TauCeti.leftNumericalQuotientMk b = (TauCeti.leftRadical b).mkQ

def TauCeti.rightNumericalQuotientMk {R : Type u_1} [CommRing R] {L : Type u₁} {M : Type u₂} {P : Type u₃} [AddCommGroup L] [Module R L] [AddCommGroup M] [Module R M] [AddCommGroup P] [Module R P] (b : L →ₗ[R] M →ₗ[R] P) : M →ₗ[R] RightNumericalQuotient b

The quotient map from the second argument to its right numerical quotient.

Equations

• TauCeti.rightNumericalQuotientMk b = (TauCeti.rightRadical b).mkQ

theorem TauCeti.leftNumericalQuotientMk_apply {R : Type u_1} [CommRing R] {L : Type u₁} {M : Type u₂} {P : Type u₃} [AddCommGroup L] [Module R L] [AddCommGroup M] [Module R M] [AddCommGroup P] [Module R P] (b : L →ₗ[R] M →ₗ[R] P) (x : L) : (leftNumericalQuotientMk b) x = Submodule.Quotient.mk x

The left numerical quotient map sends an element to its quotient class.

theorem TauCeti.rightNumericalQuotientMk_apply {R : Type u_1} [CommRing R] {L : Type u₁} {M : Type u₂} {P : Type u₃} [AddCommGroup L] [Module R L] [AddCommGroup M] [Module R M] [AddCommGroup P] [Module R P] (b : L →ₗ[R] M →ₗ[R] P) (y : M) : (rightNumericalQuotientMk b) y = Submodule.Quotient.mk y

The right numerical quotient map sends an element to its quotient class.

@[simp]

theorem TauCeti.ker_leftNumericalQuotientMk {R : Type u_1} [CommRing R] {L : Type u₁} {M : Type u₂} {P : Type u₃} [AddCommGroup L] [Module R L] [AddCommGroup M] [Module R M] [AddCommGroup P] [Module R P] (b : L →ₗ[R] M →ₗ[R] P) : (leftNumericalQuotientMk b).ker = leftRadical b

The kernel of the left numerical quotient map is the left radical.

@[simp]

theorem TauCeti.ker_rightNumericalQuotientMk {R : Type u_1} [CommRing R] {L : Type u₁} {M : Type u₂} {P : Type u₃} [AddCommGroup L] [Module R L] [AddCommGroup M] [Module R M] [AddCommGroup P] [Module R P] (b : L →ₗ[R] M →ₗ[R] P) : (rightNumericalQuotientMk b).ker = rightRadical b

The kernel of the right numerical quotient map is the right radical.

theorem TauCeti.leftNumericalQuotientMk_surjective {R : Type u_1} [CommRing R] {L : Type u₁} {M : Type u₂} {P : Type u₃} [AddCommGroup L] [Module R L] [AddCommGroup M] [Module R M] [AddCommGroup P] [Module R P] (b : L →ₗ[R] M →ₗ[R] P) : Function.Surjective ⇑(leftNumericalQuotientMk b)

The left numerical quotient map is surjective.

theorem TauCeti.rightNumericalQuotientMk_surjective {R : Type u_1} [CommRing R] {L : Type u₁} {M : Type u₂} {P : Type u₃} [AddCommGroup L] [Module R L] [AddCommGroup M] [Module R M] [AddCommGroup P] [Module R P] (b : L →ₗ[R] M →ₗ[R] P) : Function.Surjective ⇑(rightNumericalQuotientMk b)

The right numerical quotient map is surjective.

@[simp]

theorem TauCeti.leftNumericalQuotientMk_eq_zero_iff {R : Type u_1} [CommRing R] {L : Type u₁} {M : Type u₂} {P : Type u₃} [AddCommGroup L] [Module R L] [AddCommGroup M] [Module R M] [AddCommGroup P] [Module R P] (b : L →ₗ[R] M →ₗ[R] P) (x : L) : (leftNumericalQuotientMk b) x = 0 ↔ x ∈ leftRadical b

A class in the left numerical quotient vanishes exactly when its representative lies in the left radical.

@[simp]

theorem TauCeti.rightNumericalQuotientMk_eq_zero_iff {R : Type u_1} [CommRing R] {L : Type u₁} {M : Type u₂} {P : Type u₃} [AddCommGroup L] [Module R L] [AddCommGroup M] [Module R M] [AddCommGroup P] [Module R P] (b : L →ₗ[R] M →ₗ[R] P) (y : M) : (rightNumericalQuotientMk b) y = 0 ↔ y ∈ rightRadical b

A class in the right numerical quotient vanishes exactly when its representative lies in the right radical.

@[simp]

theorem TauCeti.leftNumericalQuotientMk_eq_iff {R : Type u_1} [CommRing R] {L : Type u₁} {M : Type u₂} {P : Type u₃} [AddCommGroup L] [Module R L] [AddCommGroup M] [Module R M] [AddCommGroup P] [Module R P] (b : L →ₗ[R] M →ₗ[R] P) (x x' : L) : (leftNumericalQuotientMk b) x = (leftNumericalQuotientMk b) x' ↔ x - x' ∈ leftRadical b

Two elements have the same left numerical class exactly when their difference lies in the left radical.

@[simp]

theorem TauCeti.rightNumericalQuotientMk_eq_iff {R : Type u_1} [CommRing R] {L : Type u₁} {M : Type u₂} {P : Type u₃} [AddCommGroup L] [Module R L] [AddCommGroup M] [Module R M] [AddCommGroup P] [Module R P] (b : L →ₗ[R] M →ₗ[R] P) (y y' : M) : (rightNumericalQuotientMk b) y = (rightNumericalQuotientMk b) y' ↔ y - y' ∈ rightRadical b

Two elements have the same right numerical class exactly when their difference lies in the right radical.

def TauCeti.leftNumericalPairing {R : Type u_1} [CommRing R] {L : Type u₁} {M : Type u₂} {P : Type u₃} [AddCommGroup L] [Module R L] [AddCommGroup M] [Module R M] [AddCommGroup P] [Module R P] (b : L →ₗ[R] M →ₗ[R] P) : LeftNumericalQuotient b →ₗ[R] M →ₗ[R] P

Quotienting only the first argument by the left radical gives a pairing on the left numerical quotient and the original second argument.

Equations

• TauCeti.leftNumericalPairing b = (TauCeti.leftRadical b).liftQ b ⋯

def TauCeti.rightNumericalPairing {R : Type u_1} [CommRing R] {L : Type u₁} {M : Type u₂} {P : Type u₃} [AddCommGroup L] [Module R L] [AddCommGroup M] [Module R M] [AddCommGroup P] [Module R P] (b : L →ₗ[R] M →ₗ[R] P) : L →ₗ[R] RightNumericalQuotient b →ₗ[R] P

Quotienting only the second argument by the right radical gives a pairing on the original first argument and the right numerical quotient.

Equations

• TauCeti.rightNumericalPairing b = ((TauCeti.rightRadical b).liftQ b.flip ⋯).flip

@[simp]

theorem TauCeti.leftNumericalPairing_mk {R : Type u_1} [CommRing R] {L : Type u₁} {M : Type u₂} {P : Type u₃} [AddCommGroup L] [Module R L] [AddCommGroup M] [Module R M] [AddCommGroup P] [Module R P] (b : L →ₗ[R] M →ₗ[R] P) (x : L) (y : M) : ((leftNumericalPairing b) ((leftNumericalQuotientMk b) x)) y = (b x) y

The left quotient pairing is represented by the original pairing.

@[simp]

theorem TauCeti.rightNumericalPairing_mk {R : Type u_1} [CommRing R] {L : Type u₁} {M : Type u₂} {P : Type u₃} [AddCommGroup L] [Module R L] [AddCommGroup M] [Module R M] [AddCommGroup P] [Module R P] (b : L →ₗ[R] M →ₗ[R] P) (x : L) (y : M) : ((rightNumericalPairing b) x) ((rightNumericalQuotientMk b) y) = (b x) y

The right quotient pairing is represented by the original pairing.

theorem TauCeti.leftNumericalPairing_separatingLeft {R : Type u_1} [CommRing R] {L : Type u₁} {M : Type u₂} {P : Type u₃} [AddCommGroup L] [Module R L] [AddCommGroup M] [Module R M] [AddCommGroup P] [Module R P] (b : L →ₗ[R] M →ₗ[R] P) : (leftNumericalPairing b).SeparatingLeft

Quotienting the first argument by the left radical makes the pairing left-separating.

theorem TauCeti.rightNumericalPairing_separatingRight {R : Type u_1} [CommRing R] {L : Type u₁} {M : Type u₂} {P : Type u₃} [AddCommGroup L] [Module R L] [AddCommGroup M] [Module R M] [AddCommGroup P] [Module R P] (b : L →ₗ[R] M →ₗ[R] P) : (rightNumericalPairing b).SeparatingRight

Quotienting the second argument by the right radical makes the pairing right-separating.

def TauCeti.numericalPairing {R : Type u_1} [CommRing R] {L : Type u₁} {M : Type u₂} {P : Type u₃} [AddCommGroup L] [Module R L] [AddCommGroup M] [Module R M] [AddCommGroup P] [Module R P] (b : L →ₗ[R] M →ₗ[R] P) : LeftNumericalQuotient b →ₗ[R] RightNumericalQuotient b →ₗ[R] P

The pairing descended through both the left and right radicals.

Equations

• TauCeti.numericalPairing b = LinearMap.liftQ₂ (TauCeti.leftRadical b) (TauCeti.rightRadical b) b ⋯ ⋯

@[simp]

theorem TauCeti.numericalPairing_mk {R : Type u_1} [CommRing R] {L : Type u₁} {M : Type u₂} {P : Type u₃} [AddCommGroup L] [Module R L] [AddCommGroup M] [Module R M] [AddCommGroup P] [Module R P] (b : L →ₗ[R] M →ₗ[R] P) (x : L) (y : M) : ((numericalPairing b) ((leftNumericalQuotientMk b) x)) ((rightNumericalQuotientMk b) y) = (b x) y

The numerical pairing is represented by the original pairing.

theorem TauCeti.numericalPairing_unique {R : Type u_1} [CommRing R] {L : Type u₁} {M : Type u₂} {P : Type u₃} [AddCommGroup L] [Module R L] [AddCommGroup M] [Module R M] [AddCommGroup P] [Module R P] (b : L →ₗ[R] M →ₗ[R] P) (c : LeftNumericalQuotient b →ₗ[R] RightNumericalQuotient b →ₗ[R] P) (hc : ∀ (x : L) (y : M), (c ((leftNumericalQuotientMk b) x)) ((rightNumericalQuotientMk b) y) = (b x) y) : c = numericalPairing b

The numerical pairing is the unique bilinear map between the two quotients which agrees with the original pairing on representatives.

theorem TauCeti.numericalPairing_separatingLeft {R : Type u_1} [CommRing R] {L : Type u₁} {M : Type u₂} {P : Type u₃} [AddCommGroup L] [Module R L] [AddCommGroup M] [Module R M] [AddCommGroup P] [Module R P] (b : L →ₗ[R] M →ₗ[R] P) : (numericalPairing b).SeparatingLeft

The numerical pairing has trivial left radical.

theorem TauCeti.numericalPairing_separatingRight {R : Type u_1} [CommRing R] {L : Type u₁} {M : Type u₂} {P : Type u₃} [AddCommGroup L] [Module R L] [AddCommGroup M] [Module R M] [AddCommGroup P] [Module R P] (b : L →ₗ[R] M →ₗ[R] P) : (numericalPairing b).SeparatingRight

The numerical pairing has trivial right radical.

theorem TauCeti.numericalPairing_nondegenerate {R : Type u_1} [CommRing R] {L : Type u₁} {M : Type u₂} {P : Type u₃} [AddCommGroup L] [Module R L] [AddCommGroup M] [Module R M] [AddCommGroup P] [Module R P] (b : L →ₗ[R] M →ₗ[R] P) : (numericalPairing b).Nondegenerate

Quotienting both arguments by their respective radicals produces a nondegenerate pairing.

@[simp]

theorem TauCeti.leftRadical_numericalPairing {R : Type u_1} [CommRing R] {L : Type u₁} {M : Type u₂} {P : Type u₃} [AddCommGroup L] [Module R L] [AddCommGroup M] [Module R M] [AddCommGroup P] [Module R P] (b : L →ₗ[R] M →ₗ[R] P) : leftRadical (numericalPairing b) = ⊥

The left radical of the numerical pairing is trivial.

@[simp]

theorem TauCeti.rightRadical_numericalPairing {R : Type u_1} [CommRing R] {L : Type u₁} {M : Type u₂} {P : Type u₃} [AddCommGroup L] [Module R L] [AddCommGroup M] [Module R M] [AddCommGroup P] [Module R P] (b : L →ₗ[R] M →ₗ[R] P) : rightRadical (numericalPairing b) = ⊥

The right radical of the numerical pairing is trivial.