OAI/AlgebraicGeometry/PlaneCurves/LineGeometry.lean

GitHub source file

16 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.Nagata.Workers.W14.nonzero_linearFunctional_surjective line 20

   Source documentation

   Every nonzero linear functional realizes every prescribed scalar.

   theorem nonzero_linearFunctional_surjective {K V : Type*} [Field K]
       [AddCommGroup V] [Module K V] (L : V →ₗ[K] K) (hL : L ≠ 0) :
       Function.Surjective L := by
   …

2. theorem OAI.Nagata.Workers.W14.exists_smul_of_all_minors_zero line 46

   Source documentation

   Vanishing of all two by two minors against a nonzero vector implies proportionality, over the actual coefficient field.

   theorem exists_smul_of_all_minors_zero {K ι : Type*} [Field K]
       (u v : ι → K) (hv : v ≠ 0)
       (hminor : ∀ a b, u a * v b - u b * v a = 0) :
       ∃ c : K, c • v = u := by
   …

3. theorem OAI.Nagata.Workers.W14.minor_zero_of_smul line 63

   Source documentation

   Scalar-multiple vectors have every two by two minor equal to zero.

   theorem minor_zero_of_smul {K ι : Type*} [Field K]
       (u v : ι → K) (c : K) (hc : c • v = u) (a b : ι) :
       u a * v b - u b * v a = 0 := by
   …

4. theorem OAI.Nagata.Workers.W14.homogeneous_one_eq_sum line 84
5. def OAI.Nagata.Workers.W14.homogeneousLinearMap line 111
6. theorem OAI.Nagata.Workers.W14.homogeneousLinearMap_apply line 115
7. theorem OAI.Nagata.Workers.W14.homogeneousLinearMap_ne_zero line 121
8. theorem OAI.Nagata.Workers.W14.exists_minor_ne_zero_of_projective_ne line 143

   Source documentation

   Distinct actual projective points have a nonzero two by two minor in any pair of nonzero homogeneous representatives.

   theorem exists_minor_ne_zero_of_projective_ne {K ι : Type*} [Field K]
       (u v : ι → K) (hu : u ≠ 0) (hv : v ≠ 0)
       (h : Projectivization.mk K u hu ≠ Projectivization.mk K v hv) :
       ∃ a b, u a * v b - u b * v a ≠ 0 := by
   …

9. theorem OAI.Nagata.Workers.W14.projective_ne_of_minor_ne_zero line 157

   Source documentation

   A nonzero two by two minor separates the two genuine projective points.

   theorem projective_ne_of_minor_ne_zero {K ι : Type*} [Field K]
       (u v : ι → K) (hu : u ≠ 0) (hv : v ≠ 0) (a b : ι)
       (hminor : u a * v b - u b * v a ≠ 0) :
       Projectivization.mk K u hu ≠ Projectivization.mk K v hv := by
   …

10. def OAI.Nagata.Workers.W14.coordinateLineRestriction line 177
11. theorem OAI.Nagata.Workers.W14.coordinateLineRestriction_eval line 180
12. theorem OAI.Nagata.Workers.W14.coordinateLineRestriction_homogeneous line 192
13. def OAI.Nagata.Workers.W14.polynomialInLastCoordinate line 205
14. theorem OAI.Nagata.Workers.W14.polynomialInLastCoordinate_X line 210
15. theorem OAI.Nagata.Workers.W14.polynomialInLastCoordinate_eval_zero line 215
16. theorem OAI.Nagata.Workers.W14.coordinateLine_dvd_of_restriction_zero line 233