:: 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;