:: On the Characterization of Collineations of the Segre Product of Strongly
:: Connected Partial Linear Spaces
:: by Adam Naumowicz
::
:: Received October 18, 2004
:: Copyright (c) 2004-2019 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, XBOOLE_0, STRUCT_0, PRE_TOPC, PENCIL_2, PENCIL_1,
FUNCT_1, RELAT_1, TARSKI, SUBSET_1, PRALG_1, PBOOLE, ZFMISC_1, RELAT_2,
FINSEQ_1, NAT_1, XXREAL_0, ARYTM_3, CARD_1, ARYTM_1, WAYBEL_3, RLVECT_2,
CARD_3, INTEGRA1, FUNCT_4, FINSET_1, FDIFF_1, PARSP_1, GRAPH_2, FUNCT_2,
CAT_1, RCOMP_1, FUNCOP_1, PENCIL_3, WAYBEL18;
notations TARSKI, XBOOLE_0, ZFMISC_1, XCMPLX_0, XXREAL_0, ORDINAL1, NUMBERS,
NAT_1, RELAT_1, SUBSET_1, FUNCT_1, FUNCT_2, FUNCOP_1, RELSET_1, CARD_1,
FINSET_1, FINSEQ_1, CARD_3, DOMAIN_1, STRUCT_0, PRE_TOPC, PBOOLE,
PZFMISC1, T_0TOPSP, PRALG_1, WAYBEL_3, WAYBEL18, PENCIL_1, FUNCT_7,
PENCIL_2, TOPS_2, FINSEQ_6, GRAPH_2;
constructors PZFMISC1, TOPS_2, REALSET2, T_0TOPSP, GRAPH_2, PENCIL_2,
RELSET_1, PBOOLE, FUNCT_7, PRE_POLY, FINSEQ_6;
registrations SUBSET_1, RELSET_1, FUNCT_2, XREAL_0, NAT_1, CARD_1, PBOOLE,
STRUCT_0, PENCIL_1, ORDINAL1, FUNCT_1, RELAT_1, FINSEQ_1, PRE_POLY,
WAYBEL18;
requirements REAL, BOOLE, SUBSET, NUMERALS, ARITHM;
begin :: Preliminaries
theorem :: PENCIL_3:1
for S being non empty non void TopStruct for f being Collineation
of S for p,q being Point of S st p,q are_collinear holds f.p,f.q are_collinear;
theorem :: PENCIL_3:2
for I being non empty set for i be Element of I for A being
non-Trivial-yielding 1-sorted-yielding ManySortedSet of I holds A.i is non
trivial;
theorem :: PENCIL_3:3
for S being non void identifying_close_blocks TopStruct st S is
strongly_connected holds S is without_isolated_points;
theorem :: PENCIL_3:4
for S being non empty non void identifying_close_blocks TopStruct
holds S is strongly_connected implies S is connected;
theorem :: PENCIL_3:5
for S being non void non degenerated TopStruct for L being Block of S
ex x being Point of S st not x in L;
theorem :: PENCIL_3:6
for I being non empty set for A being non-Empty
TopStruct-yielding ManySortedSet of I for p being Point of Segre_Product A
holds p is Element of Carrier A;
theorem :: PENCIL_3:7
for I being non empty set for A be 1-sorted-yielding
ManySortedSet of I for x being Element of I holds (Carrier A).x = [#](A.x);
theorem :: PENCIL_3:8
for I being non empty set for i being Element of I for A be
non-Trivial-yielding TopStruct-yielding ManySortedSet of I ex L being
Segre-like non trivial-yielding ManySortedSubset of Carrier A st indx(L)=i &
product L is Segre-Coset of A;
theorem :: PENCIL_3:9
for I being non empty set for i being Element of I for A be
non-Trivial-yielding TopStruct-yielding ManySortedSet of I for p being Point
of Segre_Product A ex L being Segre-like non trivial-yielding ManySortedSubset
of Carrier A st indx(L)=i & product L is Segre-Coset of A & p in product L;
theorem :: PENCIL_3:10
for I being non empty set for A being non-Trivial-yielding
TopStruct-yielding ManySortedSet of I for b being Segre-like non
trivial-yielding ManySortedSubset of Carrier A st product b is Segre-Coset of A
holds b.indx(b) = [#](A.indx(b));
theorem :: PENCIL_3:11
for I being non empty set for A be non-Trivial-yielding
TopStruct-yielding ManySortedSet of I for L1,L2 being Segre-like non
trivial-yielding ManySortedSubset of Carrier A st product L1 is Segre-Coset of
A & product L2 is Segre-Coset of A & indx(L1) = indx(L2) & product L1 meets
product L2 holds L1=L2;
theorem :: PENCIL_3:12
for I being non empty set for A be PLS-yielding ManySortedSet of
I for L being Segre-like non trivial-yielding ManySortedSubset of Carrier A for
B being Block of A.indx(L) holds product(L+*(indx(L),B)) is Block of
Segre_Product A;
theorem :: PENCIL_3:13
for I being non empty set for A be PLS-yielding ManySortedSet of
I for i being Element of I for p being Point of A.i for L being Segre-like non
trivial-yielding ManySortedSubset of Carrier A st i<>indx(L) holds L+*(i,{p})
is Segre-like non trivial-yielding ManySortedSubset of Carrier A;
theorem :: PENCIL_3:14
for I being non empty set for A being PLS-yielding ManySortedSet
of I for i being Element of I for S being Subset of A.i for L being Segre-like
non trivial-yielding ManySortedSubset of Carrier A holds product (L+*(i,S)) is
Subset of Segre_Product A;
theorem :: PENCIL_3:15
for I being non empty set for P being ManySortedSet of I for i
being Element of I holds {P}.i is 1-element;
theorem :: PENCIL_3:16
for I being non empty set for i being Element of I for A be
PLS-yielding ManySortedSet of I for B being Block of A.i for P being Element of
Carrier A holds product({P}+*(i,B)) is Block of Segre_Product A;
theorem :: PENCIL_3:17
for I being non empty set for A being PLS-yielding ManySortedSet
of I for p,q being Point of Segre_Product A st p<>q holds p,q are_collinear iff
for p1,q1 being ManySortedSet of I st p1=p & q1=q ex i being Element of I st (
for a,b being Point of A.i st a=p1.i & b=q1.i holds a<>b & a,b are_collinear) &
for j being Element of I st j<>i holds p1.j = q1.j;
theorem :: PENCIL_3:18
for I being non empty set for A being PLS-yielding ManySortedSet
of I for b being Segre-like non trivial-yielding ManySortedSubset of Carrier A
for x being Point of A.indx(b) ex p being ManySortedSet of I st p in product b
& {p+*(indx(b),x) qua set} = product(b+*(indx(b),{x}));
definition
let I be finite non empty set;
let b1,b2 be ManySortedSet of I;
func diff(b1,b2) -> Nat equals
:: PENCIL_3:def 1
card {i where i is Element of I: b1.i <> b2.i};
end;
theorem :: PENCIL_3:19
for I being finite non empty set for b1,b2 being ManySortedSet
of I for i being Element of I st b1.i<>b2.i holds diff(b1,b2) = diff(b1,b2+*(i,
b1.i)) + 1;
begin :: The adherence of Segre cosets
definition
let I be non empty set;
let A be PLS-yielding ManySortedSet of I;
let B1,B2 be Segre-Coset of A;
pred B1 '||' B2 means
:: PENCIL_3:def 2
for x being Point of Segre_Product A st x in B1
ex y being Point of Segre_Product A st y in B2 & x,y are_collinear;
end;
theorem :: PENCIL_3:20
for I being non empty set for A being PLS-yielding ManySortedSet
of I for B1,B2 being Segre-Coset of A st B1 '||' B2 for f being Collineation of
Segre_Product A for C1,C2 being Segre-Coset of A st C1=f.:B1 & C2=f.:B2 holds
C1 '||' C2;
theorem :: PENCIL_3:21
for I being non empty set for A being PLS-yielding ManySortedSet
of I for B1,B2 being Segre-Coset of A st B1 misses B2 holds B1 '||' B2 iff for
b1,b2 being Segre-like non trivial-yielding ManySortedSubset of Carrier A st B1
= product b1 & B2 = product b2 holds indx(b1)=indx(b2) & ex r being Element of
I st r<>indx(b1) & (for i being Element of I st i<>r holds b1.i=b2.i) & for c1,
c2 being Point of A.r st b1.r = {c1} & b2.r = {c2} holds c1,c2 are_collinear;
theorem :: PENCIL_3:22
for I being finite non empty set for A being PLS-yielding
ManySortedSet of I st for i being Element of I holds A.i is connected for i
being Element of I for p being Point of A.i for b1,b2 being Segre-like non
trivial-yielding ManySortedSubset of Carrier A st product b2 is Segre-Coset of
A & b1=b2+*(i,{p}) & not p in b2.i ex D being FinSequence of bool the carrier
of Segre_Product A st D.1=product b1 & D.(len D)=product b2 & (for i being Nat
st i in dom D holds D.i is Segre-Coset of A) & for i being Nat st 1<=i & i Permutation of I means
:: PENCIL_3:def 3
for i,j
being Element of I holds it.i=j iff for B1 being Segre-Coset of A for b1,b2
being Segre-like non trivial-yielding ManySortedSubset of Carrier A st B1 =
product b1 & f.:B1 = product b2 holds indx(b1)=i implies indx(b2)=j;
end;
begin :: Canonical embeddings and automorphisms of Segre product
definition
let I be finite non empty set;
let A be PLS-yielding ManySortedSet of I such that
for i being Element of I holds A.i is strongly_connected;
let f be Collineation of Segre_Product A;
let b1 be Segre-like non trivial-yielding ManySortedSubset of Carrier A such
that
product b1 is Segre-Coset of A;
func canonical_embedding(f,b1) -> Function of A.indx(b1),A.(
permutation_of_indices(f).indx(b1)) means
:: PENCIL_3:def 4
it is isomorphic & for a being
ManySortedSet of I st a is Point of Segre_Product A & a in product b1 for b
being ManySortedSet of I st b=f.a holds b.(permutation_of_indices(f).indx(b1))=
it.(a.indx(b1));
end;
theorem :: PENCIL_3:26
for I being finite 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 f being Collineation of Segre_Product A for B1,B2 being Segre-Coset of A st
B1 misses B2 & B1 '||' B2 for b1,b2 being Segre-like non trivial-yielding
ManySortedSubset of Carrier A st product b1 = B1 & product b2 = B2 holds
canonical_embedding(f,b1) = canonical_embedding(f,b2);
theorem :: PENCIL_3:27
for I being finite 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 f being Collineation of Segre_Product A for b1,b2 being Segre-like non
trivial-yielding ManySortedSubset of Carrier A st product b1 is Segre-Coset of
A & product b2 is Segre-Coset of A & indx(b1)=indx(b2) holds
canonical_embedding(f,b1) = canonical_embedding(f,b2);
definition
let I be finite non empty set;
let A be PLS-yielding ManySortedSet of I such that
for i being Element of I holds A.i is strongly_connected;
let f be Collineation of Segre_Product A;
let i be Element of I;
func canonical_embedding(f,i) -> Function of A.i,A.(permutation_of_indices(f
).i) means
:: PENCIL_3:def 5
for b being Segre-like non trivial-yielding ManySortedSubset
of Carrier A st product b is Segre-Coset of A & indx(b)=i holds it=
canonical_embedding(f,b);
end;
theorem :: PENCIL_3:28
for I being finite 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 f being Collineation of Segre_Product A ex s being Permutation of I, B
being Function-yielding ManySortedSet of I st for i being Element of I holds (B
.i is Function of A.i,A.(s.i) & for m being Function of A.i,A.(s.i) st m=B.i
holds m is isomorphic) & for p being Point of Segre_Product A for a being
ManySortedSet of I st a=p for b being ManySortedSet of I st b=f.p for m being
Function of A.i,A.(s.i) st m=B.i holds b.(s.i)=m.(a.i);