OAI/Algebra/Determinantal/FiberDimension.lean

GitHub source file

18 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.PermanentBorder.DeterminantFiberScheme.pencil line 10
  2. theorem OAI.PermanentBorder.DeterminantFiberScheme.map_pencil line 15
  3. theorem OAI.PermanentBorder.DeterminantFiberScheme.map_determinant line 26
  4. theorem OAI.PermanentBorder.DeterminantFiberScheme.determinant_ne_zero line 33
  5. abbrev OAI.PermanentBorder.DeterminantFiberScheme.PolynomialRing line 45
  6. def OAI.PermanentBorder.DeterminantFiberScheme.universalMatrix line 46
  7. def OAI.PermanentBorder.DeterminantFiberScheme.fiberIdeal line 49
  8. abbrev OAI.PermanentBorder.DeterminantFiberScheme.CoordinateRing line 55
  9. theorem OAI.PermanentBorder.DeterminantFiberScheme.field_point_equation line 60
  10. theorem OAI.PermanentBorder.DeterminantFiberScheme.range_le_of_variables_mem line 97
  11. theorem OAI.PermanentBorder.DeterminantFiberScheme.field_image_trdeg_le line 107
  12. theorem OAI.PermanentBorder.DeterminantFiberScheme.coordinate_ring_dimension_le line 142
  13. def OAI.PermanentBorder.DeterminantFibers.curveCoefficientField line 157
  14. lemma OAI.PermanentBorder.DeterminantFibers.coefficient_mem_curveCoefficientField line 161
  15. theorem OAI.PermanentBorder.DeterminantFibers.matrix_field_bound_over_curve line 165
  16. def OAI.PermanentBorder.SpectralDimension.normalizationDefect line 203
  17. def OAI.PermanentBorder.SpectralDimension.gradientIdeal line 213
  18. theorem OAI.PermanentBorder.SpectralDimension.field_point_critical line 221