Uniform p-integrality of the eigenform period lattice
ProvedHorizontalPadicL.eigenform_period_lattice_uniformly_integralmodular-formsmodular-symbolsnumber-theoryp-adic-l-functions
A single nonzero algebraic scalar clears the p-adic denominators of every normalized signed modular-symbol value in an MTT period system. This follows from finite generation of the integral period lattice.
Preamble
import Definitions.Def_KN_SeededThetaConstruction set_option autoImplicit false noncomputable section
Formal statement
namespace HorizontalPadicL
/-- Finite generation of the integral period lattice gives one scalar clearing
all `p`-adic denominators of the normalized signed modular symbols. -/
theorem eigenform_period_lattice_uniformly_integral
{N k p : ℕ} {ι : MTT.Qbar →+* ℂ} [Fact p.Prime]
(f : MTT.Eigenform N k ι) (hnew : IsNewEigenform f)
(ιp : MTT.Qbar →+* ℂ_[p]) (P : MTT.Periods k ι f.form) :
Nonempty (IntegralPeriodScale f ιp P) := by sorry
end HorizontalPadicLSource
Mazur--Tate--Teitelbaum modular-symbol period formalism; Kriz--Nordentoft, https://arxiv.org/pdf/2310.20678.