:: Dual Lattice of $\mathbb Z$-module Lattice
:: by Yuichi Futa and Yasunari Shidama
::
:: Received June 27, 2017
:: Copyright (c) 2017-2021 Association of Mizar Users
:: (Stowarzyszenie Uzytkownikow Mizara, Bialystok, Poland).
:: This code can be distributed under the GNU General Public Licence
:: version 3.0 or later, or the Creative Commons Attribution-ShareAlike
:: License version 3.0 or later, subject to the binding interpretation
:: detailed in file COPYING.interpretation.
:: See COPYING.GPL and COPYING.CC-BY-SA for the full text of these
:: licenses, or see http://www.gnu.org/licenses/gpl.html and
:: http://creativecommons.org/licenses/by-sa/3.0/.
environ
vocabularies GAUSSINT, NUMBERS, FINSEQ_1, SUBSET_1, RLVECT_1, STRUCT_0,
FUNCT_1, XBOOLE_0, ALGSTR_0, RELAT_1, PARTFUN1, ARYTM_3, CARD_3,
ORDINAL4, PRELAMB, XXREAL_0, TARSKI, CARD_1, SUPINF_2, ARYTM_1, NAT_1,
FINSET_1, FUNCOP_1, RLSUB_1, BINOP_1, ZFMISC_1, INT_1, RLVECT_2,
ZMODUL03, FINSEQ_4, RLVECT_3, RMOD_2, RANKNULL, UPROOTS, GROUP_1, INT_3,
VECTSP_1, MESFUNC1, REALSET1, MATRLIN, RLVECT_5, NORMSP_1, BHSP_1,
RVSUM_1, MATRIX_1, MATRIX_3, ZMATRLIN, ZMODLAT1, TREES_1, MFOLD_2,
FVSUM_1, INCSP_1, ZMODUL04, ZMODUL08, FUNCT_2, ZMODLAT2, VECTSP10,
MATRIX_6, LAPLACE, ZMODLAT3;
notations TARSKI, XBOOLE_0, ZFMISC_1, SUBSET_1, RELAT_1, FUNCT_1, ORDINAL1,
RELSET_1, PARTFUN1, MCART_1, FUNCT_2, BINOP_1, DOMAIN_1, FUNCOP_1,
REALSET1, FINSET_1, CARD_1, NUMBERS, XCMPLX_0, XXREAL_0, XREAL_0, INT_1,
FINSEQ_1, MATRIX_0, STRUCT_0, ALGSTR_0, RLVECT_1, GROUP_1, VECTSP_1,
VECTSP_4, VECTSP_6, VECTSP_7, MATRIX_1, FVSUM_1, MATRIX_3, INT_3,
ZMODUL01, ZMODUL03, GAUSSINT, ZMODUL04, ZMATRLIN, ZMODLAT1, ZMODUL08,
MATRIX_6, LAPLACE, MATRIX13, FINSEQ_4, ZMODLAT2;
constructors BINOP_2, UPROOTS, RELSET_1, REALSET1, ORDERS_1, VECTSP_9,
ZMODUL02, ZMODUL01, EUCLID, FVSUM_1, EC_PF_1, ZMODUL04, ZMODUL07,
ZMODUL05, MATRIX_6, LAPLACE, MATRIX13, FINSEQ_4, ZMODLAT2;
registrations SUBSET_1, FUNCT_1, RELSET_1, FUNCT_2, FINSET_1, NUMBERS,
XREAL_0, STRUCT_0, VALUED_0, MEMBERED, FINSEQ_1, CARD_1, INT_1, XBOOLE_0,
BINOP_2, ORDINAL1, XXREAL_0, NAT_1, INT_3, REALSET1, RELAT_1, VECTSP_1,
GAUSSINT, RAT_1, XCMPLX_0, ZMODUL03, ZMODUL04, ZMODUL06, ZMODLAT1,
ZMODUL08, FINSEQ_2, ZMODLAT2;
requirements REAL, NUMERALS, BOOLE, SUBSET, ARITHM;
begin :: 1. Summation of inner products
theorem :: ZMODLAT3:1
for L being RATional Z_Lattice, LX being Z_Lattice
st LX is Submodule of DivisibleMod(L) &
the scalar of LX = (ScProductDM(L)) || the carrier of LX
holds LX is RATional;
registration
let L be RATional Z_Lattice;
cluster EMLat(L) -> RATional;
end;
registration
let L be RATional Z_Lattice;
let r be Element of F_Rat;
cluster EMLat(r, L) -> RATional;
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
:: 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 ;>;
end;
theorem :: ZMODLAT3:2
for L being Z_Lattice, f being Function of L, INT.Ring,
F being FinSequence of L,
v, u being Vector of L, i being Nat
st i in dom F & u = F.i
holds (ScFS(v, f, F)).i = <; v, f.u * u ;>;
theorem :: ZMODLAT3:3
for L being Z_Lattice, f being Function of L, INT.Ring,
v, u being Vector of L holds
ScFS(v, f, <* u *>) = <* <; v, f.u * u ;> *>;
theorem :: ZMODLAT3:4
for L being Z_Lattice, f being Function of L, INT.Ring,
F, G being FinSequence of L,
v being Vector of L holds
ScFS(v, f, F ^ G) = ScFS(v, f, F) ^ ScFS(v, f, G);
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
:: 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));
end;
theorem :: ZMODLAT3:5
for L being Z_Lattice, v being Vector of L holds
SumSc(v, ZeroLC(L)) = 0.F_Real;
theorem :: ZMODLAT3:6
for L being Z_Lattice, v being Vector of L,
l being Linear_Combination of {}(the carrier of L)
holds SumSc(v, l) = 0.F_Real;
theorem :: ZMODLAT3:7
for L being Z_Lattice, v being Vector of L,
l being Linear_Combination of L
st Carrier l = {}
holds SumSc(v, l) = 0.F_Real;
theorem :: ZMODLAT3:8
for L being Z_Lattice, v, u being Vector of L,
l being Linear_Combination of {u}
holds SumSc(v, l) = <; v, l.u * u ;>;
theorem :: ZMODLAT3:9
for L being Z_Lattice, v being Vector of L,
l1, l2 being Linear_Combination of L
holds SumSc(v, l1+l2) = SumSc(v, l1) + SumSc(v, l2);
theorem :: ZMODLAT3:10
for L being Z_Lattice, l being Linear_Combination of L,
v being Vector of L holds
<; v, Sum(l) ;> = SumSc(v, l);
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
:: 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);
end;
theorem :: ZMODLAT3:11
for L being Z_Lattice, f being Function of DivisibleMod(L), INT.Ring,
F being FinSequence of DivisibleMod(L),
v, u being Vector of DivisibleMod(L), i being Nat
st i in dom F & u = F.i
holds (ScFS(v, f, F)).i = (ScProductDM(L)).(v, f.u * u);
theorem :: ZMODLAT3:12
for L being Z_Lattice, f being Function of DivisibleMod(L), INT.Ring,
v, u being Vector of DivisibleMod(L) holds
ScFS(v, f, <* u *>) = <* (ScProductDM(L)).(v, f.u * u) *>;
theorem :: ZMODLAT3:13
for L being Z_Lattice, f being Function of DivisibleMod(L), INT.Ring,
F, G being FinSequence of DivisibleMod(L),
v being Vector of DivisibleMod(L) holds
ScFS(v, f, F ^ G) = ScFS(v, f, F) ^ ScFS(v, f, G);
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
:: 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));
end;
theorem :: ZMODLAT3:14
for L being Z_Lattice, v being Vector of DivisibleMod(L) holds
SumSc(v, ZeroLC(DivisibleMod(L))) = 0.F_Real;
theorem :: ZMODLAT3:15
for L being Z_Lattice, v being Vector of DivisibleMod(L),
l being Linear_Combination of {}(the carrier of DivisibleMod(L))
holds SumSc(v, l) = 0.F_Real;
theorem :: ZMODLAT3:16
for L being Z_Lattice, v being Vector of DivisibleMod(L),
l being Linear_Combination of DivisibleMod(L)
st Carrier l = {}
holds SumSc(v, l) = 0.F_Real;
theorem :: ZMODLAT3:17
for L being Z_Lattice, v, u being Vector of DivisibleMod(L),
l being Linear_Combination of {u}
holds SumSc(v, l) = (ScProductDM(L)).(v, l.u * u);
theorem :: ZMODLAT3:18
for L being Z_Lattice, v being Vector of DivisibleMod(L),
l1, l2 being Linear_Combination of DivisibleMod(L)
holds SumSc(v, l1+l2) = SumSc(v, l1) + SumSc(v, l2);
theorem :: ZMODLAT3:19
for L being Z_Lattice, l being Linear_Combination of DivisibleMod(L),
v being Vector of DivisibleMod(L) holds
(ScProductDM(L)).(v, Sum(l)) = SumSc(v, l);
theorem :: ZMODLAT3:20
for n being Nat, 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 ~;
theorem :: ZMODLAT3:21
for n being Nat, 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;
theorem :: ZMODLAT3:22
for L being non trivial RATional positive-definite Z_Lattice,
b being OrdBasis of L holds
(GramMatrix(b))~ is Matrix of dim(L),F_Rat;
theorem :: 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;
theorem :: ZMODLAT3:24
for L being non trivial RATional positive-definite Z_Lattice,
b being OrdBasis of L holds
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;
theorem :: ZMODLAT3:25
for L being non trivial RATional positive-definite Z_Lattice,
b being OrdBasis of EMLat(L), 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);
begin
definition
let L be Z_Lattice;
mode Dual of L -> Vector of DivisibleMod(L) means
:: ZMODLAT3:def 5
for v being Vector of DivisibleMod(L) st v in EMbedding(L) holds
(ScProductDM(L)).(it, v) in INT.Ring;
end;
theorem :: ZMODLAT3:26
for L being Z_Lattice holds 0.DivisibleMod(L) is Dual of L;
theorem :: ZMODLAT3:27
for L being Z_Lattice, v, u being Dual of L holds
v + u is Dual of L;
theorem :: ZMODLAT3:28
for L being Z_Lattice, v being Dual of L, a being Element of INT.Ring
holds a * v is Dual of L;
definition
let L be Z_Lattice;
func DualSet(L) -> non empty Subset of DivisibleMod(L) equals
:: ZMODLAT3:def 6
the set of all v where v is Dual of L;
end;
registration
let L be Z_Lattice;
cluster DualSet(L) -> linearly-closed;
end;
definition
let L be Z_Lattice;
func DualLatMod(L) -> strict non empty LatticeStr over INT.Ring
means
:: 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):];
end;
theorem :: ZMODLAT3:29
for L being Z_Lattice holds DualLatMod(L) is Submodule of DivisibleMod(L);
theorem :: ZMODLAT3:30
for L being Z_Lattice,
v being Vector of DivisibleMod(L), 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;
definition
let L be RATional positive-definite Z_Lattice;
let I be Basis of EMLat(L);
func DualBasis(I) -> Subset of DivisibleMod(L) means
:: 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);
end;
definition
let L be RATional positive-definite Z_Lattice;
let I be Basis of EMLat(L);
func B2DB(I) -> Function of I, DualBasis(I) means
:: 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);
end;
registration
let L be RATional positive-definite Z_Lattice;
let I be Basis of EMLat(L);
cluster B2DB(I) -> onto one-to-one;
end;
theorem :: ZMODLAT3:31
for L being RATional positive-definite Z_Lattice,
I being Basis of EMLat(L) holds
card I = card DualBasis(I);
registration
let L be RATional positive-definite Z_Lattice;
let I be Basis of EMLat(L);
cluster DualBasis(I) -> finite;
end;
registration
let L be non trivial RATional positive-definite Z_Lattice;
let I be Basis of EMLat(L);
cluster DualBasis(I) -> non empty;
end;
theorem :: ZMODLAT3:32
for L being RATional positive-definite Z_Lattice,
I being Basis of EMLat(L), v being Vector of DivisibleMod(L),
l being Linear_Combination of DualBasis(I) st v in I
holds (ScProductDM(L)).(v, Sum(l)) = l.((B2DB(I)).v);
theorem :: ZMODLAT3:33
for L being RATional positive-definite Z_Lattice,
I being Basis of EMLat(L),
v being Vector of DivisibleMod(L) st v is Dual of L holds
v in Lin DualBasis(I);
registration
let L be RATional positive-definite Z_Lattice;
let I be Basis of EMLat(L);
cluster DualBasis(I) -> linearly-independent;
end;
definition
let L be RATional positive-definite Z_Lattice;
func DualLat(L) -> strict Z_Lattice means
:: 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;
end;
theorem :: ZMODLAT3:34
for L being RATional positive-definite Z_Lattice,
v being Vector of DivisibleMod(L) holds
v in DualLat(L) iff v is Dual of L;
theorem :: ZMODLAT3:35
for L being RATional positive-definite Z_Lattice holds
DualLat(L) is Submodule of DivisibleMod(L);
theorem :: ZMODLAT3:36
for L being Z_Lattice, I being Basis of EMLat(L) holds
I is Basis of EMbedding(L);
theorem :: ZMODLAT3:37
for L being Z_Lattice, I being Basis of EMbedding(L) holds
I is Basis of EMLat(L);
theorem :: ZMODLAT3:38
for L being RATional positive-definite Z_Lattice,
I being Basis of EMLat(L), v being Vector of DivisibleMod(L)
st v in DualBasis(I)
holds v is Dual of L;
theorem :: ZMODLAT3:39
for L being RATional positive-definite Z_Lattice,
I being Basis of EMLat(L) holds
DualBasis(I) is Basis of DualLat(L);
theorem :: ZMODLAT3:40
for L being RATional positive-definite Z_Lattice,
b being OrdBasis of EMLat(L), I being Basis of EMLat(L)
st I = rng b holds
(B2DB(I))*b is OrdBasis of DualLat(L);
theorem :: ZMODLAT3:41
for L be positive-definite finite-rank free Z_Lattice,
b being OrdBasis of L, e being OrdBasis of EMLat(L)
st e = (MorphsZQ(L))*b
holds GramMatrix(InnerProduct(L), b) = GramMatrix(InnerProduct(EMLat(L)), e);
theorem :: ZMODLAT3:42
for L being positive-definite finite-rank free Z_Lattice holds
GramDet(InnerProduct(L)) = GramDet(InnerProduct(EMLat(L)));
theorem :: ZMODLAT3:43
for L being RATional positive-definite Z_Lattice holds
rank(L) = rank(DualLat(L));
theorem :: ZMODLAT3:44
for L being INTegral positive-definite Z_Lattice holds
EMLat(L) is Z_Sublattice of DualLat(L);
theorem :: ZMODLAT3:45
for L being Z_Lattice,
b being OrdBasis of L
st GramMatrix(InnerProduct(L), b) is Matrix of dim(L), INT.Ring
holds L is INTegral;
theorem :: ZMODLAT3:46
for L being Z_Lattice, I being finite Subset of L, u being Vector of L
st for v being Vector of L st v in I holds <; v, u ;> in RAT holds
for v being Vector of L st v in Lin(I) holds <; v, u ;> in RAT;
theorem :: ZMODLAT3:47
for L being Z_Lattice, I being Basis of L
st for v, u being Vector of L st v in I & u in I holds <; v, u ;> in RAT
holds for v, u being Vector of L holds <; v, u ;> in RAT;
theorem :: ZMODLAT3:48
for L being Z_Lattice, I being Basis of L
st for v, u being Vector of L st v in I & u in I holds
<; v, u ;> in RAT
holds L is RATional;
theorem :: ZMODLAT3:49
for L being Z_Lattice,
b being OrdBasis of L
st GramMatrix(InnerProduct(L), b) is Matrix of dim(L), F_Rat
holds L is RATional;
registration
let L be RATional positive-definite Z_Lattice;
cluster DualLat(L) -> RATional;
end;
theorem :: ZMODLAT3:50
for L being RATional Z_Lattice, LX being Z_Lattice,
b being OrdBasis of LX
st LX is Submodule of DivisibleMod(L) &
the scalar of LX = (ScProductDM(L)) || the carrier of LX
holds GramMatrix(InnerProduct(LX), b) is Matrix of dim(LX), F_Rat;
theorem :: ZMODLAT3:51
for L being RATional positive-definite Z_Lattice,
b being OrdBasis of DualLat(L)
holds GramMatrix(InnerProduct(DualLat(L)), b) is Matrix of dim(L), F_Rat;
theorem :: ZMODLAT3:52
for L being positive-definite Z_Lattice,
LX being Z_Lattice
st LX is Submodule of DivisibleMod(L) &
the scalar of LX = (ScProductDM(L)) || the carrier of LX
holds LX is positive-definite;
registration
let L be RATional positive-definite Z_Lattice;
cluster DualLat(L) -> positive-definite;
end;
registration
let L be non trivial RATional positive-definite Z_Lattice;
cluster DualLat(L) -> non trivial;
end;