FLT/AutomorphicForm/QuaternionAlgebra/HeckeOperators/Local.lean

GitHub source file

Explanation legend Lean4 Domain Explanation Language (L4DEL)

L4DEL explanations are a separate layer. They do not change the Lean source. Intuition is explanatory prose; numbered items are a reading path; sources link the wording back to evidence.

L4DEL
Lean4 Domain Explanation Language

Credit: The upstream authors and contributors retain credit for the project and mathematics. lean4-explainer only renders their pinned source and adds the separately disclosed explanation layer.

Project sources: Pinned project documentation, Pinned FLT blueprint introduction

12 declarations, 0 contain sorry, 0 declared as axioms

Local computations for Hecke operators

Local lemmas at a finite place v for the Hecke operator T_v acting on quaternionic automorphic forms: explicit double-coset decompositions of U₁(v) · diag(πᵥ, 1) · U₁(v) inside GL₂(F_v).

Imports (4)
Imported by 2 files
  1. def TotallyDefiniteQuaternionAlgebra.WeightTwoAutomorphicForm.HeckeOperator.Local.GL2.diag The matrix element diag[α, 1] line 47 source

    Source documentation

    The matrix element diag[α, 1].

    standard axioms: Classical.choice, Quot.sound, propext what this means

    Statement uses: Field, NumberField, IsDedekindDomain.HeightOneSpectrum, NumberField.RingOfIntegers, MonoidHom, Units, IsDedekindDomain.HeightOneSpectrum.adicCompletion, Matrix.GeneralLinearGroup, Fin, OfNat.ofNat, Nat, Matrix

    Proof uses: Units.map, MonoidHom.mk, OneHom.mk, Matrix.diagonal, Matrix.vecCons, Matrix.vecEmpty

    40 instances, coercions and auxiliary constants left out.

    Tactic trace: 2 steps

    Open to load the checked before-and-after goal states.

    noncomputable def diag : (v.adicCompletion F)ˣ →* GL₂(adicCompletion F v) :=
…
  2. lemma TotallyDefiniteQuaternionAlgebra.WeightTwoAutomorphicForm.HeckeOperator.Local.GL2.unipotent_mem_localTameLevel Show that unipotent t is in U1 v for t ∈ O_v line 51 source

    Source comment

    Show that `unipotent t` is in `U1 v` for `t ∈ O_v`.

    standard axioms: Classical.choice, Quot.sound, propext what this means

    Statement uses: Field, NumberField, IsDedekindDomain.HeightOneSpectrum, NumberField.RingOfIntegers, IsDedekindDomain.HeightOneSpectrum.adicCompletion, LE.le, WithZero, Multiplicative, Int, Valuation, Valued.v, OfNat.ofNat, Membership.mem, Matrix.GeneralLinearGroup, Fin, Nat, Subgroup, Matrix, IsDedekindDomain.GL2.localTameLevel, Matrix.GeneralLinearGroup.GL2.unipotent

    Proof uses: And.intro, IsDedekindDomain.GL2.localIwahoriLevel, LT.lt, HSub.hSub, Iff.mpr, And, Eq, IsDedekindDomain.GL2.mem_localIwahoriLevel_iff_v, Eq.mpr, id, Eq.trans, True, congr, congrArg, congrFun', map_one, eq_self, map_zero, and_self, and_true and 3 more

    117 instances, coercions and auxiliary constants left out.

    Tactic trace: 2 steps

    Open to load the checked before-and-after goal states.

    lemma unipotent_mem_localTameLevel (t : v.adicCompletion F) (ht : Valued.v t ≤ 1) :
    unipotent t ∈ GL2.localTameLevel v :=
