OAI/AlgebraicGeometry/NumericalDimension/TerminalModels.lean

GitHub source file

10 declarations, 0 contain sorry, 0 declared as axioms

Terminal Models.

  1. theorem OAI.NumericalDimensionOne.smooth_relative_canonical_strict line 16
  2. theorem OAI.NumericalDimensionOne.smooth_isTerminalModel line 172
  3. lemma OAI.NumericalDimensionOne.canonical_coefficient_of_stalk_iso line 194
  4. lemma OAI.NumericalDimensionOne.canonical_comparison_strict_source_primes line 269
  5. lemma OAI.NumericalDimensionOne.Kaehler_free_of_algebraMap_bijective line 314
  6. lemma OAI.NumericalDimensionOne.canonical_coefficient_of_smooth_source_stalk_iso line 337
  7. lemma OAI.NumericalDimensionOne.IsQCartierPullback.coeff_eq_of_stalk_iso line 426
  8. lemma OAI.NumericalDimensionOne.relativeCanonical_vanishes_over_prime line 441
  9. lemma OAI.NumericalDimensionOne.relativeCanonical_effective_terminal line 464
  10. lemma OAI.NumericalDimensionOne.topDifferentialMap_bijective_of_algebraMap_bijective line 516