MATHLIBANNEX / CANONICAL DECLARATION CARD

Finite projective incidence determines a semilinear equivalence

GSS Companion · Research Project · Source-bound exposition export

Card PDF · Version 1 · source-bound reader.

Card revision 1 · Exposition revision 1 · Version 1

Card identity

lfh:lfh-declaration-card:sha256:58fdb50ad0831bf924e6577a8d8a2957d8e27df94e24525f3860b86d681d1c27

Native Card SHA-256: 9e4b04cf36edb925862f694349f56eef15b7249ca2e3b2841361ce9453d09af5
Exposition SHA-256: 14dcd6e20d1ec8cc4d59dc4c4a542bd99d82e59c9bf3d87fee297cd610cc10cd
Original exposition text SHA-256: 2eddab83cfeea74d55bbda2525c3f47d3e0fa972c62cabbc13123752f24414a5

Source-bound exposition export (Markdown)
Export SHA-256: e8f8664fa977bb2c9188baadd39551e9a33fd03cd27faff224ee6e7617768bc6

Projectivization.exists_semilinearEquiv_of_finite_span

theorem

Realizes a finite-incidence-preserving projective bijection by a semilinear equivalence.

Statement

Let be fields, let be a -vector space, and let be an -vector space. Write for and for . These are the points of the projective spaces and , respectively. For , let be the set of lines in the algebraic linear span of representatives of . In particular, .

Suppose is a bijection and

(1)

If the cardinal-valued algebraic dimension of over is at least three, there exist a field isomorphism and an additive bijection such that

(2)

The scalar identity also holds at . Thus one semilinear equivalence realizes the prescribed projective bijection on every projective point.

Assumptions

Incidence is both preserved and reflected for every finite family, not merely for the chosen basis rays. The dimension assumption means that three linearly independent vectors exist; it does not assert finite dimensionality. The spaces need no norms, inner products, or topology, and the two fields need not coincide. No assumption on the characteristic is made.

Conclusion

This is a version of the fundamental theorem of projective geometry.

The same pair works for all nonzero representatives. The semilinear equivalence includes its -semilinear inverse . In particular,

(3)

The declaration asserts existence, not uniqueness of the choices. It imposes no involution, compatibility with an involution, or continuity condition on .

Main citations

The finite-incidence realization theorem gives one field isomorphism and one semilinear equivalence realizing every projective point. The semilinear equivalence construction includes the inverse over the inverse field isomorphism.

Lean source signature (exact)

The declaration prefix below is a contiguous source excerpt, ending before its proof assignment.

theorem exists_semilinearEquiv_of_finite_span
    (e : ℙ K V ≃ ℙ L W)
    (he : ∀ (T : Set (ℙ K V)), T.Finite → ∀ p,
      p ∈ Subspace.span T ↔ e p ∈ Subspace.span (e '' T))
    (hdim : 3 ≤ Module.rank K V) :
    ∃ σ : K ≃+* L, ∃ U : V ≃ₛₗ[σ.toRingHom] W,
      ∀ (v : V) (hv : v ≠ 0), e (mk K v hv) =
        mk L (U v) (by simpa only [map_zero] using U.injective.ne hv)
In the source Mathematical meaning
Exact declarationK, L, V, W and their ambient instances Two fields and their vector spaces; neither finite dimensionality nor an analytic structure is present.
Exact declaratione : ℙ K V ≃ ℙ L W The prescribed projective bijection, not a lift constructed in advance.
Exact declarationhe, with T.Finite and arbitrary p Both directions of (1), using the algebraic projective span, for every finite and every , including .
Exact declarationhdim : 3 ≤ Module.rank K V The cardinal-valued dimension is at least three; infinite-dimensional spaces are allowed.
Exact declaration∃ σ : K ≃+* L, ∃ U : V ≃ₛₗ[σ.toRingHom] W One field isomorphism and one additive bijection with . Its inverse is semilinear over .
Exact declaration∀ (v : V) (hv : v ≠ 0), e (mk K v hv) = ... The equality for every , with the same and throughout. The vector is nonzero, so the right-hand projective point is defined.

The following source context is separate from the declaration prefix. The later comment at lines 535–536 is not part of this declaration.

Exact surrounding source context (separate excerpts)

Source lines 38–41:

universe uK uL uV uW uI
variable {K : Type uK} {L : Type uL} {V : Type uV} {W : Type uW}
variable [Field K] [Field L]
variable [AddCommGroup V] [Module K V] [AddCommGroup W] [Module L W]

Source lines 44–47:

