OAI/NumberTheory/PiExponent/Geometry/ProjectiveChartRingNaturalityCore.lean

GitHub source file

10 declarations, 0 contain sorry, 0 declared as axioms

  1. lemma OAI.PiExponentSeshadri.Projective.away_chart_preimage_self line 13
  2. lemma OAI.PiExponentSeshadri.Projective.away_chart_appLE_top line 19
  3. lemma OAI.PiExponentSeshadri.Projective.chartIso_pullback_top line 32
  4. lemma OAI.PiExponentSeshadri.Projective.awayToSection_pullback_top line 42
  5. lemma OAI.PiExponentSeshadri.Projective.awayToSection_pullback_open line 57
  6. def OAI.PiExponentSeshadri.Projective.relabeledSectionIso line 69
  7. lemma OAI.PiExponentSeshadri.Projective.relabeledSectionIso_inv line 76
  8. lemma OAI.PiExponentSeshadri.Projective.chartFiniteSectionRingEquiv_restrict line 84
  9. lemma OAI.PiExponentSeshadri.Projective.chartFinitePolynomialRingEquiv_restrict line 121
  10. lemma OAI.PiExponentSeshadri.Projective.chartFinitePolynomialRingEquiv_restrict_poly line 129