Concrete.lean`

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

Annotation provenance. This overlay contains 8 curated AI-written annotations and 1204 mechanical source-derived annotations. They have not been human-reviewed as explanations; treat them as unverified and not mathematical authority. Retained generation history: The 71 original curated annotations were produced in a Claude Sonnet 5.5 session at medium effort; Claude Opus 5.5 is recorded in that session as the advisor model, not the direct author. The bulk source-derived expansion was generated mechanically from pinned source comments by tooling developed in a GPT-5.6 Sol session at ultra reasoning; GPT-5.6 Sol did not originate the quoted source prose. On 2026-10-17 the mechanically generated source-comment annotations of the Formal Conjectures, Carleson, FLT, PFR, CompFiles, Mathematics in Lean and Theorem Proving in Lean overlays were regenerated by the same generator after three corrections made in a Claude Sonnet 5.5 session: titles no longer cut a sentence inside mathematics or end on a dangling word, workflow markers are removed from the quoted prose, and declaration names follow the scanner's namespace resolution. The boilerplate step line was dropped, and comments that were only a row of dashes no longer yield annotations. No new prose was written and no human review is claimed.

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

59 declarations, 0 contain sorry, 0 declared as axioms

Concrete Hecke operators on quaternionic automorphic forms

We define the Hecke operators Tᵥ acting on the space of weight-2 automorphic forms on a totally definite quaternion algebra. These are the concrete Hecke operators associated to a finite place v and a level subgroup U₁(S, Q), realised via the abstract double-coset construction.

Imports (7)

Imported by 3 files

lemma QuotientGroup.mk_image_finite_of_compact_of_open line 79 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Group, TopologicalSpace, IsTopologicalGroup, Subgroup, IsCompact, IsOpen, Set.Finite, HasQuotient.Quotient, Set.image, HMul.hMul, Set, Set.mul, Singleton.singleton
Proof uses: DiscreteTopology, Eq.mpr, id, Eq, congrArg, propext, discreteTopology_iff_forall_isOpen, Set.preimage, Eq.symm, Topology.IsCoinducing.isOpen_preimage, Topology.IsQuotientMap.isCoinducing, QuotientGroup.isQuotientMap_mk, Function.Surjective.image_preimage, QuotientGroup.mk_surjective, Set.iUnion, Subtype, Membership.mem, QuotientGroup.preimage_image_mk_eq_iUnion_image, Subtype.mk, Set.iUnion_subtype and 8 more
29 instances, coercions and auxiliary constants left out.

Tactic trace: 8 steps
Open to load the checked before-and-after goal states.
lemma TotallyDefiniteQuaternionAlgebra.WeightTwoAutomorphicForm.LocalLevelStruct.exists_mul_eq line 121 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Field, NumberField, CommRing, TotallyDefiniteQuaternionAlgebra.WeightTwoAutomorphicForm.LocalLevelStruct, Subtype, Matrix.GeneralLinearGroup, Fin, OfNat.ofNat, Nat, IsDedekindDomain.FiniteAdeleRing, NumberField.RingOfIntegers, Membership.mem, Subgroup, Matrix, TotallyDefiniteQuaternionAlgebra.WeightTwoAutomorphicForm.LevelStruct.U, TotallyDefiniteQuaternionAlgebra.WeightTwoAutomorphicForm.LocalLevelStruct.toStruct, IsDedekindDomain.HeightOneSpectrum, Exists, IsDedekindDomain.HeightOneSpectrum.adicCompletion, TotallyDefiniteQuaternionAlgebra.WeightTwoAutomorphicForm.LocalLevelStruct.US and 6 more
Proof uses: Exists.intro, HDiv.hDiv, Subtype.mk, Subtype.property, And.intro, Eq.mpr, id, congrArg, Subgroup.coe_div, map_div, propext, div_eq_one, of_eq_true, Eq.trans, True, IsDedekindDomain.FiniteAdeleRing.GL2.finiteAdeleIncl, MonoidHom.comp, Subgroup.subtype, Eq.refl, MonoidHom.codRestrict_apply and 3 more
82 instances, coercions and auxiliary constants left out.

Tactic trace: 6 steps
Open to load the checked before-and-after goal states.
def TotallyDefiniteQuaternionAlgebra.WeightTwoAutomorphicForm.LocalLevelStruct.heckeOperator line 131 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Field, NumberField, DivisionRing, Algebra, CommRing, AddCommGroup, Module, IsQuaternionAlgebra.NumberField.WithRigidification, TotallyDefiniteQuaternionAlgebra.WeightTwoAutomorphicForm.LocalLevelStruct, IsDedekindDomain.HeightOneSpectrum, NumberField.RingOfIntegers, Eq, MonoidHom, Subtype, Matrix.GeneralLinearGroup, Fin, OfNat.ofNat, Nat, IsDedekindDomain.HeightOneSpectrum.adicCompletion, Membership.mem and 9 more
Proof uses: LinearMap, RingHom.id, FixedPoints.submodule, AbstractHeckeOperator.heckeOperator, LinearMap.codRestrict, LinearMap.comp, Submodule.subtype, Submodule.inclusion
89 instances, coercions and auxiliary constants left out.

Tactic trace: 31 steps
Open to load the checked before-and-after goal states.
lemma TotallyDefiniteQuaternionAlgebra.WeightTwoAutomorphicForm.LocalLevelStruct.heckeOperator_mul_comm_of_ne line 161 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Field, NumberField, DivisionRing, Algebra, CommRing, AddCommGroup, Module, IsQuaternionAlgebra.NumberField.WithRigidification, TotallyDefiniteQuaternionAlgebra.WeightTwoAutomorphicForm.LocalLevelStruct, IsDedekindDomain.HeightOneSpectrum, NumberField.RingOfIntegers, Eq, MonoidHom, Subtype, Matrix.GeneralLinearGroup, Fin, OfNat.ofNat, Nat, IsDedekindDomain.HeightOneSpectrum.adicCompletion, Membership.mem and 12 more
Proof uses: LinearMap.ext, RingHom.id, Subtype.ext, LinearMap, id, Eq.mpr, FixedPoints.submodule, AbstractHeckeOperator.heckeOperator, Submodule.inclusion, LinearMap.codRestrict, LinearMap.comp, Submodule.subtype, Finset.sum, HasQuotient.Quotient, Set.Finite.toFinset, Set.image, Set, Set.mul, Singleton.singleton, HSMul.hSMul and 32 more
138 instances, coercions and auxiliary constants left out.

Tactic trace: 9 steps
Open to load the checked before-and-after goal states.
lemma TotallyDefiniteQuaternionAlgebra.WeightTwoAutomorphicForm._root_.QuotientGroup.exists_bijOn_mk_image_mul_singleton line 183 source
lemma TotallyDefiniteQuaternionAlgebra.WeightTwoAutomorphicForm.LocalLevelStruct.heckeOperator_eq_finsetSum line 199 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Field, NumberField, DivisionRing, Algebra, CommRing, AddCommGroup, Module, IsQuaternionAlgebra.NumberField.WithRigidification, TotallyDefiniteQuaternionAlgebra.WeightTwoAutomorphicForm.LocalLevelStruct, IsDedekindDomain.HeightOneSpectrum, NumberField.RingOfIntegers, Eq, MonoidHom, Subtype, Matrix.GeneralLinearGroup, Fin, OfNat.ofNat, Nat, IsDedekindDomain.HeightOneSpectrum.adicCompletion, Membership.mem and 21 more
Proof uses: TotallyDefiniteQuaternionAlgebra.WeightTwoAutomorphicForm.ext, IsDedekindDomain.FiniteAdeleRing, id, Eq.mpr, FixedPoints.submodule, LinearMap, AbstractHeckeOperator.heckeOperator, Submodule.inclusion, MulAction.fixedPoints, congrArg, AbstractHeckeOperator.heckeOperator_eq_finsetSum, of_eq_true, Eq.trans, True, congr, congrFun', Finset.sum_congr, Eq.refl, congrFun, TotallyDefiniteQuaternionAlgebra.WeightTwoAutomorphicForm.finsetSum_toFun and 2 more
145 instances, coercions and auxiliary constants left out.

Tactic trace: 4 steps
Open to load the checked before-and-after goal states.
abbrev TotallyDefiniteQuaternionAlgebra.WeightTwoAutomorphicForm.LocalLevelStruct.heckeOperatorL line 213 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Field, NumberField, DivisionRing, Algebra, CommRing, AddCommGroup, Module, Ring, IsQuaternionAlgebra.NumberField.WithRigidification, TotallyDefiniteQuaternionAlgebra.WeightTwoAutomorphicForm.LocalLevelStruct, IsDedekindDomain.HeightOneSpectrum, NumberField.RingOfIntegers, Eq, MonoidHom, Subtype, Matrix.GeneralLinearGroup, Fin, OfNat.ofNat, Nat, IsDedekindDomain.HeightOneSpectrum.adicCompletion and 11 more
Proof uses: TotallyDefiniteQuaternionAlgebra.WeightTwoAutomorphicForm.LocalLevelStruct.heckeOperator, LinearMap.mk, RingHom.id, LinearMap.toAddHom
91 instances, coercions and auxiliary constants left out.

Tactic trace: 3 steps
Open to load the checked before-and-after goal states.
lemma TotallyDefiniteQuaternionAlgebra.WeightTwoAutomorphicForm.LocalLevelStruct.heckeOperator_eq_of_mem_normalizer line 226 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Field, NumberField, DivisionRing, Algebra, CommRing, AddCommGroup, Module, IsQuaternionAlgebra.NumberField.WithRigidification, TotallyDefiniteQuaternionAlgebra.WeightTwoAutomorphicForm.LocalLevelStruct, IsDedekindDomain.HeightOneSpectrum, NumberField.RingOfIntegers, Eq, MonoidHom, Subtype, Matrix.GeneralLinearGroup, Fin, OfNat.ofNat, Nat, IsDedekindDomain.HeightOneSpectrum.adicCompletion, Membership.mem and 13 more
Proof uses: id, Eq.mpr, FixedPoints.submodule, LinearMap, AbstractHeckeOperator.heckeOperator, Submodule.inclusion, Set, MulAction.fixedPoints, congrArg, AbstractHeckeOperator.heckeOperator_eq_of_mem_normalizer, Eq.refl
130 instances, coercions and auxiliary constants left out.

Tactic trace: 3 steps
Open to load the checked before-and-after goal states.
lemma TotallyDefiniteQuaternionAlgebra.WeightTwoAutomorphicForm.LocalLevelStruct.heckeOperator_eq_of_mem line 235 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Field, NumberField, DivisionRing, Algebra, CommRing, AddCommGroup, Module, IsQuaternionAlgebra.NumberField.WithRigidification, TotallyDefiniteQuaternionAlgebra.WeightTwoAutomorphicForm.LocalLevelStruct, IsDedekindDomain.HeightOneSpectrum, NumberField.RingOfIntegers, Eq, MonoidHom, Subtype, Matrix.GeneralLinearGroup, Fin, OfNat.ofNat, Nat, IsDedekindDomain.HeightOneSpectrum.adicCompletion, Membership.mem and 11 more
Proof uses: Subtype.ext, Eq.mpr, HSMul.hSMul, id, congrArg, TotallyDefiniteQuaternionAlgebra.WeightTwoAutomorphicForm.LocalLevelStruct.heckeOperator_eq_of_mem_normalizer, Subgroup.le_normalizer, IsDedekindDomain.FiniteAdeleRing, IsDedekindDomain.FiniteAdeleRing.GL2.finiteAdeleIncl, TotallyDefiniteQuaternionAlgebra.WeightTwoAutomorphicForm.adicCompletion_smul_def, Eq.trans, TotallyDefiniteQuaternionAlgebra.WeightTwoAutomorphicForm.LevelStruct.U, TotallyDefiniteQuaternionAlgebra.WeightTwoAutomorphicForm.LocalLevelStruct.incl, Subtype.mk, TotallyDefiniteQuaternionAlgebra.WeightTwoAutomorphicForm.LevelStruct.χ, Subtype.property, of_eq_true, True, congrFun', TotallyDefiniteQuaternionAlgebra.WeightTwoAutomorphicForm.LocalLevelStruct.χ_incl and 2 more
111 instances, coercions and auxiliary constants left out.

Tactic trace: 4 steps
Open to load the checked before-and-after goal states.
lemma TotallyDefiniteQuaternionAlgebra.WeightTwoAutomorphicForm.LocalLevelStruct.heckeOperator_map_mul_of_mem_normalizer_left line 247 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Field, NumberField, DivisionRing, Algebra, CommRing, AddCommGroup, Module, IsQuaternionAlgebra.NumberField.WithRigidification, TotallyDefiniteQuaternionAlgebra.WeightTwoAutomorphicForm.LocalLevelStruct, IsDedekindDomain.HeightOneSpectrum, NumberField.RingOfIntegers, Eq, MonoidHom, Subtype, Matrix.GeneralLinearGroup, Fin, OfNat.ofNat, Nat, IsDedekindDomain.HeightOneSpectrum.adicCompletion, Membership.mem and 12 more
Proof uses: LinearMap.ext, RingHom.id, Subtype.ext, LinearMap, id, Eq.mpr, HSMul.hSMul, congrArg, TotallyDefiniteQuaternionAlgebra.WeightTwoAutomorphicForm.LocalLevelStruct.heckeOperator_eq_of_mem_normalizer, Set.Finite, HasQuotient.Quotient, Set.image, Set, Set.mul, Singleton.singleton, QuotientGroup.mk_image_finite_of_compact_of_open, TotallyDefiniteQuaternionAlgebra.WeightTwoAutomorphicForm.LocalLevelStruct.isCompact_US, TotallyDefiniteQuaternionAlgebra.WeightTwoAutomorphicForm.LocalLevelStruct.isOpen_US, Finset.sum, Set.Finite.toFinset and 69 more
173 instances, coercions and auxiliary constants left out.

Tactic trace: 35 steps
Open to load the checked before-and-after goal states.
lemma TotallyDefiniteQuaternionAlgebra.WeightTwoAutomorphicForm.LocalLevelStruct.heckeOperator_map_mul_of_mem_normalizer_right line 287 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Field, NumberField, DivisionRing, Algebra, CommRing, AddCommGroup, Module, IsQuaternionAlgebra.NumberField.WithRigidification, TotallyDefiniteQuaternionAlgebra.WeightTwoAutomorphicForm.LocalLevelStruct, IsDedekindDomain.HeightOneSpectrum, NumberField.RingOfIntegers, Eq, MonoidHom, Subtype, Matrix.GeneralLinearGroup, Fin, OfNat.ofNat, Nat, IsDedekindDomain.HeightOneSpectrum.adicCompletion, Membership.mem and 12 more
Proof uses: LinearMap.ext, RingHom.id, Subtype.ext, LinearMap, id, Set.Finite, HasQuotient.Quotient, Set.image, Set, Set.mul, Singleton.singleton, QuotientGroup.mk_image_finite_of_compact_of_open, TotallyDefiniteQuaternionAlgebra.WeightTwoAutomorphicForm.LocalLevelStruct.isCompact_US, TotallyDefiniteQuaternionAlgebra.WeightTwoAutomorphicForm.LocalLevelStruct.isOpen_US, Eq.mpr, Finset.sum, Set.Finite.toFinset, Quotient, QuotientGroup.leftRel, Quotient.out and 72 more
174 instances, coercions and auxiliary constants left out.

Tactic trace: 35 steps
Open to load the checked before-and-after goal states.
lemma TotallyDefiniteQuaternionAlgebra.WeightTwoAutomorphicForm.heckeOperatorL_tensor Hecke operators are preserved under the identification 𝒮²(U, χ; M ⊗ N) ≃ M ⊗ 𝒮²(U, χ; N) line 330 source
Source documentation
Hecke operators are preserved under the identification 𝒮²(U, χ; M ⊗ N) ≃ M ⊗ 𝒮²(U, χ; N).

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Field, NumberField, DivisionRing, Algebra, CommRing, AddCommGroup, Module, IsQuaternionAlgebra.NumberField.WithRigidification, TotallyDefiniteQuaternionAlgebra.WeightTwoAutomorphicForm.LocalLevelStruct, TotallyDefiniteQuaternionAlgebra.WeightTwoAutomorphicForm.LevelStruct.IsSufficientlySmall, TotallyDefiniteQuaternionAlgebra.WeightTwoAutomorphicForm.LocalLevelStruct.toStruct, TotallyDefiniteQuaternionAlgebra.WeightTwoAutomorphicForm.LevelStruct.IsFinite, IsScalarTower, SMulCommClass, IsDedekindDomain.HeightOneSpectrum, NumberField.RingOfIntegers, Eq, MonoidHom, Subtype, Matrix.GeneralLinearGroup and 21 more
Proof uses: Eq.mpr, id, congrArg, Eq.symm, LinearMap.comp_assoc, propext, LinearEquiv.eq_comp_toLinearMap_symm, TensorProduct.AlgebraTensorModule.curry_injective, LinearMap.ext, TensorProduct.AlgebraTensorModule.curry, TotallyDefiniteQuaternionAlgebra.WeightTwoAutomorphicForm.LocalLevelStruct.heckeOperator, LinearEquiv, TensorProduct.tmul, Subtype.ext, TotallyDefiniteQuaternionAlgebra.WeightTwoAutomorphicForm.ext, IsDedekindDomain.FiniteAdeleRing, Finset, Set.BijOn, HasQuotient.Quotient, Set.image and 27 more
200 instances, coercions and auxiliary constants left out.

Tactic trace: 7 steps
Open to load the checked before-and-after goal states.
```
lemma heckeOperatorL_tensor [ℒ.toStruct.IsSufficientlySmall D] [ℒ.toStruct.IsFinite D]
    {S N T : Type*} [CommRing S] [Module S M] [CommRing T] [Module T M] [Algebra R S] [Algebra S T]
    [AddCommGroup N] [Module S N] [Module R N]
    [IsScalarTower R S M] [IsScalarTower S T M] [SMulCommClass R T M] [IsScalarTower R S N]
    (v : HeightOneSpectrum (𝓞 F)) (hv : ℒ.χ v = 1)
    (g : GL₂(v.adicCompletion F)) [SMulCommClass R S M] :
    ℒ.heckeOperatorL D T (M ⊗[S] N) v hv g = (ℒ.toStruct.formTensor D _ _ _ _).toLinearMap ∘ₗ
      AlgebraTensorModule.lTensor T M (ℒ.heckeOperatorL D S N v hv g) ∘ₗ
      (ℒ.toStruct.formTensor D _ _ _ _).symm.toLinearMap := by
