OAI/AlgebraicGeometry/SectionFields/ScalarCharts.lean

GitHub source file

17 declarations, 0 contain sorry, 0 declared as axioms

Scalar-extension charts and descent through their function fields.

  1. def OAI.RelativeDenominators.scalarExtensionChart line 16
  2. instance OAI.RelativeDenominators.scalarExtensionChart_isOpenImmersion line 26
  3. lemma OAI.RelativeDenominators.isDominant_of_openIntegral line 36
  4. lemma OAI.RelativeDenominators.scalarExtensionChart_domain line 42
  5. def OAI.RelativeDenominators.scalarExtensionFunctionFieldEquiv line 59
  6. lemma OAI.RelativeDenominators.scalarExtensionChart_snd line 81
  7. lemma OAI.RelativeDenominators.scalarExtensionChart_fst line 95
  8. lemma OAI.RelativeDenominators.scalarExtensionFunctionFieldEquiv_constant line 109
  9. lemma OAI.RelativeDenominators.scalarExtensionFunctionFieldEquiv_algebraMap line 146
  10. lemma OAI.RelativeDenominators.scalarExtensionFunctionFieldEquiv_pullback line 177
  11. def OAI.RelativeDenominators.transportRingAction line 229
  12. def OAI.RelativeDenominators.scalarExtensionFunctionFieldEquivLeft line 252
  13. def OAI.RelativeDenominators.scalarExtensionGaloisAction line 265
  14. lemma OAI.RelativeDenominators.scalarExtensionGaloisAction_constant line 277
  15. theorem OAI.RelativeDenominators.scalarExtension_invariant_unit_descends line 304
  16. lemma OAI.RelativeDenominators.scalarExtensionGaloisAction_pullback line 345
  17. theorem OAI.RelativeDenominators.same_divisor_descends_from_galois_baseChange line 372