OAI/AlgebraicGeometry/SectionFields/FlatDescent.lean

GitHub source file

8 declarations, 0 contain sorry, 0 declared as axioms

Faithfully flat descent of fractions and injectivity of divisor pullback.

  1. theorem OAI.RelativeDenominators.fraction_mem_of_faithfullyFlat line 18
  2. theorem OAI.RelativeDenominators.fraction_unit_of_faithfullyFlat line 43
  3. lemma OAI.RelativeDenominators.functionFieldPullback_stalk line 64
  4. theorem OAI.RelativeDenominators.stalk_unit_of_flat_pullback_ord_zero line 80
  5. lemma OAI.RelativeDenominators.ord_eq_zero_of_stalk_unit line 112
  6. theorem OAI.RelativeDenominators.pullbackQCartier_eq_zero_imp line 124
  7. theorem OAI.RelativeDenominators.pullbackQCartier_injective line 157
  8. theorem OAI.RelativeDenominators.principalization_descends_from_galois_extension line 177