…
```
lemma TotallyDefiniteQuaternionAlgebra.WeightTwoAutomorphicForm.heckeOperator_eq_lTensor Hecke operators are preserved under the identification 𝒮²(U, χ; M) ≃ M ⊗ 𝒮²(U, χ; R) line 351 source
Source documentation
Hecke operators are preserved under the identification 𝒮²(U, χ; M) ≃ M ⊗ 𝒮²(U, χ; R).

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Field, NumberField, DivisionRing, Algebra, CommRing, AddCommGroup, Module, IsQuaternionAlgebra.NumberField.WithRigidification, TotallyDefiniteQuaternionAlgebra.WeightTwoAutomorphicForm.LocalLevelStruct, TotallyDefiniteQuaternionAlgebra.WeightTwoAutomorphicForm.LevelStruct.IsSufficientlySmall, TotallyDefiniteQuaternionAlgebra.WeightTwoAutomorphicForm.LocalLevelStruct.toStruct, TotallyDefiniteQuaternionAlgebra.WeightTwoAutomorphicForm.LevelStruct.IsFinite, IsDedekindDomain.HeightOneSpectrum, NumberField.RingOfIntegers, Eq, MonoidHom, Subtype, Matrix.GeneralLinearGroup, Fin, OfNat.ofNat and 19 more
Proof uses: Trans.simple, TotallyDefiniteQuaternionAlgebra.WeightTwoAutomorphicForm.LevelStruct.formCongr, TensorProduct.AlgebraTensorModule.rid, TotallyDefiniteQuaternionAlgebra.WeightTwoAutomorphicForm.LocalLevelStruct.heckeOperatorL, LinearMap.ext, Subtype.ext, TotallyDefiniteQuaternionAlgebra.WeightTwoAutomorphicForm.ext, IsDedekindDomain.FiniteAdeleRing, Finset, Set.BijOn, HasQuotient.Quotient, Set.image, HMul.hMul, Set, Set.mul, Singleton.singleton, Exists, QuotientGroup.exists_bijOn_mk_image_mul_singleton, TotallyDefiniteQuaternionAlgebra.WeightTwoAutomorphicForm.LocalLevelStruct.isOpen_US, TotallyDefiniteQuaternionAlgebra.WeightTwoAutomorphicForm.LocalLevelStruct.isCompact_US and 30 more
206 instances, coercions and auxiliary constants left out.

Tactic trace: 8 steps
Open to load the checked before-and-after goal states.
```
lemma heckeOperator_eq_lTensor [ℒ.toStruct.IsSufficientlySmall D] [ℒ.toStruct.IsFinite D]
    (v : HeightOneSpectrum (𝓞 F)) (hv : ℒ.χ v = 1) (g : GL₂(v.adicCompletion F)) :
    ℒ.heckeOperator D M v hv g = (ℒ.toStruct.formTensorScalar D _ _).toLinearMap ∘ₗ
      AlgebraTensorModule.lTensor R M (ℒ.heckeOperator D R v hv g) ∘ₗ
      (ℒ.toStruct.formTensorScalar D _ _).symm.toLinearMap := by
