theorem QuotientGroup.mk_image_finite_of_compact_of_open {G : Type u_1} [Group G] [TopologicalSpace G] [IsTopologicalGroup G] {g : G} {U V : Subgroup G} (hU : IsCompact ↑U) (hVopen : IsOpen ↑V) : (mk '' (↑U * {g})).Finite

@[reducible, inline]

noncomputable abbrev TotallyDefiniteQuaternionAlgebra.WeightTwoAutomorphicForm.U1 {F : Type u_1} [Field F] [NumberField F] {D : Type u_2} [Ring D] [Algebra F D] (r : IsQuaternionAlgebra.NumberField.Rigidification F D) (S : Finset (IsDedekindDomain.HeightOneSpectrum (NumberField.RingOfIntegers F))) : Subgroup (TensorProduct F D (IsDedekindDomain.FiniteAdeleRing (NumberField.RingOfIntegers F) F))ˣ

U1(S)

theorem TotallyDefiniteQuaternionAlgebra.WeightTwoAutomorphicForm.U1_compact {F : Type u_1} [Field F] [NumberField F] [NumberField.IsTotallyReal F] {D : Type u_2} [Ring D] [Algebra F D] [IsQuaternionAlgebra F D] (r : IsQuaternionAlgebra.NumberField.Rigidification F D) (S : Finset (IsDedekindDomain.HeightOneSpectrum (NumberField.RingOfIntegers F))) : IsCompact ↑(U1 r S)

theorem TotallyDefiniteQuaternionAlgebra.WeightTwoAutomorphicForm.U1_open {F : Type u_1} [Field F] [NumberField F] [NumberField.IsTotallyReal F] {D : Type u_2} [Ring D] [Algebra F D] [IsQuaternionAlgebra F D] (r : IsQuaternionAlgebra.NumberField.Rigidification F D) (S : Finset (IsDedekindDomain.HeightOneSpectrum (NumberField.RingOfIntegers F))) : IsOpen ↑(U1 r S)

noncomputable def TotallyDefiniteQuaternionAlgebra.WeightTwoAutomorphicForm.HeckeOperator.T {F : Type u_1} [Field F] [NumberField F] [NumberField.IsTotallyReal F] {D : Type u_2} [Ring D] [Algebra F D] [IsQuaternionAlgebra F D] (r : IsQuaternionAlgebra.NumberField.Rigidification F D) {S : Finset (IsDedekindDomain.HeightOneSpectrum (NumberField.RingOfIntegers F))} (R : Type u_3) [CommRing R] (v : IsDedekindDomain.HeightOneSpectrum (NumberField.RingOfIntegers F)) : WeightTwoAutomorphicFormOfLevel (U1 r S) R →ₗ[R] WeightTwoAutomorphicFormOfLevel (U1 r S) R

The Hecke operator T_v as an R-linear map from R-valued quaternionic weight 2 automorphic forms of level U_1(S).

noncomputable instance TotallyDefiniteQuaternionAlgebra.WeightTwoAutomorphicForm.HeckeOperator.instDecidableEqHeightOneSpectrumRingOfIntegers {F : Type u_1} [Field F] : DecidableEq (IsDedekindDomain.HeightOneSpectrum (NumberField.RingOfIntegers F))

@[reducible, inline]

noncomputable abbrev TotallyDefiniteQuaternionAlgebra.WeightTwoAutomorphicForm.HeckeOperator.diag {F : Type u_1} [Field F] [NumberField F] {D : Type u_2} [Ring D] [Algebra F D] (r : IsQuaternionAlgebra.NumberField.Rigidification F D) {v : IsDedekindDomain.HeightOneSpectrum (NumberField.RingOfIntegers F)} (α : ↥(IsDedekindDomain.HeightOneSpectrum.adicCompletionIntegers F v)) (hα : α ≠ 0) : (TensorProduct F D (IsDedekindDomain.FiniteAdeleRing (NumberField.RingOfIntegers F) F))ˣ

