LineConfigurations.lean`

GitHub source file

33 declarations, 0 contain sorry, 0 declared as axioms

Transverse projective line arrangements; Extension of finite tuples by additional distinct points

def OAI.Nagata.W06.LineArrangement.markedCoordinate line 21
Source documentation
Positive x-coordinate of mark s, where U=-x. The first mark of line zero is moved from 1 to k+1; every other first mark remains 1.
```
def markedCoordinate (k i : ℕ) (s : Fin k) : ℕ :=
…
```
theorem OAI.Nagata.W06.LineArrangement.markedCoordinate_pos line 24
theorem OAI.Nagata.W06.LineArrangement.markedCoordinate_zero line 30
theorem OAI.Nagata.W06.LineArrangement.markedCoordinate_of_ne_zero line 34
theorem OAI.Nagata.W06.LineArrangement.markedCoordinate_injective line 38
def OAI.Nagata.W06.LineArrangement.graphValue line 48
Source documentation
Affine graph of line i in the U-coordinate.
```
def graphValue (i : ℕ) (U : K) : K := (i : K) ^ 2 - (i : K) * U
```
def OAI.Nagata.W06.LineArrangement.lineValue line 51
Source documentation
The actual affine line equation evaluated at a point.
```
def lineValue (i : ℕ) (U Y : K) : K := Y - graphValue i U
```
Mentions: OAI.Nagata.W06.LineArrangement.graphValue
def OAI.Nagata.W06.LineArrangement.node line 54
Source documentation
The pairwise node of components i and j.
```
def node (i j : ℕ) : K × K := ((i : K) + (j : K), -(i : K) * (j : K))
```
def OAI.Nagata.W06.LineArrangement.markedPoint line 57
Source documentation
The k marked points of component i, in actual affine coordinates (U,Y).
```
def markedPoint (K : Type*) [Field K] (k : ℕ) (i s : Fin k) : K × K :=
…
```
theorem OAI.Nagata.W06.LineArrangement.graphValue_sub line 61
theorem OAI.Nagata.W06.LineArrangement.graphValue_at_node line 67
theorem OAI.Nagata.W06.LineArrangement.node_on_left line 72
theorem OAI.Nagata.W06.LineArrangement.node_on_right line 75
theorem OAI.Nagata.W06.LineArrangement.lineValue_at_node line 79
theorem OAI.Nagata.W06.LineArrangement.intersection_iff_node line 88
Source documentation
Distinct component graphs meet at precisely the explicitly specified node.
```
theorem intersection_iff_node (i j : ℕ) (hij : i ≠ j) (p : K × K) :
    (lineValue i p.1 p.2 = 0 ∧ lineValue j p.1 p.2 = 0) ↔ p = node i j := by
…
```
Mentions: OAI.Nagata.W06.LineArrangement.lineValue, OAI.Nagata.W06.LineArrangement.node
theorem OAI.Nagata.W06.LineArrangement.node_avoids_third line 108
Source documentation
No third distinct component passes through a pairwise node.
```
theorem node_avoids_third (i j l : ℕ) (hli : l ≠ i) (hlj : l ≠ j) :
    lineValue l (node (K := K) i j).1 (node (K := K) i j).2 ≠ 0 := by
…
```
Mentions: OAI.Nagata.W06.LineArrangement.lineValue, OAI.Nagata.W06.LineArrangement.node
theorem OAI.Nagata.W06.LineArrangement.no_triple_concurrence line 116
theorem OAI.Nagata.W06.LineArrangement.negative_mark_avoids_other_line line 123
Source documentation
Every negative-U mark on one component avoids every other component.
```
theorem negative_mark_avoids_other_line (i j v : ℕ) (hij : i ≠ j) (hv : 0 < v) :
    lineValue j (-(v : K)) (graphValue i (-(v : K))) ≠ 0 := by