…
```
structure TotallyDefiniteQuaternionAlgebra.U₁Data The U₁ we will be considering needs the following input: line 376 source
Source documentation
The U₁ we will be considering needs the following input:

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Field, NumberField, CommRing, Nat
```
structure U₁Data (p : ℕ) where
…
```
def TotallyDefiniteQuaternionAlgebra.U₁ line 396 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Field, NumberField, CommRing, Nat, TotallyDefiniteQuaternionAlgebra.U₁Data, TotallyDefiniteQuaternionAlgebra.WeightTwoAutomorphicForm.LocalLevelStruct
Proof uses: TotallyDefiniteQuaternionAlgebra.WeightTwoAutomorphicForm.LocalLevelStruct.mk, Union.union, Finset, IsDedekindDomain.HeightOneSpectrum, NumberField.RingOfIntegers, Classical.propDecidable, Eq, TotallyDefiniteQuaternionAlgebra.U₁Data.S, TotallyDefiniteQuaternionAlgebra.U₁Data.Q, ite, Subgroup, Matrix.GeneralLinearGroup, Fin, OfNat.ofNat, IsDedekindDomain.HeightOneSpectrum.adicCompletion, Matrix, Membership.mem, IsDedekindDomain.GL2.localPTameLevel, IsDedekindDomain.GL2.localIwahoriLevel, IsDedekindDomain.GL2.localFullLevel and 14 more
41 instances, coercions and auxiliary constants left out.

Tactic trace: 39 steps
Open to load the checked before-and-after goal states.
lemma TotallyDefiniteQuaternionAlgebra.U₁Data.eq_one_of_pow_eq_one_of_natDegree_le_two line 441 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Field, NumberField, CommRing, Nat, TotallyDefiniteQuaternionAlgebra.U₁Data, IsDomain, Algebra, Eq, HPow.hPow, OfNat.ofNat, LE.le, Polynomial.natDegree, minpoly
Proof uses: Classical.byContradiction, Not, IsIntegral, IsIntegral.of_pow, Nat.Prime.pos, TotallyDefiniteQuaternionAlgebra.U₁Data.prime, of_eq_true, Eq.trans, True, congrArg, IsPrimitiveRoot, Iff.mpr, And, Ne, IsPrimitiveRoot.iff_of_prime, And.intro, NeZero, NeZero.mk, Nat.Prime.ne_zero, IsCyclotomicExtension and 42 more
78 instances, coercions and auxiliary constants left out.

Tactic trace: 12 steps
Open to load the checked before-and-after goal states.
lemma TotallyDefiniteQuaternionAlgebra._root_.Polynomial.cyclotomic_of_charP line 464 source
instance TotallyDefiniteQuaternionAlgebra.(instance at line 477) line 477 source
lemma TotallyDefiniteQuaternionAlgebra.U₁Data.five_le line 483 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Field, NumberField, CommRing, Nat, TotallyDefiniteQuaternionAlgebra.U₁Data, LE.le, OfNat.ofNat
Proof uses: Decidable.byContradiction, Not, dite, False, LT.lt, Eq, Nat.Prime, of_decide_eq_true, id, Bool, Decidable.decide, Bool.true, Eq.refl, TotallyDefiniteQuaternionAlgebra.U₁Data.prime, Eq.symm, le_antisymm, Nat.ge_of_not_lt, Mathlib.Tactic.IntervalCases.of_lt_right, Nat.rawCast, Eq.mp and 67 more
79 instances, coercions and auxiliary constants left out.

Tactic trace: 17 steps
Open to load the checked before-and-after goal states.
lemma TotallyDefiniteQuaternionAlgebra.U₁Data.not_charP line 499 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Field, NumberField, CommRing, Nat, TotallyDefiniteQuaternionAlgebra.U₁Data, Not, CharP
Proof uses: AlgHom, CyclotomicField, Polynomial.IsSplittingField.lift, Polynomial.SplittingField, Polynomial.cyclotomic, Eq.mpr, Polynomial.Splits, Polynomial.map, Algebra.algebraMap, HPow.hPow, Polynomial, HSub.hSub, Polynomial.X, OfNat.ofNat, id, Eq, congrArg, Polynomial.cyclotomic_of_charP, TotallyDefiniteQuaternionAlgebra.U₁Data.prime, Eq.trans and 25 more
68 instances, coercions and auxiliary constants left out.

Tactic trace: 7 steps
Open to load the checked before-and-after goal states.
lemma TotallyDefiniteQuaternionAlgebra.U₁Data.coe_ne_zero line 510 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Field, NumberField, CommRing, Nat, TotallyDefiniteQuaternionAlgebra.U₁Data, Ne, OfNat.ofNat
Proof uses: Eq, TotallyDefiniteQuaternionAlgebra.U₁Data.not_charP, Iff.mpr, CharP, CharP.charP_iff_prime_eq_zero, TotallyDefiniteQuaternionAlgebra.U₁Data.prime
31 instances, coercions and auxiliary constants left out.

Tactic trace: 2 steps
Open to load the checked before-and-after goal states.
lemma TotallyDefiniteQuaternionAlgebra.U₁Data.eq_one_of_pow_eq_one line 518 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Field, NumberField, DivisionRing, Algebra, CommRing, Nat, TotallyDefiniteQuaternionAlgebra.U₁Data, Eq, HPow.hPow, OfNat.ofNat, IsQuaternionAlgebra
Proof uses: Classical.byContradiction, Not, Subtype, Membership.mem, Subalgebra, Algebra.adjoin, Singleton.singleton, Set, Subtype.mk, Algebra.self_mem_adjoin_singleton, IsPrimitiveRoot, Iff.mpr, orderOf, IsPrimitiveRoot.iff_orderOf, Or.resolve_left, Nat.Prime.eq_one_or_self_of_dvd, TotallyDefiniteQuaternionAlgebra.U₁Data.prime, orderOf_dvd_of_pow_eq_one, Subtype.ext, of_eq_true and 114 more
176 instances, coercions and auxiliary constants left out.

Tactic trace: 49 steps
Open to load the checked before-and-after goal states.
lemma TotallyDefiniteQuaternionAlgebra.U₁Data.χ_apply_pow line 566 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Field, NumberField, CommRing, Nat, TotallyDefiniteQuaternionAlgebra.U₁Data, IsDedekindDomain.HeightOneSpectrum, NumberField.RingOfIntegers, Subtype, Matrix.GeneralLinearGroup, Fin, OfNat.ofNat, IsDedekindDomain.HeightOneSpectrum.adicCompletion, Membership.mem, Subgroup, Matrix, TotallyDefiniteQuaternionAlgebra.WeightTwoAutomorphicForm.LocalLevelStruct.US, TotallyDefiniteQuaternionAlgebra.U₁, Eq, HPow.hPow, MonoidHom and 1 more
Proof uses: dite, And, Finset, TotallyDefiniteQuaternionAlgebra.U₁Data.S, Not, TotallyDefiniteQuaternionAlgebra.U₁Data.Q, Classical.propDecidable, Eq.mpr, ite, IsDedekindDomain.GL2.localPTameLevel, IsDedekindDomain.GL2.localIwahoriLevel, IsDedekindDomain.GL2.localFullLevel, MonoidHom.comp, Units, IsLocalRing.ResidueField, ValuationSubring, IsDedekindDomain.HeightOneSpectrum.adicCompletionIntegers, TotallyDefiniteQuaternionAlgebra.U₁Data.χS, IsDedekindDomain.GL2.localIwahoriLevel.char, MulEquiv and 18 more
90 instances, coercions and auxiliary constants left out.

Tactic trace: 6 steps
Open to load the checked before-and-after goal states.
lemma TotallyDefiniteQuaternionAlgebra.U₁Data.χ_pow line 572 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Field, NumberField, CommRing, Nat, TotallyDefiniteQuaternionAlgebra.U₁Data, IsDedekindDomain.HeightOneSpectrum, NumberField.RingOfIntegers, Eq, MonoidHom, Subtype, Matrix.GeneralLinearGroup, Fin, OfNat.ofNat, IsDedekindDomain.HeightOneSpectrum.adicCompletion, Membership.mem, Subgroup, Matrix, TotallyDefiniteQuaternionAlgebra.WeightTwoAutomorphicForm.LocalLevelStruct.US, TotallyDefiniteQuaternionAlgebra.U₁, HPow.hPow and 1 more
Proof uses: MonoidHom.ext, of_eq_true, Eq.trans, True, congrFun', congrArg, TotallyDefiniteQuaternionAlgebra.U₁Data.χ_apply_pow, eq_self
67 instances, coercions and auxiliary constants left out.

Tactic trace: 2 steps
Open to load the checked before-and-after goal states.
lemma TotallyDefiniteQuaternionAlgebra.U₁Data.toStruct_χ_apply_pow line 575 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Field, NumberField, CommRing, Nat, TotallyDefiniteQuaternionAlgebra.U₁Data, Subtype, Matrix.GeneralLinearGroup, Fin, OfNat.ofNat, IsDedekindDomain.FiniteAdeleRing, NumberField.RingOfIntegers, Membership.mem, Subgroup, Matrix, TotallyDefiniteQuaternionAlgebra.WeightTwoAutomorphicForm.LevelStruct.U, TotallyDefiniteQuaternionAlgebra.WeightTwoAutomorphicForm.LocalLevelStruct.toStruct, TotallyDefiniteQuaternionAlgebra.U₁, Eq, HPow.hPow, MonoidHom and 1 more
Proof uses: id, Eq.mpr, Subgroup.mk, Submonoid.mk, Subsemigroup.mk, Set.ofPred, IsDedekindDomain.HeightOneSpectrum, IsDedekindDomain.HeightOneSpectrum.adicCompletion, TotallyDefiniteQuaternionAlgebra.WeightTwoAutomorphicForm.LocalLevelStruct.US, IsDedekindDomain.FiniteAdeleRing.GL2.toAdicCompletion, Finset.prod, TotallyDefiniteQuaternionAlgebra.WeightTwoAutomorphicForm.LocalLevelStruct.S, MonoidHom.comp, TotallyDefiniteQuaternionAlgebra.WeightTwoAutomorphicForm.LocalLevelStruct.χ, MonoidHom.codRestrict, Subgroup.subtype, congrArg, MonoidHom.finsetProd_apply, of_eq_true, Eq.trans and 10 more
90 instances, coercions and auxiliary constants left out.

Tactic trace: 72 steps
Open to load the checked before-and-after goal states.
instance TotallyDefiniteQuaternionAlgebra.(instance at line 583) line 583 source
def TotallyDefiniteQuaternionAlgebra.HeckeOperator.T The Hecke operator T_v as an R-linear map from M-valued quaternionic weight 2 automorphic forms of level U_1(S₀) line 654 source
Source documentation
The Hecke operator T_v as an R-linear map from M-valued quaternionic weight 2 automorphic forms of level U_1(S₀).

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Field, NumberField, DivisionRing, Algebra, CommRing, AddCommGroup, Module, IsQuaternionAlgebra.NumberField.WithRigidification, Nat, TotallyDefiniteQuaternionAlgebra.U₁Data, IsDedekindDomain.HeightOneSpectrum, NumberField.RingOfIntegers, Not, Membership.mem, Finset, TotallyDefiniteQuaternionAlgebra.U₁Data.S, Module.End, Subtype, TotallyDefiniteQuaternionAlgebra.WeightTwoAutomorphicForm, Submodule and 3 more
Proof uses: TotallyDefiniteQuaternionAlgebra.WeightTwoAutomorphicForm.LocalLevelStruct.heckeOperator, Matrix.GeneralLinearGroup.diagonal, Fin, OfNat.ofNat, IsDedekindDomain.HeightOneSpectrum.adicCompletion, Matrix.vecCons, Units, IsDedekindDomain.HeightOneSpectrum.adicCompletionUniformizerUnit, Matrix.vecEmpty
42 instances, coercions and auxiliary constants left out.

Tactic trace: 1 steps
Open to load the checked before-and-after goal states.
```
noncomputable def T (𝒮 : U₁Data F R p) (v : HeightOneSpectrum (𝓞 F)) (hvS : v ∉ 𝒮.S) :
    Module.End R ((U₁ 𝒮).toStruct.form D M) :=
