OAI/AlgebraicGeometry/SectionFields/GenericFiber.lean

GitHub source file

22 declarations, 0 contain sorry, 0 declared as axioms

Generic-fibre geometry, function fields and principal presentations.

  1. theorem OAI.RelativeDenominators.flat_fromSpecStalk line 17
  2. theorem OAI.RelativeDenominators.isIso_stalkMap_of_flat_preimmersion line 33
  3. abbrev OAI.RelativeDenominators.genericFiber line 47
  4. abbrev OAI.RelativeDenominators.genericFiberι line 50
  5. abbrev OAI.RelativeDenominators.genericFiberToSpec line 53
  6. instance OAI.RelativeDenominators.genericFiberι_flat line 56
  7. instance OAI.RelativeDenominators.genericFiberι_preimmersion line 62
  8. instance OAI.RelativeDenominators.genericFiberι_stalk_iso line 65
  9. lemma OAI.RelativeDenominators.range_fromSpecStalk_generic line 69
  10. lemma OAI.RelativeDenominators.range_genericFiberι line 76
  11. lemma OAI.RelativeDenominators.genericPoint_mem_range_genericFiberι line 80
  12. instance OAI.RelativeDenominators.genericFiberι_dominant line 89
  13. instance OAI.RelativeDenominators.genericFiber_irreducible line 98
  14. instance OAI.RelativeDenominators.genericFiber_reduced line 111
  15. instance OAI.RelativeDenominators.genericFiber_integral line 119
  16. theorem OAI.RelativeDenominators.genericFiber_normal line 124
  17. instance OAI.RelativeDenominators.genericFiber_isNoetherian line 132
  18. def OAI.RelativeDenominators.genericFiberFunctionFieldEquiv line 149
  19. theorem OAI.RelativeDenominators.pullbackQCartier_eq_zero_at_of_mem_range line 168
  20. theorem OAI.RelativeDenominators.isVertical_of_genericFiber_pullback_zero line 199
  21. theorem OAI.RelativeDenominators.exists_vertical_principalization_of_genericFiber line 215
  22. theorem OAI.RelativeDenominators.relative_exact_presentation_of_genericFiber_principalization line 240