@[reducible, inline]

noncomputable abbrev TotallyDefiniteQuaternionAlgebra.Dfx (F : Type u_1) [Field F] [NumberField F] (D : Type u_2) [Ring D] [Algebra F D] : Type (max u_1 u_2)

Equations

• TotallyDefiniteQuaternionAlgebra.Dfx F D = (TensorProduct F D (DedekindDomain.FiniteAdeleRing (NumberField.RingOfIntegers F) F))ˣ

@[reducible, inline]

noncomputable abbrev TotallyDefiniteQuaternionAlgebra.incl₁ {F : Type u_1} [Field F] [NumberField F] {D : Type u_2} [Ring D] [Algebra F D] : Dˣ →* TotallyDefiniteQuaternionAlgebra.Dfx F D

Equations

• TotallyDefiniteQuaternionAlgebra.incl₁ = Units.map ↑Algebra.TensorProduct.includeLeftRingHom

@[reducible, inline]

noncomputable abbrev TotallyDefiniteQuaternionAlgebra.incl₂ (F : Type u_1) [Field F] [NumberField F] (D : Type u_2) [Ring D] [Algebra F D] : (DedekindDomain.FiniteAdeleRing (NumberField.RingOfIntegers F) F)ˣ →* TotallyDefiniteQuaternionAlgebra.Dfx F D

Equations

• TotallyDefiniteQuaternionAlgebra.incl₂ F D = Units.map ↑Algebra.toRingHom

This definition is made in mathlib-generality but is not the definition of an automorphic form unless Dˣ is compact mod centre at infinity. This hypothesis will be true if D is a totally definite quaternion algebra.

structure TotallyDefiniteQuaternionAlgebra.AutomorphicForm (F : Type u_1) [Field F] [NumberField F] (D : Type u_2) [Ring D] [Algebra F D] (R : Type u_3) [CommRing R] (W : Type u_4) [AddCommGroup W] [Module R W] [MulAction Dˣ W] (U : Subgroup (TensorProduct F D (DedekindDomain.FiniteAdeleRing (NumberField.RingOfIntegers F) F))ˣ) (χ : (DedekindDomain.FiniteAdeleRing (NumberField.RingOfIntegers F) F)ˣ →* R) : Type (max (max u_1 u_2) u_4)

• toFun : (TensorProduct F D (DedekindDomain.FiniteAdeleRing (NumberField.RingOfIntegers F) F))ˣ → W
• left_invt : ∀ (δ : Dˣ) (g : (TensorProduct F D (DedekindDomain.FiniteAdeleRing (NumberField.RingOfIntegers F) F))ˣ), ↑self (TotallyDefiniteQuaternionAlgebra.incl₁ δ * g) = δ • ↑self g
• has_character : ∀ (g : (TensorProduct F D (DedekindDomain.FiniteAdeleRing (NumberField.RingOfIntegers F) F))ˣ) (z : (DedekindDomain.FiniteAdeleRing (NumberField.RingOfIntegers F) F)ˣ), ↑self (g * (TotallyDefiniteQuaternionAlgebra.incl₂ F D) z) = χ z • ↑self g
• right_invt : ∀ (g u : (TensorProduct F D (DedekindDomain.FiniteAdeleRing (NumberField.RingOfIntegers F) F))ˣ), u ∈ U → ↑self (g * u) = ↑self g

theorem TotallyDefiniteQuaternionAlgebra.AutomorphicForm.left_invt {F : Type u_1} [Field F] [NumberField F] {D : Type u_2} [Ring D] [Algebra F D] {R : Type u_3} [CommRing R] {W : Type u_4} [AddCommGroup W] [Module R W] [MulAction Dˣ W] {U : Subgroup (TensorProduct F D (DedekindDomain.FiniteAdeleRing (NumberField.RingOfIntegers F) F))ˣ} {χ : (DedekindDomain.FiniteAdeleRing (NumberField.RingOfIntegers F) F)ˣ →* R} (self : TotallyDefiniteQuaternionAlgebra.AutomorphicForm F D R W U χ) (δ : Dˣ) (g : (TensorProduct F D (DedekindDomain.FiniteAdeleRing (NumberField.RingOfIntegers F) F))ˣ) : ↑self (TotallyDefiniteQuaternionAlgebra.incl₁ δ * g) = δ • ↑self g

