ZMODLAT3: Dual Lattice of $\mathbb Z$-module Lattice

proof end;

end;

registration

let L be RATional Z_Lattice;
let r be Element of F_Rat;

cluster EMLat (r,L) -> RATional ;

proof end;

end;

definition

let L be Z_Lattice;
let F be FinSequence of L;
let f be Function of L,INT.Ring;
let v be Vector of L;

func ScFS (v,f,F) -> FinSequence of F_Real means :defScFS: :: ZMODLAT3:def 1
( len it = len F & ( for i being Nat st i in dom it holds
it . i = <;v,((f . (F /. i)) * (F /. i));> ) );

proof end;

proof end;

end;

:: deftheorem defScFS defines ScFS ZMODLAT3:def 1 :

theorem ThScFS1: :: ZMODLAT3:2

for L being Z_Lattice
for f being Function of L,INT.Ring
for F being FinSequence of L
for v, u being Vector of L
for i being Nat st i in dom F & u = F . i holds
(ScFS (v,f,F)) . i = <;v,((f . u) * u);>

proof end;

theorem ThScFS3: :: ZMODLAT3:3

for L being Z_Lattice
for f being Function of L,INT.Ring
for v, u being Vector of L holds ScFS (v,f,<*u*>) = <*<;v,((f . u) * u);>*>

proof end;

theorem ThScFS6: :: ZMODLAT3:4

for L being Z_Lattice
for f being Function of L,INT.Ring
for F, G being FinSequence of L
for v being Vector of L holds ScFS (v,f,(F ^ G)) = (ScFS (v,f,F)) ^ (ScFS (v,f,G))

proof end;

definition

let L be Z_Lattice;
let l be Linear_Combination of L;
let v be Vector of L;

func SumSc (v,l) -> Element of F_Real means :defSumSc: :: ZMODLAT3:def 2
ex F being FinSequence of L st
( F is one-to-one & rng F = Carrier l & it = Sum (ScFS (v,l,F)) );

proof end;

proof end;

end;

:: deftheorem defSumSc defines SumSc ZMODLAT3:def 2 :

theorem LmSumSc11: :: ZMODLAT3:5

for L being Z_Lattice
for v being Vector of L holds SumSc (v,(ZeroLC L)) = 0. F_Real

proof end;

theorem :: ZMODLAT3:6

for L being Z_Lattice
for v being Vector of L
for l being Linear_Combination of {} the carrier of L holds SumSc (v,l) = 0. F_Real

proof end;

theorem LmSumSc13: :: ZMODLAT3:7

for L being Z_Lattice
for v being Vector of L
for l being Linear_Combination of L st Carrier l = {} holds
SumSc (v,l) = 0. F_Real

proof end;

theorem LmSumSc14: :: ZMODLAT3:8

for L being Z_Lattice
for v, u being Vector of L
for l being Linear_Combination of {u} holds SumSc (v,l) = <;v,((l . u) * u);>

proof end;

theorem LmSumSc1X: :: ZMODLAT3:9

for L being Z_Lattice
for v being Vector of L
for l1, l2 being Linear_Combination of L holds SumSc (v,(l1 + l2)) = (SumSc (v,l1)) + (SumSc (v,l2))

proof end;

theorem ThSumSc1: :: ZMODLAT3:10

for L being Z_Lattice
for l being Linear_Combination of L
for v being Vector of L holds <;v,(Sum l);> = SumSc (v,l)

proof end;

definition

let L be Z_Lattice;
let F be FinSequence of (DivisibleMod L);
let f be Function of (DivisibleMod L),INT.Ring;
let v be Vector of (DivisibleMod L);

func ScFS (v,f,F) -> FinSequence of F_Real means :defScFSDM: :: ZMODLAT3:def 3
( len it = len F & ( for i being Nat st i in dom it holds
it . i = (ScProductDM L) . (v,((f . (F /. i)) * (F /. i))) ) );

proof end;

proof end;

end;

:: deftheorem defScFSDM defines ScFS ZMODLAT3:def 3 :

theorem ThScFSDM1: :: ZMODLAT3:11

for L being Z_Lattice
for f being Function of (DivisibleMod L),INT.Ring
for F being FinSequence of (DivisibleMod L)
for v, u being Vector of (DivisibleMod L)
for i being Nat st i in dom F & u = F . i holds
(ScFS (v,f,F)) . i = (ScProductDM L) . (v,((f . u) * u))

proof end;

theorem ThScFSDM3: :: ZMODLAT3:12

for L being Z_Lattice
for f being Function of (DivisibleMod L),INT.Ring
for v, u being Vector of (DivisibleMod L) holds ScFS (v,f,<*u*>) = <*((ScProductDM L) . (v,((f . u) * u)))*>

proof end;

theorem ThScFSDM6: :: ZMODLAT3:13

for L being Z_Lattice
for f being Function of (DivisibleMod L),INT.Ring
for F, G being FinSequence of (DivisibleMod L)
for v being Vector of (DivisibleMod L) holds ScFS (v,f,(F ^ G)) = (ScFS (v,f,F)) ^ (ScFS (v,f,G))

