OAI/AlgebraicGeometry/RelativeTriviality/BaseChange.lean

GitHub source file

33 declarations, 0 contain sorry, 0 declared as axioms

  1. lemma OAI.CampanaPeternellSix.RelativeLineCharts.rightChartEquiv_constant line 16
  2. def OAI.CampanaPeternellSix.RelativeLineCharts.chartRing line 23
  3. instance OAI.CampanaPeternellSix.RelativeLineCharts.(instance at line 24) line 24
  4. def OAI.CampanaPeternellSix.RelativeLineCharts.chartConstants line 25
  5. def OAI.CampanaPeternellSix.RelativeLineCharts.chartCoordinate line 27
  6. def OAI.CampanaPeternellSix.RelativeLineCharts.chartEquivalence line 31
  7. lemma OAI.CampanaPeternellSix.RelativeLineCharts.chartEquivalence_constant line 34
  8. lemma OAI.CampanaPeternellSix.RelativeLineCharts.chartEquivalence_coordinate line 40
  9. lemma OAI.CampanaPeternellSix.RelativeLineCharts.chartEquivalence_symm_C line 50
  10. lemma OAI.CampanaPeternellSix.RelativeLineCharts.chartEquivalence_symm_X line 54
  11. def OAI.CampanaPeternellSix.RelativeProjectiveBaseChange.coefficientMap line 67
  12. lemma OAI.CampanaPeternellSix.RelativeProjectiveBaseChange.irrelevant_le_map_coefficientMap line 71
  13. def OAI.CampanaPeternellSix.RelativeProjectiveBaseChange.baseMap line 93
  14. lemma OAI.CampanaPeternellSix.RelativeProjectiveBaseChange.baseMap_coordinates line 96
  15. lemma OAI.CampanaPeternellSix.RelativeProjectiveBaseChange.baseMap_overBase line 109
  16. def OAI.CampanaPeternellSix.RelativeProjectiveBaseChange.chartMap line 154
  17. lemma OAI.CampanaPeternellSix.RelativeProjectiveBaseChange.chartMap_constants line 161
  18. lemma OAI.CampanaPeternellSix.RelativeProjectiveBaseChange.chartMap_coordinate line 171
  19. lemma OAI.CampanaPeternellSix.RelativeProjectiveBaseChange.chartMap_polynomial line 186
  20. lemma OAI.CampanaPeternellSix.RelativeProjectiveBaseChange.chartMap_pushout line 214
  21. lemma OAI.CampanaPeternellSix.RelativeProjectiveBaseChange.chartMap_pullback line 237
  22. def OAI.CampanaPeternellSix.RelativeProjectiveBaseChange.chartInclusion line 245
  23. lemma OAI.CampanaPeternellSix.RelativeProjectiveBaseChange.isOpenImmersion_iso_inv_comp line 249
  24. instance OAI.CampanaPeternellSix.RelativeProjectiveBaseChange.(instance at line 253) line 253
  25. lemma OAI.CampanaPeternellSix.RelativeProjectiveBaseChange.chartInclusion_toBase line 258
  26. lemma OAI.CampanaPeternellSix.RelativeProjectiveBaseChange.coefficientMap_X line 264
  27. lemma OAI.CampanaPeternellSix.RelativeProjectiveBaseChange.awayInclusion_coefficientMap line 269
  28. lemma OAI.CampanaPeternellSix.RelativeProjectiveBaseChange.chartInclusion_baseMap line 282
  29. lemma OAI.CampanaPeternellSix.RelativeProjectiveBaseChange.chartInclusion_cartesian line 288
  30. lemma OAI.CampanaPeternellSix.RelativeProjectiveBaseChange.irrelevant_le_span_variables line 305
  31. def OAI.CampanaPeternellSix.RelativeProjectiveBaseChange.twoChartCover line 319
  32. lemma OAI.CampanaPeternellSix.RelativeProjectiveBaseChange.baseMap_isPullback line 327
  33. theorem OAI.CampanaPeternellSix.RelativeProjectiveBaseChange.projectiveLine_cartesian line 347