theorem TotallyDefiniteQuaternionAlgebra.AutomorphicForm.has_character {F : Type u_1} [Field F] [NumberField F] {D : Type u_2} [Ring D] [Algebra F D] {R : Type u_3} [CommRing R] {W : Type u_4} [AddCommGroup W] [Module R W] [MulAction Dˣ W] {U : Subgroup (TensorProduct F D (DedekindDomain.FiniteAdeleRing (NumberField.RingOfIntegers F) F))ˣ} {χ : (DedekindDomain.FiniteAdeleRing (NumberField.RingOfIntegers F) F)ˣ →* R} (self : TotallyDefiniteQuaternionAlgebra.AutomorphicForm F D R W U χ) (g : (TensorProduct F D (DedekindDomain.FiniteAdeleRing (NumberField.RingOfIntegers F) F))ˣ) (z : (DedekindDomain.FiniteAdeleRing (NumberField.RingOfIntegers F) F)ˣ) : ↑self (g * (TotallyDefiniteQuaternionAlgebra.incl₂ F D) z) = χ z • ↑self g

theorem TotallyDefiniteQuaternionAlgebra.AutomorphicForm.right_invt {F : Type u_1} [Field F] [NumberField F] {D : Type u_2} [Ring D] [Algebra F D] {R : Type u_3} [CommRing R] {W : Type u_4} [AddCommGroup W] [Module R W] [MulAction Dˣ W] {U : Subgroup (TensorProduct F D (DedekindDomain.FiniteAdeleRing (NumberField.RingOfIntegers F) F))ˣ} {χ : (DedekindDomain.FiniteAdeleRing (NumberField.RingOfIntegers F) F)ˣ →* R} (self : TotallyDefiniteQuaternionAlgebra.AutomorphicForm F D R W U χ) (g : (TensorProduct F D (DedekindDomain.FiniteAdeleRing (NumberField.RingOfIntegers F) F))ˣ) (u : (TensorProduct F D (DedekindDomain.FiniteAdeleRing (NumberField.RingOfIntegers F) F))ˣ) : u ∈ U → ↑self (g * u) = ↑self g

noncomputable instance TotallyDefiniteQuaternionAlgebra.AutomorphicForm.instCoeFunForallDfx {F : Type u_1} [Field F] [NumberField F] {D : Type u_2} [Ring D] [Algebra F D] {R : Type u_3} [CommRing R] {W : Type u_4} [AddCommGroup W] [Module R W] [DistribMulAction Dˣ W] {U : Subgroup (TensorProduct F D (DedekindDomain.FiniteAdeleRing (NumberField.RingOfIntegers F) F))ˣ} {χ : (DedekindDomain.FiniteAdeleRing (NumberField.RingOfIntegers F) F)ˣ →* R} : CoeFun (TotallyDefiniteQuaternionAlgebra.AutomorphicForm F D R W U χ) fun (x : TotallyDefiniteQuaternionAlgebra.AutomorphicForm F D R W U χ) => TotallyDefiniteQuaternionAlgebra.Dfx F D → W

Equations

• TotallyDefiniteQuaternionAlgebra.AutomorphicForm.instCoeFunForallDfx = { coe := TotallyDefiniteQuaternionAlgebra.AutomorphicForm.toFun }

theorem TotallyDefiniteQuaternionAlgebra.AutomorphicForm.ext {F : Type u_1} [Field F] [NumberField F] {D : Type u_2} [Ring D] [Algebra F D] {R : Type u_3} [CommRing R] {W : Type u_4} [AddCommGroup W] [Module R W] [DistribMulAction Dˣ W] {U : Subgroup (TensorProduct F D (DedekindDomain.FiniteAdeleRing (NumberField.RingOfIntegers F) F))ˣ} {χ : (DedekindDomain.FiniteAdeleRing (NumberField.RingOfIntegers F) F)ˣ →* R} (φ : TotallyDefiniteQuaternionAlgebra.AutomorphicForm F D R W U χ) (ψ : TotallyDefiniteQuaternionAlgebra.AutomorphicForm F D R W U χ) (h : ∀ (x : (TensorProduct F D (DedekindDomain.FiniteAdeleRing (NumberField.RingOfIntegers F) F))ˣ), ↑φ x = ↑ψ x) : φ = ψ

