Quotients of a finite bilinear module by a subgroup of its radical

A subgroup K of the radical of a finite bilinear module A pairs trivially with everything, so the pairing descends to the quotient A / K:

b (x + K) (y + K) = b x y.

The resulting module is nondegenerate exactly when K is the whole radical, since the radical of the quotient is the image of rad(A). Taking K = rad(A) therefore gives the canonical nondegenerate quotient, and other choices of K arise when a specific subgroup is being divided out.

Both quotientOfLeRadical and radicalQuotient are exposed, so their carriers reduce to the Submodule quotient and a map out of either can be built directly with Submodule.liftQ or QuadraticMap.lift.

Main declarations

• TauCeti.FiniteBilinearModule.quotientOfLeRadical: the quotient by a subgroup of the radical.
• TauCeti.FiniteBilinearModule.radical_quotientOfLeRadical: the radical of the quotient is the image of the radical.
• TauCeti.FiniteBilinearModule.isNondegenerate_quotientOfLeRadical_iff: nondegeneracy holds exactly when the subgroup exhausts the radical.
• TauCeti.FiniteBilinearModule.card_quotientOfLeRadical: the order of the quotient is the index of the subgroup.
• TauCeti.FiniteBilinearModule.quotientOfLeRadicalMk_eq_iff: two elements have the same class exactly when they differ by an element of the subgroup.
• TauCeti.FiniteBilinearModule.radicalQuotient: the nondegenerate quotient by the radical.

References

• V. V. Nikulin, Integral symmetric bilinear forms and some of their applications, §1.1.
• W. Ebeling, Lattices and Codes, Chapter 1.

Quotient by a subgroup of the radical

@[reducible, inline]

abbrev TauCeti.FiniteBilinearModule.QuotientByAddSubgroup (A : FiniteBilinearModule) (K : AddSubgroup A.carrier) : Type u

The underlying additive quotient of a finite bilinear module by a subgroup.

This is a Submodule quotient, so Submodule.liftQ and QuadraticMap.lift apply to it. It is the carrier of quotientOfLeRadical when the subgroup lies in the radical.

Equations

• A.QuotientByAddSubgroup K = (A.carrier ⧸ AddSubgroup.toIntSubmodule K)

theorem TauCeti.FiniteBilinearModule.toIntSubmodule_le_ker_toBilin (A : FiniteBilinearModule) {K : AddSubgroup A.carrier} (hK : K ≤ A.radical) : AddSubgroup.toIntSubmodule K ≤ A.toBilin.ker

A subgroup of the radical, read as a ℤ-submodule, lies in the kernel of the pairing.

noncomputable def TauCeti.FiniteBilinearModule.quotientOfLeRadicalBilin (A : FiniteBilinearModule) (K : AddSubgroup A.carrier) (hK : K ≤ A.radical) : A.QuotientByAddSubgroup K →ₗ[ℤ] A.QuotientByAddSubgroup K →ₗ[ℤ] AddCircle 1

The pairing of a finite bilinear module, descended through a subgroup of its radical.

This is the underlying ℤ-bilinear map of quotientOfLeRadical.

Equations

• A.quotientOfLeRadicalBilin K hK = LinearMap.IsRefl.liftQ₂ A.toBilin (AddSubgroup.toIntSubmodule K) ⋯ ⋯

@[simp]

theorem TauCeti.FiniteBilinearModule.quotientOfLeRadicalBilin_mk (A : FiniteBilinearModule) (K : AddSubgroup A.carrier) (hK : K ≤ A.radical) (x y : A.carrier) : ((A.quotientOfLeRadicalBilin K hK) (Submodule.Quotient.mk x)) (Submodule.Quotient.mk y) = (A.pairing x) y

The descended pairing is computed by the original pairing on representatives.

noncomputable def TauCeti.FiniteBilinearModule.quotientOfLeRadical (A : FiniteBilinearModule) (K : AddSubgroup A.carrier) (hK : K ≤ A.radical) : FiniteBilinearModule

The finite bilinear module obtained by quotienting by a subgroup of the radical.

The package is exposed so that its carrier projection reduces to the Submodule quotient QuotientByAddSubgroup, which is what a map out of the quotient needs.

Equations

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

noncomputable def TauCeti.FiniteBilinearModule.quotientOfLeRadicalMk (A : FiniteBilinearModule) (K : AddSubgroup A.carrier) (hK : K ≤ A.radical) : A.carrier →+ (A.quotientOfLeRadical K hK).carrier

The quotient map onto the quotient by a subgroup of the radical.

Equations

• A.quotientOfLeRadicalMk K hK = (AddSubgroup.toIntSubmodule K).mkQ.toAddMonoidHom

theorem TauCeti.FiniteBilinearModule.quotientOfLeRadicalMk_apply (A : FiniteBilinearModule) (K : AddSubgroup A.carrier) (hK : K ≤ A.radical) (x : A.carrier) : (A.quotientOfLeRadicalMk K hK) x = Submodule.Quotient.mk x

The quotient map sends an element to its quotient class.

@[simp]

