OAI/AlgebraicGeometry/SectionFields/GeometricFiber.lean

GitHub source file

12 declarations, 0 contain sorry, 0 declared as axioms

Geometric integrality of contraction fibres and exact presentations.

  1. theorem OAI.RelativeDenominators.scalarExtensionChart_domain_of_relatively_closed line 21
  2. theorem OAI.RelativeDenominators.geometricallyIntegral_of_functionField_relatively_closed line 60
  3. def OAI.RelativeDenominators.genericPointStalkMap line 131
  4. lemma OAI.RelativeDenominators.genericPointStalkMap_compat line 136
  5. theorem OAI.RelativeDenominators.integral_rational_stalk_unit_over_generic line 158
  6. theorem OAI.RelativeDenominators.contraction_functionField_integrallyClosedIn line 185
  7. instance OAI.RelativeDenominators.fromSpecStalk_generic_dominant line 212
  8. lemma OAI.RelativeDenominators.functionFieldPullback_fromSpecStalk_generic line 219
  9. lemma OAI.RelativeDenominators.genericFiber_constant_compat line 237
  10. theorem OAI.RelativeDenominators.contraction_genericFiber_geometricallyIntegral line 265
  11. theorem OAI.RelativeDenominators.contraction_exact_presentation_of_geometricGenericFiber_principalization line 294
  12. theorem OAI.RelativeDenominators.complex_contraction_exact_presentation_of_geometricGenericFiber_principalization line 329