noncomputable def TotallyDefiniteQuaternionAlgebra.AutomorphicForm.zero {F : Type u_1} [Field F] [NumberField F] {D : Type u_2} [Ring D] [Algebra F D] {R : Type u_3} [CommRing R] {W : Type u_4} [AddCommGroup W] [Module R W] [DistribMulAction Dˣ W] {U : Subgroup (TensorProduct F D (DedekindDomain.FiniteAdeleRing (NumberField.RingOfIntegers F) F))ˣ} {χ : (DedekindDomain.FiniteAdeleRing (NumberField.RingOfIntegers F) F)ˣ →* R} : TotallyDefiniteQuaternionAlgebra.AutomorphicForm F D R W U χ

Equations

• TotallyDefiniteQuaternionAlgebra.AutomorphicForm.zero = { toFun := 0, left_invt := ⋯, has_character := ⋯, right_invt := ⋯ }

noncomputable instance TotallyDefiniteQuaternionAlgebra.AutomorphicForm.instZero {F : Type u_1} [Field F] [NumberField F] {D : Type u_2} [Ring D] [Algebra F D] {R : Type u_3} [CommRing R] {W : Type u_4} [AddCommGroup W] [Module R W] [DistribMulAction Dˣ W] {U : Subgroup (TensorProduct F D (DedekindDomain.FiniteAdeleRing (NumberField.RingOfIntegers F) F))ˣ} {χ : (DedekindDomain.FiniteAdeleRing (NumberField.RingOfIntegers F) F)ˣ →* R} : Zero (TotallyDefiniteQuaternionAlgebra.AutomorphicForm F D R W U χ)

Equations

• TotallyDefiniteQuaternionAlgebra.AutomorphicForm.instZero = { zero := TotallyDefiniteQuaternionAlgebra.AutomorphicForm.zero }

@[simp]

theorem TotallyDefiniteQuaternionAlgebra.AutomorphicForm.zero_apply {F : Type u_1} [Field F] [NumberField F] {D : Type u_2} [Ring D] [Algebra F D] {R : Type u_3} [CommRing R] {W : Type u_4} [AddCommGroup W] [Module R W] [DistribMulAction Dˣ W] {U : Subgroup (TensorProduct F D (DedekindDomain.FiniteAdeleRing (NumberField.RingOfIntegers F) F))ˣ} {χ : (DedekindDomain.FiniteAdeleRing (NumberField.RingOfIntegers F) F)ˣ →* R} (x : (TensorProduct F D (DedekindDomain.FiniteAdeleRing (NumberField.RingOfIntegers F) F))ˣ) : ↑0 x = 0

noncomputable def TotallyDefiniteQuaternionAlgebra.AutomorphicForm.neg {F : Type u_1} [Field F] [NumberField F] {D : Type u_2} [Ring D] [Algebra F D] {R : Type u_3} [CommRing R] {W : Type u_4} [AddCommGroup W] [Module R W] [DistribMulAction Dˣ W] {U : Subgroup (TensorProduct F D (DedekindDomain.FiniteAdeleRing (NumberField.RingOfIntegers F) F))ˣ} {χ : (DedekindDomain.FiniteAdeleRing (NumberField.RingOfIntegers F) F)ˣ →* R} (φ : TotallyDefiniteQuaternionAlgebra.AutomorphicForm F D R W U χ) : TotallyDefiniteQuaternionAlgebra.AutomorphicForm F D R W U χ

Equations

• φ.neg = { toFun := fun (x : (TensorProduct F D (DedekindDomain.FiniteAdeleRing (NumberField.RingOfIntegers F) F))ˣ) => -↑φ x, left_invt := ⋯, has_character := ⋯, right_invt := ⋯ }

noncomputable instance TotallyDefiniteQuaternionAlgebra.AutomorphicForm.instNeg {F : Type u_1} [Field F] [NumberField F] {D : Type u_2} [Ring D] [Algebra F D] {R : Type u_3} [CommRing R] {W : Type u_4} [AddCommGroup W] [Module R W] [DistribMulAction Dˣ W] {U : Subgroup (TensorProduct F D (DedekindDomain.FiniteAdeleRing (NumberField.RingOfIntegers F) F))ˣ} {χ : (DedekindDomain.FiniteAdeleRing (NumberField.RingOfIntegers F) F)ˣ →* R} : Neg (TotallyDefiniteQuaternionAlgebra.AutomorphicForm F D R W U χ)