theorem TauCeti.FiniteBilinearModule.quotientOfLeRadical_pairing_mk (A : FiniteBilinearModule) (K : AddSubgroup A.carrier) (hK : K ≤ A.radical) (x y : A.carrier) : ((A.quotientOfLeRadical K hK).pairing ((A.quotientOfLeRadicalMk K hK) x)) ((A.quotientOfLeRadicalMk K hK) y) = (A.pairing x) y

The quotient pairing is represented by the original pairing on representatives.

theorem TauCeti.FiniteBilinearModule.quotientOfLeRadicalMk_surjective (A : FiniteBilinearModule) (K : AddSubgroup A.carrier) (hK : K ≤ A.radical) : Function.Surjective ⇑(A.quotientOfLeRadicalMk K hK)

The quotient map by a subgroup of the radical is surjective.

@[simp]

theorem TauCeti.FiniteBilinearModule.quotientOfLeRadicalMk_ker (A : FiniteBilinearModule) (K : AddSubgroup A.carrier) (hK : K ≤ A.radical) : (A.quotientOfLeRadicalMk K hK).ker = K

The kernel of the quotient map by a subgroup of the radical is that subgroup.

@[simp]

theorem TauCeti.FiniteBilinearModule.quotientOfLeRadicalMk_eq_zero_iff (A : FiniteBilinearModule) (K : AddSubgroup A.carrier) (hK : K ≤ A.radical) (x : A.carrier) : (A.quotientOfLeRadicalMk K hK) x = 0 ↔ x ∈ K

A class in the quotient vanishes exactly when its representative lies in the subgroup.

@[simp]

theorem TauCeti.FiniteBilinearModule.quotientOfLeRadicalMk_eq_iff (A : FiniteBilinearModule) (K : AddSubgroup A.carrier) (hK : K ≤ A.radical) (x y : A.carrier) : (A.quotientOfLeRadicalMk K hK) x = (A.quotientOfLeRadicalMk K hK) y ↔ x - y ∈ K

Two elements have the same class in the quotient exactly when they differ by an element of the subgroup.

theorem TauCeti.FiniteBilinearModule.radical_quotientOfLeRadical (A : FiniteBilinearModule) (K : AddSubgroup A.carrier) (hK : K ≤ A.radical) : (A.quotientOfLeRadical K hK).radical = AddSubgroup.map (A.quotientOfLeRadicalMk K hK) A.radical

The radical of the quotient is the image of the radical: quotienting by a subgroup of the radical does not create new degeneracy.

theorem TauCeti.FiniteBilinearModule.isNondegenerate_quotientOfLeRadical_iff (A : FiniteBilinearModule) (K : AddSubgroup A.carrier) (hK : K ≤ A.radical) : (A.quotientOfLeRadical K hK).IsNondegenerate ↔ A.radical ≤ K

Nondegeneracy of the quotient. Quotienting by a subgroup of the radical leaves a nondegenerate module exactly when that subgroup exhausts the radical.

theorem TauCeti.FiniteBilinearModule.card_quotientOfLeRadical (A : FiniteBilinearModule) (K : AddSubgroup A.carrier) (hK : K ≤ A.radical) : Nat.card (A.quotientOfLeRadical K hK).carrier = K.index

The order of the quotient by a subgroup of the radical is the index of that subgroup.

Quotient by the radical

noncomputable def TauCeti.FiniteBilinearModule.radicalQuotient (A : FiniteBilinearModule) : FiniteBilinearModule

The finite bilinear module obtained by quotienting by the radical.

Exposed for the same reason as quotientOfLeRadical: so that its carrier reduces to the Submodule quotient and maps out of it are definable.

Equations

• A.radicalQuotient = A.quotientOfLeRadical A.radical ⋯

noncomputable def TauCeti.FiniteBilinearModule.radicalQuotientMk (A : FiniteBilinearModule) : A.carrier →+ A.radicalQuotient.carrier

The quotient map from a finite bilinear module to its radical quotient.

Equations

• A.radicalQuotientMk = A.quotientOfLeRadicalMk A.radical ⋯

@[simp]

theorem TauCeti.FiniteBilinearModule.radicalQuotient_pairing_mk (A : FiniteBilinearModule) (x y : A.carrier) : (A.radicalQuotient.pairing (A.radicalQuotientMk x)) (A.radicalQuotientMk y) = (A.pairing x) y

The quotient pairing is represented by the original pairing on representatives.

theorem TauCeti.FiniteBilinearModule.radicalQuotientMk_surjective (A : FiniteBilinearModule) : Function.Surjective ⇑A.radicalQuotientMk

The quotient map to the radical quotient is surjective.

@[simp]

theorem TauCeti.FiniteBilinearModule.radicalQuotientMk_ker (A : FiniteBilinearModule) : A.radicalQuotientMk.ker = A.radical

The kernel of the radical quotient map is the radical.

@[simp]

theorem TauCeti.FiniteBilinearModule.radicalQuotientMk_eq_iff (A : FiniteBilinearModule) (x y : A.carrier) : A.radicalQuotientMk x = A.radicalQuotientMk y ↔ x - y ∈ A.radical

Two elements have the same class in the radical quotient exactly when they differ by an element of the radical.

theorem TauCeti.FiniteBilinearModule.isNondegenerate_radicalQuotient (A : FiniteBilinearModule) : A.radicalQuotient.IsNondegenerate

Quotienting a finite bilinear module by its radical produces a nondegenerate module.