…
```
Mentions: TotallyDefiniteQuaternionAlgebra.U₁Data, TotallyDefiniteQuaternionAlgebra.U₁
lemma TotallyDefiniteQuaternionAlgebra.HeckeOperator.T_smul line 660 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Field, NumberField, DivisionRing, Algebra, CommRing, AddCommGroup, Module, Ring, IsQuaternionAlgebra.NumberField.WithRigidification, Nat, SMulCommClass, TotallyDefiniteQuaternionAlgebra.U₁Data, IsDedekindDomain.HeightOneSpectrum, NumberField.RingOfIntegers, Not, Membership.mem, Finset, TotallyDefiniteQuaternionAlgebra.U₁Data.S, Subtype, TotallyDefiniteQuaternionAlgebra.WeightTwoAutomorphicForm and 9 more
Proof uses: LinearMap.map_smul, TotallyDefiniteQuaternionAlgebra.WeightTwoAutomorphicForm.LocalLevelStruct.heckeOperatorL, Eq.mpr, MonoidHom, Matrix.GeneralLinearGroup, Fin, OfNat.ofNat, IsDedekindDomain.HeightOneSpectrum.adicCompletion, Subgroup, Matrix, TotallyDefiniteQuaternionAlgebra.WeightTwoAutomorphicForm.LocalLevelStruct.US, TotallyDefiniteQuaternionAlgebra.WeightTwoAutomorphicForm.LocalLevelStruct.χ, ite, TotallyDefiniteQuaternionAlgebra.U₁Data.Q, Classical.propDecidable, IsDedekindDomain.GL2.localPTameLevel, IsDedekindDomain.GL2.localIwahoriLevel, IsDedekindDomain.GL2.localFullLevel, id, congrFun' and 23 more
94 instances, coercions and auxiliary constants left out.

Tactic trace: 2 steps
Open to load the checked before-and-after goal states.
lemma TotallyDefiniteQuaternionAlgebra.HeckeOperator.T_inv line 666 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Field, NumberField, DivisionRing, Algebra, CommRing, AddCommGroup, Module, IsQuaternionAlgebra.NumberField.WithRigidification, Nat, TotallyDefiniteQuaternionAlgebra.U₁Data, IsDedekindDomain.HeightOneSpectrum, NumberField.RingOfIntegers, Not, Membership.mem, Finset, TotallyDefiniteQuaternionAlgebra.U₁Data.S, TotallyDefiniteQuaternionAlgebra.U₁Data.Q, Eq, Module.End, Subtype and 18 more
Proof uses: Units.mk, Equiv, Matrix.of, of_eq_true, HMul.hMul, Eq.trans, Nat.succ, True, congr, congrArg, Matrix.vecMul, Equiv.symm, Matrix.cons_mul, HAdd.hAdd, HSMul.hSMul, Matrix.vecHead, Matrix.vecTail, Matrix.vecMul_cons, zero_smul, congrFun' and 90 more
239 instances, coercions and auxiliary constants left out.

Tactic trace: 25 steps
Open to load the checked before-and-after goal states.
def TotallyDefiniteQuaternionAlgebra.HeckeOperator.U The Hecke operator U_{v,α} associated to the matrix (α 0;0 1) at v, considered as an R-linear map from R-valued quaternionic weight 2 automorphic forms of level U_1(S) line 723 source
Source documentation
The Hecke operator U_{v,α} associated to the matrix (α 0;0 1) at v, considered as an R-linear map from R-valued quaternionic weight 2 automorphic forms of level U_1(S). Here α is a nonzero element of 𝓞ᵥ. We do not demand the condition v ∈ S, the bad primes, but this operator should only be used in this setting. See also T r v for the good primes.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Field, NumberField, DivisionRing, Algebra, CommRing, AddCommGroup, Module, IsQuaternionAlgebra.NumberField.WithRigidification, Nat, TotallyDefiniteQuaternionAlgebra.U₁Data, IsDedekindDomain.HeightOneSpectrum, NumberField.RingOfIntegers, Membership.mem, Finset, TotallyDefiniteQuaternionAlgebra.U₁Data.Q, Subtype, IsDedekindDomain.HeightOneSpectrum.adicCompletion, ValuationSubring, IsDedekindDomain.HeightOneSpectrum.adicCompletionIntegers, Ne and 7 more
Proof uses: TotallyDefiniteQuaternionAlgebra.WeightTwoAutomorphicForm.LocalLevelStruct.heckeOperator, Matrix.GeneralLinearGroup.diagonal, Fin, Matrix.vecCons, Units, Units.mk0, Matrix.vecEmpty
75 instances, coercions and auxiliary constants left out.

Tactic trace: 3 steps
Open to load the checked before-and-after goal states.
```
noncomputable def U (𝒮 : U₁Data F R p) (v : HeightOneSpectrum (𝓞 F))
    (hvQ : v ∈ 𝒮.Q) (α : v.adicCompletionIntegers F) (hα : α ≠ 0) :
  Module.End R ((U₁ 𝒮).toStruct.form D M) :=