Equations

• TotallyDefiniteQuaternionAlgebra.AutomorphicForm.instNeg = { neg := TotallyDefiniteQuaternionAlgebra.AutomorphicForm.neg }

@[simp]

theorem TotallyDefiniteQuaternionAlgebra.AutomorphicForm.neg_apply {F : Type u_1} [Field F] [NumberField F] {D : Type u_2} [Ring D] [Algebra F D] {R : Type u_3} [CommRing R] {W : Type u_4} [AddCommGroup W] [Module R W] [DistribMulAction Dˣ W] {U : Subgroup (TensorProduct F D (DedekindDomain.FiniteAdeleRing (NumberField.RingOfIntegers F) F))ˣ} {χ : (DedekindDomain.FiniteAdeleRing (NumberField.RingOfIntegers F) F)ˣ →* R} (φ : TotallyDefiniteQuaternionAlgebra.AutomorphicForm F D R W U χ) (x : (TensorProduct F D (DedekindDomain.FiniteAdeleRing (NumberField.RingOfIntegers F) F))ˣ) : ↑(-φ) x = -↑φ x

noncomputable instance TotallyDefiniteQuaternionAlgebra.AutomorphicForm.instAdd {F : Type u_1} [Field F] [NumberField F] {D : Type u_2} [Ring D] [Algebra F D] {R : Type u_3} [CommRing R] {W : Type u_4} [AddCommGroup W] [Module R W] [DistribMulAction Dˣ W] {U : Subgroup (TensorProduct F D (DedekindDomain.FiniteAdeleRing (NumberField.RingOfIntegers F) F))ˣ} {χ : (DedekindDomain.FiniteAdeleRing (NumberField.RingOfIntegers F) F)ˣ →* R} : Add (TotallyDefiniteQuaternionAlgebra.AutomorphicForm F D R W U χ)

Equations

• TotallyDefiniteQuaternionAlgebra.AutomorphicForm.instAdd = { add := TotallyDefiniteQuaternionAlgebra.AutomorphicForm.add }

@[simp]

theorem TotallyDefiniteQuaternionAlgebra.AutomorphicForm.add_apply {F : Type u_1} [Field F] [NumberField F] {D : Type u_2} [Ring D] [Algebra F D] {R : Type u_3} [CommRing R] {W : Type u_4} [AddCommGroup W] [Module R W] [DistribMulAction Dˣ W] {U : Subgroup (TensorProduct F D (DedekindDomain.FiniteAdeleRing (NumberField.RingOfIntegers F) F))ˣ} {χ : (DedekindDomain.FiniteAdeleRing (NumberField.RingOfIntegers F) F)ˣ →* R} (φ : TotallyDefiniteQuaternionAlgebra.AutomorphicForm F D R W U χ) (ψ : TotallyDefiniteQuaternionAlgebra.AutomorphicForm F D R W U χ) (x : (TensorProduct F D (DedekindDomain.FiniteAdeleRing (NumberField.RingOfIntegers F) F))ˣ) : ↑(φ + ψ) x = ↑φ x + ↑ψ x

noncomputable instance TotallyDefiniteQuaternionAlgebra.AutomorphicForm.addCommGroup {F : Type u_1} [Field F] [NumberField F] {D : Type u_2} [Ring D] [Algebra F D] {R : Type u_3} [CommRing R] {W : Type u_4} [AddCommGroup W] [Module R W] [DistribMulAction Dˣ W] {U : Subgroup (TensorProduct F D (DedekindDomain.FiniteAdeleRing (NumberField.RingOfIntegers F) F))ˣ} {χ : (DedekindDomain.FiniteAdeleRing (NumberField.RingOfIntegers F) F)ˣ →* R} : AddCommGroup (TotallyDefiniteQuaternionAlgebra.AutomorphicForm F D R W U χ)

Equations

• TotallyDefiniteQuaternionAlgebra.AutomorphicForm.addCommGroup = AddCommGroup.mk ⋯

