A case study in formalizing projective geometry in Coq: Desargues theorem

Formalizing geometry theorems in a proof assistant like Coq is challenging. As emphasized in the literature, the non-degeneracy conditions lead to long technical proofs. In addition, when considering higher-dimensions, the amount of incidence relations (e.g. point–line, point–plane, line–plane) induce numerous technical lemmas. In this article, we investigate formalizing projective plane geometry as well as projective space geometry. We mainly focus on one of the fundamental properties of the projective space, namely Desargues property. We formally prove that it is independent of projective plane geometry axioms but can be derived from Pappus property in a two-dimensional setting. Regarding at least three-dimensional projective geometry, we present an original approach based on the notion of rank which allows to describe incidence and non-incidence relations such as equality, collinearity and coplanarity homogeneously. This approach allows to carry out proofs in a more systematic way and was successfully used to fairly easily formalize Desargues theorem in Coq. This illustrates the power and efficiency of our approach (using only ranks) to prove properties of the projective space.     

Desargues Theorem, Dynamics, and Hyperplane Arrangements

The Desargues theorem is a basic theorem in classical projective geometry. In this paper we generalize Desargues theorem in the direction of dynamical systems. Our result comprises an infinite family of configurations, having unbounded complexity. The proof of the result involves constructing special kinds of hyperplane arrangements and then projecting subsets of them into the plane.     

Ten Exceptional Geometries from Trivalent Distance Regular Graphs

The ten distance regular graphs of valency 3 and girth > 4 define ten non-isomorphic neighborhood geometries, amongst which a projective plane, a generalized quadrangle, two generalized hexagons, the tilde geometry, the Desargues configuration and the Pappus configuration. All these geometries are bislim, i.e., they have three points on each line and three lines through each point. We study properties of these geometries such as embedding rank, generating rank, representation in real spaces, alternative constructions. Our main result is a general construction method for homogeneous embeddings of flag transitive self-polar bislim geometries in real projective space.     

Placement of the Desargues configuration on a cubic curve

Hilbert and Cohn-Vossen once declared that the configurations of Desargues and Pappus are by far the most important projective configurations. These two are very similar in many respects: both are regular and self-dual, both could be constructed with ruler alone and hence exist over the rational plane, the final collinearity in both instances are automatic and both could be regarded as self-inscribed and self-circumscribed p9lygons (see [1, p. 128]). Nevertheless, there is one fundamental difference between these two configurations, viz. while the Pappus-Brianchon configuration can be realized as nine points on a non-singular cubic curve over the complex plane (in doubly infinite ways), it is impossible to get such a representation for the Desargues configuration. In fact, the configuration of Desargues can be placed in a projective plane in such a way that its vertices lie on a cubic curve over a field k if and only if k is of characteristic 2 and has at least 16 elements. Moreover, any cubic curve containing the vertices of this configuration must be singular.This research of all the three authors was supported by the HSERC of Canada.     

Steinberg triality groups acting on 2 - (v, k, 1) designs

A 2 - (v,k,1) design D = (P, B) is a system consisting of a finite set P of v points and a collection B of k-subsets of P, called blocks, such that each 2-subset of P is contained in precisely one block. Let G be an automorphism group of a 2- (v,k,1) design. Delandtsheer proved that if G is block-primitive and D is not a projective plane, then G is almost simple, that is, T ≤ G ≤ Aut(T), where T is a non-abelian simple group. In this paper, we prove that T is not isomorphic to 3D4(q). This paper is part of a project to classify groups and designs where the group acts primitively on the blocks of the design.     

A rational sextic associated with a Desargues configuration

In this paper we consider a Desargues configuration in the projective plane, i.e. ten points and ten lines, on each line we have three of the points and through each point we have three of the lines. We construct a rational curve of order 6 which has a node at each of the ten points. We have never seen this kind of curve in the literature, but it is well known that for anyn there exists a rational curve of ordern which has [(n–1)(n–2)]/2 nodes and ifn=6 we find a sextic with ten nodes. The purpose of this paper is to obtain a sextic of this kind as a locus of points in connection with special projectivities of the plane associated with the Desargues configuration and to find a rational parametric representation of it. A large part of this paper is done with MACSYMA: it is an application of computer algebra in algebraic geometry. Special cases, where we find a quintic, a quartic or a cubic, are given in the last section.     

The isostrophisms of planar ternary rings Part II

In Part I the family of ternary rings determined with respect to the base points A,B,C,D of a projective plane was considered, when the different members of the family are determined by permutations of A,B,C,D. Some of the algebraic relationships between the different rings were studied. In Part II these results are applied to problems of collineations. There is a large body of results relating the properties of ternary rings to collineations, and relating the existence of one set of collineations to the existence of others. Once several basic theorems are established many theorems involving collineations follow quite easily. The usual method of determining what a given collineation implies about a ternary ring is to compute the image points and image lines and see what results. That is not necessary for the collineations presented here using the techniques of isostrophisms.This research is included in the author's doctoral dissertation submitted to Temple University. The author would like to express his appreciation to Professor R. Artzy for his assistance in completing this work.     

On a theorem about projectivities

The main result of this paper is a theorem about projectivities in then-dimensional complex projective spaceP ⁿ (n 2). Puttingn = 2, we showed in [3] that the theorem of Desargues inP ⁿ is a special case of this theorem. And not only the theorem of Desargues but also the converse of the theorem of Pascal, the theorem of Pappus-Pascal, the theorem of Miquel, the Newton line, the Brocard points and a lot of lesser known results in the projective, the affine and the Euchdean plane were obtained from this theorem as special cases without any further proof. Many extensions of classical theorems in the projective, affine and Euclidean plane to higher dimensions can be found in the literature and probably some of these are special cases of this theorem inP ⁿ. We only give a few examples and leave it as an open problem which other special cases could be found.     

