dual

projects/LeanModularForms/.mathlib-quality/learnings.jsonl

@@ -0,0 +1,3 @@
+{"type":"style_correction","date":"2026-07-02","file":"Issues/SelfDual/Basic.lean","summary":"Per-declaration cleanup workers cannot catch cross-declaration proof-block duplication; the Phase-6.5 /simplify holistic pass found the `hdualΓ` (strictWidthInfty ∈ (dual Γ).strictPeriods) block copy-pasted across two declarations and extracted it into a shared private helper `strictWidthInfty_mem_dual_strictPeriods`.","lesson":"Always run the holistic simplify pass after per-decl golf; it is where cross-cutting DRY wins surface."}
+{"type":"mathlib_discovery","date":"2026-07-02","file":"Issues/SelfDual/Basic.lean","summary":"`Subgroup.strictWidthInfty` is a bare `dite` on `DiscreteTopology _.strictPeriods` with no congruence lemma, so `Subgroup.dual_width_eq` must reconstruct the def body under `congrArg` (rw/simp fail with 'motive is not type correct' / 'failed to synthesize Decidable'). A `strictWidthInfty_congr (h : Γ₁.strictPeriods = Γ₂.strictPeriods) : strictWidthInfty Γ₁ = strictWidthInfty Γ₂` is the missing API (upstream/dev-ticket candidate)."}
+{"type":"mathlib_discovery","date":"2026-07-03","file":"Issues/Issue34.lean","summary":"To prove a ring hom `σ : IntermediateField ℚ ℂ →+* ℂ` is real on an adjoin (`conjugate σ = σ`), do NOT hand-roll `IntermediateField.adjoin_induction` with per-operation `change`/`rw [map_*, star_*]` closure branches (~22 lines). Instead bundle both ring homs as ℚ-AlgHoms via `RingHom.equivRatAlgHom : (A →+* B) ≃ (A →ₐ[ℚ] B)` and apply `IntermediateField.algHom_ext_of_eq_adjoin (F := ℚ) rfl` (or `adjoin_algHom_ext`), reducing the goal to the generator case (`rintro x ⟨n, rfl⟩; show star (σ ⟨_,_⟩) = σ ⟨_,_⟩; exact Complex.conj_eq_iff_im.mpr (h n)`). ~22 lines → 5.","lesson":"A per-declaration cleanup worker rejected this refactor (feared manual AlgHom bundling); the /simplify holistic pass (3 of 4 angles) found it. `equivRatAlgHom` makes ℚ-linearity free, so the AlgHom ext lemmas apply to any ring hom between ℚ-algebras — the `change`-heavy adjoin_induction is the missing-API smell mathlib warns about."}

projects/LeanModularForms/LeanModularForms/Issues/Example.lean

