Module

Matrix_exists_transpose_mul_mul_eq_J.lean

Nyll.AlgebraicCurves.Foundations.Algebra.Matrix_exists_transpose_mul_mul_eq_J

2 declarations indexed from sourceView source ↗

Module documentation

Matrix exists transpose mul mul eq J

Imports12

Mathlib.Algebra.Module.Torsion.Free
Mathlib.LinearAlgebra.Dimension.Finite
Mathlib.LinearAlgebra.Dimension.Constructions
Mathlib.LinearAlgebra.FreeModule.PID
Mathlib.LinearAlgebra.Basis.Prod
Mathlib.LinearAlgebra.Matrix.BilinearForm
Mathlib.LinearAlgebra.Matrix.Basis
Mathlib.LinearAlgebra.Matrix.NonsingularInverse
Mathlib.LinearAlgebra.SymplecticGroup
Mathlib.Logic.Equiv.Sum
Mathlib.Tactic.Abel
Mathlib.Tactic.Ring.RingNF

Imported by1

Nyll.AlgebraicCurves.Foundations.Algebra.All

theorem

exists_basis

L38 ↗

AlgebraicCurves.Foundations.Algebra.Proofs.Matrix_exists_transpose_mul_mul_eq_J.SymplecticNormalFormZ.exists_basis

Source context 4 commands

Surrounding namespaces, section variables, and local commands at this declaration.

section ProofImplementation
namespace AlgebraicCurves.Foundations.Algebra.Proofs.Matrix_exists_transpose_mul_mul_eq_J
namespace SymplecticNormalFormZ
open LinearMap (BilinForm)

Lean source · statement

theorem exists_basis (k : ℕ) :
    ∀ (M : Type*) [AddCommGroup M] [Module.Free ℤ M] [Module.Finite ℤ M],
      Module.finrank ℤ M = k → ∀ B : BilinForm ℤ M, (∀ x, B x x = 0) →
      (∀ x, (∀ y, B x y = 0) → x = 0) → (∀ φ : Module.Dual ℤ M, ∃ x, ∀ y, B x y = φ y) →
      ∃ (ι : Type) (_ : Fintype ι) (e : Module.Basis (ι ⊕ ι) ℤ M),
        (∀ i j, B (e (Sum.inl i)) (e (Sum.inl j)) = 0) ∧
        (∀ i j, B (e (Sum.inr i)) (e (Sum.inr j)) = 0) ∧
        (∀ i, B (e (Sum.inr i)) (e (Sum.inl i)) = 1) ∧
        (∀ i j, i ≠ j → B (e (Sum.inr i)) (e (Sum.inl j)) = 0)

theorem

exists_transpose_mul_mul_eq_J

L227 ↗

Matrix.exists_transpose_mul_mul_eq_J

Source context 3 commands