The (global) matrix element diag[α, 1].

noncomputable def TotallyDefiniteQuaternionAlgebra.WeightTwoAutomorphicForm.HeckeOperator.unipotent_mul_diag {F : Type u_1} [Field F] [NumberField F] {D : Type u_2} [Ring D] [Algebra F D] (r : IsQuaternionAlgebra.NumberField.Rigidification F D) {v : IsDedekindDomain.HeightOneSpectrum (NumberField.RingOfIntegers F)} (α : ↥(IsDedekindDomain.HeightOneSpectrum.adicCompletionIntegers F v)) (hα : α ≠ 0) (t : ↥(IsDedekindDomain.HeightOneSpectrum.adicCompletionIntegers F v) ⧸ Ideal.span {α}) : (TensorProduct F D (IsDedekindDomain.FiniteAdeleRing (NumberField.RingOfIntegers F) F))ˣ

The (global) matrix element (unipotent t) * (diag α hα) = !![α, t; 0, 1]. Here t ∈ 𝒪ᵥ / α and we lift it arbitrarily to 𝒪ᵥ.

noncomputable def TotallyDefiniteQuaternionAlgebra.WeightTwoAutomorphicForm.HeckeOperator.unipotent_mul_diag_image {F : Type u_1} [Field F] [NumberField F] {D : Type u_2} [Ring D] [Algebra F D] (r : IsQuaternionAlgebra.NumberField.Rigidification F D) {v : IsDedekindDomain.HeightOneSpectrum (NumberField.RingOfIntegers F)} (α : ↥(IsDedekindDomain.HeightOneSpectrum.adicCompletionIntegers F v)) (hα : α ≠ 0) : Set (TensorProduct F D (IsDedekindDomain.FiniteAdeleRing (NumberField.RingOfIntegers F) F))ˣ

The set of elements unipotent_mul_diag, that is, the elements of (D ⊗ 𝔸_F^∞)ˣ which are (α t;0 1) at v and the identity elsewhere, as t runs through a set of coset reps of 𝓞ᵥ / α. These will form a set of coset representatives for U1 diag U1.

theorem TotallyDefiniteQuaternionAlgebra.WeightTwoAutomorphicForm.HeckeOperator.unipotent_mul_diag_inj {F : Type u_1} [Field F] [NumberField F] {D : Type u_2} [Ring D] [Algebra F D] (r : IsQuaternionAlgebra.NumberField.Rigidification F D) {v : IsDedekindDomain.HeightOneSpectrum (NumberField.RingOfIntegers F)} (α : ↥(IsDedekindDomain.HeightOneSpectrum.adicCompletionIntegers F v)) (hα : α ≠ 0) : Set.InjOn (unipotent_mul_diag r α hα) ⊤

noncomputable def TotallyDefiniteQuaternionAlgebra.WeightTwoAutomorphicForm.HeckeOperator.U1diagU1 {F : Type u_1} [Field F] [NumberField F] {D : Type u_2} [Ring D] [Algebra F D] (r : IsQuaternionAlgebra.NumberField.Rigidification F D) (S : Finset (IsDedekindDomain.HeightOneSpectrum (NumberField.RingOfIntegers F))) {v : IsDedekindDomain.HeightOneSpectrum (NumberField.RingOfIntegers F)} (α : ↥(IsDedekindDomain.HeightOneSpectrum.adicCompletionIntegers F v)) (hα : α ≠ 0) : Set ((TensorProduct F D (IsDedekindDomain.FiniteAdeleRing (NumberField.RingOfIntegers F) F))ˣ ⧸ U1 r S)

The double coset space U₁(S) diag(αᵥ,1) U₁(S) as a set of left cosets.

