OAI/AlgebraicGeometry/SectionFields/TensorAlgebra.lean

GitHub source file

13 declarations, 0 contain sorry, 0 declared as axioms

Tensor localizations, Galois invariants and normality of scalar extensions.

  1. theorem OAI.RelativeDenominators.algebraMap_surjective_of_isAlgebraic_tensorSelf_domain line 17
  2. def OAI.RelativeDenominators.tensorFractionAlgebra line 35
  3. lemma OAI.RelativeDenominators.tensorFraction_isLocalization line 38
  4. lemma OAI.RelativeDenominators.tensorFraction_domain line 51
  5. def OAI.RelativeDenominators.tensorFractionField line 70
  6. lemma OAI.RelativeDenominators.tensorFraction_isFractionRing line 75
  7. theorem OAI.RelativeDenominators.tensor_invariant_descends line 115
  8. def OAI.RelativeDenominators.tensorGaloisAction line 150
  9. theorem OAI.RelativeDenominators.tensor_invariant_unit_descends line 172
  10. lemma OAI.RelativeDenominators.tensor_galois_coefficient line 190
  11. def OAI.RelativeDenominators.tensorRightGaloisAlgHom line 214
  12. lemma OAI.RelativeDenominators.tensorFraction_isScalarTower line 224
  13. theorem OAI.RelativeDenominators.tensor_isIntegrallyClosed_of_galois line 238