Symplectic group

Stream: LftCM22

[Moritz Doll]

A thread for the symplectic group

@Matej Penciak and Fabien Clery.

[Moritz Doll]

@Fabien Cléry

[Heather Macbeth]

A thread for the symplectic group group ...

[Moritz Doll]

right now we are only a monoid..

[Matej Penciak]

I got kind of bogged down with some annoying technical things on the train back home.

I made the repo: https://github.com/mpenciak/symplectic_groups if you want to check it out. I didn't quite get a group instance yet because I think I made a bad choice at some point to write all my theorems in terms of the hypotheses
{A : matrix (l ⊕ l) (l ⊕ l) ℝ} (hA : A ∈ symplectic l)
instead of
(A : symplectic l)
so I've run into a weird situation where I need to prove ⟨(↑A)⁻¹, _⟩ * A = 1

[Matej Penciak]

(also people are welcome to :golf: my proofs)

[Moritz Doll]

I just came back from dinner, but I will have a look now

[Jim Fowler]

The code for symplectic_inv was removed, but it seems like

noncomputable def symplectic_inv {A : matrix (l ⊕ l) (l ⊕ l) ℝ} (hA : A ∈ symplectic_group l) [invertible A] [invertible Aᵀ]:
  symplectic_group l :=
{ val := A⁻¹,
  property :=
  begin
    rw mem_symplectic_group_iff at hA ⊢,
    apply_fun (λ x, A⁻¹ ⬝ (x) ⬝ (Aᵀ)⁻¹) at hA,
    rw matrix.transpose_nonsing_inv,
    calc A⁻¹ ⬝ J l ℝ ⬝ Aᵀ⁻¹ = A⁻¹ ⬝ (A ⬝ J l ℝ ⬝ Aᵀ) ⬝ Aᵀ⁻¹ : by exact hA.symm
    ...                     = A⁻¹ ⬝ A ⬝ J l ℝ ⬝ Aᵀ ⬝ Aᵀ⁻¹ : by simp only [matrix.mul_assoc]
    ...                     = (A⁻¹ ⬝ A) ⬝ (J l ℝ) ⬝ (Aᵀ ⬝ Aᵀ⁻¹) : by simp only [matrix.mul_assoc]
    ...                     = (has_inv.inv A ⬝ A) ⬝ (J l ℝ) ⬝ (Aᵀ ⬝ Aᵀ⁻¹) : by refl
    ...                     = (⅟ A ⬝ A) ⬝ (J l ℝ) ⬝ (Aᵀ ⬝ Aᵀ⁻¹) : by rw matrix.inv_of_eq_nonsing_inv
    ...                     = 1 ⬝ (J l ℝ) ⬝ (Aᵀ ⬝ Aᵀ⁻¹) : by rw matrix.inv_of_mul_self
    ...                     = 1 ⬝ (J l ℝ) ⬝ (Aᵀ ⬝ (⅟ (Aᵀ))) : by rw matrix.inv_of_eq_nonsing_inv
    ...                     = 1 ⬝ (J l ℝ) ⬝ 1 : by rw matrix.mul_inv_of_self
    ...                     = J l ℝ : by simp
  end }

would work.

I find that I don't fully understand why matrices use ⬝ and the situation surrounding between ⅟ versus ⁻¹ and between has_invversus invertible.

[Junyan Xu]

Isn't invertible Aᵀ redundant? You could do haveI : invertible Aᵀ := // proof after the begin.

[Moritz Doll]

thanks @Jim Fowler actually both typeclasses are redunant, because we have hA

[Yakov Pechersky]

docs#invertible is a data-carrying class, unfortunately

[Moritz Doll]

One can completely get around using invertible and the weird inversion, see the current commit in Matej's repo (commit f356924).

[Jim Fowler]

I'm new to all this, and I would have thought that typeclass inference could have produced the [invertible A] from hA, so I am not sure what effect including [invertible A] has.

[Moritz Doll]

these are called typeclass-instances. A brief and not really correct explanation is that a typeclass behaves somewhat like a structure, but it is not type, so you can add additional fields to different types and an instance is the implementation, so that you can access the fields of invertiblefor A

[Jim Fowler]

But I would have thought having hA in the tactic state would mean that 1/ would infer the invertible instance, so I'm not sure what effect including [invertible A] had.