Commit 2025-05-19 12:23 55c73a56

View on Github →

feat(Analysis/UpperHalfPlane, ModularForms): extend actions from GLPos to GL (#24830) This extends the action of GL(2, ℝ)⁺ on the upper half-plane, and the slash actions on modular forms, to actions of all of GL (Fin 2) ℝ (with elements of negative determinant acting as anti-holomorphic maps). This is mathematically extra information which we didn't have before; but the goal is also to make the modular forms code (hopefully) easier to work with, by avoiding the extra layer of coercions required by working with the subtype GL(2, ℝ)⁺.

Estimated changes

modified theorem ModularGroup.SL_neg_smul
modified theorem ModularGroup.denom_S
modified theorem ModularGroup.denom_apply
modified theorem ModularGroup.sl_moeb
modified theorem UpperHalfPlane.coe_smul
modified def UpperHalfPlane.denom
modified theorem UpperHalfPlane.im_smul
modified theorem UpperHalfPlane.mul_smul'
modified def UpperHalfPlane.num
added theorem UpperHalfPlane.num_neg
modified theorem UpperHalfPlane.re_smul
modified theorem UpperHalfPlane.smulAux'_im
added theorem UpperHalfPlane.σ_mul
added theorem UpperHalfPlane.σ_neg
added theorem UpperHalfPlane.σ_num
added theorem UpperHalfPlane.σ_sq
modified theorem ModularForm.SL_slash
modified theorem ModularForm.mul_slash
modified def ModularForm.slash
modified theorem ModularForm.slash_def
added theorem ModularForm.smul_slash