funlean.
Step 45 / 64

Master’s level

The slash action: the precise weight rule

The transformation law is a bundled equation: f ∣[k] γ = f for every allowed γ.

Start with a concrete example

For a simple example of preserving a rule, x² gives the same answer at x and −x. The slash operation checks a more specific transformation rule for a function, including a factor that depends on its weight.

A small check: try the idea

Think with the concrete example above. You can try again.

When checking the slash transformation rule, may we ignore its weight-dependent factor?

Read the answer and reasoning

No; it is part of the operation. The operation changes the input and includes the specified multiplier. The simple x² symmetry is only a starting analogy.

Build the idea in three steps

  1. A modular form replaced the vague word shape with something checkable: a precise demand relating the function’s values before and after a transformation.
  2. The library’s SlashInvariantForm carries exactly two parts: the underlying function toFun, and one demanded equation for every allowed transformation γ, written f ∣[k] γ = f.
  3. The symbol ∣[k] is the slash action, and the integer k inside the brackets is the weight. Holding this equality for every γ in the subgroup Γ is what invariance means here. ModularForm extends this same structure with differentiability and cusp behavior.

A small example

For a matrix with c = 0 and d = 1 — transformations of the form τ ↦ aτ + b — the weight factor (cτ + d)^{−k} is exactly 1, so the demand reduces to comparing f(aτ + b) with f(τ).

Lean definition · original excerpt

Mathlib · db584cd · SlashInvariantForms.lean

/-- Functions `ℍ → ℂ` that are invariant under the `SlashAction`. -/structure SlashInvariantForm where  /-- The underlying function `ℍ → ℂ`.   Do NOT use directly. Use the coercion instead. -/  toFun : ℍ → ℂ  slash_action_eq' : ∀ γ ∈ Γ, toFun ∣[k] γ = toFun /-- `SlashInvariantFormClass F Γ k` asserts `F` is a type of bundled functions that are invariant

How to read this Lean

The excerpt is the whole structure: two fields. The comment on toFun warns not to use the field directly; the coercion supplies the function view. The second field, ∀ γ ∈ Γ, toFun ∣[k] γ = toFun, is data that an author must actually verify.

Original source ↗ · L33–41Open the complete saved source

Where this idea is used

8. The secret duet
I’m lost · Help

Mika’s help desk

The slash action: the precise weight rule

One thing at a time

Read the three explanation steps first. The Lean source is there for a closer look afterwards; you do not have to read it first.

In simpler words

The transformation law is a bundled equation: f ∣[k] γ = f for every allowed γ.

Earlier ideas are listed under “Start with these ideas” on this page.

A small clue

For a matrix with c = 0 and d = 1 — transformations of the form τ ↦ aτ + b — the weight factor (cτ + d)^{−k} is exactly 1, so the demand reduces to comparing f(aτ + b) with f(τ).

Close this panel to return to the exact place you were reading. These are prepared hints for this page.

Start with the first small story →