A remarkable configuration: A generalization of computergenerated results by S.-C. Chou and its connection with a plane figure by A. Emch

The paper's starting point are four theorems on conics which can be found in a collection of computer proved results by C.-S. Chou from 1987. It not only contains a generalization of two of Chou's results but also a plane figure consisting of points, lines and conics. A suitable notation will reveal a striking symmetry of this figure. Moreover, it turns out that a plane figure from 1940 found by A. Emch using algebraic methods is very similar to ours, which we obtained synthetically. As an application in finite geometry we have gone some way towards regarding our figure as a real projective model of the finite projective plane of order 4.Dedicated to Dr. J. F. Rigby on the occasion of his 65th birthday     

The isostrophisms of planar ternary rings part I

It is well known that a projective plane nay be coordinatized by picking four arbitrary, ordered points such that no three of them are collinear. This gives rise to an algebraic structure called the planar ternary ring T with respect to the base points A,B,C,D. The existence of certain collineations in the plane will be reflected by algebraic properties in T, and conversely. In this paper the interrelationships between certain algebraic properties in T, and the linearity of those ternary rings which are obtained from T and various permutations of A,B,C,D are considered. Many well known types of algebraic structures, such as quasifields and alternative division rings will occur if the ternary rings generated by suitable permutations of A,B,C,D are linear.This research is included in the author's doctoral dissertation submitted to Temple University. The author would like to express his appreciation to Professor R. Artzy for his assistance in completing this work.     

A constructive real projective plane

The classical theory of plane projective geometry is examined constructively, using both synthetic and analytic methods. The topics include Desargues’s Theorem, harmonic conjugates, projectivities, involutions, conics, Pascal’s Theorem, poles and polars. The axioms used for the synthetic treatment are constructive versions of the traditional axioms. The analytic construction is used to verify the consistency of the axiom system; it is based on the usual model in three-dimensional Euclidean space, using only constructive properties of the real numbers. The methods of strict constructivism, following principles put forward by Errett Bishop, reveal the hidden constructive content of a portion of classical geometry. A number of open problems remain for future studies.     

某些Lie单群的传递性

设D为有限线性空间，且T G Aut（T），其中T是非交换单群，并且同构于^2B2（g），Cn（g）（n≥3），^3D4（g），E7（q），E8（q），F4（q），^2F4（q），G2（q），^2G2（q）。假设D不是射影平面，G线传递作用在D上，则T点传递。     

Compact spreads and compact translation planes over locally compact fields

We prove that a spread S over a locally compact nondlscrete field F defines a topological translation plane if and only if the spread is compact. For F=R, this is implicit in Breuning's thesis [Bre], cf. [B 2]. For the proof, we describe the point set of the projective translation plane as a quotient space of some projective space, with identifications taking place in one hyperplane. This is new even for F=R.     

Finite Projective Geometries and Classification of the Weight Hierarchies of Codes （Ⅰ）

The weight hierarchy of a binary linear [n,κ] code C is the sequence (d1,d2,...,dκ), where dr is the smallest support of an r-dimensional subcode of C. The codes of dimension 4 are collected in classes and the possible weight hierarchies in each class is determined by finite projective geometries.The possible weight hierarchies in class A, B, C, D are determined in Part (Ⅰ). The possible weight hierarchies in class E, F, G, H, I are determined in Part (Ⅱ).     

G. Martens′ Dimension Theorem for Curves of Odd Gonality

For a smooth projective irreducible algebraic curve C of odd gonality, the maximal possible dimension of the variety of special linear systems W _d ^r (C) is d-3r by a result of M. Coppens et al. Furthermore it is known that if the maximum dimension of W(C) for a curve C of odd gonality is attained then C is of very special type of curves by the recent progress made by G. Martens. The purpose of this paper is to chase an extension of the result of G. Martens; if dim W(C)=d-3r-1 for a curve C of odd gonality for some dg-4 and r1, then C must be either a smooth plane sextic, a pentagonal curve of bounded genus or a smooth plane octic.     

Nilpotent block designs I: Basic concepts for Steiner triple and quadruple systems

This paper discusses the concepts of nilpotence and the center for Steiner Triple and Quadruple Systems. The discussion is couched in the language of block designs rather than algebras. Nilpotence is closely connected to the well known doubling and tripling constructions for these designs. A sample result: a point p in an STS is projective if every triangle containing p generates the 7-element Fano plane; the p-center of the STS is the set of all projective points and is a projective geometry over GF(2). © 1999 John Wiley & Sons, Inc. J Combin Designs 7: 157–171, 1999     

Collineations of projective planes of order 10, part I

No projective plane of order 10 has a collineation group of order 9 which fixes a 12-arc, a set of twelve points no three collinear, as a set. This fact, proved in Part I, is used to prove in Part II that the full collineation group of any projective plane of order 10 has order 1, 3, or 5.     

p-Adic Automorphic Functions for the Unitary Group in Three Variables

Let G be a special unitary group in three variables over a local field and, a co-compact subgroup of G. We construct, -automorphic functions on the rigid analytic space of points in the projective plane stable under the action of tori in G.This research was partially supported by an ARC grant.2000 Mathematics Subject Classification: 11F55, 11F85, 20G25, 22E35     

Desargues configurations: minors and ambient automorphisms

We determine all possible minors of the Desargues configuration, their embeddings in projective spaces, and their ambient automorphism groups (i.e., the group of all projective collineations that leave the embedded configuration invariant) in Pappian projective spaces. Examples show that the latter problem becomes hard if the extra condition (Pappian) is dropped.