…
  3. def TotallyDefiniteQuaternionAlgebra.WeightTwoAutomorphicForm.HeckeOperator.Local.GL2.unipotentMulDiag The matrix element (unipotent t) * (diag α hα) = !![α, t; 0, 1] line 56 source

    Source documentation

    The matrix element (unipotent t) * (diag α hα) = !![α, t; 0, 1].

    standard axioms: Classical.choice, Quot.sound, propext what this means

    Statement uses: Field, NumberField, IsDedekindDomain.HeightOneSpectrum, NumberField.RingOfIntegers, Units, IsDedekindDomain.HeightOneSpectrum.adicCompletion, Matrix.GeneralLinearGroup, Fin, OfNat.ofNat, Nat

    Proof uses: HMul.hMul, Matrix, Matrix.GeneralLinearGroup.GL2.unipotent, MonoidHom, TotallyDefiniteQuaternionAlgebra.WeightTwoAutomorphicForm.HeckeOperator.Local.GL2.diag

    33 instances, coercions and auxiliary constants left out.

    noncomputable def unipotentMulDiag (t : v.adicCompletion F) :
    GL₂(v.adicCompletion F) := unipotent t * diag α

    Mentions: TotallyDefiniteQuaternionAlgebra.WeightTwoAutomorphicForm.HeckeOperator.Local.GL2.diag

  4. lemma TotallyDefiniteQuaternionAlgebra.WeightTwoAutomorphicForm.HeckeOperator.Local.GL2.unipotentMulDiag_injective line 59 source

    standard axioms: Classical.choice, Quot.sound, propext what this means

    Statement uses: Field, NumberField, IsDedekindDomain.HeightOneSpectrum, NumberField.RingOfIntegers, Units, IsDedekindDomain.HeightOneSpectrum.adicCompletion, Function.Injective, Matrix.GeneralLinearGroup, Fin, OfNat.ofNat, Nat, TotallyDefiniteQuaternionAlgebra.WeightTwoAutomorphicForm.HeckeOperator.Local.GL2.unipotentMulDiag

    Proof uses: Eq, Eq.mp, Matrix, congr, congrArg, Eq.trans, Finset.sum, Finset.univ, HMul.hMul, Equiv, Matrix.of, Matrix.vecCons, Matrix.vecEmpty, Matrix.diagonal, HAdd.hAdd, Finset.sum_congr, Eq.refl, Finset, Membership.mem, congrFun' and 16 more

    71 instances, coercions and auxiliary constants left out.

    Tactic trace: 2 steps

    Open to load the checked before-and-after goal states.

  5. lemma TotallyDefiniteQuaternionAlgebra.WeightTwoAutomorphicForm.HeckeOperator.Local.GL2.unipotentMulDiag_inv_mul_unipotentMulDiag !![α t₁; 0 1]⁻¹ * [α t₂; 0 1] = [1 (t₂ - t₁) / α; 0 1] line 64 source

    Source documentation

    !![α t₁; 0 1]⁻¹ * [α t₂; 0 1] = [1 (t₂ - t₁) / α; 0 1].

    standard axioms: Classical.choice, Quot.sound, propext what this means

    Statement uses: Field, NumberField, IsDedekindDomain.HeightOneSpectrum, NumberField.RingOfIntegers, Units, IsDedekindDomain.HeightOneSpectrum.adicCompletion, Eq, Matrix.GeneralLinearGroup, Fin, OfNat.ofNat, Nat, HMul.hMul, Matrix, Inv.inv, TotallyDefiniteQuaternionAlgebra.WeightTwoAutomorphicForm.HeckeOperator.Local.GL2.unipotentMulDiag, Matrix.GeneralLinearGroup.GL2.unipotent, HSub.hSub

    Proof uses: Trans.simple, MonoidHom, TotallyDefiniteQuaternionAlgebra.WeightTwoAutomorphicForm.HeckeOperator.Local.GL2.diag, of_eq_true, Eq.trans, Neg.neg, True, congr, congrArg, congrFun', mul_inv_rev, Matrix.GeneralLinearGroup.GL2.unipotent_inv, mul_assoc, HAdd.hAdd, sub_eq_add_neg, eq_self, Eq.mpr, id, Units.ext, Matrix.ext and 58 more

    155 instances, coercions and auxiliary constants left out.

    Tactic trace: 9 steps

    Open to load the checked before-and-after goal states.

    lemma unipotentMulDiag_inv_mul_unipotentMulDiag (t₁ t₂ : v.adicCompletion F) :
    (unipotentMulDiag α t₁)⁻¹ * unipotentMulDiag α t₂ = unipotent (α.1⁻¹ * (t₂ - t₁)) := by
