number_theory.modular_forms.slash_invariant_forms

structure slash_invariant_form (Γ : out_param (subgroup (matrix.special_linear_group (fin 2) ℤ))) (k : out_param ℤ) :

to_fun : upper_half_plane → ℂ
slash_action_eq' : ∀ (γ : ↥Γ), slash_action.map ℂ k γ self.to_fun = self.to_fun

Functions ℍ → ℂ that are invariant under the slash_action.

Instances for slash_invariant_form

@[class]

structure slash_invariant_form_class (F : Type u_1) (Γ : out_param (subgroup (matrix.special_linear_group (fin 2) ℤ))) (k : out_param ℤ) :

Type u_1

coe : F → Π (a : upper_half_plane), (λ (_x : upper_half_plane), ℂ) a
coe_injective' : function.injective slash_invariant_form_class.coe
slash_action_eq : ∀ (f : F) (γ : ↥Γ), slash_action.map ℂ k γ ⇑f = ⇑f

slash_invariant_form_class F Γ k asserts F is a type of bundled functions that are invariant under the slash_action.

Instances of this typeclass

Instances of other typeclasses for slash_invariant_form_class

slash_invariant_form_class.has_sizeof_inst

source

@[nolint, instance]

def slash_invariant_form_class.to_fun_like (F : Type u_1) (Γ : out_param (subgroup (matrix.special_linear_group (fin 2) ℤ))) (k : out_param ℤ) [self : slash_invariant_form_class F Γ k] :

fun_like F upper_half_plane (λ (_x : upper_half_plane), ℂ)

source

@[protected, instance]

def slash_invariant_form_class.slash_invariant_form (Γ : out_param (subgroup (matrix.special_linear_group (fin 2) ℤ))) (k : out_param ℤ) :

slash_invariant_form_class (slash_invariant_form Γ k) Γ k

Equations

