Euler factors in the faithful theta system are units
ProvedHorizontalPadicL.seededEulerFactors_areUnits_v2dirichlet-charactersmodular-formsnumber-theoryp-adic-l-functions
Every Euler factor in the faithful finite theta system is a unit. The augmentation has norm one by orderliness, and a group-ring element over a finite p-group is a unit exactly when its augmentation is a unit.
Preamble
import Definitions.Def_KN_SeededThetaConstructionV2 set_option autoImplicit false noncomputable section
Formal statement
namespace HorizontalPadicL
/-- The orderly-prime calculation makes every Euler factor in the faithful
theta system a unit. -/
theorem seededEulerFactors_areUnits_v2
{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)
(Θ : SeededFiniteThetaDataV2 L) :
Θ.HasUnitEulerFactors := by
sorry
end HorizontalPadicLSource
Kriz--Nordentoft, Horizontal p-adic L-functions, https://arxiv.org/pdf/2310.20678, Corollary 3.6, Definition 5.3, Corollary 5.4, Theorem 5.9, Corollary 5.10 and Corollary 5.17.