LineBases.lean`

34 declarations, 0 contain sorry, 0 declared as axioms

Polynomial coordinates and bases on a projective line

abbrev OAI.Nagata.W01.ProjectivePlaneVector line 20
theorem OAI.Nagata.W01.projective_representatives_pair_independent line 23
Source documentation
Distinct projective points have linearly independent actual representatives.
```
theorem projective_representatives_pair_independent
    (p q : Projectivization K (ProjectivePlaneVector K)) (hpq : p ≠ q) :
    LinearIndependent K ![p.rep, q.rep] := by
…
```
Mentions: OAI.Nagata.W01.ProjectivePlaneVector

theorem OAI.Nagata.W01.exists_projective_line_basis line 35

Source documentation

Two distinct points on an actual projective line extend to a basis whose third vector has linear-form value one. The first two representatives are unchanged.

theorem exists_projective_line_basis
    (L : ProjectivePlaneVector K →ₗ[K] K) (hL : L ≠ 0)
    (p q : Projectivization K (ProjectivePlaneVector K))
    (hpq : p ≠ q) (hp : L p.rep = 0) (hq : L q.rep = 0) :
    ∃ b : Basis (Fin 3) K (ProjectivePlaneVector K),
      b 0 = p.rep ∧ b 1 = q.rep ∧ L (b 2) = 1 := by
…

Mentions: OAI.Nagata.W01.ProjectivePlaneVector

theorem OAI.Nagata.W01.adapted_basis_third_coordinate line 69

Source documentation

In an adapted actual basis, linear-form evaluation is exactly the third coordinate.

theorem adapted_basis_third_coordinate
    (L : ProjectivePlaneVector K →ₗ[K] K)
    (b : Basis (Fin 3) K (ProjectivePlaneVector K))
    (h0 : L (b 0) = 0) (h1 : L (b 1) = 0) (h2 : L (b 2) = 1)
    (v : ProjectivePlaneVector K) : b.repr v 2 = L v := by
…

Mentions: OAI.Nagata.W01.ProjectivePlaneVector

theorem OAI.Nagata.W01.adapted_basis_mem_line_iff line 79

Source documentation

The actual projective line is precisely the zero third-coordinate plane.

theorem adapted_basis_mem_line_iff
    (L : ProjectivePlaneVector K →ₗ[K] K)
    (b : Basis (Fin 3) K (ProjectivePlaneVector K))
    (h0 : L (b 0) = 0) (h1 : L (b 1) = 0) (h2 : L (b 2) = 1)
    (v : ProjectivePlaneVector K) : L v = 0 ↔ b.repr v 2 = 0 := by
…

Mentions: OAI.Nagata.W01.ProjectivePlaneVector

theorem OAI.Nagata.W01.exists_three_projective_zeros_basis line 88

Source documentation

Three distinct zeros of a nonzero projective linear form admit the exact normalization needed for binary polynomial restriction, with neither coefficient zero.

theorem exists_three_projective_zeros_basis
    (L : ProjectivePlaneVector K →ₗ[K] K) (hL : L ≠ 0)
    (p₀ p₁ p₂ : Projectivization K (ProjectivePlaneVector K))
    (h01 : p₀ ≠ p₁) (h20 : p₂ ≠ p₀) (h21 : p₂ ≠ p₁)
    (h0 : L p₀.rep = 0) (h1 : L p₁.rep = 0) (h2 : L p₂.rep = 0) :
    ∃ (b : Basis (Fin 3) K (ProjectivePlaneVector K)) (a c : K),
      b 0 = p₀.rep ∧ b 1 = p₁.rep ∧ L (b 2) = 1 ∧
      a ≠ 0 ∧ c ≠ 0 ∧ p₂.rep = a • b 0 + c • b 1 := by
…

Mentions: OAI.Nagata.W01.ProjectivePlaneVector

abbrev OAI.Nagata.W01.PlanePolynomial line 133
abbrev OAI.Nagata.W01.ComplexPlaneVector line 134
def OAI.Nagata.W01.linearCoordinate line 137
Source documentation
The jth coordinate linear polynomial of an actual linear map.
```
def linearCoordinate (T : ComplexPlaneVector →ₗ[ℂ] ComplexPlaneVector) (j : Fin 3) :
    PlanePolynomial := ∑ i : Fin 3, C (T (Pi.single i 1) j) * X i
