A Greedy Algorithm to Compute Arrangements of Lines in the Projective Plane

We introduce a greedy algorithm optimizing arrangements of lines with respect to a property. We apply this algorithm to the case of simpliciality: it recovers all known simplicial arrangements of lines in a very short time and also produces a yet unknown simplicial arrangement with 35 lines. We compute a (certainly incomplete) database of combinatorially simplicial complex arrangements of hyperplanes with up to 50 lines. Surprisingly, it contains several examples whose matroids have an infinite space of realizations up to projectivities.

Base Point Freeness, Uniqueness of Decompositions and Double Points for Veronese and Segre Varieties

We prove a base point freeness result for linear systems of forms vanishing at general double points of the projective plane. For tensors we study the uniqueness problem for the representation of a tensor as a sum of terms corresponding to points and tangent vectors of the Segre variety associated with the format of the tensor. We give complete results for unions of one point and one tangent vector.

Unbounded negativity on rational surfaces in positive characteristic

We give explicit blowups of the projective plane in positive characteristic that contain smooth rational curves of arbitrarily negative self-intersection, showing that the Bounded Negativity Conjecture fails even for rational surfaces in positive characteristic. As a consequence, we show that any surface in positive characteristic admits a birational model failing the Bounded Negativity Conjecture.

On homotopy nilpotency of the octonian plane $\mathbb{O}P^2$

Let $\mathbb{O}P^2_{(p)}$ be the $p$-localization of the Cayley projective plane $\mathbb{O}P^2$ for a prime $p$ or $p=0$. We show that the homotopy nilpotency class $\textrm{nil} \Omega(\mathbb{O}P^2_{(p)})<\infty $ for $p>2$ and $\textrm{nil} \Omega (\mathbb{O}P^2_{(p)})=1$ for $p>5$ or $p=0$. The homotopy nilpotency of remaining Rosenfeld projective planes are discussed as well.

Generalizing the Algebra of Throws to Rank-3 Matroids

<p>The algebra of throws is a geometric construction which reveals the underlying algebraic operations of addition and multiplication in a projective plane. In Desarguesian projective planes, the algebra of throws is a well-defined, commutative and associative binary operation. However, when we consider an analogous operation in a more general point-line configuration that comes from rank-3 matroids, none of these properties are guaranteed. We construct lists of forbidden configurations which give polynomial time checks for certain properties. Using these forbidden configurations, we can check whether a configuration has a group structure under this analogous operation. We look at the properties of configurations with such a group structure, and discuss their connection to the jointless Dowling geometries.</p>

Generalizing the Algebra of Throws to Rank-3 Matroids

<p>The algebra of throws is a geometric construction which reveals the underlying algebraic operations of addition and multiplication in a projective plane. In Desarguesian projective planes, the algebra of throws is a well-defined, commutative and associative binary operation. However, when we consider an analogous operation in a more general point-line configuration that comes from rank-3 matroids, none of these properties are guaranteed. We construct lists of forbidden configurations which give polynomial time checks for certain properties. Using these forbidden configurations, we can check whether a configuration has a group structure under this analogous operation. We look at the properties of configurations with such a group structure, and discuss their connection to the jointless Dowling geometries.</p>

A Mechanical Verification of the Independence of Tarski's Euclidean Axiom

<p>This thesis describes the mechanization of Tarski's axioms of plane geometry in the proof verification program Isabelle. The real Cartesian plane is mechanically verified to be a model of Tarski's axioms, thus verifying the consistency of the axiom system. The Klein–Beltrami model of the hyperbolic plane is also defined in Isabelle; in order to achieve this, the projective plane is defined and several theorems about it are proven. The Klein–Beltrami model is then shown in Isabelle to be a model of all of Tarski's axioms except his Euclidean axiom, thus mechanically verifying the independence of the Euclidean axiom — the primary goal of this project. For some of Tarski's axioms, only an insufficient or an inconvenient published proof was found for the theorem that states that the Klein–Beltrami model satisfies the axiom; in these cases, alternative proofs were devised and mechanically verified. These proofs are described in this thesis — most notably, the proof that the model satisfies the axiom of segment construction, and the proof that it satisfies the five-segments axiom. The proof that the model satisfies the upper 2-dimensional axiom also uses some of the lemmas that were used to prove that the model satisfies the five-segments axiom.</p>

A Mechanical Verification of the Independence of Tarski's Euclidean Axiom

<p>This thesis describes the mechanization of Tarski's axioms of plane geometry in the proof verification program Isabelle. The real Cartesian plane is mechanically verified to be a model of Tarski's axioms, thus verifying the consistency of the axiom system. The Klein–Beltrami model of the hyperbolic plane is also defined in Isabelle; in order to achieve this, the projective plane is defined and several theorems about it are proven. The Klein–Beltrami model is then shown in Isabelle to be a model of all of Tarski's axioms except his Euclidean axiom, thus mechanically verifying the independence of the Euclidean axiom — the primary goal of this project. For some of Tarski's axioms, only an insufficient or an inconvenient published proof was found for the theorem that states that the Klein–Beltrami model satisfies the axiom; in these cases, alternative proofs were devised and mechanically verified. These proofs are described in this thesis — most notably, the proof that the model satisfies the axiom of segment construction, and the proof that it satisfies the five-segments axiom. The proof that the model satisfies the upper 2-dimensional axiom also uses some of the lemmas that were used to prove that the model satisfies the five-segments axiom.</p>