theorem TotallyDefiniteQuaternionAlgebra.WeightTwoAutomorphicForm.HeckeOperator.bijOn_unipotent_mul_diagU1_U1diagU1 {F : Type u_1} [Field F] [NumberField F] [NumberField.IsTotallyReal F] {D : Type u_2} [Ring D] [Algebra F D] [IsQuaternionAlgebra F D] (r : IsQuaternionAlgebra.NumberField.Rigidification F D) (S : Finset (IsDedekindDomain.HeightOneSpectrum (NumberField.RingOfIntegers F))) {v : IsDedekindDomain.HeightOneSpectrum (NumberField.RingOfIntegers F)} (α : ↥(IsDedekindDomain.HeightOneSpectrum.adicCompletionIntegers F v)) (hα : α ≠ 0) : Set.BijOn QuotientGroup.mk (unipotent_mul_diag_image r α hα) (U1diagU1 r S α hα)

theorem TotallyDefiniteQuaternionAlgebra.WeightTwoAutomorphicForm.HeckeOperator.unipotent_mul_diag_image_finite {F : Type u_1} [Field F] [NumberField F] [NumberField.IsTotallyReal F] {D : Type u_2} [Ring D] [Algebra F D] [IsQuaternionAlgebra F D] (r : IsQuaternionAlgebra.NumberField.Rigidification F D) {v : IsDedekindDomain.HeightOneSpectrum (NumberField.RingOfIntegers F)} (α : ↥(IsDedekindDomain.HeightOneSpectrum.adicCompletionIntegers F v)) (hα : α ≠ 0) : (unipotent_mul_diag_image r α hα).Finite

theorem TotallyDefiniteQuaternionAlgebra.WeightTwoAutomorphicForm.HeckeOperator.quot_top_finite {F : Type u_1} [Field F] [NumberField F] [NumberField.IsTotallyReal F] {D : Type u_2} [Ring D] [Algebra F D] [IsQuaternionAlgebra F D] {v : IsDedekindDomain.HeightOneSpectrum (NumberField.RingOfIntegers F)} (r : IsQuaternionAlgebra.NumberField.Rigidification F D) (α : ↥(IsDedekindDomain.HeightOneSpectrum.adicCompletionIntegers F v)) (hα : α ≠ 0) : ⊤.Finite

noncomputable def TotallyDefiniteQuaternionAlgebra.WeightTwoAutomorphicForm.HeckeOperator.U {F : Type u_1} [Field F] [NumberField F] [NumberField.IsTotallyReal F] {D : Type u_2} [Ring D] [Algebra F D] [IsQuaternionAlgebra F D] (r : IsQuaternionAlgebra.NumberField.Rigidification F D) (S : Finset (IsDedekindDomain.HeightOneSpectrum (NumberField.RingOfIntegers F))) (R : Type u_3) [CommRing R] {v : IsDedekindDomain.HeightOneSpectrum (NumberField.RingOfIntegers F)} (α : ↥(IsDedekindDomain.HeightOneSpectrum.adicCompletionIntegers F v)) (hα : α ≠ 0) : WeightTwoAutomorphicFormOfLevel (U1 r S) R →ₗ[R] WeightTwoAutomorphicFormOfLevel (U1 r S) R

The Hecke operator U_{v,α} associated to the matrix (α 0;0 1) at v, considered as an R-linear map from R-valued quaternionic weight 2 automorphic forms of level U_1(S). Here α is a nonzero element of 𝓞ᵥ. We do not demand the condition v ∈ S, the bad primes, but this operator should only be used in this setting. See also T r v for the good primes.

theorem Ne.mul {M₀ : Type u_4} [Mul M₀] [Zero M₀] [NoZeroDivisors M₀] {a b : M₀} (ha : a ≠ 0) (hb : b ≠ 0) : a * b ≠ 0

noncomputable instance TotallyDefiniteQuaternionAlgebra.WeightTwoAutomorphicForm.HeckeOperator.instDistribSMulUnitsTensorProductFiniteAdeleRingRingOfIntegers {F : Type u_1} [Field F] [NumberField F] {D : Type u_2} [Ring D] [Algebra F D] [IsQuaternionAlgebra F D] (R : Type u_3) [CommRing R] : DistribSMul (TensorProduct F D (IsDedekindDomain.FiniteAdeleRing (NumberField.RingOfIntegers F) F))ˣ (WeightTwoAutomorphicForm F D R)