…
```
Mentions: OAI.Nagata.W06.LineArrangement.lineValue, OAI.Nagata.W06.LineArrangement.graphValue
theorem OAI.Nagata.W06.LineArrangement.markedPoint_on_line line 132
theorem OAI.Nagata.W06.LineArrangement.markedPoint_avoids_other_line line 136
theorem OAI.Nagata.W06.LineArrangement.markedPoint_injective line 142
Source documentation
All k² displayed marked affine points are pairwise distinct.
```
theorem markedPoint_injective (k : ℕ) :
    Function.Injective (fun p : Fin k × Fin k => markedPoint K k p.1 p.2) := by
…
```
Mentions: OAI.Nagata.W06.LineArrangement.markedPoint
def OAI.Nagata.W06.LineArrangement.markedPoints line 160
Source documentation
The actual finite set of marked affine points.
```
def markedPoints (K : Type*) [Field K] (k : ℕ) : Finset (K × K) := by
…
```
theorem OAI.Nagata.W06.LineArrangement.card_markedPoints line 164
theorem OAI.Nagata.W06.LineArrangement.line_sets_injective line 171
Source documentation
The affine component sets are genuinely distinct, witnessed by U=-1.
```
theorem line_sets_injective :
    Function.Injective (fun i : ℕ => {p : K × K | lineValue i p.1 p.2 = 0}) := by
…
```
Mentions: OAI.Nagata.W06.LineArrangement.lineValue
theorem OAI.Nagata.W06.LineArrangement.markedCoordinate_le_succ line 193
Source documentation
Every marked positive x-coordinate is at most k+1.
```
theorem markedCoordinate_le_succ (k i : ℕ) (s : Fin k) :
    markedCoordinate k i s ≤ k + 1 := by
…
```
Mentions: OAI.Nagata.W06.LineArrangement.markedCoordinate
def OAI.Nagata.W06.LineArrangement.additionalPoint line 199
Source documentation
The extra point on line zero. For the triangle it is (-5,0).
```
def additionalPoint (K : Type*) [Field K] (k : ℕ) : K × K :=
…
```
theorem OAI.Nagata.W06.LineArrangement.additionalPoint_ne_mark line 205
Source documentation
The extra point differs from every one of the original k² marks.
```
theorem additionalPoint_ne_mark (k : ℕ) (i s : Fin k) :
    additionalPoint K k ≠ markedPoint K k i s := by
…
```
Mentions: OAI.Nagata.W06.LineArrangement.additionalPoint, OAI.Nagata.W06.LineArrangement.markedPoint
theorem OAI.Nagata.W06.LineArrangement.additionalPoint_not_mem_markedPoints line 214
theorem OAI.Nagata.W06.LineArrangement.additionalPoint_on_zero line 222
theorem OAI.Nagata.W06.LineArrangement.additionalPoint_avoids_other_line line 227
Source documentation
The extra point lies on no component other than component zero.
```
theorem additionalPoint_avoids_other_line (k j : ℕ) (hj : j ≠ 0) :
    lineValue j (additionalPoint K k).1 (additionalPoint K k).2 ≠ 0 := by
…
```
Mentions: OAI.Nagata.W06.LineArrangement.lineValue, OAI.Nagata.W06.LineArrangement.additionalPoint
theorem OAI.Nagata.W06.LineArrangement.additionalPoint_ne_node line 233
Source documentation
Its negative U-coordinate prevents coincidence with any positive pairwise node.
```
theorem additionalPoint_ne_node (k i j : ℕ) :
    additionalPoint K k ≠ node (K := K) i j := by
…
```
Mentions: OAI.Nagata.W06.LineArrangement.additionalPoint, OAI.Nagata.W06.LineArrangement.node
def OAI.Nagata.W06.LineArrangement.extendedMarkedPoints line 246
Source documentation
The concrete original marks together with the one extra point.
```
def extendedMarkedPoints (K : Type*) [Field K] (k : ℕ) : Finset (K × K) := by
…
```
theorem OAI.Nagata.W06.LineArrangement.card_insert_additionalPoint line 251
Source documentation
The explicit extra point increases the cardinality to k²+1.
```
theorem card_insert_additionalPoint (k : ℕ) :
    (extendedMarkedPoints K k).card = k ^ 2 + 1 := by
…
```
Mentions: OAI.Nagata.W06.LineArrangement.extendedMarkedPoints