…

    Mentions: TotallyDefiniteQuaternionAlgebra.WeightTwoAutomorphicForm.HeckeOperator.Local.GL2.unipotentMulDiag

  6. lemma TotallyDefiniteQuaternionAlgebra.WeightTwoAutomorphicForm.HeckeOperator.Local.GL2.localPTameLevel.conjBy_diag_mem_iff' line 80 source

    standard axioms: Classical.choice, Quot.sound, propext what this means

    Statement uses: Field, NumberField, IsDedekindDomain.HeightOneSpectrum, NumberField.RingOfIntegers, Nat, Matrix.GeneralLinearGroup, Fin, OfNat.ofNat, IsDedekindDomain.HeightOneSpectrum.adicCompletion, Membership.mem, Subgroup, Matrix, IsDedekindDomain.GL2.localPTameLevel, Units, Iff, HMul.hMul, Inv.inv, MonoidHom, TotallyDefiniteQuaternionAlgebra.WeightTwoAutomorphicForm.HeckeOperator.Local.GL2.diag, And and 7 more

    Proof uses: Trans.simple, of_eq_true, Eq.trans, True, congrFun', congrArg, IsDedekindDomain.GL2.localIwahoriLevel, Units.map, MonoidHom.mk, OneHom.mk, Matrix.diagonal, Matrix.vecCons, Matrix.vecEmpty, Exists, Ne, HDiv.hDiv, IsDedekindDomain.GL2.localPTameLevelSubgroup, Units.mk0, mul_assoc, congr and 40 more

    226 instances, coercions and auxiliary constants left out.

    Tactic trace: 6 steps

    Open to load the checked before-and-after goal states.

  7. lemma TotallyDefiniteQuaternionAlgebra.WeightTwoAutomorphicForm.HeckeOperator.Local.GL2.localPTameLevel.adicCompletionIntegers_dvd_iff line 91 source

    standard axioms: Classical.choice, Quot.sound, propext what this means

    Statement uses: Field, NumberField, IsDedekindDomain.HeightOneSpectrum, NumberField.RingOfIntegers, Subtype, IsDedekindDomain.HeightOneSpectrum.adicCompletion, Membership.mem, ValuationSubring, IsDedekindDomain.HeightOneSpectrum.adicCompletionIntegers, Iff, Dvd.dvd, LE.le, WithZero, Multiplicative, Int, Valuation, Valued.v

    Proof uses: Iff.intro, Eq, HMul.hMul, Eq.mpr, id, congrFun', congrArg, map_mul, mul_le_of_le_one_right, zero_le, Subtype.property, Eq.symm, dite, OfNat.ofNat, Classical.propDecidable, of_eq_true, Eq.trans, True, congr, Eq.mp and 18 more

    190 instances, coercions and auxiliary constants left out.

    Tactic trace: 13 steps

    Open to load the checked before-and-after goal states.

  8. lemma TotallyDefiniteQuaternionAlgebra.WeightTwoAutomorphicForm.HeckeOperator.Local.GL2.localPTameLevel.conjBy_diag_mem_iff line 101 source

    standard axioms: Classical.choice, Quot.sound, propext what this means

    Statement uses: Field, NumberField, IsDedekindDomain.HeightOneSpectrum, NumberField.RingOfIntegers, Nat, Matrix.GeneralLinearGroup, Fin, OfNat.ofNat, IsDedekindDomain.HeightOneSpectrum.adicCompletion, Membership.mem, Subgroup, Matrix, IsDedekindDomain.GL2.localPTameLevel, Subtype, ValuationSubring, IsDedekindDomain.HeightOneSpectrum.adicCompletionIntegers, Ne, Iff, HMul.hMul, Inv.inv and 16 more

    Proof uses: Eq.mpr, And, LE.le, id, Eq, congrArg, propext, TotallyDefiniteQuaternionAlgebra.WeightTwoAutomorphicForm.HeckeOperator.Local.GL2.localPTameLevel.conjBy_diag_mem_iff', Eq.symm, one_mul, mul_lt_mul_of_lt_of_le_of_nonneg_of_pos, HAdd.hAdd, Eq.mp, Exists, Not, IsDedekindDomain.GL2.localPTameLevelSubgroup, HDiv.hDiv, Iff.mpr, Iff.of_eq, Eq.trans and 13 more

    208 instances, coercions and auxiliary constants left out.

    Tactic trace: 9 steps

    Open to load the checked before-and-after goal states.

  9. def TotallyDefiniteQuaternionAlgebra.WeightTwoAutomorphicForm.HeckeOperator.Local.unipotentMulDiagU1 For each t ∈ O_v / αO_v, the left coset unipotentMulDiag U1 for a lift of t to O_v line 125 source

    Source documentation

    For each t ∈ O_v / αO_v, the left coset unipotentMulDiag U1 for a lift of t to O_v.

    standard axioms: Classical.choice, Quot.sound, propext what this means

    Statement uses: Field, NumberField, IsDedekindDomain.HeightOneSpectrum, NumberField.RingOfIntegers, Nat, Subtype, IsDedekindDomain.HeightOneSpectrum.adicCompletion, Membership.mem, ValuationSubring, IsDedekindDomain.HeightOneSpectrum.adicCompletionIntegers, Ne, OfNat.ofNat, HasQuotient.Quotient, Ideal, Ideal.span, Singleton.singleton, Set, Matrix.GeneralLinearGroup, Fin, Subgroup and 2 more

    Proof uses: Quotient.map, Submodule.quotientRel, QuotientGroup.leftRel, TotallyDefiniteQuaternionAlgebra.WeightTwoAutomorphicForm.HeckeOperator.Local.GL2.unipotentMulDiag, Units.mk0

    73 instances, coercions and auxiliary constants left out.

    Tactic trace: 7 steps

    Open to load the checked before-and-after goal states.

    noncomputable def unipotentMulDiagU1 (t : v.adicCompletionIntegers F ⧸ (Ideal.span {α})) :
    GL₂(adicCompletion F v) ⧸ GL2.localPTameLevel v p :=
