English
If |P| = |L| and HasLines, there exists a HasPoints structure on (P,L); equivalently, there is a consistent selection of a point on each line and a line through each pair of points.
Русский
При равстве кардинальностей и наличии HasLines существует структура HasPoints на (P,L).
LaTeX
$$$\\text{HasPoints}(P,L)\\quad\\text{provided } |P|=|L|$$$
Lean4
/-- If a nondegenerate configuration has a unique line through any two points, and if `|P| = |L|`,
then there is a unique point on any two lines. -/
noncomputable def hasPoints [HasLines P L] [Fintype P] [Fintype L] (h : Fintype.card P = Fintype.card L) :
HasPoints P L :=
let this : ∀ l₁ l₂ : L, l₁ ≠ l₂ → ∃ p : P, p ∈ l₁ ∧ p ∈ l₂ := fun l₁ l₂ hl => by
classical
obtain ⟨f, _, hf2⟩ := HasLines.exists_bijective_of_card_eq h
haveI : Nontrivial L := ⟨⟨l₁, l₂, hl⟩⟩
haveI := Fintype.one_lt_card_iff_nontrivial.mp ((congr_arg _ h).mpr Fintype.one_lt_card)
have h₁ : ∀ p : P, 0 < lineCount L p := fun p =>
Exists.elim (exists_ne p) fun q hq =>
(congr_arg _ Nat.card_eq_fintype_card).mpr (Fintype.card_pos_iff.mpr ⟨⟨mkLine hq, (mkLine_ax hq).2⟩⟩)
have h₂ : ∀ l : L, 0 < pointCount P l := fun l => (congr_arg _ (hf2 l)).mpr (h₁ (f l))
obtain ⟨p, hl₁⟩ := Fintype.card_pos_iff.mp ((congr_arg _ Nat.card_eq_fintype_card).mp (h₂ l₁))
by_cases hl₂ : p ∈ l₂
· exact ⟨p, hl₁, hl₂⟩
have key' : Fintype.card { q : P // q ∈ l₂ } = Fintype.card { l : L // p ∈ l } :=
((HasLines.lineCount_eq_pointCount h hl₂).trans Nat.card_eq_fintype_card).symm.trans Nat.card_eq_fintype_card
have : ∀ q : { q // q ∈ l₂ }, p ≠ q := fun q hq => hl₂ ((congr_arg (· ∈ l₂) hq).mpr q.2)
let f : { q : P // q ∈ l₂ } → { l : L // p ∈ l } := fun q => ⟨mkLine (this q), (mkLine_ax (this q)).1⟩
have hf : Function.Injective f := fun q₁ q₂ hq =>
Subtype.ext
((eq_or_eq q₁.2 q₂.2 (mkLine_ax (this q₁)).2
((congr_arg (_ ∈ ·) (Subtype.ext_iff.mp hq)).mpr (mkLine_ax (this q₂)).2)).resolve_right
fun h => (congr_arg (p ∉ ·) h).mp hl₂ (mkLine_ax (this q₁)).1)
have key' := ((Fintype.bijective_iff_injective_and_card f).mpr ⟨hf, key'⟩).2
obtain ⟨q, hq⟩ := key' ⟨l₁, hl₁⟩
exact ⟨q, (congr_arg (_ ∈ ·) (Subtype.ext_iff.mp hq)).mp (mkLine_ax (this q)).2, q.2⟩
{ ‹HasLines P L› with
mkPoint := fun {l₁ l₂} hl => Classical.choose (this l₁ l₂ hl)
mkPoint_ax := fun {l₁ l₂} hl => Classical.choose_spec (this l₁ l₂ hl) }