noncomputable def TotallyDefiniteQuaternionAlgebra.AutomorphicForm.smul {F : Type u_1} [Field F] [NumberField F] {D : Type u_2} [Ring D] [Algebra F D] {R : Type u_3} [CommRing R] {W : Type u_4} [AddCommGroup W] [Module R W] [DistribMulAction Dˣ W] {U : Subgroup (TensorProduct F D (DedekindDomain.FiniteAdeleRing (NumberField.RingOfIntegers F) F))ˣ} {χ : (DedekindDomain.FiniteAdeleRing (NumberField.RingOfIntegers F) F)ˣ →* R} [SMulCommClass R Dˣ W] (r : R) (φ : TotallyDefiniteQuaternionAlgebra.AutomorphicForm F D R W U χ) : TotallyDefiniteQuaternionAlgebra.AutomorphicForm F D R W U χ

Equations

• One or more equations did not get rendered due to their size.

noncomputable instance TotallyDefiniteQuaternionAlgebra.AutomorphicForm.instSMul {F : Type u_1} [Field F] [NumberField F] {D : Type u_2} [Ring D] [Algebra F D] {R : Type u_3} [CommRing R] {W : Type u_4} [AddCommGroup W] [Module R W] [DistribMulAction Dˣ W] {U : Subgroup (TensorProduct F D (DedekindDomain.FiniteAdeleRing (NumberField.RingOfIntegers F) F))ˣ} {χ : (DedekindDomain.FiniteAdeleRing (NumberField.RingOfIntegers F) F)ˣ →* R} [SMulCommClass R Dˣ W] : SMul R (TotallyDefiniteQuaternionAlgebra.AutomorphicForm F D R W U χ)

Equations

• TotallyDefiniteQuaternionAlgebra.AutomorphicForm.instSMul = { smul := TotallyDefiniteQuaternionAlgebra.AutomorphicForm.smul }

theorem TotallyDefiniteQuaternionAlgebra.AutomorphicForm.smul_apply {F : Type u_1} [Field F] [NumberField F] {D : Type u_2} [Ring D] [Algebra F D] {R : Type u_3} [CommRing R] {W : Type u_4} [AddCommGroup W] [Module R W] [DistribMulAction Dˣ W] {U : Subgroup (TensorProduct F D (DedekindDomain.FiniteAdeleRing (NumberField.RingOfIntegers F) F))ˣ} {χ : (DedekindDomain.FiniteAdeleRing (NumberField.RingOfIntegers F) F)ˣ →* R} [SMulCommClass R Dˣ W] (r : R) (φ : TotallyDefiniteQuaternionAlgebra.AutomorphicForm F D R W U χ) (g : (TensorProduct F D (DedekindDomain.FiniteAdeleRing (NumberField.RingOfIntegers F) F))ˣ) : ↑(r • φ) g = r • ↑φ g

noncomputable instance TotallyDefiniteQuaternionAlgebra.AutomorphicForm.module {F : Type u_1} [Field F] [NumberField F] {D : Type u_2} [Ring D] [Algebra F D] {R : Type u_3} [CommRing R] {W : Type u_4} [AddCommGroup W] [Module R W] [DistribMulAction Dˣ W] {U : Subgroup (TensorProduct F D (DedekindDomain.FiniteAdeleRing (NumberField.RingOfIntegers F) F))ˣ} {χ : (DedekindDomain.FiniteAdeleRing (NumberField.RingOfIntegers F) F)ˣ →* R} [SMulCommClass R Dˣ W] : Module R (TotallyDefiniteQuaternionAlgebra.AutomorphicForm F D R W U χ)

Equations

• TotallyDefiniteQuaternionAlgebra.AutomorphicForm.module = Module.mk ⋯ ⋯

theorem TotallyDefiniteQuaternionAlgebra.AutomorphicForm.finiteDimensional (F : Type u_1) [Field F] [NumberField F] (D : Type u_2) [Ring D] [Algebra F D] (R : Type u_3) [Field R] (W : Type u_4) [AddCommGroup W] [Module R W] [DistribMulAction Dˣ W] [SMulCommClass R Dˣ W] (U : Subgroup (TensorProduct F D (DedekindDomain.FiniteAdeleRing (NumberField.RingOfIntegers F) F))ˣ) (χ : (DedekindDomain.FiniteAdeleRing (NumberField.RingOfIntegers F) F)ˣ →* R) [FiniteDimensional R W] : FiniteDimensional R (TotallyDefiniteQuaternionAlgebra.AutomorphicForm F D R W U χ)