Documentation

TauCeti.LinearAlgebra.FiniteBilinearModule.Orthogonal.Complement

Orthogonal complements in finite bilinear modules #

This file develops the cardinality and double-complement theory of subgroups of a finite bilinear module. For a subgroup H of a possibly degenerate module A, the radical is the only obstruction to recovering H from its orthogonal complement:

H⊥⊥ = H + rad(A).

For a nondegenerate A the file also has the cardinality identity |H| |H⊥| = |A|, which is unavailable without nondegeneracy, together with its two consequences: double orthogonal complementation is the identity, and a Lagrangian subgroup has order whose square is the order of the ambient group.

The file closes with the degeneracy of a restricted pairing. Restricting the pairing to a subgroup S makes exactly the vectors of S ∩ S⊥ degenerate:

rad(A|_S) = S⊥ ∩ S.

Read at S = H⊥ and combined with the double-complement formula, this says that the pairing restricted to H⊥ has radical (H + rad(A)) ∩ H⊥, so in particular it kills the copy of H sitting inside H⊥ when H is isotropic. In general it kills H ∩ H⊥, which makes the orthogonal quotient H⊥ / (H ∩ H⊥) of TauCeti.LinearAlgebra.FiniteBilinearModule.Orthogonal.Quotient well defined.

Main declarations #

References #

Character restriction and cardinality #

source
def TauCeti.FiniteBilinearModule.pairingRestrict (A : FiniteBilinearModule) (H : AddSubgroup A.carrier) :
A.carrier →+ CharacterModule ↥H

Pair an element of A against a subgroup H, regarded as a character of H.

Equations
  • A.pairingRestrict H = { toFun := fun (x : A.carrier) => { toFun := fun (y : ↥H) => (A.pairing x) ↑y, map_zero' := ⋯, map_add' := ⋯ }, map_zero' := ⋯, map_add' := ⋯ }
Instances For
    source
    @[simp]
    theorem TauCeti.FiniteBilinearModule.pairingRestrict_apply (A : FiniteBilinearModule) (H : AddSubgroup A.carrier) (x : A.carrier) (y : ↥H) :
    ((A.pairingRestrict H) x) y = (A.pairing x) ↑y

    Evaluating the restricted pairing is evaluating the original pairing on the subtype.

    source
    @[simp]
    theorem TauCeti.FiniteBilinearModule.pairingRestrict_ker (A : FiniteBilinearModule) (H : AddSubgroup A.carrier) :
    (A.pairingRestrict H).ker = A.orthogonalComplement H

    The kernel of the restricted pairing is the orthogonal complement.

    source
    theorem TauCeti.FiniteBilinearModule.IsNondegenerate.pairingRestrict_surjective (A : FiniteBilinearModule) (hA : A.IsNondegenerate) (H : AddSubgroup A.carrier) :
    Function.Surjective ⇑(A.pairingRestrict H)

    In a nondegenerate finite bilinear module, every character of a subgroup is pairing with an element of the ambient module.

    source
    theorem TauCeti.FiniteBilinearModule.IsNondegenerate.card_mul_card_orthogonalComplement (A : FiniteBilinearModule) (hA : A.IsNondegenerate) (H : AddSubgroup A.carrier) :
    Nat.card ↥H * Nat.card ↥(A.orthogonalComplement H) = Nat.card A.carrier

    In a nondegenerate finite bilinear module, the orders of a subgroup and its orthogonal complement multiply to the order of the ambient module.

    source
    theorem TauCeti.FiniteBilinearModule.IsNondegenerate.orthogonalComplement_orthogonalComplement (A : FiniteBilinearModule) (hA : A.IsNondegenerate) (H : AddSubgroup A.carrier) :
    A.orthogonalComplement (A.orthogonalComplement H) = H

    Double orthogonal complementation is the identity in a nondegenerate finite bilinear module.

    source
    @[simp]
    theorem TauCeti.FiniteBilinearModule.orthogonalComplement_map_radicalQuotient (A : FiniteBilinearModule) (H : AddSubgroup A.carrier) :
    A.radicalQuotient.orthogonalComplement (AddSubgroup.map A.radicalQuotientMk H) = AddSubgroup.map A.radicalQuotientMk (A.orthogonalComplement H)

    Orthogonal complementation commutes with mapping to the radical quotient.

    source
    @[simp]
    theorem TauCeti.FiniteBilinearModule.orthogonalComplement_orthogonalComplement (A : FiniteBilinearModule) (H : AddSubgroup A.carrier) :
    A.orthogonalComplement (A.orthogonalComplement H) = H ⊔ A.radical

    For every subgroup of a finite bilinear module, the double orthogonal complement is the subgroup enlarged by the radical.

    source
    theorem TauCeti.FiniteBilinearModule.IsLagrangian.card_sq (A : FiniteBilinearModule) {H : AddSubgroup A.carrier} (hH : A.IsLagrangian H) (hA : A.IsNondegenerate) :
    Nat.card ↥H ^ 2 = Nat.card A.carrier

    A Lagrangian subgroup of a nondegenerate finite bilinear module has squared order equal to the order of the ambient group.

    The radical of a pairing restricted to an orthogonal complement #

    source
    theorem TauCeti.FiniteBilinearModule.radical_restrict_orthogonalComplement (A : FiniteBilinearModule) (H : AddSubgroup A.carrier) :
    (A.restrict (A.orthogonalComplement H)).radical = (H ⊔ A.radical).addSubgroupOf (A.orthogonalComplement H)

    The radical of the pairing restricted to H⊥ is the part of H + rad(A) lying in H⊥.

    It identifies the residual degeneracy that is removed when forming the orthogonal quotient.

    source
    theorem TauCeti.FiniteBilinearModule.addSubgroupOf_orthogonalComplement_le_radical_restrict (A : FiniteBilinearModule) (H : AddSubgroup A.carrier) :
    H.addSubgroupOf (A.orthogonalComplement H) ≤ (A.restrict (A.orthogonalComplement H)).radical

    The part of H lying in H⊥ is degenerate for the pairing restricted to H⊥.

    This is the inclusion which lets the restricted pairing descend to H⊥ / (H ∩ H⊥).