theorem TotallyDefiniteQuaternionAlgebra.WeightTwoAutomorphicForm.HeckeOperator.U_apply {F : Type u_1} [Field F] [NumberField F] [NumberField.IsTotallyReal F] {D : Type u_2} [Ring D] [Algebra F D] [IsQuaternionAlgebra F D] (r : IsQuaternionAlgebra.NumberField.Rigidification F D) (S : Finset (IsDedekindDomain.HeightOneSpectrum (NumberField.RingOfIntegers F))) (R : Type u_3) [CommRing R] {v : IsDedekindDomain.HeightOneSpectrum (NumberField.RingOfIntegers F)} (α : ↥(IsDedekindDomain.HeightOneSpectrum.adicCompletionIntegers F v)) (hα : α ≠ 0) (a : WeightTwoAutomorphicFormOfLevel (U1 r S) R) : ↑((U r S R α hα) a) = ∑ᶠ (gᵢ : (TensorProduct F D (IsDedekindDomain.FiniteAdeleRing (NumberField.RingOfIntegers F) F))ˣ) (_ : gᵢ ∈ Quotient.out '' U1diagU1 r S α hα), gᵢ • ↑a

theorem TotallyDefiniteQuaternionAlgebra.WeightTwoAutomorphicForm.HeckeOperator.U_apply_eq_finsum_unipotent_mul_diag_image {F : Type u_1} [Field F] [NumberField F] [NumberField.IsTotallyReal F] {D : Type u_2} [Ring D] [Algebra F D] [IsQuaternionAlgebra F D] (r : IsQuaternionAlgebra.NumberField.Rigidification F D) (S : Finset (IsDedekindDomain.HeightOneSpectrum (NumberField.RingOfIntegers F))) (R : Type u_3) [CommRing R] {v : IsDedekindDomain.HeightOneSpectrum (NumberField.RingOfIntegers F)} (α : ↥(IsDedekindDomain.HeightOneSpectrum.adicCompletionIntegers F v)) (hα : α ≠ 0) (a : WeightTwoAutomorphicFormOfLevel (U1 r S) R) : ↑((U r S R α hα) a) = ∑ᶠ (g : (TensorProduct F D (IsDedekindDomain.FiniteAdeleRing (NumberField.RingOfIntegers F) F))ˣ) (_ : g ∈ unipotent_mul_diag_image r α hα), g • ↑a

theorem TotallyDefiniteQuaternionAlgebra.WeightTwoAutomorphicForm.HeckeOperator.U_mul_aux {F : Type u_1} [Field F] [NumberField F] [NumberField.IsTotallyReal F] {D : Type u_2} [Ring D] [Algebra F D] [IsQuaternionAlgebra F D] (r : IsQuaternionAlgebra.NumberField.Rigidification F D) (S : Finset (IsDedekindDomain.HeightOneSpectrum (NumberField.RingOfIntegers F))) (R : Type u_3) [CommRing R] {v : IsDedekindDomain.HeightOneSpectrum (NumberField.RingOfIntegers F)} {α β : ↥(IsDedekindDomain.HeightOneSpectrum.adicCompletionIntegers F v)} (hα : α ≠ 0) (hβ : β ≠ 0) (a : WeightTwoAutomorphicFormOfLevel (U1 r S) R) : ∑ᶠ (i : ↥(IsDedekindDomain.HeightOneSpectrum.adicCompletionIntegers F v) ⧸ Ideal.span {α}) (j : ↥(IsDedekindDomain.HeightOneSpectrum.adicCompletionIntegers F v) ⧸ Ideal.span {β}), unipotent_mul_diag r α hα i • unipotent_mul_diag r β hβ j • ↑a = ∑ᶠ (k : ↥(IsDedekindDomain.HeightOneSpectrum.adicCompletionIntegers F v) ⧸ Ideal.span {α * β}), unipotent_mul_diag r (α * β) ⋯ k • ↑a

