Convention on the bidual

This file defines the identification of the bidual as choosen by Paul Gérardin in his paper.

Mains results

Let kbe a field, V a finite dimensional vector space over k, and Module.Dual k V its dual space. The main results are :

• convention_eval_iso : the convention that $V^{**}$ is identified with $V$ by $(x,y)=-(y,x)$.
• form_commutator_non_degenerate: the bilinear form $((x_1,y_1),(x_2,y_2))↦ (y_1(x_2)-y_2(x_1)$ is non degenerate.

def convention_dual (V : Type u_1) (k : Type u_2) [Field k] [AddCommGroup V] [Module k V] : Module.Dual k (Module.Dual k V) →ₗ[k] Module.Dual k V →ₗ[k] k

The map $(x,y)↦ - y(x)$ is a bilinear form on $V^{**}× V$.

Equations

• convention_dual V k = LinearMap.mk₂ k (fun (x : Module.Dual k (Module.Dual k V)) (y : Module.Dual k V) => -x y) ⋯ ⋯ ⋯ ⋯

@[simp]

theorem convention (V : Type u_1) (k : Type u_2) [Field k] [AddCommGroup V] [Module k V] (v : Module.Dual k V) (φ : Module.Dual k (Module.Dual k V)) : ((convention_dual V k) φ) v = -φ v

def convention_eval (V : Type u_1) (k : Type u_2) [Field k] [AddCommGroup V] [Module k V] : V →ₗ[k] Module.Dual k (Module.Dual k V)

The map $V → V^{**}$ satisfying the convention $(x,y)=-y(x)$.

Equations

• convention_eval V k = { toFun := fun (x : V) => -LinearMap.id.flip x, map_add' := ⋯, map_smul' := ⋯ }

@[simp]

theorem convention_eval_apply (V : Type u_1) (k : Type u_2) [Field k] [AddCommGroup V] [Module k V] (v : V) (φ : Module.Dual k V) : ((convention_eval V k) v) φ = -φ v

noncomputable def convention_eval_iso (V : Type u_1) (k : Type u_2) [Field k] [AddCommGroup V] [Module k V] [Module.IsReflexive k V] : V ≃ₗ[k] Module.Dual k (Module.Dual k V)

The bijection between a reflexive module and its double dual such that (x,y)=-(y,x), bundled as a LinearEquiv.

Equations

• convention_eval_iso V k = { toLinearMap := convention_eval V k, invFun := fun (x : Module.Dual k (Module.Dual k V)) => -(Module.evalEquiv k V).invFun x, left_inv := ⋯, right_inv := ⋯ }

@[simp]

theorem convention_eval_iso_apply (V : Type u_1) (k : Type u_2) [Field k] [AddCommGroup V] [Module k V] [FiniteDimensional k V] (v : V) (φ : Module.Dual k V) : ((convention_eval_iso V k) v) φ = -φ v

noncomputable def form_commutator (V : Type u_1) (k : Type u_2) [Field k] [AddCommGroup V] [Module k V] [Module.IsReflexive k V] : V × Module.Dual k V →ₗ[k] V × Module.Dual k V →ₗ[k] k

The bilinear form over $V × V^*$ that sends $((x_1,y_1),(x_2,y_2)$ to $y_1(x_2)-y_2(x_1)$.

Equations

• form_commutator V k = LinearMap.mk₂ k (fun (H1 H2 : V × Module.Dual k V) => H1.2.toFun H2.1 + ((convention_dual V k) ((↑(Module.evalEquiv k V)).toFun H1.1)) H2.2) ⋯ ⋯ ⋯ ⋯

theorem form_commutator_non_degenerate (V : Type u_1) (k : Type u_2) [Field k] [AddCommGroup V] [Module k V] [Module.IsReflexive k V] : LinearMap.BilinForm.Nondegenerate (form_commutator V k)

The bilinear form form_commutator is nondegeneracy