OAI/AlgebraicGeometry/NumericalDimension/DifferentialBaseChange.lean

GitHub source file

18 declarations, 0 contain sorry, 0 declared as axioms

Differential Base Change.

  1. lemma OAI.NumericalDimensionOne.IsCartierPullback.nsmul_local line 19
  2. lemma OAI.NumericalDimensionOne.IsCartierPullback.eq_ord_on_open line 28
  3. lemma OAI.NumericalDimensionOne.IsCartierPullback.comp line 37
  4. lemma OAI.NumericalDimensionOne.IsQCartierPullback.comp line 49
  5. lemma OAI.NumericalDimensionOne.IsCartierPullback.nonneg line 98
  6. lemma OAI.NumericalDimensionOne.IsQCartierPullback.isQCartier line 111
  7. lemma OAI.NumericalDimensionOne.IsQCartierPullback.nonneg line 116
  8. lemma OAI.NumericalDimensionOne.IsQCartierPullback.unique line 133
  9. lemma OAI.NumericalDimensionOne.IsCartierDivisor.pullback_id line 176
  10. lemma OAI.NumericalDimensionOne.IsQCartierDivisor.pullback_id line 184
  11. lemma OAI.NumericalDimensionOne.HasEffectiveCanonicalComparison.refl line 188
  12. lemma OAI.NumericalDimensionOne.canonical_chart_equation line 217
  13. lemma OAI.NumericalDimensionOne.dominant_stalk_scalar line 265
  14. theorem OAI.NumericalDimensionOne.smooth_relative_canonical_effective line 293
  15. lemma OAI.NumericalDimensionOne.exterior_volume_spans line 416
  16. theorem OAI.NumericalDimensionOne.formallyUnramified_of_topDifferential_unit line 451
  17. theorem OAI.NumericalDimensionOne.nonempty_standardSmooth_differential_basis line 511
  18. theorem OAI.NumericalDimensionOne.nonempty_smooth_stalk_differential_basis line 524