OAI/NumberTheory/Ostmann/Characters/QuartetConjugation.lean

GitHub source file

4 declarations, 0 contain sorry, 0 declared as axioms

Independent opposite conjugations on the two bottom sibling pairs

  1. def OAI.Ostmann.pairConjugate line 11
  2. theorem OAI.Ostmann.rationalTreeAmplitude_pair_conjugation line 14
  3. def OAI.Ostmann.rationalQuartetPairsValue line 29
  4. theorem OAI.Ostmann.rationalTreeAmplitude_quartet_conjugation line 44

    Source documentation

    Both opposite-conjugation choices in each sibling pair are identified with the actual diagram, independently of the choices in the other pair.

    theorem rationalTreeAmplitude_quartet_conjugation {p : ℕ} [Fact p.Prime]
    (g : ZMod p → ℂ) (D : (ZMod p)ˣ) (Q : RationalQuartetData (ZMod p)ˣ)
    (XL XR m₁ m₂ m₃ m₄ : (ZMod p)ˣ) (cL cR : Bool) :
    rationalTreeAmplitude g D Q.tree XL XR ((cL, !cL), (cR, !cR))
      ((m₁, m₂), (m₃, m₄)) =
      rationalQuartetPairsValue (pairConjugate g cL) (pairConjugate g cR)
        D Q XL XR m₁ m₂ m₃ m₄ := by
…

    Mentions: OAI.Ostmann.RationalQuartetData, OAI.Ostmann.rationalTreeAmplitude, OAI.Ostmann.rationalQuartetPairsValue, OAI.Ostmann.pairConjugate