OAI/Algebra/AffineCancellation/Cylinder.lean

GitHub source file

31 declarations, 0 contain sorry, 0 declared as axioms

  1. lemma OAI.ComplexCancellation.Cylinder.regular_quotient_of_prime line 10

    Source documentation

    Saturation needed at p=0. It does not assume the hypersurface is integral.

    lemma regular_quotient_of_prime {R : Type*} [CommRing R] [IsDomain R]
    {p h : R} (hp : Prime p) (hph : ¬p ∣ h) :
    IsLeftRegular (Ideal.Quotient.mk (Ideal.span {h}) p) := by
…

    Mentions: OAI.ComplexCancellation.p

  2. lemma OAI.ComplexCancellation.Cylinder.polynomial_C_regular line 26
  3. def OAI.ComplexCancellation.Cylinder.universal line 40
  4. def OAI.ComplexCancellation.Cylinder.parameters line 41
  5. def OAI.ComplexCancellation.Cylinder.Point.eval line 46
  6. lemma OAI.ComplexCancellation.Cylinder.Point.universal_eval line 48
  7. lemma OAI.ComplexCancellation.Cylinder.Point.eval_equation line 51
  8. lemma OAI.ComplexCancellation.Cylinder.Point.map_eval line 56
  9. lemma OAI.ComplexCancellation.Cylinder.Point.universal_eval_id line 62
  10. def OAI.ComplexCancellation.Cylinder.paramPoint line 69
  11. lemma OAI.ComplexCancellation.Cylinder.paramPoint_map line 71
  12. lemma OAI.ComplexCancellation.Cylinder.parameters_eval line 75
  13. lemma OAI.ComplexCancellation.Cylinder.p_not_dvd line 82
  14. lemma OAI.ComplexCancellation.Cylinder.p_regular line 91
  15. def OAI.ComplexCancellation.Cylinder.sourcePoint line 94
  16. lemma OAI.ComplexCancellation.Cylinder.source_equation line 98
  17. lemma OAI.ComplexCancellation.Cylinder.source_p_regular line 103
  18. lemma OAI.ComplexCancellation.Cylinder.source_p_cube line 105
  19. def OAI.ComplexCancellation.Cylinder.model line 108
  20. lemma OAI.ComplexCancellation.Cylinder.model_equation line 110
  21. def OAI.ComplexCancellation.Cylinder.coefficientMap line 112
  22. def OAI.ComplexCancellation.Cylinder.forward line 123
  23. def OAI.ComplexCancellation.Cylinder.backward line 126
  24. lemma OAI.ComplexCancellation.Cylinder.forward_X line 129
  25. lemma OAI.ComplexCancellation.Cylinder.coefficientMap_mk line 131
  26. lemma OAI.ComplexCancellation.Cylinder.forward_C line 135
  27. lemma OAI.ComplexCancellation.Cylinder.forward_source line 138
  28. lemma OAI.ComplexCancellation.Cylinder.forward_backward line 142
  29. lemma OAI.ComplexCancellation.Cylinder.backward_model line 159
  30. lemma OAI.ComplexCancellation.Cylinder.backward_forward line 168
  31. def OAI.ComplexCancellation.Cylinder.equivalence line 182

    Source documentation

    The explicit scalar-preserving polynomial cylinder isomorphism.

    def equivalence : Polynomial A ≃ₐ[ℂ] P :=
…

    Mentions: OAI.ComplexCancellation.A, OAI.ComplexCancellation.P