theorem TotallyDefiniteQuaternionAlgebra.WeightTwoAutomorphicForm.HeckeOperator.U_mul {F : Type u_1} [Field F] [NumberField F] [NumberField.IsTotallyReal F] {D : Type u_2} [Ring D] [Algebra F D] [IsQuaternionAlgebra F D] (r : IsQuaternionAlgebra.NumberField.Rigidification F D) (S : Finset (IsDedekindDomain.HeightOneSpectrum (NumberField.RingOfIntegers F))) (R : Type u_3) [CommRing R] {v : IsDedekindDomain.HeightOneSpectrum (NumberField.RingOfIntegers F)} {α β : ↥(IsDedekindDomain.HeightOneSpectrum.adicCompletionIntegers F v)} (hα : α ≠ 0) (hβ : β ≠ 0) : U r S R α hα ∘ₗ U r S R β hβ = U r S R (α * β) ⋯

theorem TotallyDefiniteQuaternionAlgebra.WeightTwoAutomorphicForm.HeckeOperator.U_comm {F : Type u_1} [Field F] [NumberField F] [NumberField.IsTotallyReal F] {D : Type u_2} [Ring D] [Algebra F D] [IsQuaternionAlgebra F D] (r : IsQuaternionAlgebra.NumberField.Rigidification F D) (S : Finset (IsDedekindDomain.HeightOneSpectrum (NumberField.RingOfIntegers F))) (R : Type u_3) [CommRing R] {v : IsDedekindDomain.HeightOneSpectrum (NumberField.RingOfIntegers F)} {α β : ↥(IsDedekindDomain.HeightOneSpectrum.adicCompletionIntegers F v)} (hα : α ≠ 0) (hβ : β ≠ 0) : U r S R α hα ∘ₗ U r S R β hβ = U r S R β hβ ∘ₗ U r S R α hα

def TotallyDefiniteQuaternionAlgebra.WeightTwoAutomorphicForm.HeckeAlgebra (F : Type u_1) [Field F] [NumberField F] [NumberField.IsTotallyReal F] (D : Type u_2) [Ring D] [Algebra F D] [IsQuaternionAlgebra F D] (r : IsQuaternionAlgebra.NumberField.Rigidification F D) (S : Finset (IsDedekindDomain.HeightOneSpectrum (NumberField.RingOfIntegers F))) (R : Type u_3) [CommRing R] : Type (max (max u_1 u_2) u_3)

HeckeAlgebra F D r S R is the Hecke algebra associated to the weight 2 R-valued automorphic forms associated to the discriminant 1 totally definite quaternion algebra D over the totally real field F, of level U₁(S) where S is a finite set of nonzero primes v of 𝓞 F. To make sense of this definition we choose a rigidification r, that is, a fixed 𝔸_F^∞-linear isomorphism D ⊗[F] 𝔸_F^∞ = M₂(𝔸_F^∞), enabling us to define level structures and Hecke operators Tᵥ and Uᵥ using 2x2 matrices.

Details: U₁(S) is the subgroup of (D ⊗[F] 𝔸_F^∞)ˣ associated, via r, to the matrices which are in GL₂(𝓞ᵥ) for all v ∉ S and which are of the form (a *; 0 a) mod v for all v ∈ S. The Hecke algebra is defined to be the sub-R-algebra of the weight 2 forms of level U₁(S) generated by the following two kinds of Hecke operators: first there are the operators Tᵥ associated to the matrices (ϖᵥ 0; 0 1) for v ∉ S (here ϖᵥ ∈ 𝔸_F^∞ is a local uniformiser supported at v). Second, there are the Hecke operators Uᵥ,ₐ for v ∈ S and 0 ≠ αᵥ ∈ 𝓞ᵥ, associated the matries (αᵥ 0; 0 1). These slightly nonstandard Hecke operators satisfy Uᵥ,ₛ * Uᵥ,ₜ = Uᵥ,ₛₜ and in particular this Hecke algebra is commutative (Hecke operators supported at distinct primes commute because the decomposition of the double cosets into single cosets can be done purely locally).

