Orderly horizontal Euler factors are units
ProvedHorizontalPadicL.seededEulerFactors_areUnitsmodular-formsmodular-symbolsnumber-theoryp-adic-l-functions
The orderly-prime condition makes the augmentation of each Euler factor a p-adic unit. Since the finite horizontal quotient is a p-group and the coefficient ring is the valuation ring of C_p, the Euler factor itself is a unit in the finite group algebra.
Deprecated. Its theta-data type uses the retired character-realization interface. Use replacement node d7505519-f8d5-47f2-9e14-774e88d6f624.
Preamble
import Definitions.Def_KN_SeededThetaConstruction set_option autoImplicit false noncomputable section
Formal statement
namespace HorizontalPadicL
/-- At an orderly prime the augmentation of the horizontal Euler factor is a
unit. Since every finite horizontal quotient is a finite `p`-group, the Euler
factor itself is a unit in its group algebra. -/
theorem seededEulerFactors_areUnits
{N k p B : ℕ} {ι : MTT.Qbar →+* ℂ} [Fact p.Prime]
(f : MTT.Eigenform N k ι) (hnew : IsNewEigenform f)
(η : DirichletCharacterWithLevel) (ιp : MTT.Qbar →+* ℂ_[p])
(L : SeededHorizontalPrimeDataV2 p ιp f η B)
(Θ : SeededFiniteThetaData L) :
Θ.HasUnitEulerFactors := by sorry
end HorizontalPadicLSource
Kriz--Nordentoft, https://arxiv.org/pdf/2310.20678, Lemma 5.1.