WikiLean Articles · Brain · Recent changes · Proposals · Flags · Stats · About

Diff — Projective plane

Revision #1499 → #2152 · back to history

modifiedProjective plane (informal)272aded857ec
FieldFrom #1499To #2152
mathlib.decl—Configuration.ProjectivePlane
mathlib.match_kind—exact
mathlib.module—Mathlib.Combinatorics.Configuration
note—Mathlib defines `Configuration.ProjectivePlane P L` axiomatically as a nondegenerate configuration with `HasPoints`, `HasLines`, and a three-points-in-general-position witness.
status—formalized
modifiedProjective plane (incidence structure)3ce758e63f2c
FieldFrom #1499To #2152
mathlib.decl—Configuration.ProjectivePlane
mathlib.match_kind—exact
mathlib.module—Mathlib.Combinatorics.Configuration
note—The class `Configuration.ProjectivePlane` packages exactly the incidence axioms (any two points on a unique line, any two lines meet, three-point configuration).
status—formalized
modifiedOrder of a projective planeef4eac632731
FieldFrom #1499To #2152
mathlib.decl—Configuration.ProjectivePlane.order
mathlib.match_kind—exact
mathlib.module—Mathlib.Combinatorics.Configuration
note—`Configuration.ProjectivePlane.order P L` is defined as `lineCount L p - 1` for the chosen configuration point, with `lineCount_eq` showing it is one less than the number of lines through any point.
status—formalized
modifiedExtended Euclidean plane161091fd27a7
FieldFrom #1499To #2152
mathlib.decl——
mathlib.match_kind——
mathlib.module——
note—No formal construction of the projective completion of the Euclidean plane (with points-at-infinity / line-at-infinity) was found.
status—not_formalized
modifiedProjective Moulton planea488f61f8d73
FieldFrom #1499To #2152
mathlib.decl——
mathlib.match_kind——
mathlib.module——
note—Grep for `Moulton` returns no Mathlib match; the Moulton plane is not formalized.
status—not_formalized
modifiedProjective plane of order three9331249737aa
FieldFrom #1499To #2152
mathlib.decl—Configuration.ofField.instProjectivePlaneProjectivizationForallFinOfNatNatOfDecidableEq
mathlib.match_kind—generalization
mathlib.module—Mathlib.Combinatorics.Configuration
note—PG(2, ZMod 3) arises by specializing the general `Projectivization K (Fin 3 → K)` projective-plane instance to `K = ZMod 3`, but no dedicated decl for the thirteen-point plane exists.
status—partial
modifiedProjective plane over a division ring PG(2,K)c5f0ff1a0eef
FieldFrom #1499To #2152
mathlib.decl—Configuration.ofField.instProjectivePlaneProjectivizationForallFinOfNatNatOfDecidableEq
mathlib.match_kind—special_case
mathlib.module—Mathlib.Combinatorics.Configuration
note—Mathlib provides `ProjectivePlane (ℙ K (Fin 3 → K)) (ℙ K (Fin 3 → K))` only for `K` a field (with `DecidableEq`), not for a general division ring.
status—partial
modifiedHomogeneous coordinatesa20c4d8d42f5
FieldFrom #1499To #2152
mathlib.decl—Projectivization
mathlib.match_kind—generalization
mathlib.module—Mathlib.LinearAlgebra.Projectivization.Basic
note—`Projectivization K V` is the quotient of nonzero vectors by scalar action — exactly homogeneous coordinates — but the name `homogeneous coordinates` is not used.
status—partial
modifiedReal projective plane RP^2b65ae0dd03bc
FieldFrom #1499To #2152
mathlib.decl—Projectivization
mathlib.match_kind—generalization
mathlib.module—Mathlib.LinearAlgebra.Projectivization.Basic
note—`Projectivization ℝ (Fin 3 → ℝ)` realizes RP² and inherits the ProjectivePlane instance, but no dedicated `RP^2` abbreviation/decl exists in Mathlib.
status—partial
modifiedComplex projective plane CP^2479d1c2bca2e
FieldFrom #1499To #2152
mathlib.decl—Projectivization
mathlib.match_kind—generalization
mathlib.module—Mathlib.LinearAlgebra.Projectivization.Basic
note—Same as RP²: `Projectivization ℂ (Fin 3 → ℂ)` instantiates CP² as a projective plane, but Mathlib has no dedicated `CP^2` decl.
status—partial
modifiedQuaternionic projective plane HP^280dd12ca7cc7
FieldFrom #1499To #2152
mathlib.decl——
mathlib.match_kind——
mathlib.module——
note—Mathlib's `Configuration.ofField` projective-plane instance requires a field, so `Projectivization` over the (non-commutative) quaternions is not equipped as a projective plane.
status—not_formalized
modifiedField planes from finite fields7aeec8e4399f
FieldFrom #1499To #2152
mathlib.decl—Configuration.ofField.instProjectivePlaneProjectivizationForallFinOfNatNatOfDecidableEq
mathlib.match_kind—generalization
mathlib.module—Mathlib.Combinatorics.Configuration
note—The PG(2, F_q) instance is obtained as a specialization of Mathlib's general `Projectivization K (Fin 3 → K)` projective-plane instance for any field K.
status—partial
addedWedderburn's theorem (finite division ring is a field)fe837d34cdca
modifiedFano plane0f8e3a147bcb
FieldFrom #1499To #2152
mathlib.decl—Configuration.ofField.instProjectivePlaneProjectivizationForallFinOfNatNatOfDecidableEq
mathlib.match_kind—generalization
mathlib.module—Mathlib.Combinatorics.Configuration
note—Grep for `Fano` returns no match; the Fano plane is only obtainable as the special case `K = ZMod 2` of the PG(2,K) instance.
status—partial
modifiedDesargues' theorem characterization of vector-space planes12d73b3da0c6
FieldFrom #1499To #2152
mathlib.decl——
mathlib.match_kind——
mathlib.module——
note—No occurrences of `Desargues` in Mathlib; neither Desargues' theorem nor the characterization of Desarguesian planes is formalized.
status—not_formalized
modifiedNon-Desarguesian plane67bceb464755
FieldFrom #1499To #2152
mathlib.decl——
mathlib.match_kind——
mathlib.module——
note—No Mathlib match for non-Desarguesian planes.
status—not_formalized
modifiedSubplane7591ced3e5bf
FieldFrom #1499To #2152
mathlib.decl——
mathlib.match_kind——
mathlib.module——
note—Grep for `subplane`/`Subplane` returns no matches in Mathlib.
status—not_formalized
modifiedBruck's theorem on subplane ordersf3cf58501072
FieldFrom #1499To #2152
mathlib.decl——
mathlib.match_kind——
mathlib.module——
note—No notion of subplane in Mathlib, so Bruck's theorem cannot be stated.
status—not_formalized
modifiedBaer subplaneb5facf1442c8
FieldFrom #1499To #2152
mathlib.decl——
mathlib.match_kind——
mathlib.module——
note—No `Baer` subplane in Mathlib.
status—not_formalized
modifiedExistence of Baer subplanes in finite Desarguesian planese59ae1457cbf
FieldFrom #1499To #2152
mathlib.decl——
mathlib.match_kind——
mathlib.module——
note—Baer subplane existence is not formalized.
status—not_formalized
modifiedFano subplane28bead8dfa21
FieldFrom #1499To #2152
mathlib.decl——
mathlib.match_kind——
mathlib.module——
note—No notion of Fano subplane in Mathlib.
status—not_formalized
modifiedFano subplanes in PG(2,q)181a1cb2dfa7
FieldFrom #1499To #2152
mathlib.decl——
mathlib.match_kind——
mathlib.module——
note—Not formalized.
status—not_formalized
modifiedGleason's theorem on Fano subplanes43f79aa624cf
FieldFrom #1499To #2152
mathlib.decl——
mathlib.match_kind——
mathlib.module——
note—Gleason's theorem on Fano subplanes is absent from Mathlib.
status—not_formalized
modifiedAffine plane8d8ca3e6c970
FieldFrom #1499To #2152
mathlib.decl——
mathlib.match_kind——
mathlib.module——
note—Mathlib has `AffineSpace`/`AffineMap` but no axiomatic incidence-geometric `AffinePlane` class.
status—not_formalized
modifiedOrder of a finite affine plane799a771cc6fc
FieldFrom #1499To #2152
mathlib.decl——
mathlib.match_kind——
mathlib.module——
note—Absent because the underlying affine-plane definition is missing.
status—not_formalized
modifiedExistence equivalence of affine and projective planes of order N1283fab58902
FieldFrom #1499To #2152
mathlib.decl——
mathlib.match_kind——
mathlib.module——
note—Requires the missing AffinePlane axiomatic side; not formalized.
status—not_formalized
modifiedEmbedding of affine plane into K P^26fc225b8380d
FieldFrom #1499To #2152
mathlib.decl——
mathlib.match_kind——
mathlib.module——
note—No formal embedding `K^2 ↪ ℙ K (Fin 3 → K)` recorded as an incidence-geometric construction.
status—not_formalized
modifiedPlanar ternary ring629d3ae42363
FieldFrom #1499To #2152
mathlib.decl——
mathlib.match_kind——
mathlib.module——
note—Grep for `PlanarTernaryRing`/`ternaryRing` returns no matches.
status—not_formalized
addedCayley plane (octonionic projective plane)60a3a49c55fe
modifiedPappian plane880499636de9
FieldFrom #1499To #2152
mathlib.decl——
mathlib.match_kind——
mathlib.module——
note—Neither Pappus' theorem in projective planes nor Pappian planes are formalized.
status—not_formalized
modifiedMoufang planea4ac5406b34c
FieldFrom #1499To #2152
mathlib.decl——
mathlib.match_kind——
mathlib.module——
note—No `Moufang` plane in Mathlib.
status—not_formalized
modifiedConstruction of finite projective plane from PTR04cceb56c245
FieldFrom #1499To #2152
mathlib.decl——
mathlib.match_kind——
mathlib.module——
note—Not formalized — PTR construction is absent.
status—not_formalized
modifiedDegenerate plane558759f1f26c
FieldFrom #1499To #2152
mathlib.decl—Configuration.Nondegenerate
mathlib.match_kind—generalization
mathlib.module—Mathlib.Combinatorics.Configuration
note—Mathlib's `Configuration.Nondegenerate` class captures the negation, but there is no dedicated `Degenerate plane` decl enumerating the seven classes.
status—partial
modifiedCollineation58603862397c
FieldFrom #1499To #2152
mathlib.decl——
mathlib.match_kind——
mathlib.module——
note—No `Collineation` decl in Mathlib for projective planes.
status—not_formalized
modifiedFixed point and fixed line of a collineation12a0c3eb76ed
FieldFrom #1499To #2152
mathlib.decl——
mathlib.match_kind——
mathlib.module——
note—Without `Collineation`, fixed-point/fixed-line concepts for collineations are unformalized.
status—not_formalized
modifiedHomographya5351fb4affd
FieldFrom #1499To #2152
mathlib.decl——
mathlib.match_kind——
mathlib.module——
note—Grep finds no `Homography` in Mathlib (the projective-linear group is the closest, but it is not formalized as a homography of PG(2,K)).
status—not_formalized
modifiedAutomorphic collineation81e8b179419b
FieldFrom #1499To #2152
mathlib.decl——
mathlib.match_kind——
mathlib.module——
note—Not formalized.
status—not_formalized
modifiedFundamental theorem of projective geometry86204eb5e58a
FieldFrom #1499To #2152
mathlib.decl——
mathlib.match_kind——
mathlib.module——
note—No formal statement of the fundamental theorem of projective geometry.
status—not_formalized
modifiedPlane dual structure7e68353cf65b
FieldFrom #1499To #2152
mathlib.decl—Configuration.Dual
mathlib.match_kind—exact
mathlib.module—Mathlib.Combinatorics.Configuration
note—`Configuration.Dual` provides the type synonym swapping points and lines, with membership defined as `Function.swap`.
status—formalized
modifiedPlane dual statement0c908d797d09
FieldFrom #1499To #2152
mathlib.decl——
mathlib.match_kind——
mathlib.module——
note—There is no meta-level operation in Mathlib for forming the syntactic dual of a statement.
status—not_formalized
modifiedDual plane is a projective plane71e74246f4a2
FieldFrom #1499To #2152
mathlib.decl—Configuration.ProjectivePlane.instProjectivePlaneDual
mathlib.match_kind—exact
mathlib.module—Mathlib.Combinatorics.Configuration
note—Mathlib provides `instance : ProjectivePlane (Dual L) (Dual P)`, witnessing that the dual of a projective plane is a projective plane.
status—formalized
modifiedSelf-dual plane0fab3bd55899
FieldFrom #1499To #2152
mathlib.decl——
mathlib.match_kind——
mathlib.module——
note—No `SelfDual` projective plane definition in Mathlib.
status—not_formalized
modifiedPrinciple of plane duality1939042e6453
FieldFrom #1499To #2152
mathlib.decl——
mathlib.match_kind——
mathlib.module——
note—The metatheorem isn't formalized; only the structural duality instance exists.
status—not_formalized
modifiedDuality and correlationda3cedd2dd19
FieldFrom #1499To #2152
mathlib.decl——
mathlib.match_kind——
mathlib.module——
note—No `Duality`/`Correlation` map between a projective plane and its dual is defined in Mathlib.
status—not_formalized
modifiedReciprocity5c33bcfa788b
FieldFrom #1499To #2152
mathlib.decl——
mathlib.match_kind——
mathlib.module——
note—`Reciprocity` in the projective-plane sense is not in Mathlib (the matches refer to quadratic reciprocity).
status—not_formalized
modifiedPolarity4c7358ecd99e
FieldFrom #1499To #2152
mathlib.decl——
mathlib.match_kind——
mathlib.module——
note—No projective-geometric `Polarity` in Mathlib.
status—not_formalized
modifiedCounting in finite projective planesc7ddb799bb66
FieldFrom #1499To #2152
mathlib.decl—Configuration.ProjectivePlane.card_points_eq_card_lines
mathlib.match_kind—exact
mathlib.module—Mathlib.Combinatorics.Configuration
note—`card_points_eq_card_lines`, `card_points`, `card_lines`, `lineCount_eq`, and `pointCount_eq` together formalize the standard `N² + N + 1` counting in finite projective planes.
status—formalized
modifiedBruck–Ryser–Chowla theorem9f4da4039102
FieldFrom #1499To #2152
mathlib.decl——
mathlib.match_kind——
mathlib.module——
note—Bruck–Ryser–Chowla is not formalized in Mathlib.
status—not_formalized
modifiedProjective plane as Steiner systeme49c3135bc85
FieldFrom #1499To #2152
mathlib.decl——
mathlib.match_kind——
mathlib.module——
note—Mathlib has no `SteinerSystem`/`SteinerTripleSystem` definition.
status—not_formalized
modifiedMOLS and projective planes3a668ff16a1c
FieldFrom #1499To #2152
mathlib.decl——
mathlib.match_kind——
mathlib.module——
note—No MOLS / Latin-square infrastructure in Mathlib.
status—not_formalized
modifiedHigher-dimensional projective spaces are Desarguesian13ca22f7e83e
FieldFrom #1499To #2152
mathlib.decl——
mathlib.match_kind——
mathlib.module——
note—Desargues' theorem itself isn't formalized, so this consequence isn't either.
status—not_formalized
modifiedNon-embeddability of non-Desarguesian planes37c151477dc0
FieldFrom #1499To #2152
mathlib.decl——
mathlib.match_kind——
mathlib.module——
note—Depends on Desargues' theorem, which is absent from Mathlib.
status—not_formalized