…
```
Mentions: TotallyDefiniteQuaternionAlgebra.U₁Data, TotallyDefiniteQuaternionAlgebra.U₁
lemma TotallyDefiniteQuaternionAlgebra.HeckeOperator.U_smul line 730 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Field, NumberField, DivisionRing, Algebra, CommRing, AddCommGroup, Module, Ring, IsQuaternionAlgebra.NumberField.WithRigidification, Nat, SMulCommClass, TotallyDefiniteQuaternionAlgebra.U₁Data, IsDedekindDomain.HeightOneSpectrum, NumberField.RingOfIntegers, Membership.mem, Finset, TotallyDefiniteQuaternionAlgebra.U₁Data.Q, Subtype, IsDedekindDomain.HeightOneSpectrum.adicCompletion, ValuationSubring and 13 more
Proof uses: LinearMap.map_smul, TotallyDefiniteQuaternionAlgebra.WeightTwoAutomorphicForm.LocalLevelStruct.heckeOperatorL, Eq.mpr, MonoidHom, Matrix.GeneralLinearGroup, Fin, Subgroup, Matrix, TotallyDefiniteQuaternionAlgebra.WeightTwoAutomorphicForm.LocalLevelStruct.US, TotallyDefiniteQuaternionAlgebra.WeightTwoAutomorphicForm.LocalLevelStruct.χ, ite, Classical.propDecidable, IsDedekindDomain.GL2.localPTameLevel, TotallyDefiniteQuaternionAlgebra.U₁Data.S, IsDedekindDomain.GL2.localIwahoriLevel, IsDedekindDomain.GL2.localFullLevel, id, congrFun', congrArg, Eq.trans and 22 more
140 instances, coercions and auxiliary constants left out.

Tactic trace: 3 steps
Open to load the checked before-and-after goal states.
lemma TotallyDefiniteQuaternionAlgebra.HeckeOperator.U_apply line 738 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Field, NumberField, DivisionRing, Algebra, CommRing, AddCommGroup, Module, IsQuaternionAlgebra.NumberField.WithRigidification, Nat, TotallyDefiniteQuaternionAlgebra.U₁Data, IsDedekindDomain.HeightOneSpectrum, NumberField.RingOfIntegers, Membership.mem, Finset, TotallyDefiniteQuaternionAlgebra.U₁Data.Q, Subtype, IsDedekindDomain.HeightOneSpectrum.adicCompletion, ValuationSubring, IsDedekindDomain.HeightOneSpectrum.adicCompletionIntegers, Ne and 26 more
Proof uses: id, Eq.trans, FixedPoints.submodule, Subgroup, TotallyDefiniteQuaternionAlgebra.WeightTwoAutomorphicForm.LocalLevelStruct.US, LinearMap, AbstractHeckeOperator.heckeOperator, Matrix.GeneralLinearGroup.diagonal, Matrix.vecCons, Units, Matrix.vecEmpty, Submodule.inclusion, Finset.image, Classical.propDecidable, Function.comp, of_eq_true, Not, False, True, congrArg and 100 more
261 instances, coercions and auxiliary constants left out.

Tactic trace: 24 steps
Open to load the checked before-and-after goal states.
lemma TotallyDefiniteQuaternionAlgebra.HeckeOperator.U_apply_of_isUnit line 766 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Field, NumberField, DivisionRing, Algebra, CommRing, AddCommGroup, Module, IsQuaternionAlgebra.NumberField.WithRigidification, Nat, TotallyDefiniteQuaternionAlgebra.U₁Data, IsDedekindDomain.HeightOneSpectrum, NumberField.RingOfIntegers, Membership.mem, Finset, TotallyDefiniteQuaternionAlgebra.U₁Data.Q, Subtype, IsDedekindDomain.HeightOneSpectrum.adicCompletion, ValuationSubring, IsDedekindDomain.HeightOneSpectrum.adicCompletionIntegers, Ne and 21 more
Proof uses: id, AbstractHeckeOperator.heckeOperator_eq_of_mem_normalizer, TotallyDefiniteQuaternionAlgebra.WeightTwoAutomorphicForm.LocalLevelStruct.US, LinearMap, FixedPoints.submodule, Subgroup, Submodule.inclusion, Eq.mpr, Subgroup.normalizer, IsDedekindDomain.GL2.localPTameLevel, congrFun', congrArg, Set, ite_eq_left_of_eq_true, Classical.propDecidable, ite, TotallyDefiniteQuaternionAlgebra.U₁Data.S, IsDedekindDomain.GL2.localIwahoriLevel, IsDedekindDomain.GL2.localFullLevel, eq_true and 32 more
222 instances, coercions and auxiliary constants left out.

Tactic trace: 6 steps
Open to load the checked before-and-after goal states.
lemma TotallyDefiniteQuaternionAlgebra.HeckeOperator.adicCompletionIntegers.finite_quotient line 777 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Field, NumberField, IsDedekindDomain.HeightOneSpectrum, NumberField.RingOfIntegers, Ideal, Subtype, IsDedekindDomain.HeightOneSpectrum.adicCompletion, Membership.mem, ValuationSubring, IsDedekindDomain.HeightOneSpectrum.adicCompletionIntegers, Ne, OfNat.ofNat, Finite, HasQuotient.Quotient
Proof uses: OrderDual, ENat, Eq, OrderIso, OrderIso.symm, IsDiscreteValuationRing.idealOrderIsoENat, Exists, OrderIso.surjective, Nat, Option.none, False, id, Eq.refl, Option.some, Ideal.finite_quotient_pow, IsLocalRing.maximalIdeal, IsNoetherian.noetherian
88 instances, coercions and auxiliary constants left out.

Tactic trace: 7 steps
Open to load the checked before-and-after goal states.
lemma TotallyDefiniteQuaternionAlgebra.HeckeOperator.adicCompletionIntegers.exists_bijOn_mk_span line 784 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, Ne, OfNat.ofNat, Exists, Finset, Set.BijOn, HasQuotient.Quotient, Ideal, Ideal.span, Singleton.singleton, Set, RingHom and 2 more
Proof uses: Finite, TotallyDefiniteQuaternionAlgebra.HeckeOperator.adicCompletionIntegers.finite_quotient, Eq.mpr, Not, Eq, id, congrArg, Bot.bot, Submodule, Eq.trans, Submodule.span, forall_congr, implies_congr, Eq.refl, Fintype, Nonempty, nonempty_fintype, Nonempty.intro, Exists.intro, Finset.image and 25 more
95 instances, coercions and auxiliary constants left out.

Tactic trace: 7 steps
Open to load the checked before-and-after goal states.
lemma TotallyDefiniteQuaternionAlgebra.HeckeOperator.U_mul_U line 797 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Field, NumberField, DivisionRing, Algebra, CommRing, AddCommGroup, Module, IsQuaternionAlgebra.NumberField.WithRigidification, Nat, TotallyDefiniteQuaternionAlgebra.U₁Data, IsDedekindDomain.HeightOneSpectrum, NumberField.RingOfIntegers, Membership.mem, Finset, TotallyDefiniteQuaternionAlgebra.U₁Data.Q, Subtype, IsDedekindDomain.HeightOneSpectrum.adicCompletion, ValuationSubring, IsDedekindDomain.HeightOneSpectrum.adicCompletionIntegers, Ne and 10 more
Proof uses: LinearMap.ext, RingHom.id, Subtype.ext, LinearMap, Set.BijOn, HasQuotient.Quotient, Ideal, Ideal.span, Singleton.singleton, Set, RingHom, Ideal.Quotient.mk, Set.univ, Exists, TotallyDefiniteQuaternionAlgebra.HeckeOperator.adicCompletionIntegers.exists_bijOn_mk_span, id, Eq.mpr, Finset.sum, HSMul.hSMul, Matrix.GeneralLinearGroup and 131 more
263 instances, coercions and auxiliary constants left out.

Tactic trace: 44 steps
Open to load the checked before-and-after goal states.
def TotallyDefiniteQuaternionAlgebra.HeckeAlgebra Documented declaration: HeckeAlgebra line 879 source
Source documentation
Given 𝒮 : U₁Data F R p, HeckeAlgebra D 𝒮 is the Hecke algebra associated to the weight 2 R-valued automorphic forms associated to the discriminant 1 totally definite quaternion algebra D over the totally real field F, of level U₁(S, Q) where S is a finite set of nonzero primes v of 𝓞 F. To make sense of this definition we choose a rigidification, that is, a fixed 𝔸_F^∞-linear isomorphism D ⊗[F] 𝔸_F^∞ = M₂(𝔸_F^∞), enabling us to define level structures and Hecke operators Tᵥ and Uᵥ using 2x2 matrices.
Details: 𝒮 : U₁Data F R p consist of a set of bad primes S of F with order p characters k(v) →* R, and a set of taylor wiles primes Q.
U₁(S, Q) is the subgroup of (D ⊗[F] 𝔸_F^∞)ˣ associated, via r, to the matrices which are in GL₂(𝓞ᵥ) for all v ∉ S ∪ Q and which are of the form (* *; 0 *) mod v for all v ∈ S, and (a *; 0 d) mod v with p ∤ ord(a/d) for v ∈ Q.
The Hecke algebra is defined to be the sub-R-algebra of the weight 2 forms of level U₁(S, Q) generated by the following two kinds of Hecke operators: first there are the operators Tᵥ associated to the matrices (ϖᵥ 0; 0 1) for v ∉ S ∪ Q (here ϖᵥ ∈ 𝔸_F^∞ is a local uniformiser supported at v). Second, there are the Hecke operators Uᵥ,ₐ for v ∈ Q and 0 ≠ αᵥ ∈ 𝓞ᵥ, associated the matries (αᵥ 0; 0 1). These slightly nonstandard Hecke operators satisfy Uᵥ,ₛ * Uᵥ,ₜ = Uᵥ,ₛₜ and in particular this Hecke algebra is commutative (Hecke operators supported at distinct primes commute because the decomposition of the double cosets into single cosets can be done purely locally).

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Field, NumberField, DivisionRing, Algebra, CommRing, IsQuaternionAlgebra.NumberField.WithRigidification, Nat, TotallyDefiniteQuaternionAlgebra.U₁Data
Proof uses: Subtype, Module.End, TotallyDefiniteQuaternionAlgebra.WeightTwoAutomorphicForm, Membership.mem, Submodule, TotallyDefiniteQuaternionAlgebra.WeightTwoAutomorphicForm.LevelStruct.form, TotallyDefiniteQuaternionAlgebra.WeightTwoAutomorphicForm.LocalLevelStruct.toStruct, TotallyDefiniteQuaternionAlgebra.U₁, Subalgebra, Algebra.adjoin, Union.union, Set, Set.ofPred, Exists, IsDedekindDomain.HeightOneSpectrum, NumberField.RingOfIntegers, Not, Finset, TotallyDefiniteQuaternionAlgebra.U₁Data.S, TotallyDefiniteQuaternionAlgebra.U₁Data.Q and 8 more
43 instances, coercions and auxiliary constants left out.
```
def HeckeAlgebra (𝒮 : U₁Data F R p) : Type _ :=
…
```
Mentions: TotallyDefiniteQuaternionAlgebra.U₁Data
instance TotallyDefiniteQuaternionAlgebra.HeckeAlgebra.instRing line 886 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Field, NumberField, DivisionRing, Algebra, CommRing, IsQuaternionAlgebra.NumberField.WithRigidification, Nat, TotallyDefiniteQuaternionAlgebra.U₁Data, Ring, TotallyDefiniteQuaternionAlgebra.HeckeAlgebra
Proof uses: Ring.mk, Semiring.mk, AddCommMonoid.mk, AddMonoid.mk, Zero.mk, Add.mk, NSMul.mk, Monoid.mk, One.mk, Mul.mk, NPow.mk, NatCast.mk, Neg.mk, Sub.mk, ZSMul.mk, IntCast.mk
43 instances, coercions and auxiliary constants left out.
instance TotallyDefiniteQuaternionAlgebra.HeckeAlgebra.instAlgebra line 890 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Field, NumberField, DivisionRing, Algebra, CommRing, IsQuaternionAlgebra.NumberField.WithRigidification, Nat, TotallyDefiniteQuaternionAlgebra.U₁Data, TotallyDefiniteQuaternionAlgebra.HeckeAlgebra
Proof uses: Algebra.mk, SMul.mk
16 instances, coercions and auxiliary constants left out.

Tactic trace: 28 steps
Open to load the checked before-and-after goal states.
instance TotallyDefiniteQuaternionAlgebra.HeckeAlgebra.(instance at line 894) line 894 source
instance TotallyDefiniteQuaternionAlgebra.HeckeAlgebra.instCommRing line 911 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Field, NumberField, DivisionRing, Algebra, CommRing, IsQuaternionAlgebra.NumberField.WithRigidification, Nat, TotallyDefiniteQuaternionAlgebra.U₁Data, TotallyDefiniteQuaternionAlgebra.HeckeAlgebra
Proof uses: inferInstance, IsMulCommutative.instCommRing
10 instances, coercions and auxiliary constants left out.
def TotallyDefiniteQuaternionAlgebra.HeckeAlgebra.T The Hecke operator Tᵥ as an element of the Hecke algebra line 916 source
Source documentation
The Hecke operator Tᵥ as an element of the Hecke algebra.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Field, NumberField, DivisionRing, Algebra, CommRing, IsQuaternionAlgebra.NumberField.WithRigidification, Nat, TotallyDefiniteQuaternionAlgebra.U₁Data, IsDedekindDomain.HeightOneSpectrum, NumberField.RingOfIntegers, Not, Membership.mem, Finset, TotallyDefiniteQuaternionAlgebra.U₁Data.S, TotallyDefiniteQuaternionAlgebra.U₁Data.Q, TotallyDefiniteQuaternionAlgebra.HeckeAlgebra
Proof uses: Subtype.mk, Module.End, Subtype, TotallyDefiniteQuaternionAlgebra.WeightTwoAutomorphicForm, Submodule, TotallyDefiniteQuaternionAlgebra.WeightTwoAutomorphicForm.LevelStruct.form, TotallyDefiniteQuaternionAlgebra.WeightTwoAutomorphicForm.LocalLevelStruct.toStruct, TotallyDefiniteQuaternionAlgebra.U₁, Subalgebra, Algebra.adjoin, Union.union, Set, Set.ofPred, Exists, Eq, TotallyDefiniteQuaternionAlgebra.HeckeOperator.T, IsDedekindDomain.HeightOneSpectrum.adicCompletion, ValuationSubring, IsDedekindDomain.HeightOneSpectrum.adicCompletionIntegers, Ne and 2 more
47 instances, coercions and auxiliary constants left out.
```
noncomputable def T (𝒮 : U₁Data F R p)
    (v : HeightOneSpectrum (𝓞 F)) (hvS : v ∉ 𝒮.S) (hvQ : v ∉ 𝒮.Q) : HeckeAlgebra D 𝒮 :=