```
Mentions: OAI.Nagata.W01.ComplexPlaneVector, OAI.Nagata.W01.PlanePolynomial
def OAI.Nagata.W01.linearSubstitution line 141
Source documentation
Literal substitution of the three coordinate linear forms.
```
def linearSubstitution (T : ComplexPlaneVector →ₗ[ℂ] ComplexPlaneVector) :
    PlanePolynomial →ₐ[ℂ] PlanePolynomial := aeval (linearCoordinate T)
```
Mentions: OAI.Nagata.W01.ComplexPlaneVector, OAI.Nagata.W01.PlanePolynomial, OAI.Nagata.W01.linearCoordinate
theorem OAI.Nagata.W01.linearSubstitution_X line 144
theorem OAI.Nagata.W01.eval_linearCoordinate line 149
Source documentation
Evaluation of a coordinate polynomial is the corresponding coordinate of T(v).
```
theorem eval_linearCoordinate (T : ComplexPlaneVector →ₗ[ℂ] ComplexPlaneVector)
    (v : ComplexPlaneVector) (j : Fin 3) :
    eval v (linearCoordinate T j) = T v j := by
…
```
Mentions: OAI.Nagata.W01.ComplexPlaneVector, OAI.Nagata.W01.linearCoordinate
theorem OAI.Nagata.W01.eval_linearSubstitution line 163
Source documentation
Actual polynomial evaluation commutes with the actual linear coordinate map.
```
theorem eval_linearSubstitution (T : ComplexPlaneVector →ₗ[ℂ] ComplexPlaneVector)
    (P : PlanePolynomial) (v : ComplexPlaneVector) :
    eval v (linearSubstitution T P) = eval (T v) P := by
…
```
Mentions: OAI.Nagata.W01.ComplexPlaneVector, OAI.Nagata.W01.PlanePolynomial, OAI.Nagata.W01.linearSubstitution
theorem OAI.Nagata.W01.linearSubstitution_inverse line 174
Source documentation
The inverse coordinate map reverses substitution on actual polynomials.
```
theorem linearSubstitution_inverse
    (e : ComplexPlaneVector ≃ₗ[ℂ] ComplexPlaneVector) (P : PlanePolynomial) :
    linearSubstitution e.symm.toLinearMap (linearSubstitution e.toLinearMap P) = P := by
…
```
Mentions: OAI.Nagata.W01.ComplexPlaneVector, OAI.Nagata.W01.PlanePolynomial, OAI.Nagata.W01.linearSubstitution
def OAI.Nagata.W01.polynomialCoordinateEquiv line 184
Source documentation
Genuine invertible polynomial coordinate substitution.
```
def polynomialCoordinateEquiv (e : ComplexPlaneVector ≃ₗ[ℂ] ComplexPlaneVector) :
    PlanePolynomial ≃ₐ[ℂ] PlanePolynomial :=
…
```
Mentions: OAI.Nagata.W01.ComplexPlaneVector, OAI.Nagata.W01.PlanePolynomial
theorem OAI.Nagata.W01.polynomialCoordinateEquiv_apply line 196
theorem OAI.Nagata.W01.linearCoordinate_homogeneous line 200
theorem OAI.Nagata.W01.linearSubstitution_homogeneous line 208
Source documentation
Linear coordinate substitution preserves the exact homogeneous degree.
```
theorem linearSubstitution_homogeneous
    (T : ComplexPlaneVector →ₗ[ℂ] ComplexPlaneVector) {P : PlanePolynomial} {d : ℕ}
    (hP : P.IsHomogeneous d) : (linearSubstitution T P).IsHomogeneous d := by
…
```
Mentions: OAI.Nagata.W01.ComplexPlaneVector, OAI.Nagata.W01.PlanePolynomial, OAI.Nagata.W01.linearSubstitution
theorem OAI.Nagata.W01.polynomialCoordinateEquiv_homogeneous_iff line 216
Source documentation
Invertible linear coordinates preserve and reflect homogeneous degree.
```
theorem polynomialCoordinateEquiv_homogeneous_iff
    (e : ComplexPlaneVector ≃ₗ[ℂ] ComplexPlaneVector) (P : PlanePolynomial) (d : ℕ) :
    (polynomialCoordinateEquiv e P).IsHomogeneous d ↔ P.IsHomogeneous d := by