…
  10. lemma TotallyDefiniteQuaternionAlgebra.WeightTwoAutomorphicForm.HeckeOperator.Local.unipotentMulDiagU1_injective Distinct t give distinct unipotent_mul_diagU1, i.e. we have a disjoint union line 137 source

    Source documentation

    Distinct t give distinct unipotent_mul_diagU1, i.e. we have a disjoint union.

    standard axioms: Classical.choice, Quot.sound, propext what this means

    Statement uses: Field, NumberField, IsDedekindDomain.HeightOneSpectrum, NumberField.RingOfIntegers, Nat, Subtype, IsDedekindDomain.HeightOneSpectrum.adicCompletion, Membership.mem, ValuationSubring, IsDedekindDomain.HeightOneSpectrum.adicCompletionIntegers, Ne, OfNat.ofNat, Function.Injective, HasQuotient.Quotient, Ideal, Ideal.span, Singleton.singleton, Set, Matrix.GeneralLinearGroup, Fin and 4 more

    Proof uses: Quot.ind, Submodule.quotientRel, Eq, Quot.mk, Iff.mpr, RingHom, Ideal.Quotient.mk, HSub.hSub, Ideal.Quotient.eq, Eq.mpr, Dvd.dvd, id, congrArg, propext, Ideal.mem_span_singleton, dvd_sub_comm, Exists.intro, HMul.hMul, Subtype.mk, Inv.inv and 37 more

    171 instances, coercions and auxiliary constants left out.

    Tactic trace: 8 steps

    Open to load the checked before-and-after goal states.

    lemma unipotentMulDiagU1_injective :
    Function.Injective (unipotentMulDiagU1 v p α hα) := by