proof end;

definition

let L be Z_Lattice;
let l be Linear_Combination of DivisibleMod L;
let v be Vector of (DivisibleMod L);

func SumSc (v,l) -> Element of F_Real means :defSumScDM: :: ZMODLAT3:def 4
ex F being FinSequence of (DivisibleMod L) st
( F is one-to-one & rng F = Carrier l & it = Sum (ScFS (v,l,F)) );

proof end;

proof end;

end;

:: deftheorem defSumScDM defines SumSc ZMODLAT3:def 4 :

theorem LmSumScDM11: :: ZMODLAT3:14

for L being Z_Lattice
for v being Vector of (DivisibleMod L) holds SumSc (v,(ZeroLC (DivisibleMod L))) = 0. F_Real

proof end;

theorem :: ZMODLAT3:15

for L being Z_Lattice
for v being Vector of (DivisibleMod L)
for l being Linear_Combination of {} the carrier of (DivisibleMod L) holds SumSc (v,l) = 0. F_Real

proof end;

theorem LmSumScDM13: :: ZMODLAT3:16

for L being Z_Lattice
for v being Vector of (DivisibleMod L)
for l being Linear_Combination of DivisibleMod L st Carrier l = {} holds
SumSc (v,l) = 0. F_Real

proof end;

theorem LmSumScDM14: :: ZMODLAT3:17

for L being Z_Lattice
for v, u being Vector of (DivisibleMod L)
for l being Linear_Combination of {u} holds SumSc (v,l) = (ScProductDM L) . (v,((l . u) * u))

proof end;

theorem LmSumScDM1X: :: ZMODLAT3:18

for L being Z_Lattice
for v being Vector of (DivisibleMod L)
for l1, l2 being Linear_Combination of DivisibleMod L holds SumSc (v,(l1 + l2)) = (SumSc (v,l1)) + (SumSc (v,l2))

proof end;

theorem ThSumScDM1: :: ZMODLAT3:19

for L being Z_Lattice
for l being Linear_Combination of DivisibleMod L
for v being Vector of (DivisibleMod L) holds (ScProductDM L) . (v,(Sum l)) = SumSc (v,l)

proof end;

theorem INVMN1: :: ZMODLAT3:20

for n being Nat
for M being Matrix of n,F_Real
for H being Matrix of n,F_Rat st M = H & M is invertible holds
( H is invertible & M ~ = H ~ )

proof end;

theorem INVMN2: :: ZMODLAT3:21

for n being Nat
for M being Matrix of n,F_Real st M is Matrix of n,F_Rat & M is invertible holds
M ~ is Matrix of n,F_Rat

proof end;

theorem ThGM3: :: ZMODLAT3:22

for L being non trivial positive-definite RATional Z_Lattice
for b being OrdBasis of L holds (GramMatrix b) ~ is Matrix of dim L,F_Rat

proof end;

theorem LmDE311A: :: ZMODLAT3:23

for X being finite Subset of RAT ex a being Element of INT st
( a <> 0 & ( for r being Element of RAT st r in X holds
a * r in INT ) )

proof end;

theorem LmDE311: :: ZMODLAT3:24

for L being non trivial positive-definite RATional Z_Lattice
for b being OrdBasis of L ex a being Element of F_Real st
( a is Element of INT.Ring & a <> 0 & a * ((GramMatrix b) ~) is Matrix of dim L,INT.Ring )

proof end;

LM0: for n being Nat
for F being FinSequence of F_Real st F = (Seg n) --> (0. F_Real) holds
Sum F = 0. F_Real

proof end;

LM1: for L being Z_Lattice
for F, F0 being FinSequence of L
for l being Linear_Combination of L
for v being Vector of L st F is one-to-one & F0 is one-to-one & Carrier l c= rng F & canFS (Carrier l) = F0 holds
Sum (ScFS (v,l,F)) = Sum (ScFS (v,l,F0))

proof end;

theorem LmDE31: :: ZMODLAT3:25

for L being non trivial positive-definite RATional Z_Lattice
for b being OrdBasis of EMLat L
for i being Nat st i in dom b holds
ex v being Vector of (DivisibleMod L) st
( (ScProductDM L) . ((b /. i),v) = 1 & ( for j being Nat st i <> j & j in dom b holds
(ScProductDM L) . ((b /. j),v) = 0 ) )

proof end;

LmDE00: for L being Z_Lattice
for v being Vector of (DivisibleMod L) holds (ScProductDM L) . ((0. (DivisibleMod L)),v) in INT.Ring

proof end;

definition

let L be Z_Lattice;

mode Dual of L -> Vector of (DivisibleMod L) means :defDualElement: :: ZMODLAT3:def 5
for v being Vector of (DivisibleMod L) st v in EMbedding L holds
(ScProductDM L) . (it,v) in INT.Ring ;

proof end;

end;

:: deftheorem defDualElement defines Dual ZMODLAT3:def 5 :

theorem LmDE0: :: ZMODLAT3:26

for L being Z_Lattice holds 0. (DivisibleMod L) is Dual of L

proof end;

