OAI/AlgebraicGeometry/SectionFields/NormalBaseChange.lean

GitHub source file

17 declarations, 0 contain sorry, 0 declared as axioms

Normality and principal-divisor descent under finite Galois base change.

  1. lemma OAI.RelativeDenominators.integrallyClosed_of_affine_open_immersion line 19
  2. lemma OAI.RelativeDenominators.integrallyClosed_spec_stalk line 32
  3. lemma OAI.RelativeDenominators.scalarExtensionChart_range line 42
  4. lemma OAI.RelativeDenominators.scalarExtensionChart_normal_stalk line 59
  5. theorem OAI.RelativeDenominators.galois_baseChange_normal line 78
  6. def OAI.RelativeDenominators.fieldAffineChartRing line 115
  7. def OAI.RelativeDenominators.fieldAffineChartMap line 118
  8. instance OAI.RelativeDenominators.(instance at line 122) line 122
  9. instance OAI.RelativeDenominators.(instance at line 125) line 125
  10. instance OAI.RelativeDenominators.fieldAffineChartRing_isDomain line 129
  11. instance OAI.RelativeDenominators.(instance at line 133) line 133
  12. def OAI.RelativeDenominators.fieldAffineChartHom line 136
  13. lemma OAI.RelativeDenominators.fieldAffineChartHom_spec line 141
  14. def OAI.RelativeDenominators.fieldAffineChartAlgebra line 146
  15. lemma OAI.RelativeDenominators.fieldAffineChart_algebraMap_spec line 151
  16. def OAI.RelativeDenominators.schemeBaseChangeGaloisAction line 159
  17. theorem OAI.RelativeDenominators.same_divisor_descends_from_galois_extension line 172