…
```
Mentions: TotallyDefiniteQuaternionAlgebra.U₁Data, TotallyDefiniteQuaternionAlgebra.HeckeAlgebra
def TotallyDefiniteQuaternionAlgebra.HeckeAlgebra.U The Hecke operator Uᵥ,ₐ as an element of the Hecke algebra line 923 source
Source documentation
The Hecke operator Uᵥ,ₐ as an element of the Hecke algebra.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Field, NumberField, DivisionRing, Algebra, CommRing, IsQuaternionAlgebra.NumberField.WithRigidification, Nat, TotallyDefiniteQuaternionAlgebra.U₁Data, IsDedekindDomain.HeightOneSpectrum, NumberField.RingOfIntegers, Membership.mem, Finset, TotallyDefiniteQuaternionAlgebra.U₁Data.Q, MonoidWithZeroHom, Subtype, IsDedekindDomain.HeightOneSpectrum.adicCompletion, ValuationSubring, IsDedekindDomain.HeightOneSpectrum.adicCompletionIntegers, TotallyDefiniteQuaternionAlgebra.HeckeAlgebra
Proof uses: MonoidWithZeroHom.mk, ZeroHom.mk, dite, Eq, OfNat.ofNat, Classical.propDecidable, Not, Subtype.mk, Module.End, TotallyDefiniteQuaternionAlgebra.WeightTwoAutomorphicForm, Submodule, TotallyDefiniteQuaternionAlgebra.WeightTwoAutomorphicForm.LevelStruct.form, TotallyDefiniteQuaternionAlgebra.WeightTwoAutomorphicForm.LocalLevelStruct.toStruct, TotallyDefiniteQuaternionAlgebra.U₁, Subalgebra, Algebra.adjoin, Union.union, Set, Set.ofPred, Exists and 4 more
71 instances, coercions and auxiliary constants left out.

Tactic trace: 15 steps
Open to load the checked before-and-after goal states.
```
noncomputable def U (𝒮 : U₁Data F R p)
    (v : HeightOneSpectrum (𝓞 F)) (hv : v ∈ 𝒮.Q) :
    v.adicCompletionIntegers F →*₀ HeckeAlgebra D 𝒮 where