noncomputable instance TotallyDefiniteQuaternionAlgebra.WeightTwoAutomorphicForm.HeckeAlgebra.instRing (F : Type u_1) [Field F] [NumberField F] [NumberField.IsTotallyReal F] (D : Type u_2) [Ring D] [Algebra F D] [IsQuaternionAlgebra F D] (r : IsQuaternionAlgebra.NumberField.Rigidification F D) (S : Finset (IsDedekindDomain.HeightOneSpectrum (NumberField.RingOfIntegers F))) (R : Type u_3) [CommRing R] : Ring (HeckeAlgebra F D r S R)

noncomputable instance TotallyDefiniteQuaternionAlgebra.WeightTwoAutomorphicForm.HeckeAlgebra.instAlgebra (F : Type u_1) [Field F] [NumberField F] [NumberField.IsTotallyReal F] (D : Type u_2) [Ring D] [Algebra F D] [IsQuaternionAlgebra F D] (r : IsQuaternionAlgebra.NumberField.Rigidification F D) (S : Finset (IsDedekindDomain.HeightOneSpectrum (NumberField.RingOfIntegers F))) (R : Type u_3) [CommRing R] : Algebra R (HeckeAlgebra F D r S R)

noncomputable instance TotallyDefiniteQuaternionAlgebra.WeightTwoAutomorphicForm.HeckeAlgebra.instCommRing (F : Type u_1) [Field F] [NumberField F] [NumberField.IsTotallyReal F] (D : Type u_2) [Ring D] [Algebra F D] [IsQuaternionAlgebra F D] (r : IsQuaternionAlgebra.NumberField.Rigidification F D) (S : Finset (IsDedekindDomain.HeightOneSpectrum (NumberField.RingOfIntegers F))) (R : Type u_3) [CommRing R] : CommRing (HeckeAlgebra F D r S R)

noncomputable def TotallyDefiniteQuaternionAlgebra.WeightTwoAutomorphicForm.HeckeAlgebra.T {F : Type u_1} [Field F] [NumberField F] [NumberField.IsTotallyReal F] (D : Type u_2) [Ring D] [Algebra F D] [IsQuaternionAlgebra F D] (r : IsQuaternionAlgebra.NumberField.Rigidification F D) {S : Finset (IsDedekindDomain.HeightOneSpectrum (NumberField.RingOfIntegers F))} (R : Type u_3) [CommRing R] (v : IsDedekindDomain.HeightOneSpectrum (NumberField.RingOfIntegers F)) (hv : v ∉ S) : HeckeAlgebra F D r S R

The Hecke operator Tᵥ as an element of the Hecke algebra.

noncomputable def TotallyDefiniteQuaternionAlgebra.WeightTwoAutomorphicForm.HeckeAlgebra.U {F : Type u_1} [Field F] [NumberField F] [NumberField.IsTotallyReal F] (D : Type u_2) [Ring D] [Algebra F D] [IsQuaternionAlgebra F D] (r : IsQuaternionAlgebra.NumberField.Rigidification F D) {S : Finset (IsDedekindDomain.HeightOneSpectrum (NumberField.RingOfIntegers F))} (R : Type u_3) [CommRing R] (v : IsDedekindDomain.HeightOneSpectrum (NumberField.RingOfIntegers F)) (hv : v ∈ S) (α : ↥(IsDedekindDomain.HeightOneSpectrum.adicCompletionIntegers F v)) (hα : α ≠ 0) : HeckeAlgebra F D r S R

The Hecke operator Uᵥ,ₐ as an element of the Hecke algebra.