OAI/NumberTheory/PiExponent/Geometry/ProjectiveGlobalPolynomials.lean

GitHub source file

17 declarations, 0 contain sorry, 0 declared as axioms

  1. abbrev OAI.PiExponent.ProjectiveGlobalPolynomials.schemeFreeOpen line 20
  2. def OAI.PiExponent.ProjectiveGlobalPolynomials.globalCochain line 23
  3. def OAI.PiExponent.ProjectiveGlobalPolynomials.globalLaurent line 28
  4. lemma OAI.PiExponent.ProjectiveGlobalPolynomials.globalLaurent_closed line 33
  5. theorem OAI.PiExponent.ProjectiveGlobalPolynomials.existsUnique_polynomial line 42
  6. lemma OAI.PiExponent.ProjectiveGlobalPolynomials.globalLaurent_injective line 49
  7. theorem OAI.PiExponent.ProjectiveGlobalPolynomials.existsUnique_section line 59
  8. def OAI.PiExponent.ProjectiveGlobalPolynomials.representedRestriction line 95
  9. lemma OAI.PiExponent.ProjectiveGlobalPolynomials.globalCochain_restrict line 101
  10. def OAI.PiExponent.ProjectiveGlobalPolynomials.coordinateChartPolynomial line 119
  11. lemma OAI.PiExponent.ProjectiveGlobalPolynomials.coordinateChartPolynomial_coefficient line 127
  12. lemma OAI.PiExponent.ProjectiveGlobalPolynomials.coordinate_globalLaurent_vertex line 140
  13. theorem OAI.PiExponent.ProjectiveGlobalPolynomials.coordinate_existsUnique_polynomial line 149
  14. theorem OAI.PiExponent.ProjectiveGlobalPolynomials.coordinate_existsUnique_section line 170
  15. def OAI.PiExponent.ProjectiveO1.globalSectionChartPolynomial line 203
  16. theorem OAI.PiExponent.ProjectiveO1.globalSection_homogeneous_polynomial line 213
  17. theorem OAI.PiExponent.ProjectiveO1.homogeneousPolynomial_globalSection line 224