FLT.AutomorphicForm.QuaternionAlgebra

source

noncomputable instance instTopologicalSpaceFiniteAdeleRingRingOfIntegers_fLT (F : Type u_1) [Field F] [NumberField F] :

TopologicalSpace (DedekindDomain.FiniteAdeleRing (NumberField.RingOfIntegers F) F)

Equations

instTopologicalSpaceFiniteAdeleRingRingOfIntegers_fLT F = sorryAx (TopologicalSpace (DedekindDomain.FiniteAdeleRing (NumberField.RingOfIntegers F) F))

source

noncomputable instance instTopologicalRingFiniteAdeleRingRingOfIntegers_fLT (F : Type u_1) [Field F] [NumberField F] :

TopologicalRing (DedekindDomain.FiniteAdeleRing (NumberField.RingOfIntegers F) F)

Equations

⋯ = ⋯

source

noncomputable instance instAlgebraTensorProduct_fLT {R : Type u_3} {D : Type u_4} {A : Type u_5} [CommRing R] [Ring D] [CommRing A] [Algebra R D] [Algebra R A] :

Algebra A (TensorProduct R D A)

Equations

instAlgebraTensorProduct_fLT = Algebra.TensorProduct.includeRight.toAlgebra' ⋯

source

noncomputable instance instFiniteTensorProduct_fLT {R : Type u_3} {D : Type u_4} {A : Type u_5} [CommRing R] [Ring D] [CommRing A] [Algebra R D] [Algebra R A] [Module.Finite R D] :

Module.Finite A (TensorProduct R D A)

Equations

⋯ = ⋯

source

noncomputable instance instFreeTensorProduct_fLT {R : Type u_3} {D : Type u_4} {A : Type u_5} [CommRing R] [Ring D] [CommRing A] [Algebra R D] [Algebra R A] [Module.Free R D] :

Module.Free A (TensorProduct R D A)

Equations

⋯ = ⋯

source

noncomputable instance instTopologicalSpaceTensorProductFiniteAdeleRingRingOfIntegers_fLT (F : Type u_1) [Field F] [NumberField F] (D : Type u_2) [Ring D] [Algebra F D] :

TopologicalSpace (TensorProduct F D (DedekindDomain.FiniteAdeleRing (NumberField.RingOfIntegers F) F))

Equations

instTopologicalSpaceTensorProductFiniteAdeleRingRingOfIntegers_fLT F D = Module.topology (DedekindDomain.FiniteAdeleRing (NumberField.RingOfIntegers F) F)

source

noncomputable instance instTopologicalRingTensorProductFiniteAdeleRingRingOfIntegers_fLT (F : Type u_1) [Field F] [NumberField F] (D : Type u_2) [Ring D] [Algebra F D] [FiniteDimensional F D] :

TopologicalRing (TensorProduct F D (DedekindDomain.FiniteAdeleRing (NumberField.RingOfIntegers F) F))

Equations

⋯ = ⋯

source

@[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))ˣ

Instances For

source

