OAI/AlgebraicGeometry/NumericalDimension/OpenSections.lean

GitHub source file

17 declarations, 0 contain sorry, 0 declared as axioms

Open Sections.

  1. theorem OAI.NumericalDimensionOne.hyperplane_intersection_component_dimension_lower line 25
  2. theorem OAI.NumericalDimensionOne.IncidenceCutChain.pure_dimension_of_embedding line 76
  3. theorem OAI.NumericalDimensionOne.exists_smooth_pure_very_ample_complete_intersection line 156
  4. theorem OAI.NumericalDimensionOne.nonempty_differential_basis_of_transcendence_basis line 228
  5. theorem OAI.NumericalDimensionOne.differential_rank_eq_trdeg line 268
  6. theorem OAI.NumericalDimensionOne.standardSmoothOfRelativeDimension_of_fractionField line 274
  7. theorem OAI.NumericalDimensionOne.isReduced_of_etale_domain_base line 304
  8. theorem OAI.NumericalDimensionOne.isReduced_of_smooth_field line 320
  9. theorem OAI.NumericalDimensionOne.scheme_isReduced_of_smooth_field line 362
  10. lemma OAI.NumericalDimensionOne.stalk_scalar_over line 406
  11. lemma OAI.NumericalDimensionOne.generic_component_stalk_isField line 416
  12. theorem OAI.NumericalDimensionOne.generic_component_stalk_trdeg line 441
  13. theorem OAI.NumericalDimensionOne.standardSmoothOfRelativeDimension_of_formallyEtaleField line 491
  14. theorem OAI.NumericalDimensionOne.smooth_relative_dimension_of_pure_dimension line 502
  15. lemma OAI.NumericalDimensionOne.generated_finite_section_cover_on_open line 566
  16. def OAI.NumericalDimensionOne.DivisorProjectiveChart.restrict line 591
  17. lemma OAI.NumericalDimensionOne.exists_affine_divisorProjectiveChart_inside line 608