…
```
Mentions: OAI.Nagata.W01.ComplexPlaneVector, OAI.Nagata.W01.PlanePolynomial, OAI.Nagata.W01.polynomialCoordinateEquiv
theorem OAI.Nagata.W01.polynomialCoordinateEquiv_dvd_iff line 226
Source documentation
Divisibility is preserved and reflected by the actual coordinate automorphism.
```
theorem polynomialCoordinateEquiv_dvd_iff
    (e : ComplexPlaneVector ≃ₗ[ℂ] ComplexPlaneVector) (P Q : PlanePolynomial) :
    polynomialCoordinateEquiv e P ∣ polynomialCoordinateEquiv e Q ↔ P ∣ Q := by
…
```
Mentions: OAI.Nagata.W01.ComplexPlaneVector, OAI.Nagata.W01.PlanePolynomial, OAI.Nagata.W01.polynomialCoordinateEquiv
def OAI.Nagata.W01.basisPolynomialChange line 236
Source documentation
Basis coordinates send a coordinate vector to the corresponding original vector.
```
def basisPolynomialChange (b : Basis (Fin 3) ℂ ComplexPlaneVector) :
    PlanePolynomial ≃ₐ[ℂ] PlanePolynomial := polynomialCoordinateEquiv b.equivFun.symm
```
Mentions: OAI.Nagata.W01.ComplexPlaneVector, OAI.Nagata.W01.PlanePolynomial, OAI.Nagata.W01.polynomialCoordinateEquiv
theorem OAI.Nagata.W01.basisPolynomialChange_eval line 239
theorem OAI.Nagata.W01.basisPolynomialChange_X line 245
Source documentation
The literal requested sum-of-coordinates substitution on each variable.
```
theorem basisPolynomialChange_X
    (b : Basis (Fin 3) ℂ ComplexPlaneVector) (j : Fin 3) :
    basisPolynomialChange b (X j) = ∑ i : Fin 3, C (b i j) * X i := by
…
```
Mentions: OAI.Nagata.W01.ComplexPlaneVector, OAI.Nagata.W01.basisPolynomialChange
theorem OAI.Nagata.W01.basisPolynomialChange_homogeneous_iff line 270
theorem OAI.Nagata.W01.basisPolynomialChange_dvd_iff line 275
theorem OAI.Nagata.W01.basisPolynomialChange_eq_eval₂ line 281
Source documentation
The coordinate automorphism equals the literal requested polynomial substitution.
```
theorem basisPolynomialChange_eq_eval₂
    (b : Basis (Fin 3) ℂ ComplexPlaneVector) (P : PlanePolynomial) :
    basisPolynomialChange b P =
      eval₂ C (fun j => ∑ i : Fin 3, C (b i j) * X i) P := by
…
```
Mentions: OAI.Nagata.W01.ComplexPlaneVector, OAI.Nagata.W01.PlanePolynomial, OAI.Nagata.W01.basisPolynomialChange
def OAI.Nagata.W01.basisProjectiveMap line 293
Source documentation
A genuine linear coordinate change induces an injective actual projective map.
```
def basisProjectiveMap (b : Basis (Fin 3) ℂ ComplexPlaneVector) :
    Projectivization ℂ ComplexPlaneVector → Projectivization ℂ ComplexPlaneVector :=
…
```
Mentions: OAI.Nagata.W01.ComplexPlaneVector
theorem OAI.Nagata.W01.basisProjectiveMap_injective line 297

theorem OAI.Nagata.W01.basisProjectiveMap_eq_mk line 302

Source documentation

The projective coordinate map is computed from the actual chosen representative.

theorem basisProjectiveMap_eq_mk
    (b : Basis (Fin 3) ℂ ComplexPlaneVector) (p : Projectivization ℂ ComplexPlaneVector)
    (v : ComplexPlaneVector) (hv : v ≠ 0) (hcoord : b.equivFun p.rep = v) :
    basisProjectiveMap b p = Projectivization.mk ℂ v hv := by
…

Mentions: OAI.Nagata.W01.ComplexPlaneVector, OAI.Nagata.W01.basisProjectiveMap

theorem OAI.Nagata.W01.basis_equivFun_vector line 311
Source documentation
Coordinate values of the original basis vectors are exact, not merely proportional.
```
theorem basis_equivFun_vector (b : Basis (Fin 3) ℂ ComplexPlaneVector) (i : Fin 3) :
    b.equivFun (b i) = Pi.single i 1 := by