@[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 F D = Units.map ↑Algebra.TensorProduct.includeLeftRingHom

Instances For

source

structure TotallyDefiniteQuaternionAlgebra.AutomorphicForm (F : Type u_1) [Field F] [NumberField F] (D : Type u_2) [Ring D] [Algebra F D] (M : Type u_3) [AddCommGroup M] :

Type (max (max u_1 u_2) u_3)

toFun : (TensorProduct F D (DedekindDomain.FiniteAdeleRing (NumberField.RingOfIntegers F) F))ˣ → M
left_invt : ∀ (d : Dˣ) (x : (TensorProduct F D (DedekindDomain.FiniteAdeleRing (NumberField.RingOfIntegers F) F))ˣ), ↑self ((Units.map ↑Algebra.TensorProduct.includeLeftRingHom) d * x) = ↑self x
loc_cst : ∃ (U : Subgroup (TensorProduct F D (DedekindDomain.FiniteAdeleRing (NumberField.RingOfIntegers F) F))ˣ), IsOpen ↑U ∧ ∀ (x u : (TensorProduct F D (DedekindDomain.FiniteAdeleRing (NumberField.RingOfIntegers F) F))ˣ), u ∈ U → ↑self (x * u) = ↑self x

Instances For

source

theorem TotallyDefiniteQuaternionAlgebra.AutomorphicForm.left_invt {F : Type u_1} [Field F] [NumberField F] {D : Type u_2} [Ring D] [Algebra F D] {M : Type u_3} [AddCommGroup M] (self : TotallyDefiniteQuaternionAlgebra.AutomorphicForm F D M) (d : Dˣ) (x : (TensorProduct F D (DedekindDomain.FiniteAdeleRing (NumberField.RingOfIntegers F) F))ˣ) :

↑self ((Units.map ↑Algebra.TensorProduct.includeLeftRingHom) d * x) = ↑self x

source

theorem TotallyDefiniteQuaternionAlgebra.AutomorphicForm.loc_cst {F : Type u_1} [Field F] [NumberField F] {D : Type u_2} [Ring D] [Algebra F D] {M : Type u_3} [AddCommGroup M] (self : TotallyDefiniteQuaternionAlgebra.AutomorphicForm F D M) :

∃ (U : Subgroup (TensorProduct F D (DedekindDomain.FiniteAdeleRing (NumberField.RingOfIntegers F) F))ˣ), IsOpen ↑U ∧ ∀ (x u : (TensorProduct F D (DedekindDomain.FiniteAdeleRing (NumberField.RingOfIntegers F) F))ˣ), u ∈ U → ↑self (x * u) = ↑self x

source

noncomputable instance TotallyDefiniteQuaternionAlgebra.AutomorphicForm.instCoeFunForallDfx {F : Type u_1} [Field F] [NumberField F] {D : Type u_2} [Ring D] [Algebra F D] {M : Type u_3} [AddCommGroup M] :

CoeFun (TotallyDefiniteQuaternionAlgebra.AutomorphicForm F D M) fun (x : TotallyDefiniteQuaternionAlgebra.AutomorphicForm F D M) => TotallyDefiniteQuaternionAlgebra.Dfx F D → M

Equations

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

source

theorem TotallyDefiniteQuaternionAlgebra.AutomorphicForm.ext_iff {F : Type u_1} [Field F] [NumberField F] {D : Type u_2} [Ring D] [Algebra F D] [FiniteDimensional F D] {M : Type u_3} [AddCommGroup M] {φ : TotallyDefiniteQuaternionAlgebra.AutomorphicForm F D M} {ψ : TotallyDefiniteQuaternionAlgebra.AutomorphicForm F D M} :

φ = ψ ↔ ∀ (x : (TensorProduct F D (DedekindDomain.FiniteAdeleRing (NumberField.RingOfIntegers F) F))ˣ), ↑φ x = ↑ψ x

source

theorem TotallyDefiniteQuaternionAlgebra.AutomorphicForm.ext {F : Type u_1} [Field F] [NumberField F] {D : Type u_2} [Ring D] [Algebra F D] [FiniteDimensional F D] {M : Type u_3} [AddCommGroup M] (φ : TotallyDefiniteQuaternionAlgebra.AutomorphicForm F D M) (ψ : TotallyDefiniteQuaternionAlgebra.AutomorphicForm F D M) (h : ∀ (x : (TensorProduct F D (DedekindDomain.FiniteAdeleRing (NumberField.RingOfIntegers F) F))ˣ), ↑φ x = ↑ψ x) :

φ = ψ

source

noncomputable def TotallyDefiniteQuaternionAlgebra.AutomorphicForm.zero {F : Type u_1} [Field F] [NumberField F] {D : Type u_2} [Ring D] [Algebra F D] {M : Type u_3} [AddCommGroup M] :

TotallyDefiniteQuaternionAlgebra.AutomorphicForm F D M

Equations

TotallyDefiniteQuaternionAlgebra.AutomorphicForm.zero = { toFun := 0, left_invt := ⋯, loc_cst := ⋯ }

Instances For

source

noncomputable instance TotallyDefiniteQuaternionAlgebra.AutomorphicForm.instZero {F : Type u_1} [Field F] [NumberField F] {D : Type u_2} [Ring D] [Algebra F D] {M : Type u_3} [AddCommGroup M] :

Zero (TotallyDefiniteQuaternionAlgebra.AutomorphicForm F D M)

Equations

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

source

@[simp]

theorem TotallyDefiniteQuaternionAlgebra.AutomorphicForm.zero_apply {F : Type u_1} [Field F] [NumberField F] {D : Type u_2} [Ring D] [Algebra F D] [FiniteDimensional F D] {M : Type u_3} [AddCommGroup M] (x : (TensorProduct F D (DedekindDomain.FiniteAdeleRing (NumberField.RingOfIntegers F) F))ˣ) :

↑0 x = 0

source

noncomputable def TotallyDefiniteQuaternionAlgebra.AutomorphicForm.neg {F : Type u_1} [Field F] [NumberField F] {D : Type u_2} [Ring D] [Algebra F D] {M : Type u_3} [AddCommGroup M] (φ : TotallyDefiniteQuaternionAlgebra.AutomorphicForm F D M) :

TotallyDefiniteQuaternionAlgebra.AutomorphicForm F D M

Equations

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

Instances For

source

noncomputable instance TotallyDefiniteQuaternionAlgebra.AutomorphicForm.instNeg {F : Type u_1} [Field F] [NumberField F] {D : Type u_2} [Ring D] [Algebra F D] {M : Type u_3} [AddCommGroup M] :

Neg (TotallyDefiniteQuaternionAlgebra.AutomorphicForm F D M)

Equations

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

source

@[simp]

theorem TotallyDefiniteQuaternionAlgebra.AutomorphicForm.neg_apply {F : Type u_1} [Field F] [NumberField F] {D : Type u_2} [Ring D] [Algebra F D] [FiniteDimensional F D] {M : Type u_3} [AddCommGroup M] (φ : TotallyDefiniteQuaternionAlgebra.AutomorphicForm F D M) (x : (TensorProduct F D (DedekindDomain.FiniteAdeleRing (NumberField.RingOfIntegers F) F))ˣ) :

↑(-φ) x = -↑φ x

source

noncomputable instance TotallyDefiniteQuaternionAlgebra.AutomorphicForm.instAdd {F : Type u_1} [Field F] [NumberField F] {D : Type u_2} [Ring D] [Algebra F D] {M : Type u_3} [AddCommGroup M] :

Add (TotallyDefiniteQuaternionAlgebra.AutomorphicForm F D M)

Equations

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

source

@[simp]

theorem TotallyDefiniteQuaternionAlgebra.AutomorphicForm.add_apply {F : Type u_1} [Field F] [NumberField F] {D : Type u_2} [Ring D] [Algebra F D] [FiniteDimensional F D] {M : Type u_3} [AddCommGroup M] (φ : TotallyDefiniteQuaternionAlgebra.AutomorphicForm F D M) (ψ : TotallyDefiniteQuaternionAlgebra.AutomorphicForm F D M) (x : (TensorProduct F D (DedekindDomain.FiniteAdeleRing (NumberField.RingOfIntegers F) F))ˣ) :

↑(φ + ψ) x = ↑φ x + ↑ψ x

source

noncomputable instance TotallyDefiniteQuaternionAlgebra.AutomorphicForm.addCommGroup {F : Type u_1} [Field F] [NumberField F] {D : Type u_2} [Ring D] [Algebra F D] [FiniteDimensional F D] {M : Type u_3} [AddCommGroup M] :

AddCommGroup (TotallyDefiniteQuaternionAlgebra.AutomorphicForm F D M)

Equations

TotallyDefiniteQuaternionAlgebra.AutomorphicForm.addCommGroup = AddCommGroup.mk ⋯

source

theorem TotallyDefiniteQuaternionAlgebra.AutomorphicForm.conjAct_mem {G : Type u_4} [Group G] (U : Subgroup G) (g : G) (x : G) :

x ∈ ConjAct.toConjAct g • U ↔ ∃ u ∈ U, g * u * g⁻¹ = x

source

theorem TotallyDefiniteQuaternionAlgebra.AutomorphicForm.toConjAct_open {G : Type u_4} [Group G] [TopologicalSpace G] [TopologicalGroup G] (U : Subgroup G) (hU : IsOpen ↑U) (g : G) :

IsOpen (ConjAct.toConjAct g • ↑U)

source

noncomputable instance TotallyDefiniteQuaternionAlgebra.AutomorphicForm.instSMulDfx {F : Type u_1} [Field F] [NumberField F] {D : Type u_2} [Ring D] [Algebra F D] [FiniteDimensional F D] {M : Type u_3} [AddCommGroup M] :

SMul (TotallyDefiniteQuaternionAlgebra.Dfx F D) (TotallyDefiniteQuaternionAlgebra.AutomorphicForm F D M)

Equations

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

source

@[simp]

theorem TotallyDefiniteQuaternionAlgebra.AutomorphicForm.sMul_eval {F : Type u_1} [Field F] [NumberField F] {D : Type u_2} [Ring D] [Algebra F D] [FiniteDimensional F D] {M : Type u_3} [AddCommGroup M] (g : TotallyDefiniteQuaternionAlgebra.Dfx F D) (f : TotallyDefiniteQuaternionAlgebra.AutomorphicForm F D M) (x : (TensorProduct F D (DedekindDomain.FiniteAdeleRing (NumberField.RingOfIntegers F) F))ˣ) :

↑(g • f) x = ↑f (x * g)

source

noncomputable instance TotallyDefiniteQuaternionAlgebra.AutomorphicForm.instMulActionDfx {F : Type u_1} [Field F] [NumberField F] {D : Type u_2} [Ring D] [Algebra F D] [FiniteDimensional F D] {M : Type u_3} [AddCommGroup M] :

MulAction (TotallyDefiniteQuaternionAlgebra.Dfx F D) (TotallyDefiniteQuaternionAlgebra.AutomorphicForm F D M)

Equations

TotallyDefiniteQuaternionAlgebra.AutomorphicForm.instMulActionDfx = MulAction.mk ⋯ ⋯