Finite Bilinear Module

Results named in Tau Ceti's TauCeti.LinearAlgebra.FiniteBilinearModule modules and in no roadmap's section, as Tau Ceti has them at commit ace60277.

TheoremNikulin's comparison theorem#

Two nondegenerate finite quadratic modules are isometric exactly when their polar bilinear modules are isometric and their Gauss-sum invariants agree.

TauCeti.FiniteQuadraticModule.nonempty_isometry_iff_bilinear_isometry_and_gaussSign_eq.{u, v}
  {A : TauCeti.FiniteQuadraticModule} {B : TauCeti.FiniteQuadraticModule} (hA : A.IsNondegenerate) :
  Nonempty (A.Isometry B) ↔
    Nonempty (A.Isometry B.toFiniteBilinearModule) ∧ A.gaussSign = B.gaussSign
Lean

Formalized in Tau Ceti as TauCeti.FiniteQuadraticModule.nonempty_isometry_iff_bilinear_isometry_and_gaussSign_eq.

Sources
LeanTauCeti.FiniteQuadraticModule.nonempty_isometry_iff_bilinear_isometry_and_gaussSign_eq
Uses 2
Statement usesTauCeti.FiniteQuadraticModule
Proof usesEuler's four-square identity for a quadratic map

TheoremNikulin's decomposition of nondegenerate quadratic modules of odd order#

A nondegenerate finite quadratic module of odd order is isometric to an orthogonal sum of odd cyclic modules q_θ^{(p)}(p^k), each of odd prime-power order m = p^k with coefficient θ prime to m.

TauCeti.FiniteQuadraticModule.exists_isometry_pi_oddCyclic.{u} (A : TauCeti.FiniteQuadraticModule)
  (hA : A.IsNondegenerate) (hodd : Odd (Nat.card A.carrier)) :
  ∃ n m,
    ∃ (hm : ∀ (i : Fin n), Odd (m i)),
      ∃ θ,
        (∀ (i : Fin n), IsPrimePow (m i) ∧ IsCoprime (↑(m i)) (θ i)) ∧
          Nonempty
            ((TauCeti.FiniteQuadraticModule.pi fun i =>
                  TauCeti.FiniteQuadraticModule.oddCyclic (m i) ⋯ (θ i)).Isometry
              A)
Lean

Formalized in Tau Ceti as TauCeti.FiniteQuadraticModule.exists_isometry_pi_oddCyclic.

Sources
LeanTauCeti.FiniteQuadraticModule.exists_isometry_pi_oddCyclic
Uses 1
Statement usesTauCeti.FiniteQuadraticModule

TheoremNikulin's generator decomposition#

A nondegenerate finite quadratic module is isometric to an orthogonal sum of Nikulin's generators: odd cyclic modules q_θ^{(p)}(p^k) of odd prime-power order m = p^k with θ prime to m, dyadic cyclic modules q_η^{(2)}(2^{k+1}) with η odd, and rank-two modules u^{(2)}(2^{k+1}) and v^{(2)}(2^{k+1}).

TauCeti.FiniteQuadraticModule.exists_isometry_prod_pi_generators.{u}
  (A : TauCeti.FiniteQuadraticModule) (hA : A.IsNondegenerate) :
  ∃ a m,
    ∃ (hm : ∀ (i : Fin a), Odd (m i)),
      ∃ θ b k η c ku d kv,
        (∀ (i : Fin a), IsPrimePow (m i) ∧ IsCoprime (↑(m i)) (θ i)) ∧
          (∀ (i : Fin b), Odd (η i)) ∧
            Nonempty
              (((TauCeti.FiniteQuadraticModule.pi fun i =>
                        TauCeti.FiniteQuadraticModule.oddCyclic (m i) ⋯ (θ i)).prod
                    ((TauCeti.FiniteQuadraticModule.pi fun i =>
                          TauCeti.FiniteQuadraticModule.dyadicCyclic (k i + 1) (η i)).prod
                      ((TauCeti.FiniteQuadraticModule.pi fun i =>
                            TauCeti.FiniteQuadraticModule.dyadicU (ku i + 1)).prod
                        (TauCeti.FiniteQuadraticModule.pi fun i =>
                          TauCeti.FiniteQuadraticModule.dyadicV (kv i + 1))))).Isometry
                A)
Lean

Formalized in Tau Ceti as TauCeti.FiniteQuadraticModule.exists_isometry_prod_pi_generators.

Sources
LeanTauCeti.FiniteQuadraticModule.exists_isometry_prod_pi_generators
Uses 1
Statement usesTauCeti.FiniteQuadraticModule

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.