slash_invariant_form_class.slash_invariant_form Γ k = {coe := slash_invariant_form.to_fun k, coe_injective' := _, slash_action_eq := _}

source

@[protected, instance]

def slash_invariant_form.has_coe_to_fun {Γ : out_param (subgroup (matrix.special_linear_group (fin 2) ℤ))} {k : out_param ℤ} :

has_coe_to_fun (slash_invariant_form Γ k) (λ (_x : slash_invariant_form Γ k), upper_half_plane → ℂ)

Equations

slash_invariant_form.has_coe_to_fun = fun_like.has_coe_to_fun

source

@[simp]

theorem slash_invariant_form_to_fun_eq_coe {Γ : out_param (subgroup (matrix.special_linear_group (fin 2) ℤ))} {k : out_param ℤ} {f : slash_invariant_form Γ k} :

f.to_fun = ⇑f

source

@[ext]

theorem slash_invariant_form_ext {Γ : out_param (subgroup (matrix.special_linear_group (fin 2) ℤ))} {k : out_param ℤ} {f g : slash_invariant_form Γ k} (h : ∀ (x : upper_half_plane), ⇑f x = ⇑g x) :

f = g

source

@[protected]

def slash_invariant_form.copy {Γ : out_param (subgroup (matrix.special_linear_group (fin 2) ℤ))} {k : out_param ℤ} (f : slash_invariant_form Γ k) (f' : upper_half_plane → ℂ) (h : f' = ⇑f) :

slash_invariant_form Γ k

Copy of a slash_invariant_form with a new to_fun equal to the old one. Useful to fix definitional equalities.

Equations

f.copy f' h = {to_fun := f', slash_action_eq' := _}

source

@[protected, nolint, instance]

def slash_invariant_form.slash_invariant_form_class.coe_to_fun {F : Type u_1} {Γ : out_param (subgroup (matrix.special_linear_group (fin 2) ℤ))} {k : out_param ℤ} [slash_invariant_form_class F Γ k] :

has_coe_to_fun F (λ (_x : F), upper_half_plane → ℂ)

Equations

slash_invariant_form.slash_invariant_form_class.coe_to_fun = fun_like.has_coe_to_fun

source

@[simp]

theorem slash_invariant_form.slash_action_eqn {F : Type u_1} {Γ : out_param (subgroup (matrix.special_linear_group (fin 2) ℤ))} {k : out_param ℤ} [slash_invariant_form_class F Γ k] (f : F) (γ : ↥Γ) :

slash_action.map ℂ k γ ⇑f = ⇑f

source

theorem slash_invariant_form.slash_action_eqn' {F : Type u_1} (k : ℤ) (Γ : subgroup (matrix.special_linear_group (fin 2) ℤ)) [slash_invariant_form_class F Γ k] (f : F) (γ : ↥Γ) (z : upper_half_plane) :

⇑f (γ • z) = (↑(↑γ 1 0) * ↑z + ↑(↑γ 1 1)) ^ k * ⇑f z

source

@[protected, instance]

def slash_invariant_form.has_coe_t {F : Type u_1} {Γ : out_param (subgroup (matrix.special_linear_group (fin 2) ℤ))} {k : out_param ℤ} [slash_invariant_form_class F Γ k] :

has_coe_t F (slash_invariant_form Γ k)

Equations

slash_invariant_form.has_coe_t = {coe := λ (f : F), {to_fun := ⇑f, slash_action_eq' := _}}

source

@[simp]

theorem slash_invariant_form.slash_invariant_form_class.coe_coe {F : Type u_1} {Γ : out_param (subgroup (matrix.special_linear_group (fin 2) ℤ))} {k : out_param ℤ} [slash_invariant_form_class F Γ k] (f : F) :

⇑↑f = ⇑f

source

@[protected, instance]

def slash_invariant_form.has_add {Γ : out_param (subgroup (matrix.special_linear_group (fin 2) ℤ))} {k : out_param ℤ} :

has_add (slash_invariant_form Γ k)

Equations

slash_invariant_form.has_add = {add := λ (f g : slash_invariant_form Γ k), {to_fun := ⇑f + ⇑g, slash_action_eq' := _}}

source

@[simp]

theorem slash_invariant_form.coe_add {Γ : out_param (subgroup (matrix.special_linear_group (fin 2) ℤ))} {k : out_param ℤ} (f g : slash_invariant_form Γ k) :

⇑(f + g) = ⇑f + ⇑g

source

@[simp]

theorem slash_invariant_form.add_apply {Γ : out_param (subgroup (matrix.special_linear_group (fin 2) ℤ))} {k : out_param ℤ} (f g : slash_invariant_form Γ k) (z : upper_half_plane) :

⇑(f + g) z = ⇑f z + ⇑g z

source

@[protected, instance]

def slash_invariant_form.has_zero {Γ : out_param (subgroup (matrix.special_linear_group (fin 2) ℤ))} {k : out_param ℤ} :

has_zero (slash_invariant_form Γ k)

Equations

slash_invariant_form.has_zero = {zero := {to_fun := 0, slash_action_eq' := _}}

source

@[simp]

theorem slash_invariant_form.coe_zero {Γ : out_param (subgroup (matrix.special_linear_group (fin 2) ℤ))} {k : out_param ℤ} :

⇑0 = 0

source

@[protected, instance]

def slash_invariant_form.has_smul {Γ : out_param (subgroup (matrix.special_linear_group (fin 2) ℤ))} {k : out_param ℤ} {α : Type u_2} [has_smul α ℂ] [is_scalar_tower α ℂ ℂ] :

has_smul α (slash_invariant_form Γ k)

Equations

slash_invariant_form.has_smul = {smul := λ (c : α) (f : slash_invariant_form Γ k), {to_fun := c • ⇑f, slash_action_eq' := _}}

source

@[simp]

theorem slash_invariant_form.coe_smul {Γ : out_param (subgroup (matrix.special_linear_group (fin 2) ℤ))} {k : out_param ℤ} {α : Type u_2} [has_smul α ℂ] [is_scalar_tower α ℂ ℂ] (f : slash_invariant_form Γ k) (n : α) :

⇑(n • f) = n • ⇑f

source

@[simp]

theorem slash_invariant_form.smul_apply {Γ : out_param (subgroup (matrix.special_linear_group (fin 2) ℤ))} {k : out_param ℤ} {α : Type u_2} [has_smul α ℂ] [is_scalar_tower α ℂ ℂ] (f : slash_invariant_form Γ k) (n : α) (z : upper_half_plane) :

⇑(n • f) z = n • ⇑f z

source

@[protected, instance]

def slash_invariant_form.has_neg {Γ : out_param (subgroup (matrix.special_linear_group (fin 2) ℤ))} {k : out_param ℤ} :

has_neg (slash_invariant_form Γ k)

Equations

slash_invariant_form.has_neg = {neg := λ (f : slash_invariant_form Γ k), {to_fun := -⇑f, slash_action_eq' := _}}

source

@[simp]

theorem slash_invariant_form.coe_neg {Γ : out_param (subgroup (matrix.special_linear_group (fin 2) ℤ))} {k : out_param ℤ} (f : slash_invariant_form Γ k) :

⇑-f = -⇑f

source

@[simp]

theorem slash_invariant_form.neg_apply {Γ : out_param (subgroup (matrix.special_linear_group (fin 2) ℤ))} {k : out_param ℤ} (f : slash_invariant_form Γ k) (z : upper_half_plane) :

(⇑-f) z = -⇑f z

source

@[protected, instance]

def slash_invariant_form.has_sub {Γ : out_param (subgroup (matrix.special_linear_group (fin 2) ℤ))} {k : out_param ℤ} :

has_sub (slash_invariant_form Γ k)

Equations

slash_invariant_form.has_sub = {sub := λ (f g : slash_invariant_form Γ k), f + -g}

source

@[simp]

theorem slash_invariant_form.coe_sub {Γ : out_param (subgroup (matrix.special_linear_group (fin 2) ℤ))} {k : out_param ℤ} (f g : slash_invariant_form Γ k) :

⇑(f - g) = ⇑f - ⇑g

source

@[simp]

theorem slash_invariant_form.sub_apply {Γ : out_param (subgroup (matrix.special_linear_group (fin 2) ℤ))} {k : out_param ℤ} (f g : slash_invariant_form Γ k) (z : upper_half_plane) :

⇑(f - g) z = ⇑f z - ⇑g z

source

@[protected, instance]

def slash_invariant_form.add_comm_group {Γ : out_param (subgroup (matrix.special_linear_group (fin 2) ℤ))} {k : out_param ℤ} :

add_comm_group (slash_invariant_form Γ k)

Equations

slash_invariant_form.add_comm_group = function.injective.add_comm_group coe_fn slash_invariant_form.add_comm_group._proof_3 slash_invariant_form.add_comm_group._proof_4 slash_invariant_form.coe_add slash_invariant_form.coe_neg slash_invariant_form.coe_sub slash_invariant_form.add_comm_group._proof_5 slash_invariant_form.add_comm_group._proof_6

source

def slash_invariant_form.coe_hom {Γ : out_param (subgroup (matrix.special_linear_group (fin 2) ℤ))} {k : out_param ℤ} :

slash_invariant_form Γ k →+ upper_half_plane → ℂ

Additive coercion from slash_invariant_form to ℍ → ℂ.

Equations

slash_invariant_form.coe_hom = {to_fun := λ (f : slash_invariant_form Γ k), ⇑f, map_zero' := _, map_add' := _}

source

theorem slash_invariant_form.coe_hom_injective {Γ : out_param (subgroup (matrix.special_linear_group (fin 2) ℤ))} {k : out_param ℤ} :

function.injective ⇑slash_invariant_form.coe_hom

source

@[protected, instance]

noncomputable def slash_invariant_form.module {Γ : out_param (subgroup (matrix.special_linear_group (fin 2) ℤ))} {k : out_param ℤ} :

module ℂ (slash_invariant_form Γ k)

Equations

slash_invariant_form.module = function.injective.module ℂ slash_invariant_form.coe_hom slash_invariant_form.coe_hom_injective slash_invariant_form.module._proof_2

source

@[protected, instance]

def slash_invariant_form.has_one {Γ : out_param (subgroup (matrix.special_linear_group (fin 2) ℤ))} :

has_one (slash_invariant_form Γ 0)

Equations

slash_invariant_form.has_one = {one := {to_fun := 1, slash_action_eq' := _}}

source

@[simp]

theorem slash_invariant_form.one_coe_eq_one {Γ : out_param (subgroup (matrix.special_linear_group (fin 2) ℤ))} :

⇑1 = 1

source

@[protected, instance]

def slash_invariant_form.inhabited {Γ : out_param (subgroup (matrix.special_linear_group (fin 2) ℤ))} {k : out_param ℤ} :

inhabited (slash_invariant_form Γ k)

Equations

slash_invariant_form.inhabited = {default := 0}

mathlib3 documentation

Slash invariant forms #