OAI/AlgebraicGeometry/NumericalDimension/IntersectionLengths.lean

GitHub source file

25 declarations, 0 contain sorry, 0 declared as axioms

Intersection Lengths.

  1. lemma OAI.NumericalDimensionOne.FiniteColength.length_quotient_chain line 18
  2. lemma OAI.NumericalDimensionOne.FiniteColength.length_quotient_image line 41
  3. theorem OAI.NumericalDimensionOne.FiniteColength.length_cokernel_restriction line 71
  4. theorem OAI.NumericalDimensionOne.TorsionLength.finiteLength_of_torsion line 96
  5. theorem OAI.NumericalDimensionOne.TorsionLength.finiteLength_birational_quotient line 117
  6. theorem OAI.NumericalDimensionOne.BirationalOrder.length_scalar_cokernel line 143
  7. theorem OAI.NumericalDimensionOne.BirationalOrder.length_birational line 174
  8. def OAI.NumericalDimensionOne.LocalLengthDecomposition.quotientLocalization line 213
  9. theorem OAI.NumericalDimensionOne.LocalLengthDecomposition.length_quotient_decomposition line 226
  10. theorem OAI.NumericalDimensionOne.LocalResidueLength.isLocalHom_atPrime line 257
  11. theorem OAI.NumericalDimensionOne.LocalResidueLength.length_atPrime_restrict line 265
  12. theorem OAI.NumericalDimensionOne.LocalResidueLength.principal_length_atPrime line 281
  13. theorem OAI.NumericalDimensionOne.NormalizedLocalIntersection.artinian_principal_quotient line 305
  14. theorem OAI.NumericalDimensionOne.NormalizedLocalIntersection.ord_eq_sum line 315
  15. abbrev OAI.NumericalDimensionOne.NormalizedStalkBranches line 349
  16. theorem OAI.NumericalDimensionOne.finite_normalizedStalkBranches line 354
  17. theorem OAI.NumericalDimensionOne.localOrder_eq_normalizedBranches line 366
  18. def OAI.NumericalDimensionOne.principalFiberPrimeEquiv line 402
  19. lemma OAI.NumericalDimensionOne.principalFiberPrimeEquiv_asIdeal line 425
  20. theorem OAI.NumericalDimensionOne.NormalizedLocalIntersection.ord_eq_finsum_branches line 446
  21. theorem OAI.NumericalDimensionOne.ringOrder_equiv line 473
  22. theorem OAI.NumericalDimensionOne.scheme_order_of_stalk_element line 479
  23. theorem OAI.NumericalDimensionOne.scheme_order_on_affine_chart line 493
  24. theorem OAI.NumericalDimensionOne.localOrder_eq_normalizationFiber line 529
  25. theorem OAI.NumericalDimensionOne.localOrder_int_eq_normalizationFiber line 591