Hecke operators

DefinitionHecke operator as a function on fixed points#✓fully proved

The Hecke operator T(g) as a function on fixed points.

AbstractHeckeOperator.HeckeOperator_toFun · 19 lines

noncomputable def HeckeOperator_toFun (a : fixedPoints V A) : fixedPoints U A :=
  ⟨∑ᶠ gᵢ ∈ Quotient.out '' (QuotientGroup.mk '' (U * {g}) : Set (G ⧸ V)), gᵢ • a.1, by
  rintro ⟨u, huU⟩
  rw [smul_finsum_mem (h.image Quotient.out), ← eq_finsum_quotient_out_of_bijOn' a]
  · rw [finsum_mem_eq_of_bijOn (fun g ↦ u • g)]
    · exact Set.InjOn.bijOn_image <| Set.injOn_of_injective (MulAction.injective u)
    · simp [mul_smul]
  · apply (Set.bijOn_comp_iff (Set.injOn_of_injective (MulAction.injective u))).1
    change Set.BijOn ((fun xbar ↦ u • xbar) ∘ (QuotientGroup.mk : G → G ⧸ V)) _ _
    rw [Set.bijOn_comp_iff]
    · rw [← Set.image_comp]
      simp only [Function.comp_apply, Quotient.out_eq, Set.image_id']
      refine Set.bijOn_image_image (f := fun (x : G) ↦ u • x) (p₁ := (QuotientGroup.mk : G → G ⧸ V))
        (fun a ↦ rfl) ?_ (Set.injOn_of_injective (MulAction.injective u))
      apply Set.bijOn_smul _ _ _ huU
    · refine Set.InjOn.image_of_comp ?_
      simp only [Function.comp_def, Quotient.out_eq]
      exact Function.Injective.injOn Function.injective_id
    ⟩

Used by 2

Used byHecke operator · Hecke operator as an additive homomorphism

DefinitionHecke operator as an additive homomorphism#✓fully proved

The Hecke operator T(g) as an additive monoid homomorphism.

noncomputable def HeckeOperator_addMonoidHom : fixedPoints V A →+ fixedPoints U A where
  toFun := HeckeOperator_toFun h
  map_zero' := by
    ext
    simp [HeckeOperator_toFun]
  map_add' a b := by
    ext
    simp only [HeckeOperator_toFun, FixedPoints.coe_add, smul_add,
      finsum_mem_add_distrib (h.image Quotient.out)]

Uses 1

Statement usesHecke operator as a function on fixed points

DefinitionHecke operator#✓fully proved

The Hecke operator T(g) as a linear map on fixed points.

noncomputable def HeckeOperator : fixedPoints V A →ₗ[R] fixedPoints U A where
  toFun := HeckeOperator_toFun h
  map_add' a b := by
    ext
    simp only [HeckeOperator_toFun, FixedPoints.coe_add, smul_add,
      finsum_mem_add_distrib (h.image Quotient.out)]
  map_smul' r a := by
    ext
    simp only [HeckeOperator_toFun, FixedPoints.coe_smul, smul_comm,
      smul_finsum_mem (h.image Quotient.out), RingHom.id_apply]

Uses 1

Statement usesHecke operator as a function on fixed points

3 fully proved

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.