…
```
Mentions: TotallyDefiniteQuaternionAlgebra.U₁Data, TotallyDefiniteQuaternionAlgebra.HeckeAlgebra
lemma TotallyDefiniteQuaternionAlgebra.HeckeAlgebra.adjoin_T_U_eq_top line 944 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Field, NumberField, DivisionRing, Algebra, CommRing, IsQuaternionAlgebra.NumberField.WithRigidification, Nat, TotallyDefiniteQuaternionAlgebra.U₁Data, Eq, Subalgebra, TotallyDefiniteQuaternionAlgebra.HeckeAlgebra, Algebra.adjoin, Union.union, Set, Set.ofPred, Exists, IsDedekindDomain.HeightOneSpectrum, NumberField.RingOfIntegers, Not, Membership.mem and 13 more
Proof uses: Subalgebra.map_injective, Module.End, TotallyDefiniteQuaternionAlgebra.WeightTwoAutomorphicForm, Submodule, TotallyDefiniteQuaternionAlgebra.WeightTwoAutomorphicForm.LevelStruct.form, TotallyDefiniteQuaternionAlgebra.WeightTwoAutomorphicForm.LocalLevelStruct.toStruct, TotallyDefiniteQuaternionAlgebra.U₁, TotallyDefiniteQuaternionAlgebra.HeckeOperator.T, TotallyDefiniteQuaternionAlgebra.HeckeOperator.U, Subalgebra.val, Subtype.val_injective, LE.le.antisymm, Subalgebra.map, Subalgebra.map_mono, le_top, Eq.mpr, LE.le, AlgHom.range, id, congrArg and 22 more
134 instances, coercions and auxiliary constants left out.

Tactic trace: 9 steps
Open to load the checked before-and-after goal states.
instance TotallyDefiniteQuaternionAlgebra.HeckeAlgebra.(instance at line 960) line 960 source
lemma TotallyDefiniteQuaternionAlgebra.HeckeAlgebra.smul_formTensorScalar_aux line 969 source
lemma TotallyDefiniteQuaternionAlgebra.HeckeAlgebra.apply_eq_smul Note: This breaks the abstraction boundary that HeckeAlgebra is defined as a subtype under the hood line 980 source
Source documentation
Note: This breaks the abstraction boundary that HeckeAlgebra is defined as a subtype under the hood. This should only be used in the forward direction to remove the abuse.

extra axioms: knownin1980s what this means
Statement uses: Field, NumberField, DivisionRing, Algebra, CommRing, IsQuaternionAlgebra.NumberField.WithRigidification, Nat, IsQuaternionAlgebra, NumberField.IsTotallyReal, IsQuaternionAlgebra.IsTotallyDefinite, TotallyDefiniteQuaternionAlgebra.U₁Data, TotallyDefiniteQuaternionAlgebra.HeckeAlgebra, Subtype, TotallyDefiniteQuaternionAlgebra.WeightTwoAutomorphicForm, Membership.mem, Submodule, TotallyDefiniteQuaternionAlgebra.WeightTwoAutomorphicForm.LevelStruct.form, TotallyDefiniteQuaternionAlgebra.WeightTwoAutomorphicForm.LocalLevelStruct.toStruct, TotallyDefiniteQuaternionAlgebra.U₁, Eq and 22 more
Proof uses: Eq.mpr, LinearEquiv, TensorProduct, TotallyDefiniteQuaternionAlgebra.WeightTwoAutomorphicForm.LevelStruct.formTensorScalar, TensorProduct.tmul, eq_of_heq, HEq, Eq.refl, HEq.refl, Eq.symm, Subtype.ext, TotallyDefiniteQuaternionAlgebra.WeightTwoAutomorphicForm.ext, Matrix.GeneralLinearGroup, Fin, IsDedekindDomain.FiniteAdeleRing, id, of_eq_true, TotallyDefiniteQuaternionAlgebra.WeightTwoAutomorphicForm.LevelStruct.formCongr, TensorProduct.AlgebraTensorModule.rid, LinearMap and 21 more
171 instances, coercions and auxiliary constants left out.

Tactic trace: 9 steps
Open to load the checked before-and-after goal states.
```
lemma apply_eq_smul (𝒮 : U₁Data F R p)
    (T : HeckeAlgebra D 𝒮) (f : (U₁ 𝒮).toStruct.form D R) :
    T.1 f = T • f := by