@@ -0,0 +1,127 @@
+import LeanModularForms.Issues.Issue55
+
+/-!
+# A congruence subgroup that is not self-dual, carrying a self-dual form
+
+This file constructs a concrete example separating three properties of a subgroup of
+`SL(2, ℤ)` and a modular form on it. The subgroup `Γ` is the preimage, modulo `3`, of the
+stabilizer of the line spanned by `(1, 1)`. It is a congruence subgroup but is not self-dual,
+yet the discriminant cusp form `Δ` restricted to it is self-dual.
+
+## Main definitions
+
+* `IssueExample.Γ`: the subgroup of `SL(2, ℤ)` whose reduction mod `3` fixes the sum
+  `γ 0 0 + γ 0 1` and `γ 1 0 + γ 1 1`.
+* `IssueExample.Δ`: the discriminant cusp form restricted from `SL(2, ℤ)` to `Γ`.
+
+## Main results
+
+* `IssueExample.result`: `Γ` is a congruence subgroup, `Γ` is not self-dual, and `Δ` is
+  self-dual.
+-/
+
+open ModularForm UpperHalfPlane MatrixGroups ComplexConjugate
+open CongruenceSubgroup Pointwise Subgroup
+open Matrix Matrix.SpecialLinearGroup Complex
+open scoped MatrixGroups ModularForm Real
+
+private lemma eta_neg_conj (z : UpperHalfPlane) :
+    conj (ModularForm.eta (-(conj (z : ℂ)))) = ModularForm.eta (z : ℂ) := by
+  have hz' : (-(conj (z : ℂ))) ∈ UpperHalfPlane.upperHalfPlaneSet := by
+    simpa using z.2
+  have hprod := (ModularForm.multipliableLocallyUniformlyOn_eta.multipliable hz').map_tprod
+    (starRingEnd ℂ) Complex.continuous_conj
+  rw [ModularForm.eta, map_mul, hprod, ModularForm.eta]
+  simp [ModularForm.eta_q, Function.Periodic.qParam, ← Complex.exp_conj, map_ofNat]
+
+namespace IssueExample
+
+/-- The subgroup of `SL(2, ℤ)` whose reduction modulo `3` stabilizes the line
+spanned by `(1, 1)`. -/
+def Γ : Subgroup SL(2, ℤ) where
+  carrier := {γ | (γ 0 0 + γ 0 1 : ZMod 3) = (γ 1 0 + γ 1 1 : ZMod 3)}
+  one_mem' := by norm_num
+  mul_mem' := by
+    intro A B hA hB
+    change ((A * B) 0 0 + (A * B) 0 1 : ZMod 3) =
+      ((A * B) 1 0 + (A * B) 1 1 : ZMod 3)
+    have hA' : (A 0 0 : ZMod 3) + (A 0 1 : ZMod 3) =
+        (A 1 0 : ZMod 3) + (A 1 1 : ZMod 3) := hA
+    have hB' : (B 0 0 : ZMod 3) + (B 0 1 : ZMod 3) =
+        (B 1 0 : ZMod 3) + (B 1 1 : ZMod 3) := hB
+    simp only [Fin.isValue, Matrix.SpecialLinearGroup.coe_mul, Matrix.mul_apply,
+      Fin.sum_univ_two, Int.cast_add, Int.cast_mul]
+    linear_combination ((B 0 0 : ZMod 3) + (B 0 1 : ZMod 3)) * hA' +
+      ((A 1 1 : ZMod 3) - (A 0 1 : ZMod 3)) * hB'
+  inv_mem' := by
+    intro A hA
+    change ((A⁻¹) 0 0 + (A⁻¹) 0 1 : ZMod 3) =
+      ((A⁻¹) 1 0 + (A⁻¹) 1 1 : ZMod 3)
+    have hA' : (A 0 0 : ZMod 3) + (A 0 1 : ZMod 3) =
+        (A 1 0 : ZMod 3) + (A 1 1 : ZMod 3) := hA
+    rw [SL2_inv_expl A]
+    simp only [Fin.isValue, cons_val', cons_val_zero, cons_val_fin_one, cons_val_one, Int.cast_neg]
+    linear_combination -hA'
+
+theorem mem_Γ (γ : SL(2, ℤ)) : γ ∈ Γ ↔ (γ 0 0 + γ 0 1 : ZMod 3) = (γ 1 0 + γ 1 1 : ZMod 3) :=
+  Iff.rfl
+
+theorem Γ_isCongruenceSubgroup : CongruenceSubgroup.IsCongruenceSubgroup Γ := by
+  refine ⟨3, by norm_num, ?_⟩
+  intro γ hγ
+  rw [CongruenceSubgroup.Gamma_mem] at hγ
+  change (γ 0 0 + γ 0 1 : ZMod 3) = (γ 1 0 + γ 1 1 : ZMod 3)
+  simp [hγ]
+
+theorem Γ_not_isSelfDual :
+    ¬ Subgroup.IsSelfDual (Γ : Subgroup (GL (Fin 2) ℝ)) := by
+  let γ : SL(2, ℤ) := ⟨!![0, 1; -1, -1], by norm_num [Matrix.det_fin_two_of]⟩
+  let γJ : SL(2, ℤ) := ⟨!![0, -1; 1, -1], by norm_num [Matrix.det_fin_two_of]⟩
+  have hγΓ : γ ∈ Γ := by
+    change ((0 : ZMod 3) + (1 : ZMod 3) = (-1 : ZMod 3) + (-1 : ZMod 3))
+    decide
+  have hγJ_not : γJ ∉ Γ := by
+    change ¬ ((0 : ZMod 3) + (-1 : ZMod 3) = (1 : ZMod 3) + (-1 : ZMod 3))
+    decide
+  have hJinv : UpperHalfPlane.J⁻¹ = UpperHalfPlane.J :=
+    inv_eq_of_mul_eq_one_right <| by simpa [sq] using UpperHalfPlane.J_sq
+  have hmapγJ : mapGL ℝ γJ = UpperHalfPlane.J * mapGL ℝ γ * UpperHalfPlane.J := by
+    ext i j
+    fin_cases i <;> fin_cases j <;>
+      norm_num [γ, γJ, UpperHalfPlane.J, Matrix.GeneralLinearGroup.coe_mul,
+        Matrix.mul_apply, Matrix.vecMul, dotProduct, Matrix.vecHead, Matrix.vecTail,
+        Fin.sum_univ_two]
+  have hdual_mem : UpperHalfPlane.J * mapGL ℝ γ * UpperHalfPlane.J ∈
+      Subgroup.dual (Γ : Subgroup (GL (Fin 2) ℝ)) := by
+    rw [Subgroup.dual, hJinv]
+    simpa [ConjAct.toConjAct_smul, hJinv] using
+      Subgroup.smul_mem_pointwise_smul (mapGL ℝ γ) (ConjAct.toConjAct UpperHalfPlane.J)
+        (Γ : Subgroup (GL (Fin 2) ℝ)) (Subgroup.mem_map.mpr ⟨γ, hγΓ, rfl⟩)
+  have hnot_mem : UpperHalfPlane.J * mapGL ℝ γ * UpperHalfPlane.J ∉
+      (Γ : Subgroup (GL (Fin 2) ℝ)) := by
+    intro hmem
+    obtain ⟨δ, hδΓ, hδ⟩ := Subgroup.mem_map.mp hmem
+    have hδ_eq : δ = γJ := mapGL_injective (by rw [hδ, ← hmapγJ])
+    exact hγJ_not (hδ_eq ▸ hδΓ)
+  intro hself
+  exact hnot_mem (by simpa [hself.isSelfDual] using hdual_mem)
+
+theorem Γ_le_SL : (Γ : Subgroup (GL (Fin 2) ℝ)) ≤ 𝒮ℒ := Subgroup.map_le_range (mapGL ℝ) Γ
+
+/-- The discriminant cusp form, restricted from the full modular group to `Γ`. -/
+noncomputable def Δ : CuspForm (Γ : Subgroup (GL (Fin 2) ℝ)) 12 :=
+  CuspForm.restrictSubgroup Γ_le_SL CuspForm.discriminant
+
+theorem Δ_isSelfDual : ModularFormClass.isSelfDual Δ := by
+  ext z
+  rw [ModularFormClass.dual_explicit]
+  change conj (ModularForm.discriminant (ofComplex (-(conj (z : ℂ))))) =
+    ModularForm.discriminant z
+  have hz' : 0 < (-(conj (z : ℂ))).im := by simpa using z.2
+  simp [ModularForm.discriminant, ofComplex_apply_of_im_pos hz', map_pow, eta_neg_conj]
+
+/-- The concrete example: `Γ` is congruence and not self-dual, while `Δ` is self-dual. -/
+theorem result : IsCongruenceSubgroup Γ ∧ ¬ Subgroup.IsSelfDual Γ ∧ ModularFormClass.isSelfDual Δ :=
+  ⟨Γ_isCongruenceSubgroup, Γ_not_isSelfDual, Δ_isSelfDual⟩
+
+end IssueExample

projects/LeanModularForms/LeanModularForms/Issues/Issue34.lean

@@ -0,0 +1,99 @@
+import LeanModularForms.Issues.Issue55
+
+open ModularForm UpperHalfPlane MatrixGroups ComplexConjugate CongruenceSubgroup Pointwise Subgroup
+  Matrix.SpecialLinearGroup HeckeRing.GL2
+
+variable {N : ℕ} [NeZero N] {k : ℤ}
+
+namespace HeckeRing.GL2
+
+namespace Newform
+
+/-- The coefficient field `ℚ(a_n : n ≥ 1)` of a newform. -/
+noncomputable def coefficientField (f : Newform N k) : IntermediateField ℚ ℂ :=
+  IntermediateField.adjoin ℚ (Set.range fun n : ℕ+ ↦ (qExpansion 1 f.toCuspForm).coeff n)
+
+/-- The coefficient field of a newform is finite-dimensional over `ℚ`. -/
+theorem coefficientField_finiteDimensional (f : Newform N k) :
+    FiniteDimensional ℚ f.coefficientField := by
+  sorry
+
+/-- The coefficient field of a newform is a number field. -/
+instance (f : Newform N k) : NumberField f.coefficientField :=
+  {to_finiteDimensional := coefficientField_finiteDimensional f}
+
+lemma coeff_mem_coefficientField (f : Newform N k) (n : ℕ+) :
+    (qExpansion 1 f.toCuspForm).coeff n ∈ f.coefficientField :=
+  IntermediateField.subset_adjoin ℚ _ (Set.mem_range_self n)
+
+lemma isSelfDual_iff_qExpansion_one_coeff_im_eq_zero (f : Newform N k) :
+    ModularFormClass.isSelfDual f.toCuspForm ↔
+      ∀ n : ℕ, ((qExpansion 1 f.toCuspForm).coeff n).im = 0 := by
+  simpa [CongruenceSubgroup.strictWidthInfty_Gamma1 N] using
+    ModularFormClass.isSelfDual_iff f.toCuspForm
+
+lemma qExpansion_one_coeff_im_eq_zero_of_coefficientField_isTotallyReal (f : Newform N k)
+    (hK : NumberField.IsTotallyReal f.coefficientField) :
+    ∀ n : ℕ, ((qExpansion 1 f.toCuspForm).coeff n).im = 0 := by
+  intro n
+  cases n with
+  | zero => simp [CuspFormClass.qExpansion_coeff_zero f.toCuspForm one_pos (one_mem_strictPeriods_Gamma1_map N)]
+  | succ n =>
+      let npos : ℕ+ := ⟨n + 1, n.succ_pos⟩
+      simpa [npos] using Complex.conj_eq_iff_im.mp (RingHom.congr_fun
+        (NumberField.IsTotallyReal.complexEmbedding_isReal (algebraMap f.coefficientField ℂ))
+        ⟨(qExpansion 1 f.toCuspForm).coeff npos, coeff_mem_coefficientField f npos⟩)
+
+/--
+For every embedding σ : K_f ↪ ℂ, the coefficientwise conjugate
+f^σ(q) = ∑ n ≥ 1, σ(a_n(f)) q^n
+is again a normalized newform. Its dual has coefficients
+a_n((f^σ)ᵛ) = overline(σ(a_n(f))).
+Galois conjugation commutes with duality:
+(f^σ)ᵛ = (fᵛ)^σ.
+-/
+theorem exists_selfDual_galoisConjugate_newform_of_isSelfDual (f : Newform N k)
+    (hself : ModularFormClass.isSelfDual f.toCuspForm) (σ : f.coefficientField →+* ℂ) :
+    ∃ g : Newform N k, ModularFormClass.isSelfDual g.toCuspForm ∧
+      ∀ n : ℕ+, (qExpansion 1 g.toCuspForm).coeff n =
+        σ ⟨(qExpansion 1 f.toCuspForm).coeff n, coeff_mem_coefficientField f n⟩ := by
+  sorry
+
+lemma complexEmbedding_coeff_im_eq_zero_of_isSelfDual (f : Newform N k)
+    (hself : ModularFormClass.isSelfDual f.toCuspForm) (σ : f.coefficientField →+* ℂ) (n : ℕ+) :
+    (σ ⟨(qExpansion 1 f.toCuspForm).coeff n, coeff_mem_coefficientField f n⟩).im = 0 := by
+  obtain ⟨g, hgself, hgcoeff⟩ := exists_selfDual_galoisConjugate_newform_of_isSelfDual f hself σ
+  rw [← hgcoeff n]
+  exact (isSelfDual_iff_qExpansion_one_coeff_im_eq_zero g).mp hgself n
+
+lemma coefficientField_isTotallyReal_of_forall_complexEmbedding_coeff_im_eq_zero
+    (f : Newform N k) (hσ : ∀ (σ : f.coefficientField →+* ℂ) (n : ℕ+),
+      (σ ⟨(qExpansion 1 f.toCuspForm).coeff n, coeff_mem_coefficientField f n⟩).im = 0) :
+    NumberField.IsTotallyReal f.coefficientField := by
+  unfold coefficientField at hσ ⊢
+  refine ⟨fun v ↦ ?_⟩
+  rw [NumberField.InfinitePlace.isReal_iff]
+  let σ := NumberField.InfinitePlace.embedding v
+  rw [NumberField.ComplexEmbedding.isReal_iff]
+  apply RingHom.equivRatAlgHom.injective
+  apply IntermediateField.algHom_ext_of_eq_adjoin (F := ℚ) rfl
+  rintro x ⟨n, rfl⟩
+  change star (σ ⟨_, _⟩) = σ ⟨_, _⟩
+  exact Complex.conj_eq_iff_im.mpr (hσ σ n)
+
+/-- A newform's coefficient field is totally real if and only if the newform is self-dual. -/
+theorem coefficientField_isTotallyReal_iff_isSelfDual (f : Newform N k) :
+    NumberField.IsTotallyReal f.coefficientField ↔ ModularFormClass.isSelfDual f.toCuspForm :=
+  ⟨fun hK ↦ (isSelfDual_iff_qExpansion_one_coeff_im_eq_zero f).mpr
+    (qExpansion_one_coeff_im_eq_zero_of_coefficientField_isTotallyReal f hK),
+    fun hself ↦ coefficientField_isTotallyReal_of_forall_complexEmbedding_coeff_im_eq_zero f
+      (complexEmbedding_coeff_im_eq_zero_of_isSelfDual f hself)⟩
+
+/-- A newform's coefficient field is CM if and only if the newform is not self-dual. -/
+theorem coefficientField_isCM_iff_not_isSelfDual (f : Newform N k) :
+    NumberField.IsCMField f.coefficientField ↔ ¬ ModularFormClass.isSelfDual f.toCuspForm := by
+  sorry
+
+end Newform
+
+end HeckeRing.GL2