English
There is a natural equivalence between the one-point compactification of a division ring K and the projectivization of the 2-dimensional K-space, i.e. the projective line over K.
Русский
Существует естественное эквивалентность одноточечной компактфикации K и проективационного пространства K^2, т. е. проективной линии над K.
LaTeX
$$$\\mathrm{OnePoint}(K)\\simeq \\mathbb{P}_K(K\\times K).$$$
Lean4
/-- The one-point compactification of a division ring `K` is equivalent to
the projectivization `ℙ K (K × K)`. -/
def equivProjectivization : OnePoint K ≃ ℙ K (K × K)
where
toFun p := p.elim (mk K (1, 0) (by simp)) (fun t ↦ mk K (t, 1) (by simp))
invFun
p :=
by
refine Projectivization.lift (fun u : { v : K × K // v ≠ 0 } ↦ if u.1.2 = 0 then ∞ else ((u.1.2)⁻¹ * u.1.1)) ?_ p
rintro ⟨-, hv⟩ ⟨⟨x, y⟩, hw⟩ t rfl
have ht : t ≠ 0 := by rintro rfl; simp at hv
by_cases h₀ : y = 0 <;> simp [h₀, ht, mul_assoc]
left_inv p := by cases p <;> simp
right_inv
p := by
induction p using ind with
| h p hp =>
obtain ⟨x, y⟩ := p
by_cases h₀ : y = 0 <;>
simp only [mk_eq_mk_iff', h₀, Projectivization.lift_mk, if_true, if_false, OnePoint.elim_infty,
OnePoint.elim_some, Prod.smul_mk, Prod.mk.injEq, smul_eq_mul, mul_zero, and_true]
· use x⁻¹
simp_all
· exact ⟨y⁻¹, rfl, inv_mul_cancel₀ h₀⟩
