OAI/AlgebraicGeometry/LogKodaira/Blowup.lean

GitHub source file

40 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.ReverseLogKodaira.Blowup.grade line 19
  2. lemma OAI.ReverseLogKodaira.Blowup.mem_grade_iff line 31
  3. def OAI.ReverseLogKodaira.Blowup.homogeneous line 35
  4. lemma OAI.ReverseLogKodaira.Blowup.homogeneous_val line 38
  5. lemma OAI.ReverseLogKodaira.Blowup.homogeneous_mem line 41
  6. instance OAI.ReverseLogKodaira.Blowup.gradedMonoid line 45
  7. def OAI.ReverseLogKodaira.Blowup.component line 57
  8. lemma OAI.ReverseLogKodaira.Blowup.component_val line 60
  9. def OAI.ReverseLogKodaira.Blowup.decompose line 64
  10. lemma OAI.ReverseLogKodaira.Blowup.decompose_apply line 74
  11. lemma OAI.ReverseLogKodaira.Blowup.grade_coeff_eq_zero line 77
  12. lemma OAI.ReverseLogKodaira.Blowup.coeff_recompose line 83
  13. instance OAI.ReverseLogKodaira.Blowup.gradedAlgebra line 100
  14. def OAI.ReverseLogKodaira.Blowup.constants line 119
  15. lemma OAI.ReverseLogKodaira.Blowup.constants_val line 128
  16. def OAI.ReverseLogKodaira.Blowup.linearTerm line 132
  17. lemma OAI.ReverseLogKodaira.Blowup.linearTerm_mem line 135
  18. abbrev OAI.ReverseLogKodaira.Blowup.Chart line 139
  19. def OAI.ReverseLogKodaira.Blowup.chartMap line 143
  20. def OAI.ReverseLogKodaira.Blowup.ratio line 148
  21. def OAI.ReverseLogKodaira.Blowup.scheme line 155
  22. def OAI.ReverseLogKodaira.Blowup.projection line 158
  23. def OAI.ReverseLogKodaira.Blowup.chartι line 162
  24. lemma OAI.ReverseLogKodaira.Blowup.chartι_projection line 165
  25. lemma OAI.ReverseLogKodaira.Blowup.chartMap_val line 174
  26. lemma OAI.ReverseLogKodaira.Blowup.ratio_mul_parameter line 179
  27. theorem OAI.ReverseLogKodaira.Blowup.ideal_map_chart_eq line 194
  28. lemma OAI.ReverseLogKodaira.Blowup.positive_homogeneous_mem_span line 208
  29. lemma OAI.ReverseLogKodaira.Blowup.irrelevant_le_span_linear line 238
  30. theorem OAI.ReverseLogKodaira.Blowup.charts_cover line 255
  31. theorem OAI.ReverseLogKodaira.Blowup.exists_chart line 260
  32. lemma OAI.ReverseLogKodaira.Blowup.linearTerm_ne_zero line 268
  33. lemma OAI.ReverseLogKodaira.Blowup.chartMap_injective line 276
  34. lemma OAI.ReverseLogKodaira.Blowup.chart_isDomain line 287
  35. def OAI.ReverseLogKodaira.Blowup.exceptionalGeneratorMap line 298
  36. def OAI.ReverseLogKodaira.Blowup.exceptionalTrivialization line 314
  37. lemma OAI.ReverseLogKodaira.Blowup.parameter_ne_zero_of_mem line 332
  38. theorem OAI.ReverseLogKodaira.Blowup.exists_regular_principal_chart line 343
  39. theorem OAI.ReverseLogKodaira.Blowup.ideal_map_baseChange line 358
  40. theorem OAI.ReverseLogKodaira.Blowup.parameter_dvd_image line 367