From mathcomp
Require Import all_ssreflect ssralg fingroup zmodp poly ssrnum.
From mathcomp
Require Import matrix mxalgebra vector falgebra ssrnum algC algnum.
From mathcomp
Require Import fieldext.
From mathcomp Require Import vector.
# Bilinear forms
(undocumented)
Set Implicit Arguments.
Unset Strict Implicit.
Unset Printing Implicit Defensive.
Local Open Scope ring_scope.
Import GRing.Theory Num.Theory.
Reserved Notation "'[ u , v ]"
(
at level 2, format "'[hv' ''[' u , '/ ' v ] ']'").
Reserved Notation "'[ u , v ]_ M"
(
at level 2, format "'[hv' ''[' u , '/ ' v ]_ M ']'").
Reserved Notation "'[ u ]_ M" (at level 2, format "''[' u ]_ M").
Reserved Notation "'[ u ]" (at level 2, format "''[' u ]").
Reserved Notation "u '``_' i"
(
at level 3, i at level 2, left associativity, format "u '``_' i").
Reserved Notation "A ^_|_" (at level 8, format "A ^_|_").
Reserved Notation "A _|_ B" (at level 69, format "A _|_ B").
Reserved Notation "eps_theta .-sesqui" (at level 2, format "eps_theta .-sesqui").
Notation
"u '``_' i"
:= (
u (
GRing.zero (
Zp_zmodType O))
i)
: ring_scope.
Notation
"''e_' i"
:= (
delta_mx 0 i)
(
format "''e_' i", at level 3)
: ring_scope.
Local Notation
"M ^ phi"
:= (
map_mx phi M).
Local Notation
"M ^t phi"
:= (
map_mx phi (
M ^T)) (
phi at level 30, at level 30).
Structure
revop
X
Y
Z
(
f
: Y -> X -> Z)
:= RevOp {
fun_of_revop
:> X -> Y -> Z;
_ : forall
x,
f x =1 fun_of_revop^~ x
}.
Lemma
eq_map_mx_id
(
R
: ringType)
m
n
(
M
: 'M[R]_(
m,n)) (
f
: R -> R)
:
f =1 id -> M ^ f = M.
Proof.
by move=> /eq_map_mx->; rewrite map_mx_id. Qed.
Module
Bilinear
.
Section
ClassDef
.
Variables (
R
: ringType) (
U
U'
: lmodType R) (
V
: zmodType) (
s
s'
: R -> V -> V).
Implicit Type phUU'V : phant (
U -> U' -> V).
Local Coercion GRing.Scale.op : GRing.Scale.law >-> Funclass.
Definition
axiom
(
f
: U -> U' -> V) (
s_law
: GRing.Scale.law s) (
eqs
: s = s_law)
(
s'_law
: GRing.Scale.law s') (
eqs'
: s' = s'_law)
:=
((
forall
u',
GRing.Linear.axiom (
f^~ u')
eqs)
* (
forall
u,
GRing.Linear.axiom (
f u)
eqs'))
%type.
Record
class_of
(
f
: U -> U' -> V)
: Prop := Class {
basel
: forall
u',
GRing.Linear.class_of s (
f^~ u')
;
baser
: forall
u,
GRing.Linear.class_of s' (
f u)
}.
Lemma
class_of_axiom
f
s_law
s'_law
Ds
Ds'
:
@axiom f s_law Ds s'_law Ds' -> class_of f.
Proof.
Structure
map
phUU'V
:= Pack {apply; _ : class_of apply}.
Local Coercion apply : map >-> Funclass.
Definition
class
(
phUU'V
: _) (
cF
: map phUU'V)
:=
let: Pack _ c as cF' := cF return class_of cF' in c.
Canonical
additiver
phU'V
phUU'V
(
u
: U)
cF
:= GRing.Additive.Pack phU'V
(
baser (
@class phUU'V cF)
u).
Canonical
linearr
phU'V
phUU'V
(
u
: U)
cF
:= GRing.Linear.Pack phU'V
(
baser (
@class phUU'V cF)
u).
Definition
applyr_head
t
(
f
: U -> U' -> V)
u
v
:= let: tt := t in f v u.
Notation
applyr
:= (
@applyr_head tt).
Canonical
additivel
phUV
phUU'V
(
u'
: U') (
cF
: map _)
:=
@GRing.
Additive.Pack _ _ phUV (
applyr cF u') (
basel (
@class phUU'V cF)
u').
Canonical
linearl
phUV
phUU'V
(
u'
: U') (
cF
: map _)
:=
@GRing.
Linear.Pack _ _ _ _ phUV (
applyr cF u') (
basel (
@class phUU'V cF)
u').
Definition
pack
(
phUV
: phant (
U -> V)) (
phU'V
: phant (
U' -> V))
(
revf
: U' -> U -> V) (
rf
: revop revf)
f
(
g
: U -> U' -> V)
of (
g = fun_of_revop rf)
:=
fun (
bFl
: U' -> GRing.Linear.map s phUV)
flc
of (
forall
u',
revf u' = bFl u')
&
(
forall
u',
phant_id (
GRing.Linear.class (
bFl u')) (
flc u'))
=>
fun (
bFr
: U -> GRing.Linear.map s' phU'V)
frc
of (
forall
u,
g u = bFr u)
&
(
forall
u,
phant_id (
GRing.Linear.class (
bFr u)) (
frc u))
=>
@Pack (
Phant _)
f (
Class flc frc).
End ClassDef.
Module
Exports
.
Delimit Scope linear_ring_scope with linR.
Notation
bilinear_for
s s' f := (
axiom f (
erefl s) (
erefl s')).
Notation
bilinear
f := (
bilinear_for *:%R *:%R f).
Notation
biscalar
f := (
bilinear_for *%R *%R f).
Notation
bilmorphism_for
s s' f := (
class_of s s' f).
Notation
bilmorphism
f := (
bilmorphism_for *:%R *:%R f).
Coercion class_of_axiom : axiom >-> bilmorphism_for.
Coercion baser : bilmorphism_for >-> Funclass.
Coercion apply : map >-> Funclass.
Notation
"{ 'bilinear' fUV | s & s' }"
:= (
map s s' (
Phant fUV))
(
at level 0, format "{ 'bilinear' fUV | s & s' }")
: ring_scope.
Notation
"{ 'bilinear' fUV | s }"
:= (
map s.
1 s.
2 (
Phant fUV))
(
at level 0, format "{ 'bilinear' fUV | s }")
: ring_scope.
Notation
"{ 'bilinear' fUV }"
:= {bilinear fUV | *:%R & *:%R}
(
at level 0, format "{ 'bilinear' fUV }")
: ring_scope.
Notation
"{ 'biscalar' U }"
:= {bilinear U -> U -> _ | *%R & *%R}
(
at level 0, format "{ 'biscalar' U }")
: ring_scope.
Notation
"[ 'bilinear' 'of' f 'as' g ]"
:=
(
@pack _ _ _ _ _ _ _ _ _ _ f g erefl _ _
(
fun=> erefl) (
fun=> idfun)
_ _ (
fun=> erefl) (
fun=> idfun)).
Notation
"[ 'bilinear' 'of' f ]"
:= [bilinear of f as f]
(
at level 0, format "[ 'bilinear' 'of' f ]")
: form_scope.
Coercion additiver : map >-> GRing.Additive.map.
Coercion linearr : map >-> GRing.Linear.map.
Canonical additiver.
Canonical linearr.
Canonical additivel.
Canonical linearl.
Notation
applyr
:= (
@applyr_head _ _ _ _ tt).
End Exports.
End Bilinear.
Include Bilinear.Exports.
Section
BilinearTheory
.
Variable
R
: ringType.
Section
GenericProperties
.
Variables (
U
U'
: lmodType R) (
V
: zmodType) (
s
: R -> V -> V) (
s'
: R -> V -> V).
Variable
f
: {bilinear U -> U' -> V | s & s'}.
Lemma
linear0r
z
: f z 0 = 0
Proof.
Lemma
linearNr
z
: {morph f z :
x
/ - x}
Proof.
Lemma
linearDr
z
: {morph f z :
x
y
/ x + y}
Proof.
Lemma
linearBr
z
: {morph f z :
x
y
/ x - y}
Proof.
Lemma
linearMnr
z
n
: {morph f z :
x
/ x *+ n}
Proof.
Lemma
linearMNnr
z
n
: {morph f z :
x
/ x *- n}
Proof.
Lemma
linear_sumr
z
I
r
(
P
: pred I)
E
:
f z (
\sum_(
i
<- r | P i)
E i)
= \sum_(
i
<- r | P i)
f z (
E i).
Proof.
Lemma
linearZr_LR
z
: scalable_for s' (
f z)
Proof.
Lemma
linearPr
z
a
: {morph f z :
u
v
/ a *: u + v >-> s' a u + v}.
Proof.
Lemma
applyrE
x
: applyr f x =1 f^~ x
Proof.
by []. Qed.
Lemma
linear0l
z
: f 0 z = 0
Proof.
by rewrite -applyrE raddf0. Qed.
Lemma
linearNl
z
: {morph f^~ z :
x
/ - x}.
Proof.
by move=> ?; rewrite -applyrE raddfN. Qed.
Lemma
linearDl
z
: {morph f^~ z :
x
y
/ x + y}.
Proof.
by move=> ??; rewrite -applyrE raddfD. Qed.
Lemma
linearBl
z
: {morph f^~ z :
x
y
/ x - y}.
Proof.
by move=> ??; rewrite -applyrE raddfB. Qed.
Lemma
linearMnl
z
n
: {morph f^~ z :
x
/ x *+ n}.
Proof.
by move=> ?; rewrite -applyrE raddfMn. Qed.
Lemma
linearMNnl
z
n
: {morph f^~ z :
x
/ x *- n}.
Proof.
by move=> ?; rewrite -applyrE raddfMNn. Qed.
Lemma
linear_suml
z
I
r
(
P
: pred I)
E
:
f (
\sum_(
i
<- r | P i)
E i)
z = \sum_(
i
<- r | P i)
f (
E i)
z.
Proof.
Lemma
linearZl_LR
z
: scalable_for s (
f^~ z).
Proof.
Lemma
linearPl
z
a
: {morph f^~ z :
u
v
/ a *: u + v >-> s a u + v}.
Proof.
by move=> ??; rewrite -applyrE linearP. Qed.
End GenericProperties.
Section
BidirectionalLinearZ
.
Variables (
U
: lmodType R) (
V
: zmodType) (
s
: R -> V -> V).
Variables (
S
: ringType) (
h
: S -> V -> V) (
h_law
: GRing.Scale.law h).
End BidirectionalLinearZ.
End BilinearTheory.
Canonical
rev_mulmx
(
R
: ringType)
m
n
p
:= @RevOp _ _ _ (
@mulmxr R m n p)
(
@mulmx R m n p) (
fun _ _ => erefl).
Canonical
mulmx_bilinear
(
R
: comRingType)
m
n
p
:= [bilinear of @mulmx R m n p].
Section
BilinearForms
.
Variables (
R
: fieldType) (
theta
: {rmorphism R -> R}).
Variables (
n
: nat) (
M
: 'M[R]_n).
Implicit Types (
a b : R) (
u v : 'rV[R]_n) (
N P Q : 'M[R]_n).
Definition
form
u
v
:= (
u *m M *m (
v ^t theta))
0 0.
Local Notation
"''[' u , v ]"
:= (
form u%R v%R)
: ring_scope.
Local Notation
"''[' u ]"
:= '[u, u] : ring_scope.
Lemma
form0l
u
: '[0, u] = 0.
Proof.
by rewrite /form !mul0mx mxE. Qed.
Lemma
form0r
u
: '[u, 0] = 0.
Proof.
Lemma
formDl
u
v
w
: '[u + v, w] = '[u, w] + '[v, w].
Proof.
by rewrite /form !mulmxDl mxE. Qed.
Lemma
formDr
u
v
w
: '[u, v + w] = '[u, v] + '[u, w].
Proof.
by rewrite /form linearD !map_mxD !mulmxDr mxE. Qed.
Lemma
formZr
a
u
v
: '[u, a *: v] = theta a * '[u, v].
Proof.
Lemma
formZl
a
u
v
: '[a *: u, v] = a * '[u, v].
Proof.
Lemma
formNl
u
v
: '[- u, v] = - '[u, v].
Proof.
Lemma
formNr
u
v
: '[u, - v] = - '[u, v].
Proof.
Lemma
formee
i
j
: '['e_i, 'e_j] = M i j.
Proof.
rewrite /form -rowE -map_trmx map_delta_mx -[M in LHS]trmxK.
by rewrite -tr_col -trmx_mul -rowE !mxE.
Qed.
Lemma
form0_eq0
: M = 0 -> forall
u
v,
'[u, v] = 0.
Proof.
End BilinearForms.
Section
Sesquilinear
.
Variable
R
: fieldType.
Variable
n
: nat.
Implicit Types (
a b : R) (
u v : 'rV[R]_n) (
N P Q : 'M[R]_n).
Section
Def
.
Variable
eps_theta
: (
bool * {rmorphism R -> R}).
Definition
sesqui
:=
[qualify
M
: 'M_n | M == ((
-1)
^+ eps_theta.
1)
*: M ^t eps_theta.
2].
Fact
sesqui_key
: pred_key sesqui
Proof.
by []. Qed.
Canonical
sesqui_keyed
:= KeyedQualifier sesqui_key.
End Def.
Local Notation
"eps_theta .-sesqui"
:= (
sesqui eps_theta).
Variables (
eps
: bool) (
theta
: {rmorphism R -> R}).
Variables (
M
: 'M[R]_n).
Local Notation
"''[' u , v ]"
:= (
form theta M u%R v%R)
: ring_scope.
Local Notation
"''[' u ]"
:= '[u, u] : ring_scope.
Lemma
sesquiE
: (
M \is (
eps,theta).
-sesqui)
= (
M == (
-1)
^+ eps *: M ^t theta).
Proof.
Lemma
sesquiP
: reflect (
M = (
-1)
^+ eps *: M ^t theta)
(
M \is (
eps,theta).
-sesqui).
Proof.
Hypothesis (
thetaK
: involutive theta).
Hypothesis (
M_sesqui
: M \is (
eps, theta).
-sesqui).
Lemma
trmx_sesqui
: M^T = (
-1)
^+ eps *: M ^ theta.
Proof.
Lemma
maptrmx_sesqui
: M^t theta = (
-1)
^+ eps *: M.
Proof.
Lemma
formC
u
v
: '[u, v] = (
-1)
^+ eps * theta '[v, u].
Proof.
Lemma
form_eq0C
u
v
: (
'[u, v] == 0)
= (
'[v, u] == 0).
Proof.
Definition
ortho
m
(
B
: 'M_(
m,n))
:= (
kermx (
M *m (
B ^t theta))).
Local Notation
"B ^_|_"
:= (
ortho B)
: ring_scope.
Local Notation
"A _|_ B"
:= (
A%MS <= B^_|_)
%MS : ring_scope.
Lemma
normalE
u
v
: (
u _|_ v)
= (
'[u, v] == 0).
Proof.
Lemma
form_eq0P
{u
v}
: reflect (
'[u, v] = 0) (
u _|_ v).
Proof.
Lemma
normalP
p
q
(
A
: 'M_(
p, n)) (
B
:'M_(
q, n))
:
reflect (
forall (
u
v
: 'rV_n)
, (
u <= A)
%MS -> (
v <= B)
%MS -> u _|_ v)
(
A _|_ B).
Proof.
Lemma
normalC
p
q
(
A
: 'M_(
p, n)) (
B
:'M_(
q, n))
: (
A _|_ B)
= (
B _|_ A).
Proof.
gen have nC : p q A B / A _|_ B -> B _|_ A; last by apply/idP/idP; apply/nC.
move=> AnB; apply/normalP => u v ? ?; rewrite normalE.
rewrite formC mulf_eq0 ?fmorph_eq0 ?signr_eq0 /=.
by rewrite -normalE (
normalP _ _ AnB).
Qed.
Lemma
normal_ortho_mx
p
(
A
: 'M_(
p, n))
: ((
A^_|_)
_|_ A).
Proof.
by []. Qed.
Lemma
normal_mx_ortho
p
(
A
: 'M_(
p, n))
: (
A _|_ (
A^_|_)).
Proof.
Lemma
rank_normal
u
: (
\rank (
u ^_|_)
>= n.
-1)
%N.
Proof.
Definition
rad
:= 1%:M^_|_.
Lemma
rad_ker
: rad = kermx M.
Proof.
Theorem
formDd
u
v
: u _|_ v -> '[u + v] = '[u] + '[v].
Proof.
Lemma
formZ
a
u
: '[a *: u]= (
a * theta a)
* '[u].
Proof.
Lemma
formN
u
: '[- u] = '[u].
Proof.
Lemma
form_sign
m
u
: '[(
-1)
^+ m *: u] = '[u].
Proof.
Lemma
formD
u
v
: let
d
:= '[u, v] in
'[u + v] = '[u] + '[v] + (
d + (
-1)
^+ eps * theta d).
Proof.
Lemma
formB
u
v
: let
d
:= '[u, v] in
'[u - v] = '[u] + '[v] - (
d + (
-1)
^+ eps * theta d).
Proof.
Lemma
formBd
u
v
: u _|_ v -> '[u - v] = '[u] + '[v].
Proof.
End Sesquilinear.
Notation
"eps_theta .-sesqui"
:= (
sesqui _ eps_theta)
: ring_scope.
Notation
symmetric_form
:= (
false, [rmorphism of idfun]).
-sesqui.
Notation
skew
:= (
true, [rmorphism of idfun]).
-sesqui.
Notation
hermitian
:= (
false, @conjC _).
-sesqui.