…
```
Mentions: OAI.Nagata.W01.ComplexPlaneVector

theorem OAI.Nagata.W01.exists_three_projective_zero_coordinates line 317

Source documentation

The third projective zero has two nonzero actual coordinates on the normalized line.

theorem exists_three_projective_zero_coordinates
    (L : ComplexPlaneVector →ₗ[ℂ] ℂ) (hL : L ≠ 0)
    (p₀ p₁ p₂ : Projectivization ℂ ComplexPlaneVector)
    (h01 : p₀ ≠ p₁) (h20 : p₂ ≠ p₀) (h21 : p₂ ≠ p₁)
    (h0 : L p₀.rep = 0) (h1 : L p₁.rep = 0) (h2 : L p₂.rep = 0) :
    ∃ (b : Basis (Fin 3) ℂ ComplexPlaneVector) (a c : ℂ),
      b 0 = p₀.rep ∧ b 1 = p₁.rep ∧ L (b 2) = 1 ∧ a ≠ 0 ∧ c ≠ 0 ∧
      b.equivFun p₀.rep = ![1, 0, 0] ∧
      b.equivFun p₁.rep = ![0, 1, 0] ∧ b.equivFun p₂.rep = ![a, c, 0] := by
…

Mentions: OAI.Nagata.W01.ComplexPlaneVector

theorem OAI.Nagata.W01.basisPolynomialChange_eval_at_coordinates line 341
Source documentation
An arbitrary polynomial has the same value in normalized coordinates and at the original genuine representative; in particular vanishing is transported.
```
theorem basisPolynomialChange_eval_at_coordinates
    (b : Basis (Fin 3) ℂ ComplexPlaneVector) (P : PlanePolynomial)
    (p : Projectivization ℂ ComplexPlaneVector) (v : ComplexPlaneVector)
    (hv : b.equivFun p.rep = v) :
    eval v (basisPolynomialChange b P) = eval p.rep P := by
…
```
Mentions: OAI.Nagata.W01.ComplexPlaneVector, OAI.Nagata.W01.PlanePolynomial, OAI.Nagata.W01.basisPolynomialChange
theorem OAI.Nagata.W01.basisPolynomialChange_linearForm_eq_X_two line 350
Source documentation
The transformed actual linear form is exactly the third variable when the basis has linear-form values 0,0,1.
```
theorem basisPolynomialChange_linearForm_eq_X_two
    (b : Basis (Fin 3) ℂ ComplexPlaneVector)
    (L : ComplexPlaneVector →ₗ[ℂ] ℂ) (P : PlanePolynomial)
    (hP : ∀ v, eval v P = L v)
    (h0 : L (b 0) = 0) (h1 : L (b 1) = 0) (h2 : L (b 2) = 1) :
    basisPolynomialChange b P = X 2 := by
…
```
Mentions: OAI.Nagata.W01.ComplexPlaneVector, OAI.Nagata.W01.PlanePolynomial, OAI.Nagata.W01.basisPolynomialChange

theorem OAI.Nagata.W01.exists_homogeneous_line_normalization line 380

Source documentation

An actual projective linear equation and three distinct zeros admit the proved coordinate arrangement and the literal equation X2, retaining both first reps.

theorem exists_homogeneous_line_normalization
    (P : PlanePolynomial) (hP : P.IsHomogeneous 1) (hne : P ≠ 0)
    (p₀ p₁ p₂ : Projectivization ℂ ComplexPlaneVector)
    (h01 : p₀ ≠ p₁) (h20 : p₂ ≠ p₀) (h21 : p₂ ≠ p₁)
    (h0 : eval p₀.rep P = 0) (h1 : eval p₁.rep P = 0) (h2 : eval p₂.rep P = 0) :
    ∃ (b : Basis (Fin 3) ℂ ComplexPlaneVector) (a c : ℂ),
      b 0 = p₀.rep ∧ b 1 = p₁.rep ∧ a ≠ 0 ∧ c ≠ 0 ∧
      b.equivFun p₀.rep = ![1, 0, 0] ∧ b.equivFun p₁.rep = ![0, 1, 0] ∧
      b.equivFun p₂.rep = ![a, c, 0] ∧ basisPolynomialChange b P = X 2 := by
…

Mentions: OAI.Nagata.W01.PlanePolynomial, OAI.Nagata.W01.ComplexPlaneVector, OAI.Nagata.W01.basisPolynomialChange