…
```
Mentions: TotallyDefiniteQuaternionAlgebra.U₁Data, TotallyDefiniteQuaternionAlgebra.HeckeAlgebra.T, TotallyDefiniteQuaternionAlgebra.HeckeAlgebra, TotallyDefiniteQuaternionAlgebra.U₁
lemma TotallyDefiniteQuaternionAlgebra.HeckeAlgebra.smul_formTensorScalar line 993 source
extra axioms: knownin1980s what this means
Statement uses: Field, NumberField, DivisionRing, Algebra, CommRing, AddCommGroup, Module, IsQuaternionAlgebra.NumberField.WithRigidification, Nat, IsQuaternionAlgebra, NumberField.IsTotallyReal, IsQuaternionAlgebra.IsTotallyDefinite, TotallyDefiniteQuaternionAlgebra.U₁Data, TotallyDefiniteQuaternionAlgebra.HeckeAlgebra, Subtype, TotallyDefiniteQuaternionAlgebra.WeightTwoAutomorphicForm, Membership.mem, Submodule, TotallyDefiniteQuaternionAlgebra.WeightTwoAutomorphicForm.LevelStruct.form, TotallyDefiniteQuaternionAlgebra.WeightTwoAutomorphicForm.LocalLevelStruct.toStruct and 8 more
Proof uses: Eq.mpr, Module.End, Subalgebra, Algebra.adjoin, Union.union, Set, Set.ofPred, Exists, IsDedekindDomain.HeightOneSpectrum, NumberField.RingOfIntegers, Not, Finset, TotallyDefiniteQuaternionAlgebra.U₁Data.S, TotallyDefiniteQuaternionAlgebra.U₁Data.Q, TotallyDefiniteQuaternionAlgebra.HeckeOperator.T, IsDedekindDomain.HeightOneSpectrum.adicCompletion, ValuationSubring, IsDedekindDomain.HeightOneSpectrum.adicCompletionIntegers, Ne, OfNat.ofNat and 5 more
124 instances, coercions and auxiliary constants left out.

Tactic trace: 1 steps
Open to load the checked before-and-after goal states.
lemma TotallyDefiniteQuaternionAlgebra.HeckeAlgebra.T_smul_def line 999 source
extra axioms: knownin1980s what this means
Statement uses: Field, NumberField, DivisionRing, Algebra, CommRing, AddCommGroup, Module, IsQuaternionAlgebra.NumberField.WithRigidification, Nat, TotallyDefiniteQuaternionAlgebra.U₁Data, IsQuaternionAlgebra, NumberField.IsTotallyReal, IsQuaternionAlgebra.IsTotallyDefinite, IsDedekindDomain.HeightOneSpectrum, NumberField.RingOfIntegers, Not, Membership.mem, Finset, TotallyDefiniteQuaternionAlgebra.U₁Data.S, TotallyDefiniteQuaternionAlgebra.U₁Data.Q and 13 more
Proof uses: TensorProduct, LinearEquiv, TotallyDefiniteQuaternionAlgebra.WeightTwoAutomorphicForm.LevelStruct.formTensorScalar, Exists, LinearEquiv.surjective, TensorProduct.inductionOn, id, TensorProduct.tmul, Eq.mpr, TotallyDefiniteQuaternionAlgebra.WeightTwoAutomorphicForm.LocalLevelStruct.heckeOperator, Matrix.GeneralLinearGroup.diagonal, Fin, OfNat.ofNat, IsDedekindDomain.HeightOneSpectrum.adicCompletion, Matrix.vecCons, Units, IsDedekindDomain.HeightOneSpectrum.adicCompletionUniformizerUnit, Matrix.vecEmpty, LinearMap.comp, LinearMap and 25 more
147 instances, coercions and auxiliary constants left out.

Tactic trace: 7 steps
Open to load the checked before-and-after goal states.
lemma TotallyDefiniteQuaternionAlgebra.HeckeAlgebra.U_smul_def line 1012 source
extra axioms: knownin1980s what this means
Statement uses: Field, NumberField, DivisionRing, Algebra, CommRing, AddCommGroup, Module, IsQuaternionAlgebra.NumberField.WithRigidification, Nat, TotallyDefiniteQuaternionAlgebra.U₁Data, IsQuaternionAlgebra, NumberField.IsTotallyReal, IsQuaternionAlgebra.IsTotallyDefinite, IsDedekindDomain.HeightOneSpectrum, NumberField.RingOfIntegers, Membership.mem, Finset, TotallyDefiniteQuaternionAlgebra.U₁Data.Q, Subtype, IsDedekindDomain.HeightOneSpectrum.adicCompletion and 17 more
Proof uses: TensorProduct, LinearEquiv, TotallyDefiniteQuaternionAlgebra.WeightTwoAutomorphicForm.LevelStruct.formTensorScalar, Exists, LinearEquiv.surjective, TensorProduct.inductionOn, id, TensorProduct.tmul, Eq.mpr, TotallyDefiniteQuaternionAlgebra.WeightTwoAutomorphicForm.LocalLevelStruct.heckeOperator, Matrix.GeneralLinearGroup.diagonal, Fin, Matrix.vecCons, Units, Units.mk0, Matrix.vecEmpty, LinearMap.comp, LinearMap, TensorProduct.AlgebraTensorModule.lTensor, LinearEquiv.symm and 29 more
188 instances, coercions and auxiliary constants left out.

Tactic trace: 7 steps
Open to load the checked before-and-after goal states.
lemma TotallyDefiniteQuaternionAlgebra.HeckeAlgebra.formMap_smul line 1024 source
extra axioms: knownin1980s what this means
Statement uses: Field, NumberField, DivisionRing, Algebra, CommRing, AddCommGroup, Module, IsQuaternionAlgebra.NumberField.WithRigidification, Nat, IsQuaternionAlgebra, NumberField.IsTotallyReal, IsQuaternionAlgebra.IsTotallyDefinite, TotallyDefiniteQuaternionAlgebra.U₁Data, LinearMap, RingHom.id, TotallyDefiniteQuaternionAlgebra.HeckeAlgebra, Subtype, TotallyDefiniteQuaternionAlgebra.WeightTwoAutomorphicForm, Membership.mem, Submodule and 6 more
Proof uses: TensorProduct, LinearEquiv, TotallyDefiniteQuaternionAlgebra.WeightTwoAutomorphicForm.LevelStruct.formTensorScalar, Exists, LinearEquiv.surjective, TensorProduct.inductionOn, Eq.mpr, TensorProduct.tmul, id, congrArg, TotallyDefiniteQuaternionAlgebra.HeckeAlgebra.smul_formTensorScalar, eq_of_heq, HEq, Eq.refl, HEq.refl, Eq.symm, Subtype.ext, TotallyDefiniteQuaternionAlgebra.WeightTwoAutomorphicForm.ext, Matrix.GeneralLinearGroup, Fin and 19 more
111 instances, coercions and auxiliary constants left out.

Tactic trace: 43 steps
Open to load the checked before-and-after goal states.
instance TotallyDefiniteQuaternionAlgebra.HeckeAlgebra.(instance at line 1036) line 1036 source
instance TotallyDefiniteQuaternionAlgebra.HeckeAlgebra.(instance at line 1047) line 1047 source
instance TotallyDefiniteQuaternionAlgebra.HeckeAlgebra.(instance at line 1060) line 1060 source
instance TotallyDefiniteQuaternionAlgebra.HeckeAlgebra.(instance at line 1065) line 1065 source
instance TotallyDefiniteQuaternionAlgebra.HeckeAlgebra.(instance at line 1071) line 1071 source
instance TotallyDefiniteQuaternionAlgebra.HeckeAlgebra.(instance at line 1074) line 1074 source
instance TotallyDefiniteQuaternionAlgebra.HeckeAlgebra.(instance at line 1077) line 1077 source
def TotallyDefiniteQuaternionAlgebra.HeckeAlgebra.anemic line 1093 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Field, NumberField, DivisionRing, Algebra, CommRing, IsQuaternionAlgebra.NumberField.WithRigidification, Nat, TotallyDefiniteQuaternionAlgebra.U₁Data, Subalgebra, TotallyDefiniteQuaternionAlgebra.HeckeAlgebra
Proof uses: Algebra.adjoin, Set.ofPred, Exists, IsDedekindDomain.HeightOneSpectrum, NumberField.RingOfIntegers, Not, Membership.mem, Finset, TotallyDefiniteQuaternionAlgebra.U₁Data.S, TotallyDefiniteQuaternionAlgebra.U₁Data.Q, Eq, TotallyDefiniteQuaternionAlgebra.HeckeAlgebra.T
19 instances, coercions and auxiliary constants left out.