…

    Mentions: TotallyDefiniteQuaternionAlgebra.WeightTwoAutomorphicForm.HeckeOperator.Local.unipotentMulDiagU1

  11. lemma TotallyDefiniteQuaternionAlgebra.WeightTwoAutomorphicForm.HeckeOperator.Local.range_unipotentMulDiagU1 Each coset in U1diagU1 is of the form unipotent_mul_diagU1 for some t ∈ O_v line 149 source

    Source documentation

    Each coset in U1diagU1 is of the form unipotent_mul_diagU1 for some t ∈ O_v.

    standard axioms: Classical.choice, Quot.sound, propext what this means

    Statement uses: Field, NumberField, IsDedekindDomain.HeightOneSpectrum, NumberField.RingOfIntegers, Nat, Subtype, IsDedekindDomain.HeightOneSpectrum.adicCompletion, Membership.mem, ValuationSubring, IsDedekindDomain.HeightOneSpectrum.adicCompletionIntegers, Ne, OfNat.ofNat, Eq, Set, HasQuotient.Quotient, Matrix.GeneralLinearGroup, Fin, Subgroup, Matrix, IsDedekindDomain.GL2.localPTameLevel and 11 more

    Proof uses: Eq.mpr, Set.univ, id, congrArg, Eq.symm, Set.image_univ, RingHom, Ideal.Quotient.mk, Function.Surjective.range_eq, Ideal.Quotient.mk_surjective, Function.comp, Set.range_comp, subset_antisymm, Iff.mpr, LE.le, Set.range_subset_iff, Exists.intro, And, Matrix.GeneralLinearGroup.GL2.unipotent, And.intro and 96 more

    311 instances, coercions and auxiliary constants left out.

    Tactic trace: 21 steps

    Open to load the checked before-and-after goal states.

    lemma range_unipotentMulDiagU1 :
    Set.range (unipotentMulDiagU1 v p α hα) =
      QuotientGroup.mk '' (GL2.localPTameLevel v p *
        {diag (Units.mk0 α (by simpa))} : Set GL₂(v.adicCompletion F)) := by
…

    Mentions: TotallyDefiniteQuaternionAlgebra.WeightTwoAutomorphicForm.HeckeOperator.Local.unipotentMulDiagU1

  12. theorem TotallyDefiniteQuaternionAlgebra.WeightTwoAutomorphicForm.HeckeOperator.Local.bijOn_unipotentMulDiagU1 The double coset space U1diagU1 is the disjoint union of unipotent_mul_diagU1 as t ranges over O_v / αO_v line 177 source

    Source documentation

    The double coset space U1diagU1 is the disjoint union of unipotent_mul_diagU1 as t ranges over O_v / αO_v.

    standard axioms: Classical.choice, Quot.sound, propext what this means

    Statement uses: Field, NumberField, IsDedekindDomain.HeightOneSpectrum, NumberField.RingOfIntegers, Nat, Subtype, IsDedekindDomain.HeightOneSpectrum.adicCompletion, Membership.mem, ValuationSubring, IsDedekindDomain.HeightOneSpectrum.adicCompletionIntegers, Ne, OfNat.ofNat, Set.BijOn, HasQuotient.Quotient, Ideal, Ideal.span, Singleton.singleton, Set, Matrix.GeneralLinearGroup, Fin and 11 more

    Proof uses: Eq.mpr, eq_of_heq, Eq, HEq, Eq.refl, HEq.refl, Eq.symm, Set.range, id, congrArg, Set.image_univ, TotallyDefiniteQuaternionAlgebra.WeightTwoAutomorphicForm.HeckeOperator.Local.range_unipotentMulDiagU1, Function.Injective.bijOn_image, TotallyDefiniteQuaternionAlgebra.WeightTwoAutomorphicForm.HeckeOperator.Local.unipotentMulDiagU1_injective

    106 instances, coercions and auxiliary constants left out.

    Tactic trace: 3 steps

    Open to load the checked before-and-after goal states.

    theorem bijOn_unipotentMulDiagU1 :
    Set.BijOn (unipotentMulDiagU1 v p α hα) Set.univ
      (QuotientGroup.mk '' (GL2.localPTameLevel v p * {diag (Units.mk0 α (by simpa))})) := by
…

    Mentions: TotallyDefiniteQuaternionAlgebra.WeightTwoAutomorphicForm.HeckeOperator.Local.unipotentMulDiagU1