local instance (σ : K ≃+* L) : RingHomInvPair σ.toRingHom σ.symm.toRingHom :=
  RingHomInvPair.of_ringEquiv σ
local instance (σ : K ≃+* L) : RingHomInvPair σ.symm.toRingHom σ.toRingHom :=
  RingHomInvPair.of_ringEquiv_symm σ

Read exact source with highlighted declaration · Raw UTF-8 source · LFH Companion ·

Technical documentation

Exact declaration for the source guide
theorem exists_semilinearEquiv_of_finite_span
    (e : ℙ K V ≃ ℙ L W)
    (he : ∀ (T : Set (ℙ K V)), T.Finite → ∀ p,
      p ∈ Subspace.span T ↔ e p ∈ Subspace.span (e '' T))
    (hdim : 3 ≤ Module.rank K V) :
    ∃ σ : K ≃+* L, ∃ U : V ≃ₛₗ[σ.toRingHom] W,
      ∀ (v : V) (hv : v ≠ 0), e (mk K v hv) =
        mk L (U v) (by simpa only [map_zero] using U.injective.ne hv) := by
Back to the reading-guide item
Exact declaration for the source guide
theorem exists_semilinearEquiv_of_finite_span
    (e : ℙ K V ≃ ℙ L W)
    (he : ∀ (T : Set (ℙ K V)), T.Finite → ∀ p,
      p ∈ Subspace.span T ↔ e p ∈ Subspace.span (e '' T))
    (hdim : 3 ≤ Module.rank K V) :
    ∃ σ : K ≃+* L, ∃ U : V ≃ₛₗ[σ.toRingHom] W,
      ∀ (v : V) (hv : v ≠ 0), e (mk K v hv) =
        mk L (U v) (by simpa only [map_zero] using U.injective.ne hv) := by
Back to the reading-guide item
Exact declaration for the source guide
theorem exists_semilinearEquiv_of_finite_span
    (e : ℙ K V ≃ ℙ L W)
    (he : ∀ (T : Set (ℙ K V)), T.Finite → ∀ p,
      p ∈ Subspace.span T ↔ e p ∈ Subspace.span (e '' T))
    (hdim : 3 ≤ Module.rank K V) :
    ∃ σ : K ≃+* L, ∃ U : V ≃ₛₗ[σ.toRingHom] W,
      ∀ (v : V) (hv : v ≠ 0), e (mk K v hv) =
        mk L (U v) (by simpa only [map_zero] using U.injective.ne hv) := by
Back to the reading-guide item
Exact declaration for the source guide
theorem exists_semilinearEquiv_of_finite_span
    (e : ℙ K V ≃ ℙ L W)
    (he : ∀ (T : Set (ℙ K V)), T.Finite → ∀ p,
      p ∈ Subspace.span T ↔ e p ∈ Subspace.span (e '' T))
    (hdim : 3 ≤ Module.rank K V) :
    ∃ σ : K ≃+* L, ∃ U : V ≃ₛₗ[σ.toRingHom] W,
      ∀ (v : V) (hv : v ≠ 0), e (mk K v hv) =
        mk L (U v) (by simpa only [map_zero] using U.injective.ne hv) := by
Back to the reading-guide item
Exact declaration for the source guide
theorem exists_semilinearEquiv_of_finite_span
    (e : ℙ K V ≃ ℙ L W)
    (he : ∀ (T : Set (ℙ K V)), T.Finite → ∀ p,
      p ∈ Subspace.span T ↔ e p ∈ Subspace.span (e '' T))
    (hdim : 3 ≤ Module.rank K V) :
    ∃ σ : K ≃+* L, ∃ U : V ≃ₛₗ[σ.toRingHom] W,
      ∀ (v : V) (hv : v ≠ 0), e (mk K v hv) =
        mk L (U v) (by simpa only [map_zero] using U.injective.ne hv) := by
Back to the reading-guide item
Exact declaration for the source guide
theorem exists_semilinearEquiv_of_finite_span
    (e : ℙ K V ≃ ℙ L W)
    (he : ∀ (T : Set (ℙ K V)), T.Finite → ∀ p,
      p ∈ Subspace.span T ↔ e p ∈ Subspace.span (e '' T))
    (hdim : 3 ≤ Module.rank K V) :
    ∃ σ : K ≃+* L, ∃ U : V ≃ₛₗ[σ.toRingHom] W,
      ∀ (v : V) (hv : v ≠ 0), e (mk K v hv) =
        mk L (U v) (by simpa only [map_zero] using U.injective.ne hv) := by
Back to the reading-guide item