search

felixwellen / synthetic-geometry

Synthetic geometry. Probably mostly algebraic geometry.
MIT License
23 stars 4 forks source link

Constancy of functions on P^n #27

Open MatthiasHu opened 1 year ago

MatthiasHu commented 1 year ago

This PR derives the fact that all functions ℙ n → ⟨ k ⟩ are constant from the special case n = 1 (which still needs to be formalized):

all-functions-constant :
  {n : ℕ} →
  ((f : ℙ one → ⟨ k ⟩) → 2-Constant f) →
  (f : ℙ n → ⟨ k ⟩) →
  2-Constant f

A little bit of reorganization was necessary for this: The "characterization of linear equivalence" and "standard points" parts of the LineThroughPoints file were moved to their own files. The StandardPoints file also contains a couple of lemmas now.

felixwellen commented 1 year ago

With a recent version of cubical, there seems to be a missing open AlgebraHoms in SQC.Consequences

felixwellen commented 1 year ago

Opened a PR for that: #28