:: A Projective Closure and Projective Horizon of an Affine Space
:: by Henryk Oryszczyszyn and Krzysztof Pra\.zmowski
::
:: Received December 17, 1990
:: Copyright (c) 1990-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 DIRAF, SUBSET_1, STRUCT_0, AFF_4, INCSP_1, AFF_1, ANALOAF,
RELAT_1, TARSKI, PARSP_1, XBOOLE_0, ARYTM_3, SETFAM_1, ZFMISC_1, EQREL_1,
RELAT_2, ANPROJ_1, INCPROJ, MCART_1, FDIFF_1, ANPROJ_2, AFF_2, VECTSP_1,
AFPROJ;
notations TARSKI, XBOOLE_0, ZFMISC_1, SUBSET_1, DOMAIN_1, EQREL_1, RELSET_1,
RELAT_1, RELAT_2, XTUPLE_0, MCART_1, STRUCT_0, ANALOAF, DIRAF, AFF_1,
AFF_4, AFF_2, PAPDESAF, INCSP_1, INCPROJ;
constructors DOMAIN_1, EQREL_1, AFF_1, AFF_2, TRANSLAC, INCPROJ, AFF_4,
RELSET_1, XTUPLE_0;
registrations XBOOLE_0, SUBSET_1, RELSET_1, STRUCT_0, INCPROJ, XTUPLE_0;
requirements SUBSET, BOOLE;
begin
reserve AS for AffinSpace;
reserve A,K,M,X,Y,Z,X9,Y9 for Subset of AS;
reserve zz for Element of AS;
reserve x,y for set;
:: The aim of this article is to formalize the well known construction of
:: the projective closure of an affine space. We begin with some evident
:: properties of planes in affine planes.
theorem :: AFPROJ:1
AS is AffinPlane & X=the carrier of AS implies X is being_plane;
theorem :: AFPROJ:2
AS is AffinPlane & X is being_plane implies X = the carrier of AS;
theorem :: AFPROJ:3
AS is AffinPlane & X is being_plane & Y is being_plane implies X= Y;
theorem :: AFPROJ:4
X=the carrier of AS & X is being_plane implies AS is AffinPlane;
theorem :: AFPROJ:5
not A // K & A '||' X & A '||' Y & K '||' X & K '||' Y & A is
being_line & K is being_line & X is being_plane & Y is being_plane implies X
'||' Y;
theorem :: AFPROJ:6
X is being_plane & A '||' X & X '||' Y implies A '||' Y;
:: Next we distinguish two sets, one consisting of the lines, the second
:: consisting of the planes of a given affine space and we consider two
:: equivalence relations defined on each of these sets; theses relations
:: are in fact the relation of parallelity restricted to suitable area.
:: Their equivalence classes are called directions (of lines and planes,
:: respectively); they are intended to be considered as new objects which
:: extend the given affine space to a projective space.
definition
let AS;
func AfLines(AS) -> Subset-Family of AS equals
:: AFPROJ:def 1
{A: A is being_line};
end;
definition
let AS;
func AfPlanes(AS) -> Subset-Family of AS equals
:: AFPROJ:def 2
{A: A is being_plane};
end;
theorem :: AFPROJ:7
for x holds (x in AfLines(AS) iff ex X st x=X & X is being_line);
theorem :: AFPROJ:8
for x holds (x in AfPlanes(AS) iff ex X st x=X & X is being_plane);
definition
let AS;
func LinesParallelity(AS) -> Equivalence_Relation of AfLines(AS) equals
:: AFPROJ:def 3
{[K,
M]: K is being_line & M is being_line & K '||' M};
end;
definition
let AS;
func PlanesParallelity(AS) -> Equivalence_Relation of AfPlanes(AS) equals
:: AFPROJ:def 4
{[
X,Y]: X is being_plane & Y is being_plane & X '||' Y};
end;
definition
let AS,X;
func LDir(X) -> Subset of AfLines(AS) equals
:: AFPROJ:def 5
Class(LinesParallelity(AS),X);
end;
definition
let AS,X;
func PDir(X) -> Subset of AfPlanes(AS) equals
:: AFPROJ:def 6
Class(PlanesParallelity(AS),X);
end;
theorem :: AFPROJ:9
X is being_line implies for x holds x in LDir(X) iff ex Y st x=Y
& Y is being_line & X '||' Y;
theorem :: AFPROJ:10
X is being_plane implies for x holds x in PDir(X) iff ex Y st x=
Y & Y is being_plane & X '||' Y;
theorem :: AFPROJ:11
X is being_line & Y is being_line implies (LDir(X)=LDir(Y) iff X // Y);
theorem :: AFPROJ:12
X is being_line & Y is being_line implies (LDir(X)=LDir(Y) iff X '||' Y);
theorem :: AFPROJ:13
X is being_plane & Y is being_plane implies (PDir(X)=PDir(Y) iff X '||' Y);
definition
let AS;
func Dir_of_Lines(AS) -> non empty set equals
:: AFPROJ:def 7
Class LinesParallelity(AS);
end;
definition
let AS;
func Dir_of_Planes(AS) -> non empty set equals
:: AFPROJ:def 8
Class PlanesParallelity(AS);
end;
theorem :: AFPROJ:14
for x holds x in Dir_of_Lines(AS) iff ex X st x=LDir(X) & X is being_line;
theorem :: AFPROJ:15
for x holds x in Dir_of_Planes(AS) iff ex X st x=PDir(X) & X is being_plane;
:: The point is to guarantee that the classes of new objects consist of really
:: new objects. Clearly the set of directions of lines and the set of affine
:: points do not intersect. However we cannot claim, in general, that the set
:: of affine lines and the set of directions of planes do not intersect; this
:: is evidently true only in the case of affine planes. Therefore we have to
:: modify (slightly) a construction of the set of lines of the projective
:: closure of affine space, when compared with (naive) intuitions.
theorem :: AFPROJ:16
the carrier of AS misses Dir_of_Lines(AS);
theorem :: AFPROJ:17
AS is AffinPlane implies AfLines(AS) misses Dir_of_Planes(AS);
theorem :: AFPROJ:18
for x holds (x in [:AfLines(AS),{1}:] iff ex X st x=[X,1] & X is being_line);
theorem :: AFPROJ:19
for x holds (x in [:Dir_of_Planes(AS),{2}:] iff ex X st x=[PDir(
X),2] & X is being_plane);
definition
let AS;
func ProjectivePoints(AS) -> non empty set equals
:: AFPROJ:def 9
(the carrier of AS) \/
Dir_of_Lines(AS);
end;
definition
let AS;
func ProjectiveLines(AS) -> non empty set equals
:: AFPROJ:def 10
[:AfLines(AS),{1}:] \/ [:
Dir_of_Planes(AS),{2}:];
end;
definition
let AS;
func Proj_Inc(AS) -> Relation of ProjectivePoints(AS),ProjectiveLines(AS)
means
:: AFPROJ:def 11
for x,y being object
holds [x,y] in it iff (ex K st K is being_line & y=[K,1]
& (x in the carrier of AS & x in K or x = LDir(K))) or ex K,X st K is
being_line & X is being_plane & x=LDir(K) & y=[PDir(X),2] & K '||' X;
end;
definition
let AS;
func Inc_of_Dir(AS) -> Relation of Dir_of_Lines(AS),Dir_of_Planes(AS) means
:: AFPROJ:def 12
for x,y being object
holds [x,y] in it iff ex A,X st x=LDir(A) & y=PDir(X) & A is
being_line & X is being_plane & A '||' X;
end;
definition
let AS;
func IncProjSp_of(AS) -> strict IncProjStr equals
:: AFPROJ:def 13
IncProjStr (#
ProjectivePoints(AS), ProjectiveLines(AS), Proj_Inc(AS) #);
end;
definition
let AS;
func ProjHorizon(AS) -> strict IncProjStr equals
:: AFPROJ:def 14
IncProjStr (#Dir_of_Lines(
AS), Dir_of_Planes(AS), Inc_of_Dir(AS) #);
end;
theorem :: AFPROJ:20
for x holds (x is POINT of IncProjSp_of(AS) iff (x is Element of
AS or ex X st x=LDir(X) & X is being_line));
theorem :: AFPROJ:21
x is Element of the Points of ProjHorizon(AS) iff ex X st x=LDir(X) &
X is being_line;
theorem :: AFPROJ:22
x is Element of the Points of ProjHorizon(AS) implies x is POINT
of IncProjSp_of(AS);
theorem :: AFPROJ:23
for x holds (x is LINE of IncProjSp_of(AS) iff ex X st (x=[X,1]
& X is being_line or x=[PDir(X),2] & X is being_plane));
theorem :: AFPROJ:24
x is Element of the Lines of ProjHorizon(AS) iff ex X st x=PDir(X) & X
is being_plane;
theorem :: AFPROJ:25
x is Element of the Lines of ProjHorizon(AS) implies [x,2] is
LINE of IncProjSp_of(AS);
reserve x,y,z,t,u,w for Element of AS;
reserve K,X,Y,Z,X9,Y9 for Subset of AS;
reserve a,b,c,d,p,q,r,p9 for POINT of IncProjSp_of(AS);
reserve A for LINE of IncProjSp_of(AS);
theorem :: AFPROJ:26
x=a & [X,1]=A implies (a on A iff X is being_line & x in X);
theorem :: AFPROJ:27
x=a & [PDir(X),2]=A implies not a on A;
theorem :: AFPROJ:28
a=LDir(Y) & [X,1]=A & Y is being_line & X is being_line implies
(a on A iff Y '||' X);
theorem :: AFPROJ:29
a=LDir(Y) & A=[PDir(X),2] & Y is being_line & X is being_plane
implies (a on A iff Y '||' X);
theorem :: AFPROJ:30
X is being_line & a=LDir(X) & A=[X,1] implies a on A;
theorem :: AFPROJ:31
X is being_line & Y is being_plane & X c= Y & a=LDir(X) & A=[
PDir(Y),2] implies a on A;
theorem :: AFPROJ:32
Y is being_plane & X c= Y & X9 // X & a=LDir(X9) & A=[PDir(Y),2]
implies a on A;
theorem :: AFPROJ:33
A=[PDir(X),2] & X is being_plane & a on A implies a is not Element of
AS;
theorem :: AFPROJ:34
A=[X,1] & X is being_line & p on A & p is not Element of AS implies p=LDir(X)
;
theorem :: AFPROJ:35
A=[X,1] & X is being_line & p on A & a on A & a<>p & not p is
Element of AS implies a is Element of AS;
theorem :: AFPROJ:36
for a being Element of the Points of ProjHorizon(AS),A being
Element of the Lines of ProjHorizon(AS) st a=LDir(X) & A=PDir(Y) & X is
being_line & Y is being_plane holds (a on A iff X '||' Y);
theorem :: AFPROJ:37
for a being Element of the Points of ProjHorizon(AS),a9 being
Element of the Points of IncProjSp_of(AS),A being Element of the Lines of
ProjHorizon(AS),A9 being LINE of IncProjSp_of(AS) st a9=a & A9=[A,2] holds (a
on A iff a9 on A9);
reserve A,K,M,N,P,Q for LINE of IncProjSp_of(AS);
theorem :: AFPROJ:38
for a,b being Element of the Points of ProjHorizon(AS), A,K
being Element of the Lines of ProjHorizon(AS) st a on A & a on K & b on A & b
on K holds a=b or A=K;
theorem :: AFPROJ:39
for A being Element of the Lines of ProjHorizon(AS) ex a,b,c
being Element of the Points of ProjHorizon(AS) st a on A & b on A & c on A & a
<>b & b<>c & c <>a;
theorem :: AFPROJ:40
for a,b being Element of the Points of ProjHorizon(AS) ex A
being Element of the Lines of ProjHorizon(AS) st a on A & b on A;
theorem :: AFPROJ:41
for x,y being Element of the Points of ProjHorizon(AS), X being
Element of the Lines of IncProjSp_of(AS) st x<>y & [x,X] in the Inc of
IncProjSp_of(AS) & [y,X] in the Inc of IncProjSp_of(AS) ex Y being Element of
the Lines of ProjHorizon(AS) st X=[Y,2];
theorem :: AFPROJ:42
for x being POINT of IncProjSp_of(AS),X being Element of the
Lines of ProjHorizon(AS) st [x,[X,2]] in the Inc of IncProjSp_of(AS) holds x is
Element of the Points of ProjHorizon(AS);
theorem :: AFPROJ:43
Y is being_plane & X is being_line & X9 is being_line & X c= Y &
X9 c= Y & P=[X,1] & Q=[X9,1] implies ex q st q on P & q on Q;
theorem :: AFPROJ:44
for a,b,c,d,p being Element of the Points of ProjHorizon(AS),M,N
,P,Q being Element of the Lines of ProjHorizon(AS) st a on M & b on M & c on N
& d on N & p on M & p on N & a on P & c on P & b on Q & d on Q & not p on P &
not p on Q & M<>N ex q being Element of the Points of ProjHorizon(AS) st q on P
& q on Q;
registration
let AS;
cluster IncProjSp_of(AS) -> partial linear up-2-dimensional up-3-rank
Vebleian;
end;
registration
cluster strict 2-dimensional for IncProjSp;
end;
registration
let AS be AffinPlane;
cluster IncProjSp_of(AS) -> 2-dimensional;
end;
theorem :: AFPROJ:45
IncProjSp_of(AS) is 2-dimensional implies AS is AffinPlane;
theorem :: AFPROJ:46
AS is not AffinPlane implies ProjHorizon(AS) is IncProjSp;
theorem :: AFPROJ:47
ProjHorizon(AS) is IncProjSp implies AS is not AffinPlane;
theorem :: AFPROJ:48
for M,N being Subset of AS, o,a,b,c,a9,b9,c9 being Element
of AS st M is being_line & N is being_line & M<>N & o in M & o in N
& o<>b & o<>b9 & o<>c9 & b in M & c in M & a9 in N & b9 in N & c9 in N & a,b9
// b,a9 & b,c9 // c,b9 & (a=b or b=c or a=c) holds a,c9 // c,a9;
theorem :: AFPROJ:49
IncProjSp_of(AS) is Pappian implies AS is Pappian;
theorem :: AFPROJ:50
for A,P,C being Subset of AS, o,a,b,c,a9,b9,c9 being Element
of AS st o in A & o in P & o in C & o<>a & o<>b & o<>c & a in A & b
in P & b9 in P & c in C & c9 in C & A is being_line & P is being_line & C is
being_line & A<>P & A<>C & a,b // a9,b9 & a,c // a9,c9 & (o=a9 or a=a9) holds b
,c // b9,c9;
theorem :: AFPROJ:51
IncProjSp_of(AS) is Desarguesian implies AS is Desarguesian;
theorem :: AFPROJ:52
IncProjSp_of(AS) is Fanoian implies AS is Fanoian;