:: On Cosets in Segre's Product of Partial Linear Spaces
:: by Adam Naumowicz
::
:: Received August 14, 2001
:: Copyright (c) 2001-2018 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 NUMBERS, FINSEQ_1, NAT_1, FINSEQ_3, RELAT_1, ARYTM_1, ORDINAL4,
RFINSEQ, SUBSET_1, TARSKI, XBOOLE_0, XXREAL_0, ARYTM_3, CARD_1, FUNCT_1,
PARTFUN1, PRALG_1, PBOOLE, RLVECT_2, FUNCT_4, STRUCT_0, PENCIL_1, CARD_3,
INTEGRA1, ZFMISC_1, PRE_TOPC, FUNCT_2, CAT_1, RCOMP_1, RELAT_2, PENCIL_2,
WAYBEL18;
notations TARSKI, XBOOLE_0, ZFMISC_1, SUBSET_1, ORDINAL1, NUMBERS, XCMPLX_0,
NAT_1, RELAT_1, NAT_D, FUNCT_1, RELSET_1, PARTFUN1, FUNCT_2, STRUCT_0,
XXREAL_0, RFINSEQ, CARD_1, FINSEQ_1, CARD_3, PRE_TOPC, PBOOLE, PZFMISC1,
TOPS_2, T_0TOPSP, PRALG_1, FUNCT_7, WAYBEL18, PENCIL_1;
constructors RFINSEQ, NAT_D, PZFMISC1, TOPS_2, T_0TOPSP, POLYNOM1, PENCIL_1,
REAL_1, RELSET_1, PBOOLE, FUNCT_7;
registrations SUBSET_1, FUNCT_1, PARTFUN1, FUNCT_2, XXREAL_0, XREAL_0, NAT_1,
STRUCT_0, BORSUK_2, PENCIL_1, ORDINAL1, FINSEQ_1, RELSET_1, PRE_POLY,
WAYBEL18;
requirements REAL, BOOLE, SUBSET, NUMERALS, ARITHM;
begin :: Preliminaries on finite sequences
definition
let D be set;
let p be FinSequence of D;
let i,j be Nat;
func Del(p,i,j) -> FinSequence of D equals
:: PENCIL_2:def 1
(p|(i -' 1))^(p/^j);
end;
theorem :: PENCIL_2:1
for D being set,p being FinSequence of D,i,j being Element of NAT
holds rng Del(p,i,j) c= rng p;
theorem :: PENCIL_2:2
for D being set,p being FinSequence of D,i,j being Element of NAT
st i in dom p & j in dom p holds len Del(p,i,j) = len p - j + i - 1;
theorem :: PENCIL_2:3
for D being set,p being FinSequence of D,i,j being Element of NAT
st i in dom p & j in dom p holds len Del(p,i,j) = 0 implies i=1 & j=len p;
theorem :: PENCIL_2:4
for D being set,p being FinSequence of D,i,j,k being Element of
NAT st i in dom p & 1 <= k & k <= i-1 holds Del(p,i,j).k = p.k;
theorem :: PENCIL_2:5
for p,q being FinSequence, k being Element of NAT holds len p + 1
<= k implies (p^q).k=q.(k-len p);
theorem :: PENCIL_2:6
for D being set,p being FinSequence of D,i,j,k being Element of
NAT st i in dom p & j in dom p & i <= j & i <= k & k <= len p - j + i - 1 holds
Del(p,i,j).k = p.(j -'i + k + 1);
scheme :: PENCIL_2:sch 1
FinSeqOneToOne{X,Y,D()->set,f()-> FinSequence of D(),P[set,set]}: ex g being
one-to-one FinSequence of D() st X() = g.1 & Y()=g.len g & rng g c= rng f() &
for j being Element of NAT st 1 <= j & j < len g holds P[g.j,g.(j+1)]
provided
X() = f().1 & Y()=f().len f() and
for i being Element of NAT, d1,d2 being set st 1 <= i & i < len f()
& d1 =f().i & d2 = f().(i+1) holds P[d1,d2];
begin :: Segre cosets
theorem :: PENCIL_2:7
for I being non empty set for A being 1-sorted-yielding
ManySortedSet of I for L being ManySortedSubset of Carrier A for i being
Element of I for S being Subset of A.i holds L+*(i,S) is ManySortedSubset of
Carrier A;
definition
let I be non empty set;
let A be non-Trivial-yielding TopStruct-yielding ManySortedSet of I;
mode Segre-Coset of A -> Subset of Segre_Product A means
:: PENCIL_2:def 2
ex L being
Segre-like non trivial-yielding ManySortedSubset of Carrier A st it = product L
& L.indx(L) = [#](A.indx(L));
end;
theorem :: PENCIL_2:8
for I being non empty set for A being non-Trivial-yielding
TopStruct-yielding ManySortedSet of I for B1,B2 being Segre-Coset of A st 2 c=
card(B1 /\ B2) holds B1 = B2;
definition
let S be TopStruct;
let X,Y be Subset of S;
pred X,Y are_joinable means
:: PENCIL_2:def 3
ex f being FinSequence of bool the
carrier of S st X = f.1 & Y = f.(len f) & (for W being Subset of S st W in rng
f holds W is closed_under_lines strong) & for i being Element of NAT st 1 <= i
& i < len f holds 2 c= card((f.i) /\ (f.(i+1)));
end;
theorem :: PENCIL_2:9
for S being TopStruct for X,Y being Subset of S st X,Y are_joinable ex
f being one-to-one FinSequence of bool the carrier of S st (X = f.1 & Y = f.(
len f) & (for W being Subset of S st W in rng f holds W is closed_under_lines
strong) & for i being Element of NAT st 1 <= i & i < len f holds 2 c= card((f.i
) /\ (f.(i+1))));
theorem :: PENCIL_2:10
for S being TopStruct for X being Subset of S st X is
closed_under_lines strong holds X,X are_joinable;
theorem :: PENCIL_2:11
for I being non empty set for A being PLS-yielding ManySortedSet
of I for X,Y being Subset of Segre_Product A st X is non trivial
closed_under_lines strong & Y is non trivial closed_under_lines strong & X,Y
are_joinable for X1,Y1 being Segre-like non trivial-yielding ManySortedSubset
of Carrier A st X = product X1 & Y = product Y1 holds indx(X1) = indx(Y1) &
for i being object st i <> indx(X1) holds X1.i = Y1.i;
begin :: Collineations of Segre product
theorem :: PENCIL_2:12
for S being 1-sorted for T being non empty 1-sorted for f being
Function of S,T st f is bijective holds f" is bijective;
definition
let S,T be TopStruct;
let f be Function of S,T;
attr f is isomorphic means
:: PENCIL_2:def 4
f is bijective open & f" is bijective open;
end;
registration
let S be non empty TopStruct;
cluster isomorphic for Function of S,S;
end;
definition
let S be non empty TopStruct;
mode Collineation of S is isomorphic Function of S,S;
end;
definition
let S be non empty non void TopStruct;
let f be Collineation of S;
let l be Block of S;
redefine func f.:l -> Block of S;
end;
definition
let S be non empty non void TopStruct;
let f be Collineation of S;
let l be Block of S;
redefine func f"l -> Block of S;
end;
theorem :: PENCIL_2:13
for S being non empty TopStruct for f being Collineation of S
holds f" is Collineation of S;
theorem :: PENCIL_2:14
for S being non empty TopStruct for f being Collineation of S
for X being Subset of S st X is non trivial holds f.:X is non trivial;
theorem :: PENCIL_2:15
for S being non empty TopStruct for f being Collineation of S for X
being Subset of S st X is non trivial holds f"X is non trivial;
theorem :: PENCIL_2:16
for S being non empty non void TopStruct for f being
Collineation of S for X being Subset of S st X is strong holds f.:X is strong
;
theorem :: PENCIL_2:17
for S being non empty non void TopStruct for f being Collineation of S
for X being Subset of S st X is strong holds f"X is strong;
theorem :: PENCIL_2:18
for S being non empty non void TopStruct for f being
Collineation of S for X being Subset of S st X is closed_under_lines holds f.:X
is closed_under_lines;
theorem :: PENCIL_2:19
for S being non empty non void TopStruct for f being Collineation of S
for X being Subset of S st X is closed_under_lines holds f"X is
closed_under_lines;
theorem :: PENCIL_2:20
for S being non empty non void TopStruct for f being
Collineation of S for X,Y being Subset of S st X is non trivial & Y is non
trivial & X,Y are_joinable holds f.:X,f.:Y are_joinable;
theorem :: PENCIL_2:21
for S being non empty non void TopStruct for f being Collineation of S
for X,Y being Subset of S st X is non trivial & Y is non trivial & X,Y
are_joinable holds f"X,f"Y are_joinable;
theorem :: PENCIL_2:22
for I being non empty set for A being PLS-yielding ManySortedSet
of I st for i being Element of I holds A.i is strongly_connected for W being
Subset of Segre_Product A st W is non trivial strong closed_under_lines holds
union {Y where Y is Subset of Segre_Product A : Y is non trivial strong
closed_under_lines & W,Y are_joinable} is Segre-Coset of A;
theorem :: PENCIL_2:23
for I being non empty set for A being PLS-yielding ManySortedSet
of I st for i being Element of I holds A.i is strongly_connected for B being
set holds B is Segre-Coset of A iff ex W being Subset of Segre_Product A st W
is non trivial strong closed_under_lines & B = union {Y where Y is Subset of
Segre_Product A : Y is non trivial strong closed_under_lines & W,Y are_joinable
};
theorem :: PENCIL_2:24
for I being non empty set for A being PLS-yielding ManySortedSet
of I st for i being Element of I holds A.i is strongly_connected for B being
Segre-Coset of A for f being Collineation of Segre_Product A holds f.:B is
Segre-Coset of A;
theorem :: PENCIL_2:25
for I being non empty set for A being PLS-yielding ManySortedSet of I
st for i being Element of I holds A.i is strongly_connected for B being
Segre-Coset of A for f being Collineation of Segre_Product A holds f"B is
Segre-Coset of A;