hyperbolic bilinear forms

Stream: mathlib4

[Sahan Wijetunga]

Recently we formalized some theory about hyperbolic bilinear forms in the VERSEIM REU (see github). The definition we are following is essentially the one in The Algebraic and Geometric Theory of Quadratic Forms. We are thinking of contributing some of the content to mathlib, after cleaning up the code.

I'm writing here to ask for advice regarding the process. I included below an immediate result we would get from doing this, namely some characterization of isomorphisms of alternating forms. (See the verseim github for proofs of essentially the below statements)

import Mathlib.Tactic
import Mathlib.LinearAlgebra.BilinearForm.Orthogonal


variable {k V W : Type*} [Field k] [AddCommGroup V]
     [AddCommGroup W] [Module k V] [Module k W]
    {B : LinearMap.BilinForm k V} {B' : LinearMap.BilinForm k W}

variable (B) (B') in
@[ext]
structure Isometries
  where
    equiv : V ≃ₗ[k] W
    compat : ∀ x y, B' (equiv x) (equiv y) = B x y

-- Notation so that `V₁ ≃[k,B₁,B₂] V₂` denotes `Isometries B₁ B₂`
notation:26 lhs:26 "≃[" field:26 "," lhb:26 ","
  rhb:26 "]" rhs:26 =>
  Isometries (k:= field) (V := lhs) (W := rhs) lhb rhb

@[ext]
structure Hypspace (B : LinearMap.BilinForm k V) (ε : k) where
  I : Type
  basis : Module.Basis (I ⊕ I) k V
  isotropic_left : ∀ i j,
    B (basis (Sum.inl i)) (basis (Sum.inl j)) = 0
  isotropic_right : ∀ i j,
    B (basis (Sum.inr i)) (basis (Sum.inr j)) = 0
  orthog1: ∀ i, ∀ j, (i ≠ j) →
    B (basis (Sum.inl i)) (basis (Sum.inr j)) = 0
  orthog2: ∀ i, ∀ j, (i ≠ j) → B (basis (Sum.inr i)) (basis (Sum.inl j))
   = 0
  unital_corr: ∀ i, B (basis (Sum.inl i)) (basis (Sum.inr i)) = 1
  other_corr: ∀ i, B (basis (Sum.inr i)) (basis (Sum.inl i)) = ε

noncomputable def Hypspace.iso_from_iso_index {ε : k}
 (H : Hypspace B ε) (H' : Hypspace B' ε) (π : H.I ≃ H'.I) :
  V ≃[k, B, B'] W := by sorry

noncomputable def alternating_is_hyperbolic (balt : B.IsAlt) (hd : B.Nondegenerate)
    [FiniteDimensional k V] : Hypspace B (-1) := by sorry

noncomputable def iso_index_from_rank_eq {ε : k} (H : Hypspace B ε) (H' : Hypspace B' ε)
  (h : Module.finrank k V = Module.finrank k W)
  [FiniteDimensional k V][FiniteDimensional k W] :
  H.I ≃ H'.I := by sorry

noncomputable def alternate_iso (balt : B.IsAlt) (balt' : B'.IsAlt) [FiniteDimensional k V]
[FiniteDimensional k W] (hd : B.Nondegenerate) (hd' : B'.Nondegenerate)
(h : Module.finrank k V = Module.finrank k W) :
  V ≃[k, B, B'] W := by
    let H := alternating_is_hyperbolic balt hd
    let H' := alternating_is_hyperbolic balt' hd'
    exact H.iso_from_iso_index H' (iso_index_from_rank_eq H H' h)

Some questions:

• How should I formalize Hypspace? Is it fine as is or would making it a predicate on bases make more sense, and then formalize alternating_is_hyperbolic as a definition + a theorem if it satisfies the predicate?
• Should isomorphisms over bilinear forms be implemented in the way I see it currently in mathlib, in a definition of a linear isomorphism with a separate theorem that it commutes with the form? It felt a bit akward to state things this way (hence the separate definition of isomorphism first)
• Should we just fork mathlib and submit a pull request and make changes as requested, or try cleaning things up first?
• Are there any results like this in mathlib?

We're planning to use https://github.com/sahanwijetunga/Hyperbolic as the new repository (to leave the REU one unchanged)

Thanks! Any feedback would be appreciated

[Eric Wieser]

For Isometries, I suggest you follow the approach used by docs#QuadraticMap.Isometry, and extend LinearEquiv

[Sahan Wijetunga]

Got it, thanks!

[Eric Wieser]

To give a slightly longer reply: it's great to see more development on quadratic and bilinear forms in Mathlib! I know @Jonathan Hanke has some projects in this direction planned too.

How should I formalize Hypspace?

It's not clear to me whether the I : Type* bundled inside the structure is going to become problematic. Could you share a page / chapter / equation number for the reference you linked?

Should isomorphisms over bilinear forms be implemented in the way I see it currently in mathlib

(answered above)

Should we just fork mathlib and submit a pull request and make changes as requested, or try cleaning things up first?

Especially for a first PR, it's usually good to start with around 200 lines of code to get used to mathlib style. So you might want to consider making a PR with just isometries of bilinear spaces, and their compositions etc

[Eric Wieser]

Looking briefly at your repository, it seems your HyperbolicForm is a generalization of docs#LinearMap.dualProd

[Sahan Wijetunga]

My definition was just to formulate a way to describe a direct sum of hyperbolic 2 spaces, and that seemed to be the most convenient way (2-spaces being defined in say page 12 in the pdf).

Thanks for pointing out docs#LinearMap.dualProd. @George McNinch just brought up to me earlier that you can define hyperbolic as an isomorphism to the natural form on $V \times V^*$ (which is the one that agrees with the thing you linked).

[Sahan Wijetunga]

I'll start with just formalizing isometries of bilinear forms then. For hyperbolic space, should I avoid explicitly definining it as its own structure, and then just use an equivalence directly to LinearMap.dualProd?