theorem LmDE1: :: ZMODLAT3:27

for L being Z_Lattice
for v, u being Dual of L holds v + u is Dual of L

proof end;

theorem LmDE2: :: ZMODLAT3:28

for L being Z_Lattice
for v being Dual of L
for a being Element of INT.Ring holds a * v is Dual of L

proof end;

definition

let L be Z_Lattice;

func DualSet L -> non empty Subset of (DivisibleMod L) equals :: ZMODLAT3:def 6
{ v where v is Dual of L : verum } ;

proof end;

end;

:: deftheorem defines DualSet ZMODLAT3:def 6 :

registration

let L be Z_Lattice;

cluster DualSet L -> non empty linearly-closed ;

coherence

proof end;

end;

definition

let L be Z_Lattice;

func DualLatMod L -> non empty strict LatticeStr over INT.Ring means :defDualMod: :: ZMODLAT3:def 7
( the carrier of it = DualSet L & the addF of it = the addF of (DivisibleMod L) || (DualSet L) & the ZeroF of it = 0. (DivisibleMod L) & the lmult of it = the lmult of (DivisibleMod L) | [: the carrier of INT.Ring,(DualSet L):] & the scalar of it = (ScProductDM L) | [:(DualSet L),(DualSet L):] );

proof end;

uniqueness ;

end;

:: deftheorem defDualMod defines DualLatMod ZMODLAT3:def 7 :

theorem :: ZMODLAT3:29

for L being Z_Lattice holds DualLatMod L is Submodule of DivisibleMod L

proof end;

theorem LmDE21: :: ZMODLAT3:30

for L being Z_Lattice
for v being Vector of (DivisibleMod L)
for I being Basis of (EMbedding L) st ( for u being Vector of (DivisibleMod L) st u in I holds
(ScProductDM L) . (v,u) in INT.Ring ) holds
v is Dual of L

proof end;

definition

let L be positive-definite RATional Z_Lattice;
let I be Basis of (EMLat L);

func DualBasis I -> Subset of (DivisibleMod L) means :defDualBasis: :: ZMODLAT3:def 8
for v being Vector of (DivisibleMod L) holds
( v in it iff ex u being Vector of (EMLat L) st
( u in I & (ScProductDM L) . (u,v) = 1 & ( for w being Vector of (EMLat L) st w in I & u <> w holds
(ScProductDM L) . (w,v) = 0 ) ) );

proof end;

proof end;

end;

:: deftheorem defDualBasis defines DualBasis ZMODLAT3:def 8 :

definition

let L be positive-definite RATional Z_Lattice;
let I be Basis of (EMLat L);

func B2DB I -> Function of I,(DualBasis I) means :defB2DB: :: ZMODLAT3:def 9
( dom it = I & rng it = DualBasis I & ( for v being Vector of (EMLat L) st v in I holds
( (ScProductDM L) . (v,(it . v)) = 1 & ( for w being Vector of (EMLat L) st w in I & v <> w holds
(ScProductDM L) . (w,(it . v)) = 0 ) ) ) );

proof end;

proof end;

end;

:: deftheorem defB2DB defines B2DB ZMODLAT3:def 9 :

registration

let L be positive-definite RATional Z_Lattice;
let I be Basis of (EMLat L);

cluster B2DB I -> one-to-one onto ;

proof end;

end;

theorem ThDB1: :: ZMODLAT3:31

for L being positive-definite RATional Z_Lattice
for I being Basis of (EMLat L) holds card I = card (DualBasis I)

proof end;

registration

let L be positive-definite RATional Z_Lattice;
let I be Basis of (EMLat L);

cluster DualBasis I -> finite ;

proof end;

end;

registration

let L be non trivial positive-definite RATional Z_Lattice;
let I be Basis of (EMLat L);

cluster DualBasis I -> non empty ;

proof end;

end;

theorem LmDE32: :: ZMODLAT3:32

for L being positive-definite RATional Z_Lattice
for I being Basis of (EMLat L)
for v being Vector of (DivisibleMod L)
for l being Linear_Combination of DualBasis I st v in I holds
(ScProductDM L) . (v,(Sum l)) = l . ((B2DB I) . v)

proof end;

theorem ThDE3: :: ZMODLAT3:33

for L being positive-definite RATional Z_Lattice
for I being Basis of (EMLat L)
for v being Vector of (DivisibleMod L) st v is Dual of L holds
v in Lin (DualBasis I)

proof end;

registration

let L be positive-definite RATional Z_Lattice;
let I be Basis of (EMLat L);

cluster DualBasis I -> linearly-independent ;

proof end;

end;

definition

let L be positive-definite RATional Z_Lattice;

func DualLat L -> strict Z_Lattice means :defDualLat: :: ZMODLAT3:def 10
( the carrier of it = DualSet L & 0. it = 0. (DivisibleMod L) & the addF of it = the addF of (DivisibleMod L) || the carrier of it & the lmult of it = the lmult of (DivisibleMod L) | [: the carrier of INT.Ring, the carrier of it:] & the scalar of it = (ScProductDM L) || the carrier of it );