Linear algebra exercise

Stream: new members

[Valentin Bosshard]

Hi, I am Valentin and this is my first question here. I am trying to do a linear algebra exercise that almost directly follows from unpacking the definitions. However, I have some problems when I want to apply a statement that holds for x∈ N in a situation x : ↥N. Can I do that? If yes, how? I guess the answer might be very simple, but asking here would save me a lot of time and gives me the opportunity to introduce myself.
I included a not-so-minimal mwe because maybe you have other suggestions on how I can improve my writing style or in case you have a much shorter proof that I can learn from. (To my mathematical background: I am a PhD student in symplectic geometry and therefore thought I might experiment some more in lean by looking at statements about symplectic vector spaces and this is my first attempt).

import linear_algebra.bilinear_form

variables {R : Type*} {M : Type*} [semiring R] [add_comm_monoid M] [module R M]

def is_isotropic (B : bilin_form R M) (N : submodule R M) : Prop :=
N ≤ B.orthogonal N

lemma is_isotropic_iff_restrict_eq_zero (B : bilin_form R M) (N : submodule R M) :
  is_isotropic B N ↔ B.restrict N = 0 :=
begin
  rw [is_isotropic, bilin_form.ext_iff, set_like.le_def],
  split,
  { intro h,
    simp,
    intros,
    sorry
  },
  { intros h x hx,
    simp,
    intros n hm,
    refine bilin_form.is_ortho_def.mpr _,
    simp at h,
    specialize h ⟨n, hm⟩,
    specialize h ⟨x, hx⟩,
    exact h
  }
end

Of course, I want to do something like specialize h x but then I get:

type mismatch at application
  h x
term
  x
has type
  ↥N : Type u_2
but is expected to have type
  ?m_1 ∈ N : Prop
state:
R : Type u_1,
M : Type u_2,
_inst_1 : semiring R,
_inst_2 : add_comm_monoid M,
_inst_3 : module R M,
B : bilin_form R M,
N : submodule R M,
h : ∀ ⦃x : M⦄, x ∈ N → x ∈ B.orthogonal N,
x y : ↥N
⊢ ⇑B ↑x ↑y = 0

[Eric Wieser]

Note that x.prop is often better than x.property, as the latter uses the ↑ that Patrick remarks is better

[Notification Bot]

Valentin Bosshard has marked this topic as unresolved.

[Valentin Bosshard]

In linear_algebra/bilinear_form there are several lemmas that can be generalized from symmetric bilinear forms to reflexive bilinear forms (which would be nice for me because I want to say something about alternating bilinear forms). The proofs themselves do almost not need any changes. Can I request permission to push these changes? My github name is tinval.

[Riccardo Brasca]

Invitation sent!

[Riccardo Brasca]

Have a look at this before opening your first PR

[Riccardo Brasca]

We also have a nice video

[Heather Macbeth]

Welcome @Valentin Bosshard! Nice to see another differential geometer here. We were discussing a few accessible targets related to symplectic geometry a few months ago, if you're interested:
https://leanprover.zulipchat.com/#narrow/stream/116395-maths/topic/Symplectic.20geometry
But yes, it's a long way to Fukaya categories :)