OAI/AlgebraicGeometry/SectionFields/GaloisAction.lean

GitHub source file

12 declarations, 0 contain sorry, 0 declared as axioms

Functorial Cartier pullback and the geometric Galois action.

  1. theorem OAI.RelativeDenominators.pullbackQCartier_comp line 18
  2. theorem OAI.RelativeDenominators.principalDivisor_eq_of_over_base line 51
  3. def OAI.RelativeDenominators.scalarExtensionAutomorphism line 82
  4. instance OAI.RelativeDenominators.scalarExtensionAutomorphism_isIso line 94
  5. lemma OAI.RelativeDenominators.scalarExtensionAutomorphism_fst line 103
  6. lemma OAI.RelativeDenominators.scalarExtensionAutomorphism_snd line 111
  7. lemma OAI.RelativeDenominators.constantToFunctionField_comp_spec line 119
  8. lemma OAI.RelativeDenominators.scalarExtensionAutomorphism_pullback_constant line 129
  9. lemma OAI.RelativeDenominators.functionFieldPullback_congr line 142
  10. lemma OAI.RelativeDenominators.scalarExtensionAutomorphism_pullback_pullback line 149
  11. theorem OAI.RelativeDenominators.scalarExtensionGaloisAction_eq_pullback line 169
  12. lemma OAI.RelativeDenominators.schemeBaseChangeGaloisAction_eq_pullback line 204