OAI/AlgebraicGeometry/StableCoordinate/ZeroFiberSpecialization.lean

GitHub source file

28 declarations, 0 contain sorry, 0 declared as axioms

Specializing the five-variable presentation at p = 0

This module proves, by explicit algebra maps, that specializing the hypersurface presentation before or after imposing its defining equation gives the same coordinate algebra. No field, reducedness, or geometric assumptions are used.

  1. abbrev OAI.StableCoordinate.ZeroFiber.Five line 19
  2. def OAI.StableCoordinate.ZeroFiber.sourceX line 21
  3. def OAI.StableCoordinate.ZeroFiber.sourceH line 23
  4. def OAI.StableCoordinate.ZeroFiber.sourceIdeal line 26
  5. abbrev OAI.StableCoordinate.ZeroFiber.Hypersurface line 27
  6. def OAI.StableCoordinate.ZeroFiber.hypersurfaceMk line 29
  7. def OAI.StableCoordinate.ZeroFiber.parameterIdeal line 31
  8. abbrev OAI.StableCoordinate.ZeroFiber.SourceRing line 32
  9. def OAI.StableCoordinate.ZeroFiber.sourceMk line 34
  10. lemma OAI.StableCoordinate.ZeroFiber.sourceMk_parameter line 37
  11. lemma OAI.StableCoordinate.ZeroFiber.sourceMk_relation line 41
  12. def OAI.StableCoordinate.ZeroFiber.specialize line 48
  13. lemma OAI.StableCoordinate.ZeroFiber.specialize_relation line 51
  14. lemma OAI.StableCoordinate.ZeroFiber.specialize_vanishes line 55
  15. def OAI.StableCoordinate.ZeroFiber.specializeHypersurface line 64
  16. lemma OAI.StableCoordinate.ZeroFiber.specializeHypersurface_mk line 67
  17. lemma OAI.StableCoordinate.ZeroFiber.specializeHypersurface_vanishes line 70
  18. def OAI.StableCoordinate.ZeroFiber.specializeQuotient line 80
  19. lemma OAI.StableCoordinate.ZeroFiber.specializeQuotient_mk line 83
  20. def OAI.StableCoordinate.ZeroFiber.includeVariables line 86
  21. lemma OAI.StableCoordinate.ZeroFiber.includeVariables_relation line 89
  22. lemma OAI.StableCoordinate.ZeroFiber.includeVariables_vanishes line 98
  23. def OAI.StableCoordinate.ZeroFiber.includeQuotient line 107
  24. lemma OAI.StableCoordinate.ZeroFiber.includeQuotient_mk line 110
  25. lemma OAI.StableCoordinate.ZeroFiber.specialize_include line 113
  26. lemma OAI.StableCoordinate.ZeroFiber.include_specialize line 121
  27. def OAI.StableCoordinate.ZeroFiber.specializationEquiv line 131

    Source documentation

    Specialize p to zero in the hypersurface presentation.

    def specializationEquiv : SourceRing K ≃ₐ[K] Ring K :=
…

    Mentions: OAI.StableCoordinate.ZeroFiber.SourceRing, OAI.StableCoordinate.ZeroFiber.Ring

  28. def OAI.StableCoordinate.ZeroFiber.sourceZeroFiberEquiv line 137

    Source documentation

    The zero fiber of the five-variable hypersurface presentation is a three-variable polynomial algebra.

    def sourceZeroFiberEquiv : SourceRing K ≃ₐ[K] Three K :=
…

    Mentions: OAI.StableCoordinate.ZeroFiber.SourceRing, OAI.StableCoordinate.ZeroFiber.Three