OAI/AlgebraicGeometry/SectionFields/Constants.lean

GitHub source file

11 declarations, 0 contain sorry, 0 declared as axioms

Constants and function fields under geometric integrality and open charts.

  1. theorem OAI.RelativeDenominators.global_constants_surjective_of_geometricallyIntegral line 18
  2. def OAI.RelativeDenominators.constantToFunctionField line 62
  3. theorem OAI.RelativeDenominators.rational_function_constant_of_divisor_zero line 70
  4. theorem OAI.RelativeDenominators.functionFieldPullback_bijective_of_open line 90
  5. def OAI.RelativeDenominators.functionFieldOpenEquiv line 104
  6. def OAI.RelativeDenominators.chartFunctionFieldEquiv line 112
  7. lemma OAI.RelativeDenominators.chartFunctionFieldEquiv_algebraMap line 125
  8. lemma OAI.RelativeDenominators.functionFieldPullback_comp line 143
  9. lemma OAI.RelativeDenominators.functionFieldPullback_constant line 157
  10. lemma OAI.RelativeDenominators.constantToFunctionField_spec line 169
  11. lemma OAI.RelativeDenominators.functionFieldPullback_spec_algebraMap line 179