OAI/LinearAlgebra/CirculantHadamard/BinaryLocalRing.lean

GitHub source file

23 declarations, 0 contain sorry, 0 declared as axioms

One concrete local ring and residue field

For the actual cyclotomic coefficient algebra B u, choose a maximal ideal containing two. Both first-order calculations use the same localization and the same residue field. The choices depend only on u, not on a character or on which of the three norm elements is being considered.

  1. def OAI.CirculantHadamard.BinaryLocalRing.twoIdeal line 22
  2. instance OAI.CirculantHadamard.BinaryLocalRing.twoIdeal_isMaximal line 25
  3. theorem OAI.CirculantHadamard.BinaryLocalRing.two_mem line 28
  4. abbrev OAI.CirculantHadamard.BinaryLocalRing.O line 31
  5. instance OAI.CirculantHadamard.BinaryLocalRing.local_algebra line 35

    Source comment

    Name the canonical localization algebra directly. This avoids searching through iterated-localization algebra instances for these concrete carriers.
    instance local_algebra (u : ℕ) : Algebra (B u) (O u) :=
…

    Mentions: OAI.CirculantHadamard.BinaryLocalRing.O

  6. instance OAI.CirculantHadamard.BinaryLocalRing.fraction_algebra line 38
  7. abbrev OAI.CirculantHadamard.BinaryLocalRing.k line 41
  8. def OAI.CirculantHadamard.BinaryLocalRing.toLocal line 43
  9. theorem OAI.CirculantHadamard.BinaryLocalRing.toLocal_injective line 45
  10. def OAI.CirculantHadamard.BinaryLocalRing.toFraction line 50

    Source documentation

    The same localization embeds into the fraction field used for the alternating products.

    def toFraction (u : ℕ) : O u →ₐ[B u] FractionRing (B u) :=
…

    Mentions: OAI.CirculantHadamard.BinaryLocalRing.O

  11. theorem OAI.CirculantHadamard.BinaryLocalRing.toFraction_toLocal line 54
  12. theorem OAI.CirculantHadamard.BinaryLocalRing.toFraction_injective line 58
  13. instance OAI.CirculantHadamard.BinaryLocalRing.local_charZero line 71
  14. instance OAI.CirculantHadamard.BinaryLocalRing.residue_charTwo line 77
  15. def OAI.CirculantHadamard.BinaryLocalRing.residue line 80
  16. def OAI.CirculantHadamard.BinaryLocalRing.gaussianToLocal line 82
  17. def OAI.CirculantHadamard.BinaryLocalRing.imaginary line 85
  18. theorem OAI.CirculantHadamard.BinaryLocalRing.imaginary_sq line 87
  19. theorem OAI.CirculantHadamard.BinaryLocalRing.residue_imaginary line 91
  20. theorem OAI.CirculantHadamard.BinaryLocalRing.two_ne_zero line 94
  21. theorem OAI.CirculantHadamard.BinaryLocalRing.norm_isUnit line 98

    Source documentation

    Every one of the actual character norms supplies its own local unit.

    theorem norm_isUnit (u : ℕ) (hu : Odd u) (x y : B u)
    (hxy : x * y = (u : B u) ^ 2) : IsUnit (toLocal u x) := by
…

    Mentions: OAI.CirculantHadamard.BinaryLocalRing.toLocal

  22. def OAI.CirculantHadamard.BinaryLocalRing.normUnit line 106

    Source documentation

    The unit value is the localized character value, not an unrelated witness.

    def normUnit (u : ℕ) (hu : Odd u) (x y : B u)
    (hxy : x * y = (u : B u) ^ 2) : (O u)ˣ :=
…

    Mentions: OAI.CirculantHadamard.BinaryLocalRing.O

  23. theorem OAI.CirculantHadamard.BinaryLocalRing.normUnit_val line 110