:: Lattice of $\mathbb Z$-module :: by Yuichi Futa and Yasunari Shidama :: :: Received December 30, 2015 :: Copyright (c) 2015-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, RAT_1, XBOOLE_0, ALGSTR_0, RELAT_1, PARTFUN1, ARYTM_3, CARD_3, ORDINAL4, PRELAMB, XXREAL_0, TARSKI, CARD_1, SUPINF_2, MSSUBFAM, ARYTM_1, NAT_1, FINSET_1, FUNCOP_1, RLSUB_1, QC_LANG1, BINOP_1, ZFMISC_1, INT_1, ZMODUL01, ZMODUL03, FINSEQ_4, RLVECT_3, RMOD_2, RANKNULL, UNIALG_1, FUNCT_7, GROUP_1, INT_3, COMPLEX1, VECTSP_1, MESFUNC1, XCMPLX_0, REALSET1, MATRLIN, ZMODUL02, RLVECT_5, ZMODUL06, NORMSP_1, BHSP_1, ABIAN, RVSUM_1, MATRIX_1, MATRIX_3, MOD_3, ZMATRLIN, FUNCT_5, ZMODLAT1, TREES_1, MFOLD_2, BILINEAR, HAHNBAN, FVSUM_1, INCSP_1; notations TARSKI, XBOOLE_0, ZFMISC_1, SUBSET_1, RELAT_1, FUNCT_1, ORDINAL1, RELSET_1, PARTFUN1, FUNCT_2, BINOP_1, DOMAIN_1, FUNCOP_1, REALSET1, FINSET_1, CARD_1, FUNCT_5, XCMPLX_0, XXREAL_0, INT_1, RAT_1, COMPLEX1, FINSEQ_1, ABIAN, MATRIX_0, STRUCT_0, ALGSTR_0, RLVECT_1, GROUP_1, VECTSP_1, VECTSP_4, VECTSP_7, MATRIX_1, FVSUM_1, MATRIX_3, HAHNBAN1, INT_3, BILINEAR, ZMODUL01, ZMODUL03, GAUSSINT, ZMODUL04, ZMODUL06, ZMATRLIN; constructors BINOP_2, UPROOTS, ZMODUL01, REALSET1, EUCLID, FVSUM_1, FUNCT_3, ALGSTR_1, EC_PF_1, MATRIX_3, ZMODUL04, ZMODUL06, ABIAN, ZMATRLIN, ZMODUL07, RELSET_1; registrations SUBSET_1, FUNCT_1, RELSET_1, FUNCT_2, FINSET_1, NUMBERS, XREAL_0, STRUCT_0, RLVECT_1, VALUED_0, MEMBERED, FINSEQ_1, CARD_1, INT_1, ZMODUL01, XBOOLE_0, BINOP_2, ORDINAL1, XXREAL_0, NAT_1, ALGSTR_0, INT_3, REALSET1, RELAT_1, VECTSP_1, VECTSP_2, FUNCT_3, XCMPLX_0, ZMODUL03, ZMODUL04, ZMODUL05, ZMODUL06, ABIAN, MATRIX_0, ZMATRLIN; requirements REAL, NUMERALS, BOOLE, SUBSET, ARITHM; begin :: 1. Definition of lattices of $\mathbb Z$-module theorem :: ZMODLAT1:1 for D, E being non empty set, n, m being Nat, M being Matrix of n,m,D st for i, j being Nat st [i, j] in Indices M holds M*(i,j) in E holds M is Matrix of n,m,E; definition let F be 1-sorted; struct (ModuleStr over F) LatticeStr over F (# carrier -> set, addF -> BinOp of the carrier, ZeroF -> Element of the carrier, lmult -> Function of [: the carrier of F, the carrier :], the carrier, scalar -> Function of [: the carrier, the carrier :], the carrier of F_Real #); end; registration let F be 1-sorted; cluster strict non empty for LatticeStr over F; end; registration let F be 1-sorted; let D be non empty set, Z be Element of D, a be BinOp of D,m be Function of [:the carrier of F, D:], D, s be Function of [: D,D:],the carrier of F_Real; cluster LatticeStr(#D,a,Z,m,s#) -> non empty; end; definition let X be non empty LatticeStr over INT.Ring; let x, y be Vector of X; func <; x, y ;> -> Element of F_Real equals :: ZMODLAT1:def 1 (the scalar of X).[x, y]; end; definition let X be non empty LatticeStr over INT.Ring; let x be Vector of X; func ||. x .|| -> Element of F_Real equals :: ZMODLAT1:def 2 <; x, x ;>; end; definition let IT be non empty LatticeStr over INT.Ring; attr IT is Z_Lattice-like means :: ZMODLAT1:def 3 (for x being Vector of IT st for y being Vector of IT holds <; x, y ;> = 0 holds x = 0.IT) & (for x, y being Vector of IT holds <; x, y ;> = <; y, x ;>) & (for x, y, z being Vector of IT, a being Element of INT.Ring holds <; x+y, z ;> = <; x, z ;> + <; y, z ;> & <; a*x, y ;> = a * <; x, y ;>); end; definition let V be Z_Module, sc be Function of [: the carrier of V, the carrier of V :], the carrier of F_Real; func GenLat (V, sc) -> non empty LatticeStr over INT.Ring equals :: ZMODLAT1:def 4 LatticeStr (# the carrier of V, the addF of V, 0.V, the lmult of V, sc #); end; registration cluster vector-distributive scalar-distributive scalar-associative scalar-unital Abelian add-associative right_zeroed right_complementable strict for non empty LatticeStr over INT.Ring; end; registration let V be Z_Module; let sc be Function of [: the carrier of V, the carrier of V :], the carrier of F_Real; cluster GenLat (V, sc) -> Abelian add-associative right_zeroed right_complementable scalar-distributive vector-distributive scalar-associative scalar-unital; end; theorem :: ZMODLAT1:2 for V being Z_Module, sc being Function of [: the carrier of V, the carrier of V :], the carrier of F_Real holds GenLat (V,sc) is Submodule of V; theorem :: ZMODLAT1:3 for V being Z_Module, sc being Function of [: the carrier of V, the carrier of V :], the carrier of F_Real holds V is Submodule of GenLat (V,sc); registration cluster free for Abelian add-associative right_zeroed right_complementable scalar-distributive vector-distributive scalar-associative scalar-unital non empty LatticeStr over INT.Ring; end; registration let V be free Z_Module; let sc be Function of [: the carrier of V, the carrier of V :], the carrier of F_Real; cluster GenLat (V,sc) -> free; end; registration cluster torsion-free for Abelian add-associative right_zeroed right_complementable scalar-distributive vector-distributive scalar-associative scalar-unital non empty LatticeStr over INT.Ring; end; theorem :: ZMODLAT1:4 for V being finite-rank free Z_Module, sc being Function of [: the carrier of V, the carrier of V :], the carrier of F_Real holds GenLat (V,sc) is finite-rank; registration cluster finite-rank for free Abelian add-associative right_zeroed right_complementable scalar-distributive vector-distributive scalar-associative scalar-unital non empty LatticeStr over INT.Ring; end; registration let V be finite-rank free Z_Module; let sc be Function of [: the carrier of V, the carrier of V :], the carrier of F_Real; cluster GenLat (V,sc) -> finite-rank; end; theorem :: ZMODLAT1:5 for V being finite-rank free Z_Module, f being Function of [:the carrier of (0).V, the carrier of (0).V:], the carrier of F_Real st f = [:the carrier of (0).V, the carrier of (0).V:] --> 0.F_Real holds GenLat ((0).V,f) is Z_Lattice-like; registration cluster Z_Lattice-like for non empty LatticeStr over INT.Ring; end; registration cluster Z_Lattice-like for finite-rank free Abelian add-associative right_zeroed right_complementable scalar-distributive vector-distributive scalar-associative scalar-unital non empty LatticeStr over INT.Ring; end; registration cluster strict for finite-rank free Z_Lattice-like Abelian add-associative right_zeroed right_complementable scalar-distributive vector-distributive scalar-associative scalar-unital non empty LatticeStr over INT.Ring; end; definition mode Z_Lattice is finite-rank free Z_Lattice-like Abelian add-associative right_zeroed right_complementable scalar-distributive vector-distributive scalar-associative scalar-unital non empty LatticeStr over INT.Ring; end; theorem :: ZMODLAT1:6 for V being non trivial torsion-free Z_Module, Z being Submodule of V, v being non zero Vector of V, f being Function of [:the carrier of Z, the carrier of Z:], the carrier of F_Real st Z = Lin{v} & (for v1, v2 being Vector of Z, a, b being Element of INT.Ring st v1 = a*v & v2 = b*v holds f.(v1, v2) = a*b) holds GenLat (Z,f) is Z_Lattice-like; registration cluster non trivial for Z_Lattice; end; registration let V be torsion-free Z_Module; cluster Z_MQ_VectSp(V) -> scalar-distributive vector-distributive scalar-associative scalar-unital add-associative right_zeroed right_complementable Abelian for non empty ModuleStr over F_Rat; end; theorem :: ZMODLAT1:7 for L being Z_Lattice, v, u being Vector of L holds <; v, -u ;> = - <; v, u ;> & <; -v, u ;> = - <; v, u ;>; theorem :: ZMODLAT1:8 for L being Z_Lattice, v, u, w being Vector of L holds <; v, u + w ;> = <; v, u ;> + <; v, w ;>; theorem :: ZMODLAT1:9 for L being Z_Lattice, v, u being Vector of L, a being Element of INT.Ring holds <; v, a*u ;> = a * <; v, u ;>; theorem :: ZMODLAT1:10 for L being Z_Lattice, v, u, w being Vector of L, a, b being Element of INT.Ring holds <; a*v + b*u, w ;> = a * <; v, w ;> + b * <; u, w ;> & <; v, a*u + b*w ;> = a * <; v, u ;> + b * <; v, w ;>; theorem :: ZMODLAT1:11 for L being Z_Lattice, v, u, w being Vector of L holds <; v-u, w ;> = <; v, w ;> - <; u, w ;> & <; v, u-w ;> = <; v, u ;> - <; v, w ;>; theorem :: ZMODLAT1:12 for L being Z_Lattice, v being Vector of L holds <; v, 0.L ;> = 0 & <; 0.L, v ;> = 0; :: Integral Lattice definition let IT be Z_Lattice; attr IT is INTegral means :: ZMODLAT1:def 5 for v, u being Vector of IT holds <; v, u ;> in INT; end; registration cluster INTegral for Z_Lattice; end; registration let L be INTegral Z_Lattice; let v, u be Vector of L; cluster <; v, u ;> -> integer; end; registration let L be INTegral Z_Lattice; let v be Vector of L; cluster ||. v .|| -> integer; end; theorem :: ZMODLAT1:13 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 INT holds for v being Vector of L st v in Lin(I) holds <; v, u ;> in INT; theorem :: ZMODLAT1:14 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 INT holds for v, u being Vector of L holds <; v, u ;> in INT; theorem :: ZMODLAT1:15 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 INT holds L is INTegral; definition let IT be Z_Lattice; attr IT is positive-definite means :: ZMODLAT1:def 6 for v being Vector of IT st v <> 0.IT holds ||. v .|| > 0; end; registration cluster non trivial INTegral positive-definite for Z_Lattice; end; theorem :: ZMODLAT1:16 for L being positive-definite Z_Lattice, v being Vector of L holds ||. v .|| = 0 iff v = 0.L; theorem :: ZMODLAT1:17 for L being positive-definite Z_Lattice, v being Vector of L holds ||. v .|| >= 0; definition let IT be INTegral Z_Lattice; attr IT is even means :: ZMODLAT1:def 7 for v being Vector of IT holds ||. v .|| is even; end; registration cluster even for INTegral Z_Lattice; end; notation let L be Z_Lattice; synonym dim(L) for rank(L); end; definition let L be Z_Lattice; let v, u be Vector of L; pred v, u are_orthogonal means :: ZMODLAT1:def 8 <; v, u ;> = 0; symmetry; end; theorem :: ZMODLAT1:18 for L being Z_Lattice, v, u being Vector of L holds v, u are_orthogonal implies v, -u are_orthogonal & -v, u are_orthogonal & -v, -u are_orthogonal; theorem :: ZMODLAT1:19 for L being Z_Lattice, v, u being Vector of L holds v, u are_orthogonal implies ||. v + u .|| = ||. v .|| + ||. u .||; theorem :: ZMODLAT1:20 for L being Z_Lattice, v, u being Vector of L holds v, u are_orthogonal implies ||. v - u .|| = ||. v .|| + ||. u .||; :: Sublattice definition let L be Z_Lattice; mode Z_Sublattice of L -> Z_Lattice means :: ZMODLAT1:def 9 the carrier of it c= the carrier of L & 0.it = 0.L & the addF of it = (the addF of L) || the carrier of it & the lmult of it = (the lmult of L) | [:the carrier of INT.Ring, the carrier of it:] & the scalar of it = (the scalar of L) || the carrier of it; end; theorem :: ZMODLAT1:21 for L being Z_Lattice, L1 being Z_Sublattice of L holds L1 is Submodule of L; theorem :: ZMODLAT1:22 for x being object, L being Z_Lattice, L1, L2 being Z_Sublattice of L holds x in L1 & L1 is Z_Sublattice of L2 implies x in L2; theorem :: ZMODLAT1:23 for x being object, L being Z_Lattice, L1 being Z_Sublattice of L holds x in L1 implies x in L; theorem :: ZMODLAT1:24 for L being Z_Lattice, L1 being Z_Sublattice of L, w being Vector of L1 holds w is Vector of L; theorem :: ZMODLAT1:25 for L being Z_Lattice, L1, L2 being Z_Sublattice of L holds 0.L1 = 0.L2; theorem :: ZMODLAT1:26 for L being Z_Lattice, L1 being Z_Sublattice of L, v1, v2 being Vector of L, w1, w2 being Vector of L1 holds w1 = v1 & w2 = v2 implies w1 + w2 = v1 + v2; theorem :: ZMODLAT1:27 for L being Z_Lattice, L1 being Z_Sublattice of L, v being Vector of L, w being Vector of L1, a being Element of INT.Ring holds w = v implies a * w = a * v; theorem :: ZMODLAT1:28 for L being Z_Lattice, L1 being Z_Sublattice of L, v being Vector of L, w being Vector of L1 holds w = v implies -w = -v; theorem :: ZMODLAT1:29 for L being Z_Lattice, L1 being Z_Sublattice of L, v1, v2 being Vector of L, w1, w2 being Vector of L1 holds w1 = v1 & w2 = v2 implies w1 - w2 = v1 - v2; theorem :: ZMODLAT1:30 for L being Z_Lattice, L1 being Z_Sublattice of L holds 0.L in L1; theorem :: ZMODLAT1:31 for L being Z_Lattice, L1, L2 being Z_Sublattice of L holds 0.L1 in L2; theorem :: ZMODLAT1:32 for L being Z_Lattice, L1 being Z_Sublattice of L holds 0.L1 in L; theorem :: ZMODLAT1:33 for L being Z_Lattice, L1 being Z_Sublattice of L, v1, v2 being Vector of L holds v1 in L1 & v2 in L1 implies v1 + v2 in L1; theorem :: ZMODLAT1:34 for L being Z_Lattice, L1 being Z_Sublattice of L, v being Vector of L, a being Element of INT.Ring holds v in L1 implies a * v in L1; theorem :: ZMODLAT1:35 for L being Z_Lattice, L1 being Z_Sublattice of L, v being Vector of L holds v in L1 implies -v in L1; theorem :: ZMODLAT1:36 for L being Z_Lattice, L1 being Z_Sublattice of L, v1, v2 being Vector of L holds v1 in L1 & v2 in L1 implies v1 - v2 in L1; theorem :: ZMODLAT1:37 for L being positive-definite Z_Lattice, A being non empty set, ze being Element of A, ad being BinOp of A, mu being Function of [:the carrier of INT.Ring, A:],A, sc being Function of [:A, A:],the carrier of F_Real st A is linearly-closed Subset of L & ze = 0.L & ad = (the addF of L) || A & mu = (the lmult of L) | [:the carrier of INT.Ring, A:] & sc = (the scalar of L) || A holds LatticeStr (# A, ad, ze, mu, sc #) is Z_Sublattice of L; theorem :: ZMODLAT1:38 for L being Z_Lattice, L1 being Z_Sublattice of L, w1, w2 being Vector of L1, v1, v2 being Vector of L st w1 = v1 & w2 = v2 holds <; w1, w2 ;> = <; v1, v2 ;>; registration let L be INTegral Z_Lattice; cluster -> INTegral for Z_Sublattice of L; end; registration let L be positive-definite Z_Lattice; cluster -> positive-definite for Z_Sublattice of L; end; definition let V,W be ModuleStr over INT.Ring; mode FrForm of V,W is Function of [:the carrier of V,the carrier of W:], the carrier of F_Real; end; definition let V, W be ModuleStr over INT.Ring; func NulFrForm(V,W) -> FrForm of V,W equals :: ZMODLAT1:def 10 [:the carrier of V,the carrier of W:] --> 0.F_Real; end; definition let V, W be non empty ModuleStr over INT.Ring; let f, g be FrForm of V,W; func f+g -> FrForm of V,W means :: ZMODLAT1:def 11 for v being Vector of V, w being Vector of W holds it.(v,w) = f.(v,w)+g.(v,w); end; definition let V, W be non empty ModuleStr over INT.Ring; let f be FrForm of V,W; let a be Element of F_Real; func a*f -> FrForm of V,W means :: ZMODLAT1:def 12 for v being Vector of V, w being Vector of W holds it.(v,w) = a*f.(v,w); end; definition let V, W be non empty ModuleStr over INT.Ring; let f be FrForm of V,W; func -f -> FrForm of V,W means :: ZMODLAT1:def 13 for v being Vector of V, w being Vector of W holds it.(v,w) = -f.(v,w); end; definition let V, W be non empty ModuleStr over INT.Ring; let f be FrForm of V,W; redefine func -f equals :: ZMODLAT1:def 14 (- 1.F_Real) *f; end; definition let V, W be non empty ModuleStr over INT.Ring; let f, g be FrForm of V,W; func f-g -> FrForm of V,W equals :: ZMODLAT1:def 15 f + -g; end; definition let V, W be non empty ModuleStr over INT.Ring; let f, g be FrForm of V,W; redefine func f - g means :: ZMODLAT1:def 16 for v being Vector of V, w being Vector of W holds it.(v,w) = f.(v,w) - g.(v,w); end; definition let V, W be non empty ModuleStr over INT.Ring; let f, g be FrForm of V,W; redefine func f+g; commutativity; end; theorem :: ZMODLAT1:39 for V, W being non empty ModuleStr over INT.Ring, f being FrForm of V,W holds f + NulFrForm(V,W) = f; theorem :: ZMODLAT1:40 for V, W being non empty ModuleStr over INT.Ring, f, g, h being FrForm of V,W holds f+g+h = f+(g+h); theorem :: ZMODLAT1:41 for V, W being non empty ModuleStr over INT.Ring, f being FrForm of V,W holds f - f = NulFrForm(V,W); theorem :: ZMODLAT1:42 for V, W being non empty ModuleStr over INT.Ring, a being Element of F_Real, f, g being FrForm of V,W holds a*(f+g) = a*f+a*g; theorem :: ZMODLAT1:43 for V, W being non empty ModuleStr over INT.Ring, a, b being Element of F_Real, f being FrForm of V,W holds (a+b)*f = a*f+b*f; theorem :: ZMODLAT1:44 for V, W being non empty ModuleStr over INT.Ring, a, b being Element of F_Real, f being FrForm of V,W holds (a*b)*f = a*(b*f); theorem :: ZMODLAT1:45 for V, W being non empty ModuleStr over INT.Ring, f being FrForm of V,W holds (1.F_Real)*f = f; definition let V be ModuleStr over INT.Ring; mode FrFunctional of V is Function of the carrier of V, the carrier of F_Real; end; definition let V be non empty ModuleStr over INT.Ring; let f, g be FrFunctional of V; func f+g -> FrFunctional of V means :: ZMODLAT1:def 17 for x being Element of V holds it.x = f.x + g.x; end; definition let V be non empty ModuleStr over INT.Ring; let f be FrFunctional of V; func -f -> FrFunctional of V means :: ZMODLAT1:def 18 for x being Element of V holds it.x = - (f.x); end; definition let V be non empty ModuleStr over INT.Ring; let f, g be FrFunctional of V; func f-g -> FrFunctional of V equals :: ZMODLAT1:def 19 f+-g; end; definition let V be non empty ModuleStr over INT.Ring; let v be Element of F_Real; let f be FrFunctional of V; func v*f -> FrFunctional of V means :: ZMODLAT1:def 20 for x being Element of V holds it.x = v*(f.x); end; definition let V be ModuleStr over INT.Ring; func 0FrFunctional(V) -> FrFunctional of V equals :: ZMODLAT1:def 21 [#]V --> 0.F_Real; end; definition let V be non empty ModuleStr over INT.Ring; let F be FrFunctional of V; attr F is homogeneous means :: ZMODLAT1:def 22 for x being Vector of V, r being Scalar of V holds F.(r*x) = r*F.x; end; definition let V be non empty ModuleStr over INT.Ring; let F be FrFunctional of V; attr F is 0-preserving means :: ZMODLAT1:def 23 F.(0.V) = 0.F_Real; end; registration let V be Z_Module; cluster homogeneous -> 0-preserving for FrFunctional of V; end; registration let V be non empty ModuleStr over INT.Ring; cluster 0FrFunctional(V) -> additive; end; registration let V be non empty ModuleStr over INT.Ring; cluster 0FrFunctional(V) -> homogeneous; end; registration let V be non empty ModuleStr over INT.Ring; cluster 0FrFunctional(V) -> 0-preserving; end; registration let V be non empty ModuleStr over INT.Ring; cluster additive homogeneous 0-preserving for FrFunctional of V; end; theorem :: ZMODLAT1:46 for V be non empty ModuleStr over INT.Ring, f, g be FrFunctional of V holds f+g = g+f; theorem :: ZMODLAT1:47 for V being non empty ModuleStr over INT.Ring, f, g, h being FrFunctional of V holds f+g+h = f+(g+h); theorem :: ZMODLAT1:48 for V being non empty ModuleStr over INT.Ring, x being Element of V holds (0FrFunctional(V)).x = 0.F_Real; theorem :: ZMODLAT1:49 for V being non empty ModuleStr over INT.Ring, f being FrFunctional of V holds f + 0FrFunctional(V) = f; theorem :: ZMODLAT1:50 for V being non empty ModuleStr over INT.Ring, f being FrFunctional of V holds f-f = 0FrFunctional(V); theorem :: ZMODLAT1:51 for V being non empty ModuleStr over INT.Ring, r being Element of F_Real, f, g being FrFunctional of V holds r*(f+g) = r*f+r*g; theorem :: ZMODLAT1:52 for V being non empty ModuleStr over INT.Ring, r, s being Element of F_Real, f being FrFunctional of V holds (r+s)*f = r*f+s*f; theorem :: ZMODLAT1:53 for V being non empty ModuleStr over INT.Ring, r, s being Element of F_Real, f being FrFunctional of V holds (r*s)*f = r*(s*f); theorem :: ZMODLAT1:54 for V being non empty ModuleStr over INT.Ring, f being FrFunctional of V holds (1.F_Real)*f = f; registration let V be non empty ModuleStr over INT.Ring; let f,g be additive FrFunctional of V; cluster f+g -> additive; end; registration let V be non empty ModuleStr over INT.Ring; let f be additive FrFunctional of V; cluster -f -> additive; end; registration let V be non empty ModuleStr over INT.Ring; let v be Element of F_Real; let f be additive FrFunctional of V; cluster v*f -> additive; end; registration let V be non empty ModuleStr over INT.Ring; let f, g be homogeneous FrFunctional of V; cluster f+g -> homogeneous; end; registration let V be non empty ModuleStr over INT.Ring; let f be homogeneous FrFunctional of V; cluster -f -> homogeneous; end; registration let V be non empty ModuleStr over INT.Ring; let v be Element of F_Real; let f be homogeneous FrFunctional of V; cluster v*f -> homogeneous; end; definition let V, W be non empty ModuleStr over INT.Ring; let f be FrForm of V,W, v be Vector of V; func FrFunctionalFAF(f,v) -> FrFunctional of W equals :: ZMODLAT1:def 24 (curry f).v; end; definition let V, W be non empty ModuleStr over INT.Ring; let f be FrForm of V,W, w be Vector of W; func FrFunctionalSAF(f,w) -> FrFunctional of V equals :: ZMODLAT1:def 25 (curry' f).w; end; theorem :: ZMODLAT1:55 for V, W being non empty ModuleStr over INT.Ring, f being FrForm of V,W, v being Vector of V holds dom (FrFunctionalFAF(f,v)) = the carrier of W & rng (FrFunctionalFAF(f,v)) c= the carrier of F_Real & for w being Vector of W holds (FrFunctionalFAF(f,v)).w = f.(v,w); theorem :: ZMODLAT1:56 for V, W being non empty ModuleStr over INT.Ring, f being FrForm of V,W, w being Vector of W holds dom (FrFunctionalSAF(f,w)) = the carrier of V & rng (FrFunctionalSAF(f,w)) c= the carrier of F_Real & for v being Vector of V holds (FrFunctionalSAF(f,w)).v = f.(v,w); theorem :: ZMODLAT1:57 for V being non empty ModuleStr over INT.Ring, x being Element of V holds (0FrFunctional(V)).x = 0.F_Real; theorem :: ZMODLAT1:58 for V, W being non empty ModuleStr over INT.Ring, v being Vector of V holds FrFunctionalFAF(NulFrForm(V,W),v) = 0FrFunctional(W); theorem :: ZMODLAT1:59 for V, W being non empty ModuleStr over INT.Ring, w being Vector of W holds FrFunctionalSAF(NulFrForm(V,W),w) = 0FrFunctional(V); theorem :: ZMODLAT1:60 for V, W being non empty ModuleStr over INT.Ring, f, g being FrForm of V,W, w being Vector of W holds FrFunctionalSAF(f+g,w) = FrFunctionalSAF(f,w) + FrFunctionalSAF(g,w); theorem :: ZMODLAT1:61 for V, W being non empty ModuleStr over INT.Ring, f, g being FrForm of V,W, v being Vector of V holds FrFunctionalFAF(f+g,v) = FrFunctionalFAF(f,v) + FrFunctionalFAF(g,v); theorem :: ZMODLAT1:62 for V, W being non empty ModuleStr over INT.Ring, f being FrForm of V,W, a being Element of F_Real, w being Vector of W holds FrFunctionalSAF(a*f,w) = a*FrFunctionalSAF(f,w); theorem :: ZMODLAT1:63 for V, W being non empty ModuleStr over INT.Ring, f being FrForm of V,W, a being Element of F_Real, v being Vector of V holds FrFunctionalFAF(a*f,v) = a*FrFunctionalFAF(f,v); theorem :: ZMODLAT1:64 for V, W being non empty ModuleStr over INT.Ring, f being FrForm of V,W, w being Vector of W holds FrFunctionalSAF(-f,w) = -FrFunctionalSAF(f,w); theorem :: ZMODLAT1:65 for V, W being non empty ModuleStr over INT.Ring, f being FrForm of V,W, v being Vector of V holds FrFunctionalFAF(-f,v) = -FrFunctionalFAF(f,v); theorem :: ZMODLAT1:66 for V, W being non empty ModuleStr over INT.Ring, f, g being FrForm of V,W, w being Vector of W holds FrFunctionalSAF(f-g,w) = FrFunctionalSAF(f,w) - FrFunctionalSAF(g,w); theorem :: ZMODLAT1:67 for V, W being non empty ModuleStr over INT.Ring, f, g being FrForm of V,W, v being Vector of V holds FrFunctionalFAF(f-g,v) = FrFunctionalFAF(f,v) - FrFunctionalFAF(g,v); definition let V, W be non empty ModuleStr over INT.Ring; let f be FrFunctional of V; let g be FrFunctional of W; func FrFormFunctional(f,g) -> FrForm of V,W means :: ZMODLAT1:def 26 for v being Vector of V, w being Vector of W holds it.(v,w)= f.v * g.w; end; theorem :: ZMODLAT1:68 for V, W being non empty ModuleStr over INT.Ring, f being FrFunctional of V, v being Vector of V, w being Vector of W holds FrFormFunctional(f,0FrFunctional(W)).(v,w) = 0.INT.Ring; theorem :: ZMODLAT1:69 for V, W being non empty ModuleStr over INT.Ring, g being FrFunctional of W, v being Vector of V, w being Vector of W holds FrFormFunctional(0FrFunctional(V),g).(v,w) = 0.INT.Ring; theorem :: ZMODLAT1:70 for V, W being non empty ModuleStr over INT.Ring, f being FrFunctional of V holds FrFormFunctional(f,0FrFunctional(W)) = NulFrForm(V,W); theorem :: ZMODLAT1:71 for V, W being non empty ModuleStr over INT.Ring, g being FrFunctional of W holds FrFormFunctional(0FrFunctional(V),g) = NulFrForm(V,W); theorem :: ZMODLAT1:72 for V, W being non empty ModuleStr over INT.Ring, f being FrFunctional of V, g being FrFunctional of W, v being Vector of V holds FrFunctionalFAF(FrFormFunctional(f,g),v) = f.v * g; theorem :: ZMODLAT1:73 for V, W being non empty ModuleStr over INT.Ring, f being FrFunctional of V, g being FrFunctional of W, w being Vector of W holds FrFunctionalSAF(FrFormFunctional(f,g),w) = g.w * f; begin :: 2. Bilinear forms over real number field $\mathbb R$, and their properties definition let V, W be non empty ModuleStr over INT.Ring; let f be FrForm of V,W; attr f is additiveFAF means :: ZMODLAT1:def 27 for v being Vector of V holds FrFunctionalFAF (f,v) is additive; attr f is additiveSAF means :: ZMODLAT1:def 28 for w being Vector of W holds FrFunctionalSAF (f,w) is additive; end; definition let V, W be non empty ModuleStr over INT.Ring; let f be FrForm of V,W; attr f is homogeneousFAF means :: ZMODLAT1:def 29 for v being Vector of V holds FrFunctionalFAF(f,v) is homogeneous; attr f is homogeneousSAF means :: ZMODLAT1:def 30 for w being Vector of W holds FrFunctionalSAF(f,w) is homogeneous; end; registration let V, W be non empty ModuleStr over INT.Ring; cluster NulFrForm(V,W) -> additiveFAF; cluster NulFrForm(V,W) -> additiveSAF; end; registration let V, W be non empty ModuleStr over INT.Ring; cluster additiveFAF additiveSAF for FrForm of V,W; end; registration let V, W be non empty ModuleStr over INT.Ring; cluster NulFrForm(V,W) -> homogeneousFAF; cluster NulFrForm(V,W) -> homogeneousSAF; end; registration let V, W be non empty ModuleStr over INT.Ring; cluster additiveFAF homogeneousFAF additiveSAF homogeneousSAF for FrForm of V,W; end; definition let V, W be non empty ModuleStr over INT.Ring; mode bilinear-FrForm of V,W is additiveSAF homogeneousSAF additiveFAF homogeneousFAF FrForm of V,W; end; registration let V, W be non empty ModuleStr over INT.Ring; let f be additiveFAF FrForm of V,W, v be Vector of V; cluster FrFunctionalFAF(f,v) -> additive; end; registration let V, W be non empty ModuleStr over INT.Ring; let f be additiveSAF FrForm of V,W, w be Vector of W; cluster FrFunctionalSAF(f,w) -> additive; end; registration let V, W be non empty ModuleStr over INT.Ring; let f be homogeneousFAF FrForm of V,W, v be Vector of V; cluster FrFunctionalFAF(f,v) -> homogeneous; end; registration let V, W be non empty ModuleStr over INT.Ring; let f be homogeneousSAF FrForm of V,W, w be Vector of W; cluster FrFunctionalSAF(f,w) -> homogeneous; end; registration let V, W be non empty ModuleStr over INT.Ring; let f be FrFunctional of V, g be additive FrFunctional of W; cluster FrFormFunctional(f,g) -> additiveFAF; end; registration let V, W be non empty ModuleStr over INT.Ring; let f be additive FrFunctional of V, g be FrFunctional of W; cluster FrFormFunctional(f,g) -> additiveSAF; end; registration let V, W be non empty ModuleStr over INT.Ring; let f be FrFunctional of V, g be homogeneous FrFunctional of W; cluster FrFormFunctional(f,g) -> homogeneousFAF; end; registration let V, W be non empty ModuleStr over INT.Ring; let f be homogeneous FrFunctional of V, g be FrFunctional of W; cluster FrFormFunctional(f,g) -> homogeneousSAF; end; registration let V be non trivial ModuleStr over INT.Ring, W be non empty ModuleStr over INT.Ring; let f be FrFunctional of V, g be FrFunctional of W; cluster FrFormFunctional(f,g) -> non trivial; end; registration let V be non empty ModuleStr over INT.Ring, W be non trivial ModuleStr over INT.Ring; let f be FrFunctional of V, g be FrFunctional of W; cluster FrFormFunctional(f,g) -> non trivial; end; definition let V be non empty ModuleStr over INT.Ring; let F be FrFunctional of V; attr F is 0-preserving means :: ZMODLAT1:def 31 F.(0.V) = 0.F_Real; end; registration let V be Z_Module; cluster homogeneous -> 0-preserving for FrFunctional of V; end; registration let V be non empty ModuleStr over INT.Ring; cluster 0FrFunctional(V) -> 0-preserving; end; registration let V be non empty ModuleStr over INT.Ring; cluster additive homogeneous 0-preserving for FrFunctional of V; end; registration let V be non trivial free Z_Module; cluster additive homogeneous non constant non trivial for FrFunctional of V; end; theorem :: ZMODLAT1:74 for V being non trivial free Z_Module, f being non constant 0-preserving FrFunctional of V ex v being Vector of V st v <> 0.V & f.v <> 0.F_Real; registration let V, W be non trivial free Z_Module; let f be non constant 0-preserving FrFunctional of V, g be non constant 0-preserving FrFunctional of W; cluster FrFormFunctional(f,g) -> non constant; end; definition let V be non empty ModuleStr over INT.Ring; mode linear-FrFunctional of V is additive homogeneous FrFunctional of V; end; registration let V, W be non trivial free Z_Module; cluster non trivial non constant additiveFAF homogeneousFAF additiveSAF homogeneousSAF for FrForm of V,W; end; registration let V, W be non empty ModuleStr over INT.Ring; let f, g be additiveSAF FrForm of V,W; cluster f+g -> additiveSAF; end; registration let V, W be non empty ModuleStr over INT.Ring; let f, g be additiveFAF FrForm of V,W; cluster f+g -> additiveFAF; end; registration let V, W be non empty ModuleStr over INT.Ring; let f be additiveSAF FrForm of V,W; let a be Element of F_Real; cluster a*f -> additiveSAF; end; registration let V, W be non empty ModuleStr over INT.Ring; let f be additiveFAF FrForm of V,W; let a be Element of F_Real; cluster a*f -> additiveFAF; end; registration let V, W be non empty ModuleStr over INT.Ring; let f be additiveSAF FrForm of V,W; cluster -f -> additiveSAF; end; registration let V, W be non empty ModuleStr over INT.Ring; let f be additiveFAF FrForm of V,W; cluster -f -> additiveFAF; end; registration let V, W be non empty ModuleStr over INT.Ring; let f, g be additiveSAF FrForm of V,W; cluster f-g -> additiveSAF; end; registration let V, W be non empty ModuleStr over INT.Ring; let f, g be additiveFAF FrForm of V,W; cluster f-g -> additiveFAF; end; registration let V, W be non empty ModuleStr over INT.Ring; let f, g be homogeneousSAF FrForm of V,W; cluster f+g -> homogeneousSAF; end; registration let V, W be non empty ModuleStr over INT.Ring; let f, g be homogeneousFAF FrForm of V,W; cluster f+g -> homogeneousFAF; end; registration let V, W be non empty ModuleStr over INT.Ring; let f be homogeneousSAF FrForm of V,W; let a be Element of F_Real; cluster a*f -> homogeneousSAF; end; registration let V, W be non empty ModuleStr over INT.Ring; let f be homogeneousFAF FrForm of V,W; let a be Element of F_Real; cluster a*f -> homogeneousFAF; end; registration let V, W be non empty ModuleStr over INT.Ring; let f be homogeneousSAF FrForm of V,W; cluster -f -> homogeneousSAF; end; registration let V, W be non empty ModuleStr over INT.Ring; let f be homogeneousFAF FrForm of V,W; cluster -f -> homogeneousFAF; end; registration let V, W be non empty ModuleStr over INT.Ring; let f, g be homogeneousSAF FrForm of V,W; cluster f-g -> homogeneousSAF; end; registration let V, W be non empty ModuleStr over INT.Ring; let f, g be homogeneousFAF FrForm of V,W; cluster f-g -> homogeneousFAF; end; theorem :: ZMODLAT1:75 for V, W being non empty ModuleStr over INT.Ring, v, u being Vector of V, w being Vector of W, f being FrForm of V,W st f is additiveSAF holds f.(v+u,w) = f.(v,w) + f.(u,w); theorem :: ZMODLAT1:76 for V,W being non empty ModuleStr over INT.Ring, v being Vector of V, u, w being Vector of W, f being FrForm of V,W st f is additiveFAF holds f.(v,u+w) = f.(v,u) + f.(v,w); theorem :: ZMODLAT1:77 for V,W being non empty ModuleStr over INT.Ring, v, u being Vector of V, w, t being Vector of W, f being additiveSAF additiveFAF FrForm of V,W holds f.(v+u,w+t) = f.(v,w) + f.(v,t) + (f.(u,w) + f.(u,t)); theorem :: ZMODLAT1:78 for V, W being right_zeroed non empty ModuleStr over INT.Ring, f being additiveFAF FrForm of V,W, v being Vector of V holds f.(v,0.W) = 0.INT.Ring; theorem :: ZMODLAT1:79 for V, W being right_zeroed non empty ModuleStr over INT.Ring, f being additiveSAF FrForm of V,W, w being Vector of W holds f.(0.V,w) = 0.INT.Ring; theorem :: ZMODLAT1:80 for V, W being non empty ModuleStr over INT.Ring, v being Vector of V, w being Vector of W, a being Element of INT.Ring, f being FrForm of V,W st f is homogeneousSAF holds f.(a*v,w) = a*f.(v,w); theorem :: ZMODLAT1:81 for V, W being non empty ModuleStr over INT.Ring, v being Vector of V, w being Vector of W, a being Element of INT.Ring, f being FrForm of V,W st f is homogeneousFAF holds f.(v,a*w) = a*f.(v,w); theorem :: ZMODLAT1:82 for V, W being add-associative right_zeroed right_complementable vector-distributive scalar-distributive scalar-associative scalar-unital non empty ModuleStr over INT.Ring, f being homogeneousSAF FrForm of V,W, w being Vector of W holds f.(0.V,w) = 0.F_Real; theorem :: ZMODLAT1:83 for V, W being add-associative right_zeroed right_complementable vector-distributive scalar-distributive scalar-associative scalar-unital non empty ModuleStr over INT.Ring, f being homogeneousFAF FrForm of V,W, v being Vector of V holds f.(v,0.W) = 0.F_Real; theorem :: ZMODLAT1:84 for V, W being Z_Module, v, u being Vector of V, w being Vector of W, f being additiveSAF homogeneousSAF FrForm of V,W holds f.(v-u,w) = f.(v,w) - f.(u,w); theorem :: ZMODLAT1:85 for V, W being Z_Module, v being Vector of V, w, t being Vector of W, f being additiveFAF homogeneousFAF FrForm of V,W holds f.(v,w-t) = f.(v,w) - f.(v,t); theorem :: ZMODLAT1:86 for V, W being Z_Module, v, u being Vector of V, w, t being Vector of W, f being bilinear-FrForm of V,W holds f.(v-u,w-t) = f.(v,w) - f.(v,t) -(f.(u,w) - f.(u,t)); theorem :: ZMODLAT1:87 for V,W being add-associative right_zeroed right_complementable vector-distributive scalar-distributive scalar-associative scalar-unital non empty ModuleStr over INT.Ring, v, u being Vector of V, w, t being Vector of W, a, b being Element of INT.Ring, f being bilinear-FrForm of V,W holds f.(v+a*u,w+b*t) = f.(v,w) + b*f.(v,t) + (a*f.(u,w) + a*(b*f.(u,t))); theorem :: ZMODLAT1:88 for V, W being Z_Module, v, u being Vector of V, w, t being Vector of W, a, b being Element of INT.Ring, f being bilinear-FrForm of V,W holds f.(v-a*u,w-b*t) = f.(v,w) - b*f.(v,t) - (a*f.(u,w) - a*(b*f.(u,t))); theorem :: ZMODLAT1:89 for V, W being right_zeroed non empty ModuleStr over INT.Ring, f being FrForm of V,W st f is additiveFAF or f is additiveSAF holds f is constant iff for v being Vector of V, w being Vector of W holds f.(v,w) = 0.INT.Ring; begin :: 3. Matrices of bilinear form over real number field $\mathbb R$ definition let V1, V2 be finite-rank free Z_Module; let b1 be OrdBasis of V1, b2 be OrdBasis of V2; let f be bilinear-FrForm of V1,V2; func BilinearM(f, b1, b2) -> Matrix of len b1, len b2, F_Real means :: ZMODLAT1:def 32 for i, j being Nat st i in dom b1 & j in dom b2 holds it*(i,j) = f.(b1/.i, b2/.j); end; theorem :: ZMODLAT1:90 for V being finite-rank free Z_Module, F being linear-FrFunctional of V, y being FinSequence of V, x being FinSequence of INT.Ring, X, Y being FinSequence of F_Real st X = x & len y = len x & len X = len Y & (for k being Nat st k in Seg len x holds Y.k = F.(y/.k)) holds X "*" Y = F.(Sum lmlt (x,y)); theorem :: ZMODLAT1:91 for V1, V2 being finite-rank free Z_Module, b2 being OrdBasis of V2, b3 being OrdBasis of V2, f being bilinear-FrForm of V1, V2, v1 being Vector of V1, v2 being Vector of V2, X, Y being FinSequence of F_Real st len X = len b2 & len Y = len b2 & ( for k being Nat st k in Seg len b2 holds Y.k = f.(v1, b2/.k)) & X = (v2|-- b2) holds Y "*" X = f.(v1, v2); theorem :: ZMODLAT1:92 for V1, V2 being finite-rank free Z_Module, b1 being OrdBasis of V1, f being bilinear-FrForm of V1, V2, v1 being Vector of V1, v2 being Vector of V2, X,Y being FinSequence of F_Real st len X = len b1 & len Y = len b1 & ( for k being Nat st k in Seg len b1 holds Y.k = f.(b1/.k, v2) ) & X = (v1 |-- b1) holds X "*" Y = f.(v1, v2); theorem :: ZMODLAT1:93 for M being Matrix of INT.Ring holds M is Matrix of F_Real; definition let M be Matrix of INT.Ring; func inttorealM(M) -> Matrix of F_Real equals :: ZMODLAT1:def 33 M; end; definition let n, m be Nat; let M be Matrix of n,m,INT.Ring; redefine func inttorealM(M) -> Matrix of n,m,F_Real; end; definition let n be Nat; let M be Matrix of n,INT.Ring; redefine func inttorealM(M) -> Matrix of n,F_Real; end; theorem :: ZMODLAT1:94 for m, l, n being Nat for S being Matrix of l,m,INT.Ring, T being Matrix of m,n,INT.Ring, S1 being Matrix of l,m,F_Real, T1 being Matrix of m,n,F_Real st S = S1 & T = T1 & 0 < l & 0 < m holds S*T = S1*T1; theorem :: ZMODLAT1:95 for n being Nat holds 1.(INT.Ring,n) = 1.(F_Real,n); theorem :: ZMODLAT1:96 for V1, V2 being finite-rank free Z_Module, b1 being OrdBasis of V1, b2 being OrdBasis of V2, b3 being OrdBasis of V2, f being bilinear-FrForm of V1, V2 st 0 < rank V1 holds BilinearM(f, b1, b3) = BilinearM(f, b1, b2) * ( (inttorealM(AutMt(id(V2), b3, b2))) @); theorem :: ZMODLAT1:97 for V1, V2 being finite-rank free Z_Module, b1 being OrdBasis of V1, b2 being OrdBasis of V2, b3 being OrdBasis of V1, f being bilinear-FrForm of V1, V2 st 0 < rank V1 holds BilinearM(f, b3, b2) = inttorealM(AutMt(id(V1), b3, b1)) * BilinearM(f, b1, b2); theorem :: ZMODLAT1:98 for V being finite-rank free Z_Module, b1, b2 being OrdBasis of V, f being bilinear-FrForm of V,V st 0 < rank V holds BilinearM(f, b2, b2) = inttorealM( AutMt(id(V), b2, b1)) * BilinearM(f, b1, b1) * ((inttorealM( AutMt(id(V), b2, b1)))@); theorem :: ZMODLAT1:99 for V being finite-rank free Z_Module, b1, b2 being OrdBasis of V, M being Matrix of rank(V),F_Real st M = AutMt(id(V), b1, b2) holds ( Det M = 1 & Det M@ = 1) or ( Det M = -1 & Det M@ = -1); theorem :: ZMODLAT1:100 for V being finite-rank free Z_Module, b1, b2 being OrdBasis of V, M being Matrix of rank(V),F_Real st M = AutMt(id(V), b1, b2) holds |. Det M .| = 1; theorem :: ZMODLAT1:101 for V being finite-rank free Z_Module, b1, b2 being OrdBasis of V, f being bilinear-FrForm of V, V holds Det BilinearM(f, b2, b2) = Det BilinearM(f, b1, b1); theorem :: ZMODLAT1:102 for V being finite-rank free Z_Module, b1, b2 being OrdBasis of V, f being bilinear-FrForm of V, V holds |. Det BilinearM(f, b2, b2) .| = |. Det BilinearM(f, b1, b1) .|; definition let V be finite-rank free Z_Module; let f be bilinear-FrForm of V, V; let b be OrdBasis of V; func GramMatrix(f, b) -> Matrix of rank(V),F_Real equals :: ZMODLAT1:def 34 BilinearM(f, b, b); end; definition let V be finite-rank free Z_Module; let f be bilinear-FrForm of V, V; func GramDet(f) -> Element of F_Real means :: ZMODLAT1:def 35 for b being OrdBasis of V holds it = Det GramMatrix(f, b); end; definition let L be Z_Lattice; func InnerProduct(L) -> FrForm of L,L equals :: ZMODLAT1:def 36 the scalar of L; end; registration let L be Z_Lattice; cluster InnerProduct(L) -> additiveSAF homogeneousSAF additiveFAF homogeneousFAF; end; definition let L be Z_Lattice; let b be OrdBasis of L; func GramMatrix(b) -> Matrix of dim(L),F_Real equals :: ZMODLAT1:def 37 GramMatrix(InnerProduct(L),b); end; definition let L be Z_Lattice; func GramDet(L) -> Element of F_Real equals :: ZMODLAT1:def 38 GramDet(InnerProduct(L)); end; theorem :: ZMODLAT1:103 for L being INTegral Z_Lattice holds InnerProduct(L) is bilinear-Form of L,L; theorem :: ZMODLAT1:104 for L being INTegral Z_Lattice, b being OrdBasis of L holds GramMatrix(b) is Matrix of dim(L),INT.Ring; registration let L be INTegral Z_Lattice; cluster GramDet(L) -> integer; end;