Glossary

Defined in this project

Every definition in this project, under its own name: the first paragraph of its description, or how it is declared when it has none. Theorems are not listed here: they are results, not words.

A · B · C · D · E · F · G · H · I · J · K · L · M · N · O · P · Q · R · S · T · U · V · W · X · Y · Z · Other

A

action def

The action of the Lie algebra of left-invariant derivations on a Lie group G on smooth real-valued functions on G, viewed as a Lie algebra homomorphism. · AutomorphicForm.GLn.action

actionTensorC def

Complexification of AutomorphicForm.GLn.action: the Lie action of the complexified Lie algebra on the complexification of smooth real functions on G. · AutomorphicForm.GLn.actionTensorC

actionTensorCAlg def

Extension of AutomorphicForm.GLn.actionTensorC to the universal enveloping algebra of the complexified Lie algebra. · AutomorphicForm.GLn.actionTensorCAlg

actionTensorCAlg' def

Variant of actionTensorCAlg whose codomain is the ℂ-linear endomorphisms of the complexified function space. · AutomorphicForm.GLn.actionTensorCAlg'

actionTensorCAlg'2 def

Restriction of actionTensorCAlg' to the centre of the universal enveloping algebra. · AutomorphicForm.GLn.actionTensorCAlg'2

actionTensorCAlg'3 def

The ℂ-algebra map from the centre of the universal enveloping algebra to the endomorphism algebra of complex-valued smooth functions on G. · AutomorphicForm.GLn.actionTensorCAlg'3

add def

addition z+w of complex numbers · Hurwitz.add

add def

Addition on the space of automorphic forms over a totally definite quaternion algebra. · TotallyDefiniteQuaternionAlgebra.WeightTwoAutomorphicForm.add

addMonoidHom def

The Hecke operator T_g = [UgV] : A^V → A^U packaged as an additive monoid homomorphism. · AbstractHeckeOperator.heckeOperator.addMonoidHom

adicArithFrob def

def Field.AbsoluteGaloisGroup.adicArithFrob : Γ Kᵥ · Field.AbsoluteGaloisGroup.adicArithFrob

adicCompletionIntegersRingHom def

The restriction of adicCompletionSemialgHom to a map 𝓞_v → 𝓞_w. · IsDedekindDomain.HeightOneSpectrum.Extension.adicCompletionIntegersRingHom

adicCompletionIntegersUniformizer def

A uniformiser associated to v in the integers of the completion Kᵥ. · IsDedekindDomain.HeightOneSpectrum.adicCompletionIntegersUniformizer

adicCompletionSemialgHom def

If w of L divides v of K, underSemialgHom v w pf is the canonical map Kᵥ → L_w lying above K → L. Here we actually use the type synonyms WithVal K and WithVal L. · IsDedekindDomain.HeightOneSpectrum.Extension.adicCompletionSemialgHom

adicCompletionUniformizer def

A uniformiser associated to v in the completion Kᵥ. · IsDedekindDomain.HeightOneSpectrum.adicCompletionUniformizer

adicCompletionUniformizerUnit def

A uniformiser associated to v in the units of the completion Kᵥ. · IsDedekindDomain.HeightOneSpectrum.adicCompletionUniformizerUnit

adjoinRange def

The k-subalgebra A ⊆ End_k(V) generated by the image of ρ. · Slop.OddRep.adjoinRange

adjoinRange abbrev

Compatibility alias for Slop.OddRep.adjoinRange. · Slop.OddRepOrig.adjoinRange

adjoinSingletonEquivAdjoinRootMinpoly' def

def AlgEquiv.adjoinSingletonEquivAdjoinRootMinpoly' (F : Type*) {R : Type*} [Field F] [Ring R] [Algebra F R] (x : R) : Algebra.adjoin F ({x} : Set R) ≃ₐ[F] AdjoinRoot (minpoly F x) · AlgEquiv.adjoinSingletonEquivAdjoinRootMinpoly'

Alg def

The universal enveloping algebra over ℂ of the complexified Lie algebra of G. · AutomorphicForm.GLn.Alg

AlgebraTypeCardLT def

The type of all finite R-algebras of cardinality less than N, presented as a sigma type over Fin N. · AlgebraTypeCardLT

algEquiv def

adicCompletion.equiv as a K-algebra isomorphism onto the underlying completion. · IsDedekindDomain.HeightOneSpectrum.adicCompletion.algEquiv

algEquiv def

Given a rigidification of D, D ⊗ 𝔸ᶠ is isomorphic to M₂(𝔸ᶠ). · IsQuaternionAlgebra.NumberField.WithRigidification.algEquiv

algEquiv def

The isomorphism of residue fields for a residue algebra. · IsResidueAlgebra.algEquiv

algEquivMixedSpace def

If K is a number field, this is the ℝ-linear iso between ∏_v|∞ K_v and ℝ^r × ℂ^s, with the usual notation. · NumberField.InfiniteAdeleRing.algEquivMixedSpace

algHomEquivOfIsDomain def

def Pi.algHomEquivOfIsDomain {ι R₀ S : Type*} {R : ι → Type*} [Finite ι] [DecidableEq ι] [CommSemiring R₀] [∀ i, Ring (R i)] [∀ i, Algebra R₀ (R i)] [Ring S] [Algebra R₀ S] [IsDomain S] : ((Π i, R i) … · Pi.algHomEquivOfIsDomain

anemic def

def anemic : Subalgebra R (HeckeAlgebra D 𝒮) · TotallyDefiniteQuaternionAlgebra.HeckeAlgebra.anemic

annihilator def

The annihilator of an element a : M in the module of R-linear maps M →ₗ[R] N: those f with f a = 0. · AutomorphicForm.GLn.annihilator

arithFrobAt' def

def _root_.arithFrobAt' [Q.IsPrime] [Finite (R ⧸ Q.under R)] : G · IsArithFrobAt._root_.arithFrobAt'

autGroup def

The automorphism group of a Weierstrass curve E over a field: the admissible changes of variables fixing E, i.e. the stabiliser of E under the action of VariableChange K. · WeierstrassCurve.autGroup

autGroupMulEquiv def

Aut(E) ≅ ℤ/2 for j(E) ∉ {0, 1728}. The automorphism group of E is {±1}, so it is isomorphic to Multiplicative (ZMod 2): it has exactly two elements — 1 and negVariableChange E … · WeierstrassCurve.autGroupMulEquiv

AutomorphicFormForGLnOverQ structure

Automorphic forms for GL_n/Q with weight ρ. · AutomorphicForm.GLn.AutomorphicFormForGLnOverQ

a₄ def

The coefficient a₄ = -5s₃ = -5q - 45q² - ⋯ of the Tate curve y² + xy = x³ + a₄x + a₆. · TateCurve.a₄

a₄Formal def

The formal a₄-series a₄(q) = -5s₃(q) ∈ ℤ⟦q⟧ of the Tate curve: the integral version of WeierstrassCurve.tateA₄. · TateCurve.a₄Formal

a₆ def

The coefficient a₆ = -(5s₃ + 7s₅)/12 = -q - 23q² - ⋯ of the Tate curve y² + xy = x³ + a₄x + a₆. (Division by 12 is implemented as scalar multiplication by 12⁻¹ ∈ ℚ(u); note that 5σ₃(n) + 7σ₅(n) is always divisible by 12, so … · TateCurve.a₆

a₆Formal def

The formal a₆-series a₆(q) = -(5s₃(q) + 7s₅(q))/12 ∈ ℤ⟦q⟧ of the Tate curve: the integral version of WeierstrassCurve.tateA₆. The division is exact, since 12 ∣ 5d³ + 7d⁵ for every d. · TateCurve.a₆Formal

B

B1 def

B1 is the statement of FLT. · FLT.Bosses.B1

B2 def

B2 is the statement that FLT is true for primes p ≥ 5. · FLT.Bosses.B2

B3 def

B3 is the statement that there is no Frey Package. A Frey package is 4 integers a,b,c,p satisfying a^p+b^p=c^p and some other conditions (for example p is prime and at least 5, a,b,c are pairwise coprime etc). These conditions guarantee … · FLT.Bosses.B3

B4 def

B4 is the statement that if E is the Frey curve attached to a Frey package (a,b,c,p), then E[p] is a reducible Galois representation. · FLT.Bosses.B4

baseChange def

Base change of a Lie algebra homomorphism f : L →ₗ⁅R⁆ L' along a commutative algebra A over R. · AutomorphicForm.GLn.LieHom.baseChange

baseChange def

Base change of a Lie module homomorphism f : M →ₗ⁅R,L⁆ N along a commutative algebra A over R. · AutomorphicForm.GLn.LieModuleHom.baseChange

baseChange def

def FramedGaloisRep.baseChange [IsTopologicalRing B] (ρ : FramedGaloisRep K A n) (f : A →+* B) (hf : Continuous f) : FramedGaloisRep K B n · FramedGaloisRep.baseChange

baseChange def

def GaloisRep.baseChange [IsTopologicalRing B] [Algebra A B] [ContinuousSMul A B] [Module.Finite A M] [Module.Free A M] (ρ : GaloisRep K A M) : GaloisRep K B (B ⊗[A] M) · GaloisRep.baseChange

baseChange abbrev

The canonical ring homomorphism L ⊗_K K_v → ∏_{w|v} L_w as an L-algebra map. · IsDedekindDomain.HeightOneSpectrum.adicCompletion.baseChange

baseChange def

The canonical map from the adeles of K to the adeles of L · NumberField.AdeleRing.baseChange

baseChange def

The canonical map from the infinite adeles of K to the infinite adeles of L · NumberField.InfiniteAdeleRing.baseChange

baseChange abbrev

The L-algebra map L ⊗[K] v.Completion to the product of all completions of L lying above v, induced by piExtension. · NumberField.InfinitePlace.Completion.baseChange

baseChange def

Base change of a representation along a commutative R-algebra R': extends ρ : G → GL(V) to R' ⊗[R] V. · Representation.baseChange

baseChange def

Base change of a representation along a field extension l/k: G acts on l ⊗[k] V by 1 ⊗ ρ(g). · Slop.OddRep.baseChange

baseChange abbrev

Compatibility alias for Slop.OddRep.baseChange. · Slop.OddRepOrig.baseChange

baseChange def

Base extension of an R-algebra map B → C to an A-linear map B ⊗ A → C ⊗ A. Available in the TensorProduct.RightActions scope. · TensorProduct.RightActions.AlgebraMap.baseChange

baseChange def

The continuous A-linear map (A a topological ring, tensor products have the module topology) A ⊗[R] M ≃ A ⊗[R] N associated to an abstract R-linear isomorphism M ≃ N. · TensorProduct.RightActions.ContinuousLinearEquiv.baseChange

baseChange abbrev

Base extension of an R-linear iso V → W to an A-linear iso V ⊗ A → W ⊗ A. Available in the TensorProduct.RightActions scope. · TensorProduct.RightActions.LinearEquiv.baseChange

baseChange abbrev

Base extension of an R-linear map V → W to an A-linear map V ⊗ A → W ⊗ A. Available in the TensorProduct.RightActions scope. · TensorProduct.RightActions.LinearMap.baseChange

baseChangeAdeleAlgEquiv def

The 𝔸_K^∞-algebra isomorphism L ⊗_K 𝔸_K^∞ ≅ 𝔸_L^∞. · IsDedekindDomain.FiniteAdeleRing.baseChangeAdeleAlgEquiv

baseChangeAdeleAlgHom def

The canonical 𝔸 K-algebra homomorphism (L ⊗_K 𝔸 K) → 𝔸 L induced by the maps from L and 𝔸 K into 𝔸 L. · NumberField.AdeleRing.baseChangeAdeleAlgHom

baseChangeAdeleContinuousAlgEquiv def

The continuous 𝔸_K^∞-algebra isomorphism L ⊗_K 𝔸_K^∞ ≅ 𝔸_L^∞ · IsDedekindDomain.FiniteAdeleRing.baseChangeAdeleContinuousAlgEquiv

baseChangeAdeleEquiv def

The canonical 𝔸_K-algebra homeomorphism from L ⊗_K 𝔸_K to 𝔸_L induced by the base change map 𝔸_K → 𝔸_L. · NumberField.AdeleRing.baseChangeAdeleEquiv

baseChangeAlgAdeleEquiv def

The canonical 𝔸_K-algebra isomorphism from L ⊗_K 𝔸_K to 𝔸_L induced by the base change map 𝔸_K → 𝔸_L. · NumberField.AdeleRing.baseChangeAlgAdeleEquiv

baseChangeAlgEquiv def

The L-algebra isomorphism L ⊗_K 𝔸_K^∞ ≅ 𝔸_L^∞. · IsDedekindDomain.FiniteAdeleRing.baseChangeAlgEquiv

baseChangeAlgEquiv def

The L-algebra isomorphism L ⊗[K] K_v ≅ ∏_{w|v} L_w. · IsDedekindDomain.HeightOneSpectrum.adicCompletion.baseChangeAlgEquiv

baseChangeAlgEquiv def

The L-algebra isomorphism L ⊗[K] 𝔸_K = 𝔸_L. · NumberField.AdeleRing.baseChangeAlgEquiv

baseChangeAlgEquiv def

The $L$-algebra isomorphism $L\otimes_K K_{\infty} \cong L_{\infty}$. · NumberField.InfiniteAdeleRing.baseChangeAlgEquiv

baseChangeContinuousAlgEquiv def

The continuous L-algebra isomorphism L ⊗_K 𝔸_K^∞ ≅ 𝔸_L^∞ · IsDedekindDomain.FiniteAdeleRing.baseChangeContinuousAlgEquiv

baseChangeContinuousAlgEquiv def

The continuous L-algebra isomorphism L ⊗[K] K_v ≅ ∏_{w|v} L_w. · IsDedekindDomain.HeightOneSpectrum.adicCompletion.baseChangeContinuousAlgEquiv

baseChangeEquiv def

The L-algebra homeomorphism L ⊗[K] 𝔸 K = 𝔸 L. · NumberField.AdeleRing.baseChangeEquiv

baseChangeEquiv def

def baseChangeEquiv [Algebra K∞ L∞] [Pi.FiberwiseSMul (fun a => a.comap (algebraMap K L)) Completion Completion] : L ⊗[K] K∞ ≃A[L] L∞ · NumberField.InfiniteAdeleRing.baseChangeEquiv

baseChangeEquiv def

The L-algebra homeomorphism between L ⊗[K] v.Completion and the product of all completions of L lying above v. · NumberField.InfinitePlace.Completion.baseChangeEquiv

baseChangeEquiv' def

The canonical L-algebra isomorphism from L ⊗_K 𝔸_K to 𝔸_L induced by the K-algebra base change map 𝔸_K → 𝔸_L. · NumberField.AdeleRing.baseChangeEquiv'

baseChangeLinearEquiv def

The L-linear isomorphism L ⊗ A_K^∞ ≅ A_L^∞ given by composing the previous four maps. · IsDedekindDomain.FiniteAdeleRing.baseChangeLinearEquiv

baseChangeOfAlgebraMap def

def SemialgHom.baseChangeOfAlgebraMap [Semiring A] [Algebra R S] [Algebra R A] [Semiring B] [Algebra S B] (ψ : A →ₛₐ[algebraMap R S] B) : S ⊗[R] A →ₐ[S] B · SemialgHom.baseChangeOfAlgebraMap

baseChangeRight abbrev

The canonical ring homomorphism L ⊗_K K_v → ∏_{w|v} L_w as an K_v-linear map. · IsDedekindDomain.HeightOneSpectrum.adicCompletion.baseChangeRight

baseChangeRight abbrev

The v.Completion-algebra map L ⊗[K] v.Completion to the product of all completions of L lying above v, induced by piExtension. · NumberField.InfinitePlace.Completion.baseChangeRight

baseChangeRightOfAlgebraMap def

def SemialgHom.baseChangeRightOfAlgebraMap [Algebra R S] [CommSemiring A] [Algebra R A] [CommSemiring B] [Algebra S B] (ψ : A →ₛₐ[algebraMap R S] B) : letI · SemialgHom.baseChangeRightOfAlgebraMap

basis def

Right action version of Algebra.TensorProduct.basis -- base extension of a basis over a tensor product. · TensorProduct.RightActions.Algebra.TensorProduct.basis

bdryKer def

The coboundary map into the kernel model: the differential corestricted to the cocycles of the next degree. In degree 0 the junk value d 0 0 = 0 makes its range ⊥, matching the convention of HomologicalComplex.homologyIsCokernel. · ContinuousCohomology.bdryKer

bGlobal abbrev

bGlobal is FiniteAdeleRing (𝓞 K) K-basis for FiniteAdeleRing (𝓞 K) K ⊗[K] B. · bGlobal

bLocal abbrev

bLocal is v.adicCompletion K-basis for v.adicCompletion K ⊗[K] B. · bLocal

bound def

def Module.UniformlyBoundedRank.bound : ℕ · Module.UniformlyBoundedRank.bound

bracketBilin def

The action of a Lie R-algebra on a Lie R-module, as an R-bilinear map. · IsDedekindDomain.bracketBilin

C

C def

An auxiliary set C used in the proof of Fukisaki's lemma. Defined as T⁻¹X × X. · NumberField.AdeleRing.DivisionAlgebra.Aux.C

changeScalars def

Produces an S'-linear algebra isomorphism from an S-linear algebra isomorphism f : A ≃ₐ[S] B which also has scalars S'. · AlgEquiv.changeScalars

changeScalars def

Produces an S'-linear algebra map from an S-linear algebra map f : A →ₐ[S] B which also has scalars S'. · AlgHom.changeScalars

changeScalars def

Produces an S'-linear continuous algebra isomorphism from a continuous algebra isomorphism f : A ≃A[S] B which also has scalars S'. · ContinuousAlgEquiv.changeScalars

changeScalars def

Given a linear isomorphism f : A ≃ₗ[S] B which also satisfies f (s' • a) = s' • f a for s : S', with both S and S' sharing a common base ring R, then f.changeScalars R S' returns f viewed as an S'-algebra isomorphism. · LinearEquiv.changeScalars

changeScalars def

Given a linear map f : A →ₗ[S] B which also satisfies f (s' • a) = s' • f a for s : S', with both S and S' sharing a common base ring R, then f.changeScalars R S' returns f viewed as an S'-algebra homomorphism. · LinearMap.changeScalars

char def

def GL2.localIwahoriLevel.char (v : HeightOneSpectrum (𝓞 F)) : GL2.localIwahoriLevel v →* (IsLocalRing.ResidueField (v.adicCompletionIntegers F))ˣ · IsDedekindDomain.GL2.localIwahoriLevel.char

charFrob def

def GaloisRep.charFrob (ρ : GaloisRep K A M) : Polynomial A · GaloisRep.charFrob

chooseBasisPiScalarRight def

The canonical continuous R-linear isomorphism M ⊗[R] V ≃ (ι → M) where V is a finite free R-module with basis indexed by ι, M is a commutative R-algebra, and M ⊗[R] V has the M-module topology. · ContinuousLinearEquiv.chooseBasisPiScalarRight

chooseBasisPiScalarRight def

The M-algebra isomorphism M ⊗ V ≃ₗ[M] (ι → M) coming from the canonical ι-indexed basis of a finite free R-module V. · LinearEquiv.chooseBasisPiScalarRight

chooseBasisPiScalarRight' def

The canonical continuous M-linear isomorphism M ⊗[R] V ≃ (ι → M) where V is a finite free R-module with basis indexed by ι, M is a commutative R-algebra, and M ⊗[R] V has the M-module topology. · ContinuousLinearEquiv.chooseBasisPiScalarRight'

classification def

The classification of automorphic forms for GL₀/ℚ: they are in bijection with ℂ. · AutomorphicForm.GL0.classification

classification def

The classification of automorphic forms for GL₀/ℚ of weight ρ: they are in bijection with ℂ. · AutomorphicForm.GLn.classification

coeHomₜ def

Units.val as a ContinuousMonoidHom. · Units.coeHomₜ

cohomologyIsoQuot def

Continuous cohomology identified with the quotient of the kernel model of the cocycles by the coboundaries, carrying the quotient topology. · ContinuousCohomology.cohomologyIsoQuot

cokerCongr def

Cokernels of morphisms identified under an isomorphism of the targets are isomorphic. · TopModuleCat.cokerCongr

cokerDesc def

The universal property of the concrete quotient TopModuleCat.coker: a morphism killing the range descends to the quotient. · TopModuleCat.cokerDesc

cokerDescBilinear def

Descend a bilinear pairing, bundled as a morphism into the internal hom, along cokernel projections in all three slots. · TopModuleCat.cokerDescBilinear

cokerDescCLM def

Descend a continuous linear map along cokernel projections on both sides. · TopModuleCat.cokerDescCLM

colength def

The length of R ⧸ I as a natural number (junk value 0 when the length is infinite; see colength_coe for the case of an ideal of definition). · DimensionTheorem.colength

ComapFiberwiseSMul class

Utility class which specialises RestrictedProduct.FiberwiseSMul to the case of finite adele rings. · IsDedekindDomain.FiniteAdeleRing.ComapFiberwiseSMul

comapHom abbrev

The map from v.Completion to w.Completion whenever the infinite place w of L lies above the infinite place v of K. · NumberField.InfinitePlace.Completion.comapHom

comm def

The A-algebra isomorphism A ⊗ B = B ⊗ A, available in the TensorProduct.RightActions scope. · TensorProduct.RightActions.Algebra.TensorProduct.comm

comm def

The A-module isomorphism A ⊗ M = M ⊗ A, available in the TensorProduct.RightActions scope. · TensorProduct.RightActions.Module.TensorProduct.comm

commContinuousAddMonoidHom def

B ⊗ 𝔸_K^f ≃ 𝔸_K^f ⊗ B as topological additive groups. · FiniteAdeleRing.TensorProduct.commContinuousAddMonoidHom

commLinearMap def

B ⊗ 𝔸_K^f ≃ 𝔸_K^f ⊗ B as 𝔸_K^f-modules. · FiniteAdeleRing.TensorProduct.commLinearMap

comp def

The composition of two semi-algebra maps. · SemialgHom.comp

compAlgHom def

The composition (B →ₛₐ[ψ] C) ∘ (A →ₐ[S] B) → A →ₛₐ[ψ] C` of a semi-algebra map with an algebra map to give a semi-algebra map. · SemialgHom.compAlgHom

compLeftAlgHom def

Composing MulActionHom on the left as an AlgHom. · MulActionHom.compLeftAlgHom

completionIdeal abbrev

The maximal ideal of the integers of the completion of v. · IsDedekindDomain.HeightOneSpectrum.completionIdeal

Component abbrev

The k-th component of the patching algebra: the ultraproduct of the rings R i / m(R i)^k along the ultrafilter F. · PatchingAlgebra.Component

Component abbrev

The α-th component of the patching module associated to (i) a family of modules M i over a commutative ring R, (ii) an ultrafilter on the index set for the M i and (iii) an ideal of R. This is the ultraproduct of M i / α • M i … · PatchingModule.Component

componentMap abbrev

The transition ring homomorphism between components: Component j → Component k for k ≤ j, induced by R i / m^j → R i / m^k. · PatchingAlgebra.componentMap

componentMap abbrev

The transition linear map between components for ideals α ≤ β: Component α → Component β. · PatchingModule.componentMap

componentMapModule abbrev

Functoriality of PatchingModule.Component in the family of modules: a family of linear maps f i : M i →ₗ[R] N i induces a map between the α-th components. · PatchingModule.componentMapModule

componentMapRingHom abbrev

Functoriality on components: a family of local ring homomorphisms f i : R i →+* R' i induces a ring homomorphism between the k-th components of the two patching systems. · PatchingAlgebra.componentMapRingHom

conj def

def GaloisRep.conj (ρ : GaloisRep K A M) (e : M ≃ₗ[A] N) : GaloisRep K A N · GaloisRep.conj

conjClassElements def

The finset of non-identity elements of G' lying in some conjugate of the subgroup H. · Dickson.conjClassElements

conjEquiv def

The multiplicative isomorphism between G and its image k₀ G k₀⁻¹ under conjugation by k₀. · Dickson.conjEquiv

conjEquiv def

def GaloisRep.conjEquiv (e : M ≃ₗ[A] N) : GaloisRep K A M ≃ GaloisRep K A N · GaloisRep.conjEquiv

conjNonidentity def

The finset of non-identity elements of the conjugate subgroup H.map (MulAut.conj g). · Dickson.conjNonidentity

constEquiv def

def PatchingAlgebra.constEquiv (R : Type*) [CommRing R] [IsLocalRing R] [TopologicalSpace R] [IsTopologicalRing R] [CompactSpace R] [IsNoetherianRing R] [IsAdicTopology R] : R ≃ₐ[R] PatchingAlgebra … · PatchingAlgebra.constEquiv

constEquiv def

def PatchingModule.constEquiv [IsLocalRing R] [T2Space R] [IsNoetherianRing R] (M) [AddCommGroup M] [Module R M] [Module.Finite R M] : M ≃ₗ[R] PatchingModule R (fun _ ↦ M) F · PatchingModule.constEquiv

continuousAlgEquivMixedSpace def

If K is a number field, this is the continuous ℝ-linear iso between ∏_v|∞ K_v and ℝ^r × ℂ^s, with the usual notation. · NumberField.InfiniteAdeleRing.continuousAlgEquivMixedSpace

continuousAlgEquivOfAlgEquiv def

An algebra isomorphism between two topological algebras over R with the R-module topology is automatically an algebra homeomorphism. · IsModuleTopology.continuousAlgEquivOfAlgEquiv

continuousAlgEquivOfIsBiscalar def

An algebra isomorphism e : A →ₐ[S] B which also has scalars S', with A and B both having the S'-module topology, is automatically continuous. · IsModuleTopology.continuousAlgEquivOfIsBiscalar

continuousLinearEquiv def

Given a linear isomorphism between two topological modules with the module topology, upgrades it to a continuous linear isomorphism using the fact that linear maps between modules with the module topology are automatically continuous. · IsModuleTopology.continuousLinearEquiv

continuousLinearEquiv def

A continuous R-linear equivalence e : G ≃L[R] H sending the submodule G' ≤ G onto H' ≤ H descends to a continuous R-linear equivalence G ⧸ G' ≃L[R] H ⧸ H'. · Submodule.Quotient.continuousLinearEquiv

continuousLinearEquivOfIsBiscalar def

A linear equivalence e : A ≃ₗ[S] B which also has scalars S', with A and B both having the S'-module topology, is automatically continuous. · IsModuleTopology.continuousLinearEquivOfIsBiscalar

continuousMulEquiv def

def QuotientGroup.continuousMulEquiv {G H : Type*} [Group G] (N : Subgroup G) [N.Normal] [Group H] (M : Subgroup H) [M.Normal] [TopologicalSpace G] [TopologicalSpace H] (e : G ≃ₜ* H) (h : … · QuotientGroup.continuousMulEquiv

ContinuousSemialgHom structure

A SemialgHom (i.e., ψ such that ψ (r • a) = φ r • ψ a for some φ : R →+* S) that is also continuous. · ContinuousSemialgHom

ContinuousSemialgHomClass class

ContinuousSemialgHomClass F φ A B states that F is the type of continuous semi-algebra maps from A to B with respect to φ. · ContinuousSemialgHomClass

ContinuousSMulDiscrete class

ContinuousSMulDiscrete G M means that the action G × M → M is continuous when M is given the discrete topology (See continuousSMulDiscrete_iff). · ContinuousSMulDiscrete

cup def

The cup product on continuous group cohomology induced by an intertwining map f : ρ1 →ⁱL linHom ρ2 ρ3: descend the kernel-model cup product cupKerHom to the quotients by the coboundaries on all three slots, and transport along … · ContinuousCohomology.cup

cupCochain abbrev

The cup product pairing on homogeneous cochains, obtained from the cup product pairing cupComplex on the coinduced resolutions by taking invariants. · ContinuousCohomology.cupCochain

cupCocycles def

The cup product pairing on the cycles of the homogeneous cochain complexes, transporting cupKerHom along the identification cyclesIsoKer of the cycles with the kernel models. · ContinuousCohomology.cupCocycles

cupCocyclesAux abbrev

The cup product of two cocycles, as a cocycle: by the Leibniz rule cup_d_comm, the differential of σ ∪ τ vanishes when d σ = 0 and d τ = 0. · ContinuousCohomology.cupCocyclesAux

cupComplex def

The degree-(m, n) cup product pairing on the coinduced resolutions, as a morphism from the m-th level to the internal hom of the n-th and r-th levels, obtained from cupPair by reindexing along r = m + n. · ContRepresentation.cupComplex

cupKerCLM def

For a fixed cocycle σ, cupping with σ restricts to a continuous linear map between the kernels of the differentials on homogeneous cochains. · ContinuousCohomology.cupKerCLM

cupKerHom def

The cup product bundled as a morphism from the kernel of the differential into the internal hom of the kernel models. · ContinuousCohomology.cupKerHom

cupPair def

The degree-(m, n) cup product pairing on the coinduced resolutions, defined by iterating cupSucc starting from cupZeroSucc, bundled with the joint continuity of its underlying pairing (which is needed to keep iterating). · ContRepresentation.cupPair

cupSucc def

The inductive step of the cup product: an intertwining map F : π₁ →ⁱL linHom π₂ π₃ whose underlying pairing (v, w) ↦ F v w is jointly continuous induces an intertwining map π₁.coind₁ →ⁱL linHom π₂ π₃.coind₁ sending σ and τ to `x … · ContRepresentation.cupSucc

cupZeroSucc def

The degree-(0, n) cup product pairing: an intertwining map f : ρ1 →ⁱL linHom ρ2 ρ3 pairs a degree-0 cochain σ with a degree-n cochain τ by (σ ∪ τ) g = resolutionCLM (f (σ g)) n (τ g), intertwining the coinduced … · ContRepresentation.cupZeroSucc

cupZeroSuccAux def

The pairing resolutionX (of ρ2) n × M1 → resolutionX (of ρ3) n underlying the cup product, sending (y, v) to resolutionCLM (f v) n y, as a continuous map. The joint continuity of the uncurried pairing of f propagates through the … · ContRepresentation.cupZeroSuccAux

cyclesIsoKer def

The cycles of a complex of topological modules, identified with the kernel of the differential carrying the subspace topology. · HomologicalComplex.cyclesIsoKer

CyclicPartitionConfig structure

Combinatorial data for one class in a cyclic partition: f conjugate cyclic subgroups, each of order d. · Dickson.CyclicPartitionConfig

CyclotomicCharacterAux def

The cyclotomic character · CyclotomicCharacterAux

CyclotomicCharacterZHat def

The Zhat-adic cyclotomic character. · CyclotomicCharacterZHat

c₄Formal def

The formal c₄-series c₄(q) = 1 + 240s₃(q) = 1 + 240q + 2160q² + ⋯ ∈ ℤ⟦q⟧ of the Tate curve: the q-expansion of the Eisenstein series E₄. · TateCurve.c₄Formal

D

deformationFunctor def

def deformationFunctor (ρ : (repnFunctor n G 𝓞).obj .residueField) : Subfunctor (repnQuotFunctor n G 𝓞) · Deformation.deformationFunctor

depth def

Not sure if we should use IsRegular or IsWeaklyRegular. They agree for nontrivial finite modules over local rings. Using IsWeaklyRegular gives depth R 0 = ∞, which is the right one according to stacks. · Module.depth

det def

def GaloisRep.det (ρ : GaloisRep K A M) : Γ K →ₜ* A · GaloisRep.det

detConditionFunctor def

The subfunctor of representations with det = εₗ. · Deformation.detConditionFunctor

Df abbrev

Df is notation for D ⊗ 𝔸_K^∞ · NumberField.AdeleRing.DivisionAlgebra.Aux.Df

Dfx abbrev

Dfx is notation for (D ⊗ 𝔸_K^∞)ˣ. · NumberField.AdeleRing.DivisionAlgebra.Aux.Dfx

Dfx abbrev

Dfx is an abbreviation for $(D\otimes_F\mathbb{A}_F^\infty)^\times.$ · TotallyDefiniteQuaternionAlgebra.Dfx

diag def

The matrix element diag[α, 1]. · TotallyDefiniteQuaternionAlgebra.WeightTwoAutomorphicForm.HeckeOperator.Local.GL2.diag

diagonal def

The invertible diagonal matrix associated to a vector of units (the diagonal entries). · Matrix.GeneralLinearGroup.diagonal

dilationGL def

The dilation x ↦ c x (for c ≠ 0) as the element !![c, 0; 0, 1] of GL₂(K p). · Dickson.dilationGL

dilationHomOfFix def

The group homomorphism from a finite subgroup H of PGLOf (K p) fixing infinity to (K p)ˣ, sending each element to its dilation parameter. · Dickson.dilationHomOfFix

dilationParam def

For g fixing ∞, the nonzero scalar c such that conjugation by g sends the translation by x to the translation by c x. · Dickson.dilationParam

dilationPGL def

The dilation x ↦ c x (for c ≠ 0) as an element of PGLOf (K p) = PGL₂(𝔽̄_p). · Dickson.dilationPGL

Dinf abbrev

Dinf is notation for D ⊗ 𝔸_K^∞ · NumberField.AdeleRing.DivisionAlgebra.Aux.Dinf

DinfTensorPiEquivPiTensor def

tensorPiEquivPiTensor applied to Dinf, as a continuous ℝ-linear equiv. · NumberField.InfiniteAdeleRing.DinfTensorPiEquivPiTensor

DinfTensorPiEquivPiTensorAux def

tensorPiEquivPiTensor applied to Dinf, as a ℝ-linear equiv. · NumberField.InfiniteAdeleRing.DinfTensorPiEquivPiTensorAux

DinfTensorPiEquivPiTensorMulEquiv def

tensorPiEquivPiTensor applied to Dinf, as a mul equiv. · NumberField.InfiniteAdeleRing.DinfTensorPiEquivPiTensorMulEquiv

Dinfx abbrev

Dinfx is notation for (D ⊗ 𝔸_K^∞)ˣ · NumberField.AdeleRing.DivisionAlgebra.Aux.Dinfx

directSumPiEquivPiSum def

⨁ⱼ(∏ᵢ Nᵢⱼ) ≅ ∏ᵢ(⨁ⱼNᵢⱼ) if j ranges over a finite index set and i over an arbitrary index set. This variant is for R-modules and gives an R-module isomorphism. · directSumPiEquivPiSum

DIso abbrev

The K-algebra equivalence of D and K^n. · NumberField.AdeleRing.DivisionAlgebra.Aux.DIso

D𝔸Iso abbrev

The 𝔸_K-algebra equivalence of D_𝔸 and 𝔸_K^d. · NumberField.AdeleRing.DivisionAlgebra.Aux.D𝔸Iso

D𝔸IsoTop abbrev

The topological 𝔸_K-linear equivalence D_𝔸 ≃ 𝔸_K^d. · NumberField.AdeleRing.DivisionAlgebra.Aux.D𝔸IsoTop

D𝔸ProdRight abbrev

The K-algebra isomorphism D_𝔸 ≃ D_∞ × D_f -- adelic D is infinite adele D times finite adele D. · NumberField.AdeleRing.DivisionAlgebra.Aux.D𝔸ProdRight

D𝔸ProdRight' abbrev

The 𝔸_K linear map D_𝔸 ≃ D_∞ × D_f. · NumberField.AdeleRing.DivisionAlgebra.Aux.D𝔸ProdRight'

D𝔸ProdRight'' abbrev

The continuous additive isomorphism D_𝔸 ≃ D_∞ × D_f. · NumberField.AdeleRing.DivisionAlgebra.Aux.D𝔸ProdRight''

D𝔸ProdRightUnits abbrev

The equivalence of the units of D_𝔸 and the product of the units of (D ⊗ 𝔸_K^f) and (D ⊗ 𝔸_K^∞). · NumberField.AdeleRing.DivisionAlgebra.Aux.D𝔸ProdRightUnits

E

E def

An auxiliary set E used in the proof of Fujisaki's lemma. · NumberField.AdeleRing.DivisionAlgebra.Aux.E

e def

If φ : Kᵥ ⊗[K] B ≃ Kᵥ ⊗[K] B is continuous and additive then f φ is the associated continuous additive isomorphism Kᵥ^n ≃ Kᵥ^n coming from the "canonical" K-basis of B. · FiniteAdeleRing.Aux.e

e def

e z = exp (2πiz). We will take u = e z and q = e τ. · TateCurve.Blueprint.e

e def

A nonarchimedean analogue 0! + 1! + 2! + ⋯ of e = 1/0! + 1/1! + 1/2! + ⋯. It is defined as the function whose value at ZMod n is the sum of i! for 0 ≤ i < n. · ZHat.e

E12 def

The elementary matrix e₁₂ a = !![1, a; 0, 1] as an element of SL₂(F). · SL2.E12

E21 def

The elementary matrix e₂₁ b = !![1, 0; b, 1] as an element of SL₂(F). · SL2.E21

Efamily def

An auxiliary definition of an increasing family of compact subsets of D_𝔸, defined as the product of a compact neighbourhood of 0 at the finite places and a compact neighbourhood of 0, scaled by r, at the infinite places. · NumberField.AdeleRing.DivisionAlgebra.Aux.Efamily

Eigenform def

Type parametrising eigen spaces of the anemic hecke algebra on S(U, ℂ). · TotallyDefiniteQuaternionAlgebra.HeckeAlgebra.Eigenform

eigenspace def

The eigenspace parametrised by an Eigenform. · TotallyDefiniteQuaternionAlgebra.HeckeAlgebra.Eigenform.eigenspace

eigenvalue abbrev

The Tₚ-eigenvalue of an eigenform. · TotallyDefiniteQuaternionAlgebra.HeckeAlgebra.Eigenform.eigenvalue

endSelf def

End_A(A) ≃ A. · Module.endSelf

Equiv def

Any two direct limits of the same directed system are isomorphic. · IsDirectLimit.Equiv

equivAlgHom def

The eigenforms corresponds exactly to maps from 𝕋 to ℂ. · TotallyDefiniteQuaternionAlgebra.HeckeAlgebra.Eigenform.equivAlgHom

equivChar def

1-dimensional framed galois reps are equivalent to (continuous) characters. · FramedGaloisRep.equivChar

equivComponent def

def PatchingModule.equivComponent (α : Ideal R) (hα : IsOpen (X · PatchingModule.equivComponent

equivFunHomeo def

def Module.Basis.equivFunHomeo (K R : Type*) [Field K] [Ring R] [Module K R] [Module.Finite K R] [TopologicalSpace K] [TopologicalSpace R] [IsTopologicalRing R] [IsTopologicalRing K] … · IsModuleTopology.Module.Basis.equivFunHomeo

equivOfAlgebra def

def AlgebraTypeCardLT.equivOfAlgebra (N : ℕ) {M : Type*} [Ring M] [Algebra R M] [Finite M] (hM : Nat.card M < N) : M ≃ₐ[R] Fin ((AlgebraTypeCardLT.ofAlgebra R N M hM).1) · AlgebraTypeCardLT.equivOfAlgebra

equivOfAlgebra def

def TopologicalAlgebraTypeCardLT.equivOfAlgebra (N : ℕ) (M : Type*) [Ring M] [Algebra R M] [TopologicalSpace M] [T2Space M] [ContinuousSMul R M] [Finite M] (hM : Nat.card M < N) : M ≃ₐ[R] Fin … · TopologicalAlgebraTypeCardLT.equivOfAlgebra

equivOfEq def

Transport of the affine point group along an equality of Weierstrass curves. · WeierstrassCurve.Affine.Point.equivOfEq

equivOfModule def

def ModuleTypeCardLT.equivOfModule (N : ℕ) {M : Type*} [AddCommGroup M] [Module R M] [Finite M] (hM : Nat.card M < N) : M ≃ₗ[R] Fin ((ModuleTypeCardLT.ofModule R N M hM).1) · ModuleTypeCardLT.equivOfModule

equivOfModule def

def TopologicalModuleTypeCardLT.equivOfModule (N : ℕ) (M : Type*) [AddCommGroup M] [Module R M] [TopologicalSpace M] [T2Space M] [ContinuousSMul R M] [Finite M] (hM : Nat.card M < N) : M ≃L[R] Fin … · TopologicalModuleTypeCardLT.equivOfModule

equivPi def

Choice of an R-linear isomorphism M ≃ R^(finrank R M) for a finite free module M over a ring R with the strong rank condition. · Module.Finite.equivPi

equivPrimesOver def

The primes of B extending v are precisely the primes of B lying over v.asIdeal. · IsDedekindDomain.HeightOneSpectrum.Extension.equivPrimesOver

equivVariableChange def

The group isomorphism (C • W).Point ≃+ W.Point induced by the admissible change of variables (x, y) ↦ (u²x + r, u³y + u²sx + t), with inverse coming from C⁻¹. · WeierstrassCurve.Affine.Point.equivVariableChange

etaleSubalgebraEquiv def

Given a representative for each orbit of X under G := Gal(L/K), and for each x : X a choice of σ that sends x to the representative, we obtain a K-algebra isomorphism between G-equivariant homs from X and the product of … · MulAction.etaleSubalgebraEquiv

evalAlgebraMap def

The K-algebra map 𝔸_K^f → Kᵥ from the finite adele ring of K to a completion. · IsDedekindDomain.FiniteAdeleRing.evalAlgebraMap

evalAlgHom def

Evaluating a MulActionHom is an AlgHom, bundled as a MulActionHom. · MulActionHom.evalAlgHom

evalAt def

Evaluation of a rational function in ℚ(u) at a complex number, with junk value 0 at the (finitely many) poles. · TateCurve.Blueprint.evalAt

evalAtHom def

For transcendental u, evaluation at u is a ring homomorphism ℚ(u) →+* ℂ (there are no poles to produce junk values). · TateCurve.Blueprint.evalAtHom

evalContinuousAddMonoidHom def

The continuous additive projection from a restricted product of topological additive groups to a factor. · RestrictedProduct.evalContinuousAddMonoidHom

evalContinuousAlgebraMap def

The continuous K-algebra map 𝔸_K^f → Kᵥ from the finite adele ring of K to a completion. · IsDedekindDomain.FiniteAdeleRing.evalContinuousAlgebraMap

evalInt def

The evaluation ∑ₙ Fₙqⁿ ∈ k of an integral power series F ∈ ℤ⟦X⟧ at a point q of a topological field (junk value if the series does not converge). · TateCurve.evalInt

evalMulActionHom def

Evaluating a AlgHom is an MulActionHom, bundled as a AlgHom. · AlgHom.evalMulActionHom

eventuallyProd def

Given a filter F on the index set and a family of submodules N i ≤ M i, the submodule of Π i, M i consisting of those tuples v for which v i ∈ N i holds F-eventually. · eventuallyProd

ExistsListTransvecMulDiagonalMulListTransvec def

The claim that a matrix is a product of transvections, a diagonal matrix, and more transvections. Always true if the base ring is a field. · Matrix.Pivot.ExistsListTransvecMulDiagonalMulListTransvec

extendScalars def

Promote an A-algebra equivalence C ≃ₐ[A] D to a B-algebra equivalence, where B is an intermediate algebra A → B → C and D inherits a B-algebra structure via the restricted map. · AlgEquiv.extendScalars

Extension def

If B is an A-algebra and v : HeightOneSpectrum A is a nonzero prime, then v.Extension B is the subtype of HeightOneSpeectrum B consisting of valuations of B which restrict to v. · IsDedekindDomain.HeightOneSpectrum.Extension

Extension abbrev

If L / K are fields and v is an infinite place of K, then we say an infinite place w of L extends v if w can be constructed from a complex embedding L →+* ℂ whose restriction to K is an associated complex embedding `K … · NumberField.InfinitePlace.Extension

F

f def

If φ : 𝔸_K^f ⊗[K] B ≃ 𝔸_K^f ⊗[K] B is continuous and 𝔸_K^f-linear then f φ is the associated continuous linear isomorphism (𝔸_K^f)^n ≃ (𝔸_K^f)^n coming from the "canonical" K-basis of B. · FiniteAdeleRing.Aux.f

fdRep def

The finite-dimensional ℂ-representation of O(n) associated to a preweight w. · AutomorphicForm.GLn.preweight.fdRep

FiberwiseSMul class

A class encoding the product scalar multiplication of ∀ b : β, R b on ∀ a : α, M a that is determined by the fibers of a supplied function f : α → β on indices. Specifically, if f a = b, then (r • x) a = r b • x a for any `r : ∀ … · Pi.FiberwiseSMul

FiberwiseSMul class

A class encoding the product scalar multiplication of Πʳ b, [R b, A b]_[𝓕] on Πʳ a, [M a, B a]_[𝓖] that is determined by the fibers of a supplied function f : α → β on indices. Specifically, if f a = b, then (r • x) a = r b • x a … · RestrictedProduct.FiberwiseSMul

finiteAdeleIncl def

def GL2.finiteAdeleIncl (v : HeightOneSpectrum (𝓞 F)) : GL₂(v.adicCompletion F) →* GL₂(𝔸ᶠ[F]) · IsDedekindDomain.FiniteAdeleRing.GL2.finiteAdeleIncl

finiteEquivPi abbrev

Base change of Module.Finite.equivPi to an R-algebra N: the equivalence N ⊗[R] M ≃ₗ[N] Fin (finrank R M) → N. · TensorProduct.AlgebraTensorModule.finiteEquivPi

finsuppLeftTensorPiEquivPiTensor def

If B is finite then tensoring by the free module with basis B commutes with arbitrary products. · finsuppLeftTensorPiEquivPiTensor

fintype def

There are only finitely many nonzero primes of B above a nonzero prime of A. · IsDedekindDomain.HeightOneSpectrum.Extension.fintype

FixedPoints def

If M acts on A then FixedPoints M A is the type of elements of A which are fixed elementwise by all of M. · AddAction.FixedPoints

FixedPoints def

If M acts on A then FixedPoints M A is the type of elements of A which are fixed elementwise by all of M. · MulAction.FixedPoints

fixedPoints def

The set of fixed points of the action of g : PGLOf (K p) on the projective line ℙ¹(K p). · Dickson.fixedPoints

flatFunctor def

The subfunctor of flat lifts. This probably only makes sense when 𝓞 is v-adic. · Deformation.flatFunctor

flatten def

The canonical map from a restricted product of products over fibres of a map on indexing sets to the restricted product over the original indexing set. · RestrictedProduct.flatten

flattenEquiv def

The canonical bijection from a restricted product of products over fibres of a map on indexing sets to the restricted product over the original indexing set. · RestrictedProduct.flattenEquiv

flattenEquiv' def

The equivalence given by flatten when both restricted products are over the cofinite filter. · RestrictedProduct.flattenEquiv'

flattenHomeomorph def

The canonical homeomorphism from a restricted product of products over fibres of a map on indexing sets to the restricted product over the original indexing set. · RestrictedProduct.flattenHomeomorph

flattenHomeomorph' def

The homeomorphism given by flatten when both restricted products are over the cofinite filter and there's a topology on the factors. · RestrictedProduct.flattenHomeomorph'

form def

The subspace of modular forms of a given level. · TotallyDefiniteQuaternionAlgebra.WeightTwoAutomorphicForm.LevelStruct.form

formCongr def

Mapping automorphic forms of a fixed level along a linear equiv. · TotallyDefiniteQuaternionAlgebra.WeightTwoAutomorphicForm.LevelStruct.formCongr

formEquiv def

If U is sufficiently small, S(U, χ) is isomorphic to the finite free module with basis Dˣ＼GL₂(𝔸ᶠ[F])／U. · TotallyDefiniteQuaternionAlgebra.WeightTwoAutomorphicForm.LevelStruct.formEquiv

formEquivOfSection def

Given a section to the projection Dˣ＼GL₂(𝔸ᶠ[F])／U → GL₂(𝔸ᶠ[F]), S(U, χ) is isomorphic to the finite free module with basis Dˣ＼GL₂(𝔸ᶠ[F])／U. · TotallyDefiniteQuaternionAlgebra.WeightTwoAutomorphicForm.LevelStruct.formEquivOfSection

formMap def

Mapping automorphic forms of a fixed level along a linear map. · TotallyDefiniteQuaternionAlgebra.WeightTwoAutomorphicForm.LevelStruct.formMap

formMapₗ def

formMap as a linear map. · TotallyDefiniteQuaternionAlgebra.WeightTwoAutomorphicForm.LevelStruct.formMapₗ

formSubmodule abbrev

Should not be used directly. · TotallyDefiniteQuaternionAlgebra.WeightTwoAutomorphicForm.LevelStruct.formSubmodule

formTensor def

If U is sufficiently small, then M ⊗ S(U, N) = S(U, M ⊗ N). · TotallyDefiniteQuaternionAlgebra.WeightTwoAutomorphicForm.LevelStruct.formTensor

formTensorScalar def

If U is sufficiently small, then M ⊗ S(U, R) = S(U, M). · TotallyDefiniteQuaternionAlgebra.WeightTwoAutomorphicForm.LevelStruct.formTensorScalar

FqInK def

The subfield 𝔽_{p^m} sitting inside K p = 𝔽̄_p, i.e. the set of x with x ^ (p ^ m) = x. · Dickson.FqInK

frame def

def GaloisRep.frame (ρ : GaloisRep K A M) (b : Module.Basis n A M) : FramedGaloisRep K A n · GaloisRep.frame

FramedGaloisRep abbrev

A framed galois rep is a galois rep with a distinguished basis. We implement it by via a galois rep on Aⁿ. · FramedGaloisRep

freeModuleTensorPiEquiv def

The isomorphism M ⊗ ∏ᵢ Nᵢ ≅ (B →₀ R) ⊗ ∏ᵢ Nᵢ, where M is assumed free and B is the basis of M given by Lean's global axiom-of-choice operator. This is an auxiliary definition. · freeModuleTensorPiEquiv

freyCurve def

The elliptic curve over ℚ associated to a Frey package. The conditions imposed upon a Frey package guarantee that the running hypotheses in Section 4.1 of [Serre] all hold. We put the curve into the form where the equation is semistable … · FreyPackage.freyCurve

freyCurveInt def

The Weierstrass curve over ℤ associated to a Frey package. The conditions imposed upon a Frey package guarantee that the running hypotheses in Section 4.1 of [Serre] all hold. We put the curve into the form where the equation is … · FreyPackage.freyCurveInt

FreyPackage structure

A Frey Package is a 4-tuple (a,b,c,p) of integers satisfying $a^p+b^p=c^p$ and some other inequalities and congruences. These facts guarantee that all of the all the results in section 4.1 of Serre's paper [serre] apply to the … · FreyPackage

fromQuaternion def

Rounds a quaternion to a nearby Hurwitz integer; serves as a left inverse to toQuaternion. · Hurwitz.fromQuaternion

fromSelf def

The structure map of a proartinian local algebra as a morphism in the category. · Deformation.ProartinianCat.fromSelf

fundamentalDomain def

The fundamental domain ℤ^ x [0,1) for 𝔸_ℚ ⧸ ℚ. · Rat.AdeleRing.fundamentalDomain

G

g def

If ψ : (𝔸_K^f)^n ≃ (𝔸_K^f)^n is continuous and 𝔸_K^f-linear then g φ is the associated continuous additive isomorphism Πʳ[Kᵥ^n, 𝓞ᵥ^n] → Πʳ[Kᵥ^n,𝓞ᵥ^n]. · FiniteAdeleRing.Aux.g

galoisFieldRingHom def

A ring embedding GaloisField p m →+* K p of 𝔽_{p^m} into 𝔽̄_p, with image FqInK p m. · Dickson.galoisFieldRingHom

GaloisRep def

GaloisRep K A M are the A-linear galois reps of a field K on the A-module M. · GaloisRep

galoisRep def

The continuous Galois representation associated to an elliptic curve over a field. · WeierstrassCurve.galoisRep

GaloisRepFamily def

GaloisRepFamily K E d is an (unrelated) collection of d-dimensional p-adic Galois representations of the absolute Galois group of the field K, parametrised by field maps from the number field E into the algebraic closure of ℚ_p as p … · GaloisRepFamily

GL def

Functoriality of GLₘ: a ring homomorphism A →+* B induces a group homomorphism GLₘ(A) →* GLₘ(B) by applying it entrywise. · AutomorphicForm.GLn._root_.RingHom.GL

GL def

def FramedGaloisRep.GL : FramedGaloisRep K A n ≃ (Γ K →ₜ* GL n A) · FramedGaloisRep.GL

glActionProjectiveLine def

The natural GL₂(K p)-action on the projective line ℙ¹(K p). · Dickson.glActionProjectiveLine

glMapOfBasis def

A representation ρ : G → GL(V) of G on a finite free R-module V together with a basis 𝓑 of V gives rise to a group homomorphism G → GL_ι(R) via the matrix of ρ g in the basis 𝓑. · Representation.glMapOfBasis

groupSMul def

The adelic group action on the space of automorphic forms over a totally definite quaternion algebra. · TotallyDefiniteQuaternionAlgebra.WeightTwoAutomorphicForm.groupSMul

growthDeg def

The growth degree d(R) of the Hilbert–Samuel function: the least d such that ℓ(R ⧸ 𝔪ⁿ) = O(nᵈ). · DimensionTheorem.growthDeg

GrowthLE def

f : ℕ → ℕ grows at most like n ^ d. We use (n + 1) ^ d to avoid degenerate behavior at n = 0. · DimensionTheorem.GrowthLE

H

haarMeasure def

Given a locally compact topological ring R such that Rˣ → R is an open embedding. If dx is an additive haar measure on R, then dx/δ(x) is a multiplicative haar measure on Rˣ, where δ is the Haar character. · MeasureTheory.Units.haarMeasure

haarQuot def

The haar measure on GL₂(𝔸ᶠ[F]) that gives Π GL₂(𝒪ᵥ) measure one. · TotallyDefiniteQuaternionAlgebra.WeightTwoAutomorphicForm.haarQuot

HasCyclicPartition def

HasCyclicPartition G configs states that the finite group G is covered by cyclic subgroups (intersecting pairwise trivially) whose orders and conjugate counts match configs. · Dickson.HasCyclicPartition

HasFlatProlongationAt def

A galois rep ρ : Γ K → Aut_A(M) has a flat prolongation at v if M (when viewed as a Γ Kᵥ) module is isomorphic to the geometric points of a finite etale hopf algebra over Kᵥ, and there exists an finite flat hopf algebra over 𝒪ᵥ … · GaloisRep.HasFlatProlongationAt

HeckeAlgebra def

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 … · TotallyDefiniteQuaternionAlgebra.HeckeAlgebra

heckeOperator def

The Hecke operator T_g = [UgV] : A^V → A^U as an R-linear map, where R is any ring acting on A and commuting with the G-action. · AbstractHeckeOperator.heckeOperator

heckeOperator def

def LocalLevelStruct.heckeOperator (v : HeightOneSpectrum (𝓞 F)) (hv : ℒ.χ v = 1) (g : GL₂(v.adicCompletion F)) : Module.End R (ℒ.toStruct.form D M) · TotallyDefiniteQuaternionAlgebra.WeightTwoAutomorphicForm.LocalLevelStruct.heckeOperator

heckeOperatorL abbrev

abbrev LocalLevelStruct.heckeOperatorL (v : HeightOneSpectrum (𝓞 F)) (hv : ℒ.χ v = 1) (g : GL₂(v.adicCompletion F)) [SMulCommClass R S M] : Module.End S (ℒ.toStruct.form D M) · TotallyDefiniteQuaternionAlgebra.WeightTwoAutomorphicForm.LocalLevelStruct.heckeOperatorL

heightOneSpectrum def

The bijection HeightOneSpectrum A ≃ HeightOneSpectrum B induced by a ring isomorphism between A and B. · RingEquiv.heightOneSpectrum

heightOneSpectrumComap def

Pulling back elements of HeightOneSpectrum along a ring isomorphism. · RingEquiv.heightOneSpectrumComap

hilbertSamuel def

The Hilbert–Samuel function of a local ring: n ↦ ℓ(R ⧸ 𝔪ⁿ). · DimensionTheorem.hilbertSamuel

Hom structure

The type of morphisms in ProartinianCat 𝓞. · Deformation.ProartinianCat.Hom

homEquivProdFixedPoints def

Given a representative for each orbit of X under G, and for each x : X a choice of σ that sends x to the representative, we obtain a bijection between G-equivariant homs from X and the product of Stab(x)-fixed points over … · MulAction.homEquivProdFixedPoints

homOfBilinear def

Bundle a bilinear pairing with jointly continuous uncurried form into a morphism to the internal hom. Stating this for abstract topological modules keeps all instance searches on abstract carriers. · TopModuleCat.homOfBilinear

homologyIsoCoker def

The homology of a complex of topological modules, identified with the quotient of the cycles by the boundaries, carrying the quotient topology. · HomologicalComplex.homologyIsoCoker

Hurwitz structure

Hurwitz integers in the quaternions. ℤ-Basis 1, ω=(-1+i+j+k)/2, i and ωi=(-1-i+j-k)/2. · Hurwitz

HurwitzHat def

The base change of the Hurwitz quaternions to ZHat. · HurwitzHat

HurwitzRat def

The quaternion algebra ℚ + ℚi + ℚj + ℚk. · HurwitzRat

HurwitzRatHat def

The "profinite Hurwitz quaternions" over the finite adeles of ℚ; a free rank 4 module generated by 1, i, j, and (1+i+j+k)/2. · HurwitzRatHat

I

idealQuotientEquiv def

Bijection between ideals of R / I and ideals of R containing I, via comap/map along the quotient map. · Ideal.idealQuotientEquiv

iHom abbrev

The internal hom of two topological representations: the topological representation on the space of continuous linear maps A →L[k] B, with G acting by conjugation. · TopRep.iHom

incl abbrev

The inclusion Dˣ → D_𝔸ˣ as a group homomorphism. · NumberField.AdeleRing.DivisionAlgebra.Aux.incl

incl def

The natural ring homomorphism from the product ∏ i, R i into PatchingAlgebra R F. · PatchingAlgebra.incl

incl def

The natural (ι → R)-linear map ∏ i, M i → PatchingModule R M F. · PatchingModule.incl

incl def

def incl : ℒ.US v →* ℒ.toStruct.U · TotallyDefiniteQuaternionAlgebra.WeightTwoAutomorphicForm.LocalLevelStruct.incl

inclD𝔸quot abbrev

The obvious map Dˣ \ D_𝔸^(1) to Dˣ \ (Dfx K D). · NumberField.AdeleRing.DivisionAlgebra.Aux.inclD𝔸quot

inclKn𝔸Kn abbrev

The inclusion of K^n into 𝔸^n. · NumberField.AdeleRing.DivisionAlgebra.Aux.inclKn𝔸Kn

includeLeftSubgroup def

The additive subgroup D of D_𝔸. · NumberField.AdeleRing.DivisionAlgebra.Aux.includeLeftSubgroup

inclusionLinearMap def

A linear map version of RestrictedProduct.inclusion : if 𝓕 ≤ 𝓖 then there's a linear map Πʳ i, [R i, C i]_[𝓖] →ₗ[A] Πʳ i, [R i, C i]_[𝓕] where the R i are A-modules and the C i are submodules. · RestrictedProduct.inclusionLinearMap

incl₁ abbrev

The inclusion Dˣ → (D ⊗ 𝔸_K^∞)ˣ as a group homomorphism. · NumberField.AdeleRing.DivisionAlgebra.Aux.incl₁

incl₂ def

The inclusion of ringHaarCharKer D_𝔸 into the product space D_𝔸 × D_𝔸ᵐᵒᵖ. · NumberField.AdeleRing.DivisionAlgebra.Aux.incl₂

indexSupport def

def indexSupport (u : Πʳ i, [G i, A i]) : Finset ι · RestrictedProduct.indexSupport

infinitePlaceCompletionContinuousAlgEquiv def

The continuous ℤ-algebra isomorphism between Rat.infinitePlace.Completion and ℝ. (We use continuous ℤ-algebra equivalences in place of continuous ring equivalences since we don't have the latter.) · Rat.infinitePlaceCompletionContinuousAlgEquiv

infinity def

The point ∞ = [1 : 0] of the projective line ℙ¹(K p). · Dickson.infinity

inner def

def LevelStruct.inner (ℒ : LevelStruct F R) (f g : ℒ.form D ℂ) : ℂ · TotallyDefiniteQuaternionAlgebra.WeightTwoAutomorphicForm.LevelStruct.inner

innerSummand def

The summand appearing in the Petersson inner product. · TotallyDefiniteQuaternionAlgebra.WeightTwoAutomorphicForm.LevelStruct.innerSummand

integerBallIdeal def

The open ball {x ∈ 𝒪[K] | v(x) < γ} of the ring of integers is an ideal: ultrametrically it is closed under addition, and multiplying by an integral element only shrinks the valuation. · ValuativeRel.integerBallIdeal

integerBaseChangeLinearEquiv def

The B-module isomorphism B ⊗[A] K_v ≅ ∏_{w|v} L_w. · IsDedekindDomain.HeightOneSpectrum.adicCompletion.integerBaseChangeLinearEquiv

integerMap def

The restriction of algebraMap k l to the rings of integers: 𝒪[k] is the subring (valuation k).integer of k, and valuation_algebraMap_le_one says algebraMap k l maps it into (valuation l).integer. · ValuativeExtension.integerMap

integers abbrev

The subring of ℂ generated by the eigenvalues of an eigenform. · TotallyDefiniteQuaternionAlgebra.HeckeAlgebra.Eigenform.integers

integerSubmodule def

𝓞_v as an A-submodule of K_v. · IsDedekindDomain.HeightOneSpectrum.adicCompletion.integerSubmodule

integralAdeles abbrev

The integral adele subring inside the finite adele ring. · IsDedekindDomain.FiniteAdeleRing.integralAdeles

IntegralClosure def

IntegralClosure R A is the integral closure of R in A as a type. We don't use the subring directly to avoid horrendous timeouts. · IntegralClosure

invariantsObjIHom abbrev

The comparison morphism from the invariants of the internal hom of two levels of the coinduced resolutions to the internal hom of the corresponding homogeneous cochains, restricting an equivariant continuous linear map to the invariants on … · ContRepresentation.invariantsObjIHom

InverseLimit def

InverseLimit G f is the Inverse Limit of the objects G i glued by functions f. · InverseLimit

InverseSystemHom def

InverseSystemHom G f maps states that a indexed family of maps : W →G i have image in the InverseLimit G f subset of the product · InverseLimit.InverseSystemHom

IsAbsolutelyIrreducible class

IsAbsolutelyIrreducible ρ states that a given Representation ρ over a field k is absolutely irreducible, meaning that all the possible base change extensions are irreducible. · Representation.IsAbsolutelyIrreducible

IsAbsolutelyIrreducible def

A representation is absolutely irreducible if it remains irreducible after base change to an algebraic closure of k. · Slop.OddRep.IsAbsolutelyIrreducible

IsAbsolutelyIrreducible abbrev

Compatibility alias for Slop.OddRep.IsAbsolutelyIrreducible. · Slop.OddRepOrig.IsAbsolutelyIrreducible

IsAdicTopology class

IsAdicTopology R says that the topology on the local topological ring R is the maximal ideal-adic one, that is, that a basis of neighbourhoods of 0 in R is given by powers of the maximal ideal of R. · IsLocalRing.IsAdicTopology

IsAutomorphicOfLevel def

A 2-dimensional Galois representation ρ of the absolute Galois group of a totally real field of even degree is said to be automorphic if it comes from a weight 2 trivial character square-free level automorphic form on a totally definite … · GaloisRep.IsAutomorphicOfLevel

IsBiscalar class

If f : A → B where A and B are both R- and S-modules, then IsBiscalar R S f asserts that f satisfies the linear scalar property for both R and S. I.e., - f (r • a) = r • f a - f (s • a) = s • f a for all r : R, `s : … · IsBiscalar

isCompatible def

A family ρ_λ of E_λ-adic Galois representations GaloisRepFamily K E d of the absolute Galois group of a number field K is compatible if there is a finite set S of finite places of K and, for each finite place v of K not … · GaloisRepFamily.isCompatible

IsConjugateLift class

If w is an infinite place of L lying above the infinite place v of K, then there are two possibilities: - w.embedding extends v.embedding. - conjugate w.embedding extends v.embedding. · NumberField.InfinitePlace.Extension.IsConjugateLift

IsConstantOn structure

The function f : GL_n(𝔸_f) × GL_n(ℝ) → ℂ is right-U-invariant in the finite-adelic variable, where U is an open compact subgroup. · AutomorphicForm.GLn.IsConstantOn

IsCoprime def

An element z of ℤ̂ is coprime to N if its image in ℤ/Nℤ is a unit. · QHat.IsCoprime

IsDirectLimit class

IsDirectLimit f g states that P is the direct limit of the system (M i, f i j hij). It requires: * surj: says every element of P comes from some M i via the canonical map g i. * inj: says that if two elements of (possibly … · IsDirectLimit

IsExtension abbrev

If L/K and f : K →+* ℂ, g : L →+* ℂ, then we say g is an extension of f if g restricted to K is f. · NumberField.ComplexEmbedding.IsExtension

isExtensionEquivSum def

The extensions g : L →+* ℂ of f : K →+* ℂ are the direct sum of the mixed and the unmixed extensions. · NumberField.ComplexEmbedding.isExtensionEquivSum

IsFinite abbrev

Actually true for all totally definite quaternion algebra D but the instance is provided elsewhere. · TotallyDefiniteQuaternionAlgebra.WeightTwoAutomorphicForm.LevelStruct.IsFinite

IsFlatAt class

A galois rep ρ : Γ K → Aut_A(M) is flat at v if A/I ⊗ M has a flat prolongation at v for all open ideals I. · GaloisRep.IsFlatAt

IsHardlyRamified structure

Let R be a compact Hausdorff local topological ring (for example any complete Noetherian local ring with the maximal ideal-adic topology) having finite residue field of characteristic ℓ > 2, and let ρ : Gal(Qbar/Q) → GL_2(R) be a … · GaloisRepresentation.IsHardlyRamified

isInitialSelf def

𝓞 is initial in ProartinianCat. · Deformation.ProartinianCat.isInitialSelf

IsIrreducible def

Irreducibility of a Galois representation over a field. · GaloisRep.IsIrreducible

IsLift class

If w is an infinite place of L lying above the infinite place v of K, then there are two possibilities: - w.embedding extends v.embedding. - conjugate w.embedding extends v.embedding. · NumberField.InfinitePlace.Extension.IsLift

IsLocalProartinianAlgebra class

A local proartinian algebra is a topological ring that is local and proartinian, and that the induced map on the residue fields is bijective. · Deformation.IsLocalProartinianAlgebra

IsMixedExtension abbrev

If L/K and f : K →+* ℂ, g : L →+* ℂ, then g is a mixed extension of f if the image of f is real while the image of g is complex. · NumberField.ComplexEmbedding.IsMixedExtension

IsPatchingSystem class

A family of modules M i is a patching system along the filter F if for every open ideal α ⊆ R, the annihilator Ann (M i) is F-eventually contained in α. · IsPatchingSystem

IsProartinian class

A topological ring is proartinian if it is linearly topologized, complete hausdorff, and all its discrete quotients are artinian. · IsProartinian

IsProdSMul class

A class encoding the product scalar multiplication of R × S on M × N of the format x • y = (x.1 • y.1, x.2 • y.2). Use this as an assumption instead of constructing the R × S action on M × N. · Prod.IsProdSMul

isProductAt def

A submonoid U of a resticted product of monoids is a product at i if U can be written as Uᵢ × Uⁱ with Uᵢ supported at the i'th component and Uⁱ supported away from i. · RestrictedProduct.SubmonoidClass.isProductAt

IsQuaternionAlgebra class

IsQuaternionAlgebra F D says that D is a quaternion algebra over the field F, i.e. a four-dimensional central simple F-algebra. · IsQuaternionAlgebra

IsResidueAlgebra class

IsResidueAlgebra 𝓞 indicates that A [Algebra 𝓞 A] has the same residue field as 𝓞. It is sufficient for the natural map 𝓞 to 𝓴 A to be surjective. The actual ≃+* between residue fields is given in IsResidueAlgebra.ringEquiv. · IsResidueAlgebra

IsSlowlyIncreasing structure

A function f : GL_n(ℝ) → ℂ is slowly increasing if there exist C, N such that ‖f M‖ ≤ C · s(M)^N for all M, where s is an auxiliary "size" function. · AutomorphicForm.GLn.IsSlowlyIncreasing

IsSmooth structure

A function on GL_n(𝔸_f) × GL_n(ℝ) is smooth if it is continuous, locally constant in the finite-adelic variable, and C^∞ in the archimedean variable. · AutomorphicForm.GLn.IsSmooth

IsSufficientlySmall class

A level struct is sufficiently small if the associated character has finite order coprime to [Δ_g : Fˣ] for all g. · TotallyDefiniteQuaternionAlgebra.WeightTwoAutomorphicForm.LevelStruct.IsSufficientlySmall

isTerminalResidueField def

def isTerminalResidueField : IsTerminal (residueField (𝓞 · Deformation.ProartinianCat.isTerminalResidueField

IsTopologicalModule class

IsTopologicalModule R M states that the topology in M makes scalar multiplication and addition into continuous maps. · IsTopologicalModule

IsTotallyDefinite class

A quaternion algebra D over a number field F is totally definite if D ⊗[F, v] ℝ is isomorphic to the Hamilton quaternions ℍ for all real places v (that is, for all ring homomorphisms F → ℝ). · IsQuaternionAlgebra.IsTotallyDefinite

IsTrivial def

A GLₙ-weight ρ is trivial if it is the one-dimensional trivial representation. · AutomorphicForm.GLn.Weight.IsTrivial

IsUnimodularGroup class

A group with topolgoy is a unimodular group if it is a locally compact topological group such that the modular character is trivial. (i.e. left haar measure = right haar measure) · IsUnimodularGroup

IsUnmixedExtension abbrev

If L/K and f : K →+* ℂ, g : L →+* ℂ, then g is an unmixed extension of f if g is an extension of f but is not a mixed extension. In other words, the image of f is real if and only if the image of g is real. · NumberField.ComplexEmbedding.IsUnmixedExtension

IsUnramified abbrev

A quaternion algebra over a number field is unramified if it is split at all finite places. This is implemented as the existence of a rigidification of D, that is, an isomorphism D ⊗[F] 𝔸_F^∞ = M₂(𝔸_F^∞). · IsQuaternionAlgebra.NumberField.IsUnramified

IsUnramifiedAt class

The class of galois reps unramified at v. · GaloisRep.IsUnramifiedAt

i₁ abbrev

The canonical inclusion ℚ → ℚ̂ = ℚ ⊗_ℤ ℤ̂ sending q to q ⊗ 1. · QHat.i₁

i₂ abbrev

The canonical inclusion ℤ̂ → ℚ̂ := ℚ ⊗_ℤ ℤ̂ sending z to 1 ⊗ z. · QHat.i₂

J

jInv def

The formal series 1/j = Δ(q)/c₄(q)³ = q - 744q² + 356652q³ - ⋯ ∈ ℤ⟦q⟧: the reciprocal of the j-invariant of the Tate curve. Since c₄³ has constant coefficient 1 its inverse PowerSeries.invOfUnit (c₄Formal ^ 3) 1 has integer … · TateCurve.jInv

jInvReverse def

The formal inverse j-series ψ = X + 744X² + 750420X³ + 872769632X⁴ + ⋯ ∈ ℤ⟦X⟧: the compositional inverse PowerSeries.substInv of jInv, so that formally q = ψ(1/j) (Silverman, ATAEC V.5.2 — the integrality of the coefficients is … · TateCurve.jInvReverse

j₁ abbrev

The inclusion from D=ℚ+ℚi+ℚj+ℚk to D ⊗ 𝔸, with 𝔸 the finite adeles of ℚ. · HurwitzRatHat.j₁

j₂ abbrev

The inclusion from the profinite Hurwitz quaternions to to 𝔸+𝔸i+𝔸j+𝔸k, with 𝔸 the finite adeles of ℚ. · HurwitzRatHat.j₂

K

K abbrev

An algebraic closure K p of the finite field 𝔽_p = ZMod p. · Dickson.K

ker abbrev

abbrev GaloisRep.ker (ρ : GaloisRep K A M) : Subgroup (Γ K) · GaloisRep.ker

kerLift' def

The induced map from the quotient by the kernel to the codomain. · QuotientGroup.kerLift'

L

leAddSubgroup def

The largest two-sided ideal contained in a given additive subgroup G ≤ α: those x ∈ α whose two-sided span is contained in G. · TwoSidedIdeal.leAddSubgroup

leftModuleTensorEquiv def

If A is a localization of R, tensoring two A-modules over A is the same as tensoring them over R. This is IsLocalization.moduleTensorEquiv as an M₁-linear equivalence (more generally an M'-linear equivalence where M₁ is an … · IsLocalization.leftModuleTensorEquiv

LevelStruct structure

The structure of an compact open U, and a continuous character on U that is trivial on 𝔸ᶠˣ. · TotallyDefiniteQuaternionAlgebra.WeightTwoAutomorphicForm.LevelStruct

levelStruct def

A somewhat arbitrarily chosen level of an automorphic form. · TotallyDefiniteQuaternionAlgebra.WeightTwoAutomorphicForm.LevelStruct._root_.TotallyDefiniteQuaternionAlgebra.WeightTwoAutomorphicForm.levelStruct

lift def

lift G f maps inverseSystemHom is the canonical function from W to the inverse limit of the G_j built by x ↦ Π maps_j x. For the monoid homomorphism see liftMonoidHom, for the ring homomorphism see liftRingHom, for the linear map … · InverseLimit.lift

lift def

Construct a map P₁ → P₂ from a direct limit by sending each element to its preimage in some component M i and applying g₂ i. Used to define morphisms out of direct limits. · IsDirectLimit.lift

lift def

The universal property of the direct limit: define a linear map from the direct limit by giving a compatible family of linear maps from the components. Each element of the limit is sent according to its representative in some component. · IsDirectLimit.Module.lift

lift def

A continuous family of ring homomorphisms f i : R∞ →+* R i lifts uniquely to a ring homomorphism R∞ →+* PatchingAlgebra R F. · PatchingAlgebra.lift

liftComponent def

A family of linear maps f i : M₀ →ₗ[R] M i lifts to a linear map M₀ / α • M₀ → Component α. · PatchingModule.liftComponent

liftFunctor def

def liftFunctor (ρ : (repnFunctor n G 𝓞).obj .residueField) : Subfunctor (repnFunctor n G 𝓞) · Deformation.liftFunctor

liftLinearMap def

LinearMap version of lift G f maps inverseSystemHom · InverseLimit.liftLinearMap

liftModIdeal def

Given a linear map f : M / I • M → N / I • N, produce the induced linear map between the corresponding quotients of M / J • M and N / J • N modulo I. · Submodule.liftModIdeal

liftModIdealEquiv def

Promote Submodule.liftModIdeal to a linear equivalence: a linear equivalence between R-modules M /IM and N/IN lifts to one between (M/JM)/I and (N/JM)/I. · Submodule.liftModIdealEquiv

liftMonoidHom def

MonoidHom version of lift G f maps inverseSystemHom · InverseLimit.liftMonoidHom

liftOfRightInverse' def

def liftOfRightInverse' (hf : Function.RightInverse f_inv f) : { g : G₁ →* G₃ // f.ker ≤ g.ker } ≃ (G₂ →* G₃) · MonoidHom.liftOfRightInverse'

liftOfRightInverseAux' def

Auxiliary definition used to define liftOfRightInverse · MonoidHom.liftOfRightInverseAux'

liftOfSurjective' abbrev

abbrev liftOfSurjective' (hf : Function.Surjective f) : { g : G₁ →* G₃ // f.ker ≤ g.ker } ≃ (G₂ →* G₃) · MonoidHom.liftOfSurjective'

liftQuotientₗ def

def Pi.liftQuotientₗ {ι R M : Type*} [CommRing R] [AddCommGroup M] [Module R M] [Finite ι] (f : (ι → R) →ₗ[R] M) (I : Ideal R) : (ι → R ⧸ I) →ₗ[R] M ⧸ (I • ⊤ : Submodule R M) · Pi.liftQuotientₗ

liftRingHom def

RingHom version of lift G f maps inverseSystemHom · InverseLimit.liftRingHom

linearEquiv def

Any two direct limits of the same directed system are isomorphic. · IsDirectLimit.Module.linearEquiv

linearEquiv' def

An equivalence e : α ≃ β gives a linear equivalence α ≃ₗ[R] β, where the R-module structure on α is the one obtained by transporting the R-module structure on β back along e. · Equiv.linearEquiv'

LinearEquivTensorProduct def

The canonical K-linear isomorphism L ≅ K ⊗ B. · IsDedekindDomain.LinearEquivTensorProduct

linearEquivTensorProductModule def

The canonical A-linear isomorphism L ⊗ M ≅ B ⊗ M for any K-module M. · IsDedekindDomain.linearEquivTensorProductModule

linearEquivTensorProductModuleLeft def

The canonical B-linear isomorphism L ⊗ M ≅ B ⊗ M for any K-module M. · IsDedekindDomain.linearEquivTensorProductModuleLeft

linearMap def

def IsPatchingSystem.linearMap (α : Ideal R) (i) : (Fin (rank R M F) → R ⧸ α) →ₗ[R] M i ⧸ (α • ⊤ : Submodule R (M i)) · IsPatchingSystem.linearMap

linearMap def

def Module.UniformlyBoundedRank.linearMap (i) : (Fin (rank R M F) → R) →ₗ[R] M i · Module.UniformlyBoundedRank.linearMap

linearMapComponent def

Components of a linear map. · RestrictedProduct.linearMapComponent

linHom def

The continuous representation of G on M2 →L[k] M3 by conjugation, g • φ = ρ3 g ∘L φ ∘L ρ2 g⁻¹, where M2 →L[k] M3 carries the topology induced from the compact-open topology on C(M2, M3). · ContRepresentation.linHom

linHom abbrev

The internal hom of two topological modules: the space of continuous linear maps A →L[k] B carrying the topology induced from the compact-open topology on C(A, B). · TopModuleCat.linHom

linHomMap def

Pre- and post-composition induce a morphism between the internal homs of topological modules. · TopModuleCat.linHomMap

localcomponent def

If φ : 𝔸_K^f ⊗[K] V → 𝔸_K^f ⊗[K] V is 𝔸_K^f-linear and p : HeightOneSpectrum (𝓞 K) then localcomponent R K V p φ : Kₚ ⊗[K] V →[K] Kₚ ⊗[K] V is the associated map φₚ defined as `Kₚ ⊗[K] V --(single)--> 𝔸_K^f ⊗ V --(φ)--> 𝔸_K^f ⊗ V … · IsDedekindDomain.FiniteAdeleRing.TensorProduct.localcomponent

localcomponentEquiv def

If φ : 𝔸_K^f ⊗[K] V → 𝔸_K^f ⊗[K] V is 𝔸_K^f-linear and p : HeightOneSpectrum (𝓞 K) then localcomponent R K V p φ : Kₚ ⊗[K] V →[K] Kₚ ⊗[K] V is the associated map φₚ defined as `Kₚ ⊗[K] V --(single)--> 𝔸_K^f ⊗ V --(φ)--> 𝔸_K^f ⊗ V … · IsDedekindDomain.FiniteAdeleRing.TensorProduct.localcomponentEquiv

localFullLevel def

GL₂(𝒪ᵥ) as a subgroup of GL₂(Fᵥ). · IsDedekindDomain.GL2.localFullLevel

localFullLevel def

M_2(O_v) as a subring of M_2(F_v). · IsDedekindDomain.M2.localFullLevel

localFullLevelEquiv def

def GL2.localFullLevelEquiv (v : HeightOneSpectrum (𝓞 F)) : GL2.localFullLevel v ≃* GL₂(v.adicCompletionIntegers F) · IsDedekindDomain.GL2.localFullLevelEquiv

localIdempotent def

localIdempotent R K p is the finite adele which is 1 at p and 0 elsewhere. · IsDedekindDomain.FiniteAdeleRing.localIdempotent

localInertiaGroup def

def localInertiaGroup : Subgroup (Γ Kᵥ) · localInertiaGroup

localIwahoriLevel def

local U₀(v), defined as a subgroup of GL₂(Fᵥ) given by matrices in GL₂(𝒪ᵥ) congruent to (* *;0 *) mod v. · IsDedekindDomain.GL2.localIwahoriLevel

LocalLevelStruct structure

A way to construct LevelStruct via a family of local level structs on finitely many finite places. · TotallyDefiniteQuaternionAlgebra.WeightTwoAutomorphicForm.LocalLevelStruct

localPTameLevel def

local U_1(v), defined as a subgroup of GL₂(Fᵥ) given by matrices in GL₂(𝒪ᵥ) congruent to (a *;0 b) mod v with p ∤ ord_{k(v)}(a/b). · IsDedekindDomain.GL2.localPTameLevel

localPTameLevelSubgroup def

def GL2.localPTameLevelSubgroup (v : HeightOneSpectrum (𝓞 F)) (p : ℕ) : Subgroup (v.adicCompletion F)ˣ · IsDedekindDomain.GL2.localPTameLevelSubgroup

localTameAbelianInertiaGroup def

def localTameAbelianInertiaGroup : Subgroup (Γ Kᵥ) · localTameAbelianInertiaGroup

localTameLevel def

local U_1(v), defined as a subgroup of GL₂(Fᵥ) given by matrices in GL₂(𝒪ᵥ) congruent to (a *;0 a) mod v. · IsDedekindDomain.GL2.localTameLevel

localUniformiser def

localUniformiser v is an adele which is 1 at all finite places except v, where it is a uniformiser. · IsDedekindDomain.FiniteAdeleRing.localUniformiser

localUniformiserUnit def

localUniformiser v is an idele which is 1 at all finite places except v, where it is a uniformiser. · IsDedekindDomain.FiniteAdeleRing.localUniformiserUnit

localUnit def

localUnit K α for α : (v.adicCompletion K)ˣ, is the finite idele which is α at v and 1 elsewhere. · IsDedekindDomain.FiniteAdeleRing.localUnit

lTensor def

The R-linear map φ : M ⊗_R ∏'_i [N i, L i]_[𝓕] → ∏'_i [M ⊗_R (N i), M ⊗_R (L i)]_[𝓕] given by φ (m ⊗ n) i = m ⊗ (n i). · RestrictedProduct.lTensor

lTensorEquiv def

The R-linear isomorphism given by lTensor when M is a finite flat R-module. · RestrictedProduct.lTensorEquiv

lTensorEquivLeft def

The M-linear isomorphism given by lTensor when M is a finite flat R-module. · RestrictedProduct.lTensorEquivLeft

lTensorLeft def

The M-linear map φ : M ⊗_R ∏'_i [N i, L i]_[𝓕] → ∏'_i [M ⊗_R (N i), M ⊗_R (L i)]_[𝓕] given by φ (m ⊗ n) i = m ⊗ (n i). · RestrictedProduct.lTensorLeft

lTensorPrincipalEquiv def

R-Linear isomorphism that's propositionally equal to lTensor. · RestrictedProduct.lTensorPrincipalEquiv

L₁ def

The lower elementary generator !![1, 0; 1, 1] of SL₂(𝔽₃). · L₁

M

M def

An auxiliary set used in the proof of compact_quotient'. · NumberField.AdeleRing.DivisionAlgebra.Aux.M

map def

def AlgebraicClosure.map {K L : Type*} [Field K] [Field L] (f : K →+* L) : AlgebraicClosure K →+* AlgebraicClosure L · AlgebraicClosure.map

map def

Mapping double cosets across MonoidHoms. · DoubleCoset.map

map abbrev

abbrev FramedGaloisRep.map (ρ : FramedGaloisRep K A n) (f : K →+* L) : FramedGaloisRep L A n · FramedGaloisRep.map

map def

def GaloisRep.map (ρ : GaloisRep K A M) (f : K →+* L) : GaloisRep L A M · GaloisRep.map

map def

Base change of a TransvectionStruct along a ring homomorphism. · Matrix.TransvectionStruct.map

map def

Functoriality of PatchingAlgebra in the family of local rings. · PatchingAlgebra.map

map def

Functoriality of PatchingModule in the family of modules. · PatchingModule.map

map abbrev

Mapping a LevelStruct along a ring hom. · TotallyDefiniteQuaternionAlgebra.WeightTwoAutomorphicForm.LevelStruct.map

map def

A family of linear maps f i : M i →ₗ[R i] N i induces a linear map between the corresponding ultraproducts. · UltraProduct.map

map def

The map on points for an elliptic curve over k induced by a morphism of k-algebras is a group homomorphism. · WeierstrassCurve.Points.map

mapAlongLinearMap def

Given two restricted products Πʳ (i : ι₁), [R₁ i, B₁ i]_[𝓕₁] and Πʳ (j : ι₂), [R₂ j, B₂ j]_[𝓕₂] of A-modules, RestrictedProduct.mapAlongLinearMap gives an A-linear map between them. The data needed is a function f : ι₂ → ι₁ … · RestrictedProduct.mapAlongLinearMap

mapEquiv def

A family of ring isomorphisms R i ≃+* R' i lifts to an isomorphism of patching algebras. · PatchingAlgebra.mapEquiv

mapEquiv def

A family of linear equivalences M i ≃ₗ[R] N i lifts to a linear equivalence between the corresponding patching modules. · PatchingModule.mapEquiv

mapMatrix def

The ContinuousAlgHom between spaces of square matrices induced by an ContinuousAlgHom between their coefficients. This is Matrix.map as an ContinuousAlgHom. · ContinuousAlgHom.mapMatrix

mapOfIsPatchingSystem def

def PatchingModule.mapOfIsPatchingSystem : (Fin (rank R M F) → R) →ₗ[R] PatchingModule R M F · PatchingModule.mapOfIsPatchingSystem

mapRingHom def

The ring homomorphism 𝔸_K^∞ → 𝔸_L^∞ for L/K an extension of number fields. · IsDedekindDomain.FiniteAdeleRing.mapRingHom

mapRingHom def

A family of ring homomorphisms f i : R i →+* S i induces a ring homomorphism between the corresponding ultraproducts. · UltraProduct.mapRingHom

mapSemialgHom def

The ring homomorphism 𝔸_K^∞ → 𝔸_L^∞ for L/K an extension of number fields, as a morphism lying over the canonical map K → L. · IsDedekindDomain.FiniteAdeleRing.mapSemialgHom

mapSemialgHom def

The semialgebra homomorphism Completion α →ₛₐ[f] Completion β induced from a continuous ring homomorphism f : α →+* β. · UniformSpace.Completion.mapSemialgHom

mapUnits def

Any ContinuousMulEquiv induces a ContinuousMulEquiv on units. · ContinuousMulEquiv.mapUnits

mapVariableChange def

The group homomorphism (C • W).Point →+ W.Point induced by the admissible change of variables (x, y) ↦ (u²x + r, u³y + u²sx + t). · WeierstrassCurve.Affine.Point.mapVariableChange

mapVariableChangeFun def

The underlying map (C • W).Point → W.Point of the change of variables, sending 0 to 0 and (x, y) to (u²x + r, u³y + u²sx + t). · WeierstrassCurve.Affine.Point.mapVariableChangeFun

mapₗ def

Mapping an automorphic form along a linear map. · TotallyDefiniteQuaternionAlgebra.WeightTwoAutomorphicForm.mapₗ

mapₜ def

The continuous group homomorphism on units induced by a ContinuousMonoidHom. · Units.mapₜ

matrixEquiv def

Set.matrix is equivalent to matrices on the subtype. · Set.matrixEquiv

matrixEquiv def

Subring.matrix is equivalent to matrices on the subtype. · Subring.matrixEquiv

maximalCompact def

def GL2.maximalCompact : Subgroup GL₂(𝔸ᶠ[F]) · IsDedekindDomain.FiniteAdeleRing.GL2.maximalCompact

MaximalPQuotient abbrev

The maximal p-quotient of a group. · MaximalPQuotient

minGenPrimary def

δ(R): the minimal number of generators of an ideal of definition of R, i.e. of an 𝔪-primary ideal (an ideal with radical 𝔪). · DimensionTheorem.minGenPrimary

mk abbrev

Constructor for FiniteAdeleRing R K. An abbrev. · IsDedekindDomain.FiniteAdeleRing.mk

mk abbrev

Quotient map into the maximal p-quotient of a group. · MaximalPQuotient.mk

mkForm def

A constructor for forms in S(U, χ). · TotallyDefiniteQuaternionAlgebra.WeightTwoAutomorphicForm.LevelStruct.mkForm

mkFormA abbrev

A constructor for forms in S(U, χ) which instead asks for behaviour on U 𝔸ˣ. · TotallyDefiniteQuaternionAlgebra.WeightTwoAutomorphicForm.LevelStruct.mkFormA

module' abbrev

Transfer Module across an Equiv, where the additive structure on the source is itself obtained by transporting the one on the target back along the equivalence. · Equiv.module'

ModuleBaseChangeContinuousLinearEquiv def

𝔸_K ⊗[K] V = 𝔸_L ⊗[L] V as topological additive groups for V an L-module and K ⊆ L number fields. · NumberField.AdeleRing.ModuleBaseChangeContinuousLinearEquiv

ModuleBaseChangeLinearEquiv def

V ⊗[K] 𝔸_K = V ⊗[L] 𝔸_L as L-modules for V an L-module and K ⊆ L number fields. · NumberField.AdeleRing.ModuleBaseChangeLinearEquiv

ModuleTypeCardLT def

The type of all finite R-modules of cardinality less than N, presented as a sigma type over Fin N. · ModuleTypeCardLT

monomial def

The degree-n monomial in the elements of s indexed by a symmetric power. · DimensionTheorem.monomial

mopContinuousMulEquiv def

For any ring R, we have ring isomorphism Matₙₓₙ(Rᵒᵖ) ≅ (Matₙₓₙ(R))ᵒᵖ given by transpose. · MeasureTheory.Matrix.mopContinuousMulEquiv

mul def

Multiplication z*w of two Hurwitz numbers · Hurwitz.mul

mulEquivMultiplicativeZModTwo def

A group G with exactly two elements — the identity 1 and a distinguished element g ≠ 1, every element being equal to one of the two — is isomorphic to Multiplicative (ZMod 2), via the isomorphism sending g to … · mulEquivMultiplicativeZModTwo

mulLeft def

The F-linear equivalence on an F-algebra induced by left multiplication by a unit · _root_.LinearEquiv.mulLeft

mulLeft def

Multiplication on the left by a unit of an F-algebra which is a topological ring, is a continuous F-linear homeomorphism. · MeasureTheory._root_.ContinuousLinearEquiv.mulLeft

mulRight def

The F-linear equivalence on an F-algebra induced by right multiplication by a unit · _root_.LinearEquiv.mulRight

mulRight def

Multiplication on the right by a unit of an F-algebra which is a topological ring, is a continuous F-linear homeomorphism. · MeasureTheory._root_.ContinuousLinearEquiv.mulRight

mulRightEquiv def

The isomorphism H\G/K ≃ H\G/g⁻¹Kg sending HaK to H(ag)(g⁻¹Kg). · DoubleCoset.mulRightEquiv

mulSingleHom def

RestrictedProduct.mulSingle as a MonoidHom. · IsDedekindDomain.FiniteAdeleRing._root_.RestrictedProduct.mulSingleHom

mulSupport def

def mulSupport (u : Πʳ i, [G i, A i]) : Set ι · RestrictedProduct.mulSupport

N

narrowSLiftFunctor def

The functor of narrow S-lifts of ρ, consisting of representations of GL₂ satisfying: 1. It is a lift of ρ. 2. Its determinant is equal to εₗ, the l-adic cyclotomic character. 3. It is unramified outside l and S. 4. Its … · Deformation.narrowSLiftFunctor

narrowSLiftUniversalRing def

The universal lifting ring Rᵘⁿⁱᵛ representing the functor of narrow S-lifts. · Deformation.narrowSLiftUniversalRing

narrowSLiftUniversalRingCorepresentableBy def

The universal lifting ring Rᵘⁿⁱᵛ represents the functor of narrow S-lifts. · Deformation.narrowSLiftUniversalRingCorepresentableBy

narrowTraceConditionFunctor def

The subfunctor of representations whose trace is 2 on Iᵥ. · Deformation.narrowTraceConditionFunctor

neg def

The negation -z of a Hurwitz number · Hurwitz.neg

neg def

Negation on the space of automorphic forms over a totally definite quaternion algebra. · TotallyDefiniteQuaternionAlgebra.WeightTwoAutomorphicForm.neg

negVariableChange def

The automorphism [-1] : (x, y) ↦ (x, -y - a₁x - a₃) of a Weierstrass curve, as an admissible change of variables ⟨-1, 0, -a₁, -a₃⟩. It fixes E (negVariableChange_smul_self) and is an involution (negVariableChange_mul_self). · WeierstrassCurve.negVariableChange

nodePoly def

The node polynomial c₄ T² + a₁ c₄ T - (54 b₆ - 3 b₂ b₄ + a₂ c₄), whose roots are the slopes of the two tangent directions at the node of a multiplicative reduction; its splitting over the residue field governs whether the reduction … · WeierstrassCurve.nodePoly

norm def

The norm of a Hurwitz integer: the integer z * star z, equivalently the squared absolute value of the corresponding quaternion. · Hurwitz.norm

Normal class

(U, χ) is normal in (U', χ') if U ≤ U' is normal and χ'|_U = χ. · TotallyDefiniteQuaternionAlgebra.WeightTwoAutomorphicForm.LevelStruct.Normal

normalizerQuotient def

The index |N_G(P)| / |P| of a Sylow p-subgroup P in its normalizer in G. · Dickson.normalizerQuotient

normDilationParam def

The dilation parameter of an element g of the normalizer of the Sylow p-subgroup P, as a scalar in K p. · Dickson.normDilationParam

nTorsion abbrev

The n-torsion subgroup of an elliptic curve E over k: the kernel of multiplication by n on the group of k-points of E. · WeierstrassCurve.nTorsion

O

of abbrev

Make a ProartinianCat from an unbundled algebra. · Deformation.ProartinianCat.of

ofAlgebra def

def AlgebraTypeCardLT.ofAlgebra (N : ℕ) (M : Type*) [Ring M] [Algebra R M] [Finite M] (hM : Nat.card M < N) : AlgebraTypeCardLT R N · AlgebraTypeCardLT.ofAlgebra

ofAlgebra def

def TopologicalAlgebraTypeCardLT.ofAlgebra (N : ℕ) (M : Type*) [Ring M] [Algebra R M] [TopologicalSpace M] [T2Space M] [ContinuousSMul R M] [Finite M] (hM : Nat.card M < N) : … · TopologicalAlgebraTypeCardLT.ofAlgebra

ofComplex def

Make an automorphic form for GL₀/ℚ from a complex number · AutomorphicForm.GL0.ofComplex

ofComplex def

Make an automorphic form for GLₙ/ℚ of trivial weight ρ from a complex number z, returning the constant function with value z. · AutomorphicForm.GLn.ofComplex

ofEquiv def

Build an isomorphism in the category ProartinianCat R from a ContinuousAlgEquiv between Algebras. · Deformation.ProartinianCat.ofEquiv

ofGL abbrev

abbrev FramedGaloisRep.ofGL · FramedGaloisRep.ofGL

ofHom abbrev

Typecheck an ContinuousAlgHom as a morphism in ProartinianCat. · Deformation.ProartinianCat.ofHom

ofIsModuleTopology def

We can upgrade an AlgEquiv between algebras with the module topology into a ContinuousAlgEquiv. · ContinuousAlgEquiv.ofIsModuleTopology

ofIsTerminal def

The subfunctor defined by pulling back a subset of the terminal component. · CategoryTheory.Subfunctor.ofIsTerminal

ofLeft def

The projection G/K → H\G/K. · DoubleCoset.ofLeft

ofModule def

def ModuleTypeCardLT.ofModule (N : ℕ) (M : Type*) [AddCommGroup M] [Module R M] [Finite M] (hM : Nat.card M < N) : ModuleTypeCardLT R N · ModuleTypeCardLT.ofModule

ofModule def

def TopologicalModuleTypeCardLT.ofModule (N : ℕ) (M : Type*) [AddCommGroup M] [Module R M] [TopologicalSpace M] [T2Space M] [ContinuousSMul R M] [Finite M] (hM : Nat.card M < N) : … · TopologicalModuleTypeCardLT.ofModule

ofPi def

Auxiliary ring homomorphism from sequences ℕ → ∀ i, R i of representatives modulo the filter F to the product of components, used in the construction of incl. · PatchingAlgebra.ofPi

ofPi def

Auxiliary linear map from indexed sequences of representatives to the product of components, used to construct PatchingModule.incl. · PatchingModule.ofPi

ofQuotient def

def Measure.ofQuotient : Measure G · MeasureTheory.Measure.ofQuotient

ofQuotientIntegrand def

def Measure.ofQuotientIntegrand (f : G → ℝ≥0∞) (g : G ⧸ N) : ℝ≥0∞ · MeasureTheory.Measure.ofQuotientIntegrand

ofRight def

The projection H\G → H\G/K. · DoubleCoset.ofRight

one def

The Hurwitz number 1. · Hurwitz.one

opContinuousMulEquiv def

Units.opEquiv (taking x to x) as a ContinuousMulEquiv. · Units.opContinuousMulEquiv

OpenIdeals def

The set of open ideals of a topological ring R. · OpenIdeals

opMeasurableEquiv def

MulOpposite.op as a MeasurableEquiv. · MulOpposite.opMeasurableEquiv

orbitInfty def

The orbit of ∞ under the subgroup G', i.e. the set of points g • ∞ for g ∈ G'. · Dickson.orbitInfty

P

p1Act def

The action of a matrix M on the four points of ℙ¹(𝔽₃), obtained by applying M to a representative vector and projecting back. · p1Act

P1Fq def

The copy of ℙ¹(𝔽_q) (q = p^m) inside the projective line: ∞ together with the points [c : 1] for c ∈ 𝔽_{p^m}. · Dickson.P1Fq

P1point def

The point [c : 1] of the projective line ℙ¹(𝔽̄_p) associated to c : K p. · Dickson.P1point

p1Proj def

In ZMod 3 every element is its own inverse, so we can use v 0 * v 1 in place of v 0 * (v 1)⁻¹ (the latter does not reduce definitionally, since ZMod.inv is defined via Nat.gcdA). · p1Proj

p1Rep def

A choice of representative vector in 𝔽₃² for each of the four points of ℙ¹(𝔽₃). · p1Rep

padicEquiv def

def padicEquiv : FiniteAdeleRing (𝓞 ℚ) ℚ ≃ₐ[ℚ] Πʳ (p : Nat.Primes), [ℚ_[p], subring p] · Rat.FiniteAdeleRing.padicEquiv

padicNatDen def

The smallest positive natural n : ℕ for which x p * n is a p-adic integer for all p. · RestrictedProduct.padicNatDen

padicNum def

The element of (p : Nat.Primes) → ℤ_[p] obtained by multiplying by padicNatDen. · RestrictedProduct.padicNum

pairStabilizer def

The subgroup of G consisting of the elements that fix both x and y on the projective line. · Dickson.pairStabilizer

partitionTerm abbrev

A single summand 1 / sᵢ * (1 - 1 / zᵢ) appearing in the class-equation sum. · Dickson.partitionTerm

PatchingAlgebra def

The patching algebra: the inverse limit of the components R i / m^k glued along the ultrafilter F. · PatchingAlgebra

PatchingModule def

The patching module for a family M i of modules over a commutative topological ring R. This is an inverse limit over α of ultraproducts of M i / α • M i along the ultrafilter F, where α ranges over open ideals of R. · PatchingModule

periodPair def

The pair of periods (τ, 1), for τ not real. Its PeriodPair.lattice is Λ_τ = ℤτ + ℤ. · TateCurve.Blueprint.periodPair

PGL abbrev

The projective general linear group PGL₂(K p), i.e. GL₂(K p) modulo its centre. · Dickson.PGL

pglMap def

The group homomorphism PGL₂(F) → PGL₂(L) induced by a ring homomorphism f : F →+* L. · Dickson.pglMap

PGLOf abbrev

The projective general linear group PGL₂(F) over a field F, i.e. GL₂(F) modulo its centre. The development in FLT.Slop.PGL2 works with this explicit quotient model throughout; it is definitionally equal to `Matrix.ProjGenLinGroup … · Dickson.PGLOf

Phi def

The set of points on the projective line fixed by some non-identity element of G. · Dickson.Phi

PhiType abbrev

The subtype of points on the projective line fixed by some non-identity element of G. · Dickson.PhiType

pi' def

The product of a family of submodules N i ≤ M i, viewed as a submodule of Π i, M i over the product ring Π i, R i. · Submodule.pi'

piAdicIntegerSubmodule def

∏_{w∣v} 𝓞_w as an 𝓞_v-submodule of ∏_{w∣v} L_w · IsDedekindDomain.FiniteAdeleRing.piAdicIntegerSubmodule

piCongrFiberwise def

Let f : α → β be a function on index types. A family of R-algebra equivalences, indexed by b : β, between the product over the fiber of b under f given as ∀ (σ : { a : α // f a = b }) → γ₁ σ.1) ≃ₐ[R] γ₂ b lifts to an … · AlgEquiv.piCongrFiberwise

piCongrRight def

def _root_.ContinuousMulEquiv.piCongrRight (ψ : Π i, (G i) ≃ₜ* (H i)) : (∀ i, G i) ≃ₜ* (∀ i, H i) · MeasureTheory._root_.ContinuousMulEquiv.piCongrRight

piEquiv abbrev

A continuous additive isomorphism (𝔸_K)ⁿ ≃ 𝔸_L for n = [L:K] · NumberField.AdeleRing.piEquiv

piEquiv def

The $K_{\infty}$-linear homeomorphism $K_{\infty}^{[L:K]} \cong L_{\infty}$. · NumberField.InfiniteAdeleRing.piEquiv

piEquiv def

The Kᵥ-linear homeomorphism between Kᵥ^d and the product of all completions of L lying above v, where d = [K : L]. · NumberField.InfinitePlace.Completion.piEquiv

piEquivPiSubtypeProd def

def ContinuousMulEquiv.piEquivPiSubtypeProd {ι : Type*} (p : ι → Prop) (Y : ι → Type*) [(i : ι) → TopologicalSpace (Y i)] [(i : ι) → Mul (Y i)] [DecidablePred p] : ((i : ι) → Y i) ≃ₜ* ((i : { x : ι … · ContinuousMulEquiv.piEquivPiSubtypeProd

piExtension def

The map from v.Completion to the product of all completions of L lying above v. · NumberField.InfinitePlace.Completion.piExtension

piIndex def

def RingHom.piIndex {ι S : Type*} {R : ι → Type*} [_root_.Finite ι] [DecidableEq ι] [∀ i, Semiring (R i)] [Semiring S] [Nontrivial S] (f : (Π i, R i) →+* S) : ι · RingHom.piIndex

piMap' def

A more dependent version of LinearMap.piMap, making a product of linear maps into a linear map over the product of rings. · LinearMap.piMap'

piQuotientEquiv def

A continuous additive isomorphism (𝔸_K / K)ⁿ = 𝔸_L / L where n = [L:K]. · NumberField.AdeleRing.piQuotientEquiv

piScalarPiComm def

Given φ : α → β → Type* and R : α → Type* such that φ a b is an R a module for all a b, this is the continuous linear equivalence between ∀ a b, φ a b and ∀ b a, φ a b with product scalars. This is Equiv.piComm as a … · ContinuousLinearEquiv.piScalarPiComm

piScalarPiComm def

Given φ : α → β → Type* and R : α → Type* such that φ a b is an R a module for all a b, this is the linear equivalence between ∀ a b, φ a b and ∀ b a, φ a b with product scalars. This is Equiv.piComm as a product-scalar … · LinearEquiv.piScalarPiComm

piScalarPiCongrFiberwise def

Let f : α → β be a function on index types. A family of R b-linear homeomorphisms, indexed by b : β, between the product over the fiber of b under f given as ∀ (σ : { a : α // f a = b }) → γ₁ σ.1) ≃ₗ[R b] γ₂ b lifts to an … · ContinuousLinearEquiv.piScalarPiCongrFiberwise

piScalarPiCongrFiberwise def

Let f : α → β be a function on index types. A family of R b-linear equivalences, indexed by b : β, between the product over the fiber of b under f given as ∀ (σ : { a : α // f a = b }) → γ₁ σ.1) ≃ₗ[R b] γ₂ b lifts to an … · LinearEquiv.piScalarPiCongrFiberwise

piSubringSubmodule def

If B i is subring of R i then (B i)^n is a B i-submodule of (R i)^n. · RestrictedProduct.piSubringSubmodule

piUnique def

def ContinuousMulEquiv.piUnique {ι : Type*} (M : ι → Type*) [(j : ι) → Mul (M j)] [(j : ι) → TopologicalSpace (M j)] [Unique ι] : ((j : ι) → M j) ≃ₜ* M default · ContinuousMulEquiv.piUnique

preimage def

Given an element p : P in the direct limit, preimage f g p returns an element of M (preimageIndex f g p) that maps to p under g (preimageIndex f g p). · IsDirectLimit.preimage

preimage def

def preimage (r : A) : 𝓞 · IsResidueAlgebra.preimage

preimageComapFinset def

Given an inclusion of Dedekind domains A → B, making B finite over A, this is the preimage of a Finset of finite places of A, as a Finset of finite places of B. · IsDedekindDomain.HeightOneSpectrum.preimageComapFinset

preimageIndex def

Given an element p : P in the direct limit, preimageIndex f g p returns an index in ι such that p is in the image of the map g (preimageIndex f g p) : M (preimageIndex f g p) →ₗ[R] P. · IsDirectLimit.preimageIndex

preweight structure

A preweight for GLₙ is a continuous representation of the real orthogonal group O(n) on a finite-dimensional complex vector space. · AutomorphicForm.GLn.preweight

prime def

The (minimal) prime corresponding to an eigenform. · TotallyDefiniteQuaternionAlgebra.HeckeAlgebra.Eigenform.prime

primeQuotient def

𝕋/𝔭(f) = 𝒪(f) · TotallyDefiniteQuaternionAlgebra.HeckeAlgebra.Eigenform.primeQuotient

principalEquivProd def

The canonical isomorphism between Πʳ i, [R i, A i]_[𝓟 S] and (Π i ∈ S, R i) × (Π i ∉ S, A i) · RestrictedProduct.principalEquivProd

principalLinearEquivProd def

Module equivalence version of principalEquivProd. · RestrictedProduct.principalLinearEquivProd

principalMulEquivProd def

Additive monoid equivalence of principalEquivProd. · RestrictedProduct.principalMulEquivProd

ProartinianCat structure

The category of local proartinian algebras over 𝓞 with fixed residue field 𝕜. · Deformation.ProartinianCat

prod def

The product of two continuous semi-algebra isomorphisms on the same domain. · ContinuousSemialgHom.prod

prod def

The product of two semi-algebra maps on the same domain. · SemialgHom.prod

prodCongr def

def _root_.ContinuousMulEquiv.prodCongr (φ : A ≃ₜ* B) (ψ : C ≃ₜ* D) : A × C ≃ₜ* B × D · MeasureTheory._root_.ContinuousMulEquiv.prodCongr

prodMap def

the product of two continuous semi-algebra isomorphisms on different domains. · ContinuousSemialgHom.prodMap

prodMap def

The product of two semi-algebra maps on separate domains. · SemialgHom.prodMap

prodToSupOfRight def

If K is contained in the centralizer of H, then H ⊔ K is given by HK and the map H × K → HK is a group homomorphism. · Subgroup.prodToSupOfRight

ProjectiveLine abbrev

The projective line ℙ¹(K p) over K p. · Dickson.ProjectiveLine

projPiIndex def

def RingHom.projPiIndex {ι S : Type*} {R : ι → Type*} [_root_.Finite ι] [DecidableEq ι] [∀ i, Semiring (R i)] [Semiring S] [IsDomain S] (f : (Π i, R i) →+* S) : R f.piIndex →+* S · RingHom.projPiIndex

PSL abbrev

The projective special linear group PSL₂(K p). · Dickson.PSL

PSL2F3 abbrev

The projective special linear group PSL₂(𝔽₃). · PSL2F3

PSLImageInPGL def

The image of PSL₂(F) inside PGL₂(F), namely the range of SL2ToPGL F. · PSLImageInPGL

Q

q def

The Tate parameter of an elliptic curve E, given by a minimal Weierstrass equation with split multiplicative reduction over a nonarchimedean local field k: the unique element q of k with 0 < |q| < 1 such that `j(E) = j(q) = q⁻¹ + … · WeierstrassCurve.q

QHat abbrev

The "profinite completion" of ℚ is defined to be ℚ ⊗ ZHat, with ZHat the profinite completion of ℤ. · QHat

quadraticCharacter def

The quadratic character of Aut(M/K) attached to a separable quadratic subextension K ⊆ L ⊆ M: it sends σ to 1 if σ fixes L pointwise, and to -1 otherwise. · quadraticCharacter

quadraticTwist def

The quadratic twist of an elliptic curve E over K by a separable quadratic extension L/K: the twist WeierstrassCurve.quadraticTwistBy by an arbitrarily chosen generator θ ∈ L ∖ K. The twist is independent of this choice up to … · WeierstrassCurve.quadraticTwist

quadraticTwistBy def

The quadratic twist of a Weierstrass curve E over K by an element θ of an extension L/K: the twist WeierstrassCurve.quadraticTwistOf by the trace and norm of θ. This is "the" quadratic twist of E by the extension L/K … · WeierstrassCurve.quadraticTwistBy

quadraticTwistOf def

The quadratic twist of a Weierstrass curve E over K by parameters t, n, to be thought of as the trace and norm of a generator θ of a separable quadratic extension L/K (see WeierstrassCurve.quadraticTwistBy), so that `θ² = tθ … · WeierstrassCurve.quadraticTwistOf

quadraticTwistPointEquiv def

The isomorphism Eᴸ(M) ≅ E(M) on M-points, for any field M in a tower K ⊆ L ⊆ M: the base change to M of a choice of isomorphism between Eᴸ and E over L. It is natural in M (quadraticTwistPointEquiv_map) and transforms … · WeierstrassCurve.quadraticTwistPointEquiv

quadraticTwistVarChange def

A choice of change of variables over L carrying E to its quadratic twist Eᴸ. Using the explicit isomorphism of exists_smul_baseChange_and_map_eq (rather than an arbitrary one) ensures its Galois cocycle is exactly [-1] … · WeierstrassCurve.quadraticTwistVarChange

qUnit def

The Tate parameter as an element of kˣ. · WeierstrassCurve.qUnit

qUnitSepClosure def

The image of the Tate parameter in a separable closure Ω of k, as a unit. (Ω is not a nonarchimedean local field, so this is not literally (E.baseChange Ω).qUnit.) · WeierstrassCurve.qUnitSepClosure

quotientConjActEquivImageMulSingleton def

def _root_.QuotientGroup.quotientConjActEquivImageMulSingleton {G : Type*} [Group G] {g : G} {U V : Subgroup G} : U ⧸ (ConjAct.toConjAct g • V).subgroupOf U ≃ (QuotientGroup.mk '' (U * {g}) : Set (G … · _root_.QuotientGroup.quotientConjActEquivImageMulSingleton

quotientEquiv def

Mapping double cosets across MulEquivs. · DoubleCoset.quotientEquiv

quotientEquiv def

def PatchingModule.quotientEquiv : (PatchingModule Λ M F ⧸ (𝔫 • ⊤ : Submodule Λ (PatchingModule Λ M F))) ≃ₗ[Λ] PatchingModule Λ (fun i ↦ (M i) ⧸ (𝔫 • ⊤ : Submodule Λ (M i))) F · PatchingModule.quotientEquiv

quotientEquivFixedFieldEmb def

def InfiniteGalois.quotientEquivFixedFieldEmb [IsGalois K L] (G : ClosedSubgroup (L ≃ₐ[K] L)) : ((L ≃ₐ[K] L) ⧸ G.1) ≃ (fixedField G.1 →ₐ[K] L) · InfiniteGalois.quotientEquivFixedFieldEmb

quotientEquivOver def

def PatchingModule.quotientEquivOver [Module.Finite Λ M₀] : (PatchingModule Λ M F ⧸ (𝔫 • ⊤ : Submodule Λ (PatchingModule Λ M F))) ≃ₗ[Λ] M₀ · PatchingModule.quotientEquivOver

quotientKerEquivMap def

First isomorphism theorem restricted to a subgroup. · Subgroup.quotientKerEquivMap

quotientPi def

For a finite family of topological additive groups G i and subgroups p i ≤ G i, the canonical continuous additive isomorphism (∏ i, G i) ⧸ (∏ i, p i) ≃ₜ+ ∏ i, (G i ⧸ p i). · ContinuousAddEquiv.quotientPi

quotientPiContinuousLinearEquiv def

For a finite family of topological R-modules G i and submodules p i ≤ G i, the canonical continuous R-linear equivalence (∏ i, G i) ⧸ ∏ i, p i ≃L[R] ∏ i, G i ⧸ p i. · Submodule.quotientPiContinuousLinearEquiv

quotientTo def

def PatchingAlgebra.quotientTo [∀ (i : ι), IsLocalRing (R i ⧸ Ideal.map (algebraMap Λ (R i)) 𝔫)] : (PatchingAlgebra R F ⧸ 𝔫.map (algebraMap Λ (PatchingAlgebra R F))) →+* PatchingAlgebra (fun i ↦ R i … · PatchingAlgebra.quotientTo

quotientTo def

def PatchingModule.quotientTo : (PatchingModule Λ M F ⧸ (𝔫 • ⊤ : Submodule Λ (PatchingModule Λ M F))) →ₗ[Λ] PatchingModule Λ (fun i ↦ (M i) ⧸ (𝔫 • ⊤ : Submodule Λ (M i))) F · PatchingModule.quotientTo

quotientToOver def

def PatchingAlgebra.quotientToOver : (PatchingAlgebra R F ⧸ 𝔫.map (algebraMap Λ (PatchingAlgebra R F))) →+* R₀ · PatchingAlgebra.quotientToOver

R

RamifiedExtension abbrev

For a given infinite place v of K, RamifiedExtension L v are all the infinite places of L / K that extend v and are ramified over K. · NumberField.InfinitePlace.RamifiedExtension

rangeLTensor def

M ⊗_R (L i) as an R-submodule of M ⊗_R (N i). · RestrictedProduct.rangeLTensor

rangeLTensorLeft def

M ⊗_R (L i) as an M-submodule of M ⊗_R (N i). · RestrictedProduct.rangeLTensorLeft

rank def

def Module.UniformlyBoundedRank.rank : ℕ · Module.UniformlyBoundedRank.rank

ratsub abbrev

The image of ℚ inside ℚ̂ as an additive subgroup. · QHat.ratsub

realToCompletion def

The canonical ℝ-algebra structure on InfinitePlace.Completion. · NumberField.InfiniteAdeleRing.realToCompletion

repnFunctor def

repnFunctor n G 𝓞 is the functor taking R to continuous reps G → GLₙ(R). · Deformation.repnFunctor

repnQuotFunctor def

def repnQuotFunctor : ProartinianCat 𝓞 ⥤ Type u · Deformation.repnQuotFunctor

residueField def

The residue field 𝕜 as a proartinian local algebra. · Deformation.ProartinianCat.residueField

residueFieldEquiv def

If S = A[X]/(P) is local with maximal ideal 𝔪_A · S, then its residue field is (A/𝔪_A)[X]/(P mod 𝔪_A). · AdjoinRoot.residueFieldEquiv

ResidueFieldEquivCompletionResidueField def

The canonical isomorphism from A / v to 𝓞ᵥ / v, where 𝓞ᵥ is the integers of the completion Kᵥ of the field of fractions K of A. · IsDedekindDomain.HeightOneSpectrum.ResidueFieldEquivCompletionResidueField

ResidueFieldToCompletionResidueField def

The canonical ring homomorphism from A / v to 𝓞ᵥ / v, where 𝓞ᵥ is the integers of the completion Kᵥ of the field of fractions of A. · IsDedekindDomain.HeightOneSpectrum.ResidueFieldToCompletionResidueField

residueMap def

The induced map of residue fields 𝒪[k]/𝓂[k] →+* 𝒪[l]/𝓂[l], from the local homomorphism integerMap. (An honest definition, not a sorry: it is IsLocalRing.ResidueField.map of integerMap k l.) · ValuativeExtension.residueMap

resolutionCLM def

The functorial extension of a continuous linear map u : M2 →L[k] M3 (not necessarily equivariant) to the i-th level of the standard resolutions, applying u pointwise under the iterated C(G, ·). · ContRepresentation.resolutionCLM

resolutionXCast def

Transport between two levels of the standard resolution along an equality of indices, as a continuous linear map. · ContRepresentation.resolutionXCast

restrict def

Restriction of LevelStruct to an open subset. · TotallyDefiniteQuaternionAlgebra.WeightTwoAutomorphicForm.LevelStruct.restrict

restrictedProduct def

GL_2(𝔸_F^∞) is isomorphic and homeomorphic to the restricted product of the local components GL_2(F_v). · IsDedekindDomain.FiniteAdeleRing.GL2.restrictedProduct

restrictedProductCongr def

The additive monoid isomorphism between restricted products when the indices and factors are equivalent, provided compatibility criteria on the restriction filters and factors. · AddEquiv.restrictedProductCongr

restrictedProductCongr def

The equivalence between restricted products when the indices and factors are equivalent, provided compatibility criteria on the restriction filters and factors. · Equiv.restrictedProductCongr

restrictedProductCongr def

The linear isomorphism between restricted products when the indices and factors are equivalent, provided compatibility criteria on the restriction filters and factors. · LinearEquiv.restrictedProductCongr

restrictedProductCongr def

The multiplicative monoid isomorphism between restricted products when the indices and factors are equivalent, provided compatibility criteria on the restriction filters and factors. · MulEquiv.restrictedProductCongr

restrictedProductCongr def

The ring isomorphism between restricted products when the indices and factors are equivalent, provided compatibility criteria on the restriction filters and factors. · RingEquiv.restrictedProductCongr

restrictedProductCongrLeft def

The additive monoid isomorphism between restricted products on the same factors on different indices, when the indices are equivalent, with compatibility on the restriction filters. Applying the equivalence on the left-hand side. · AddEquiv.restrictedProductCongrLeft

restrictedProductCongrLeft def

The equivalence between restricted products on the same factors on different indices, when the indices are equivalent, with compatibility on the restriction filters. Applying the equivalence on the left-hand side. · Equiv.restrictedProductCongrLeft

restrictedProductCongrLeft def

The linear isomorphism between restricted products on the same factors on different indices, when the indices are equivalent, with compatibility on the restriction filters. Applying the equivalence on the left-hand side. · LinearEquiv.restrictedProductCongrLeft

restrictedProductCongrLeft def

The multiplicative monoid isomorphism between restricted products on the same factors on different indices, when the indices are equivalent, with compatibility on the restriction filters. Applying the equivalence on the left-hand side. · MulEquiv.restrictedProductCongrLeft

restrictedProductCongrLeft def

The ring isomorphism between restricted products on the same factors on different indices, when the indices are equivalent, with compatibility on the restriction filters. Applying the equivalence on the right-hand side. · RingEquiv.restrictedProductCongrLeft

restrictedProductCongrLeft' def

The additive monoid isomorphism between restricted products on the same factors on different indices, when the indices are equivalent, with compatibility on the restriction filters. Applying the equivalence on the right-hand side. · AddEquiv.restrictedProductCongrLeft'

restrictedProductCongrLeft' def

The equivalence between restricted products on the same factors on different indices, when the indices are equivalent, with compatibility on the restriction filters. Applying the equivalence on the right-hand side. · Equiv.restrictedProductCongrLeft'

restrictedProductCongrLeft' def

The linear isomorphism between restricted products on the same factors on different indices, when the indices are equivalent, with compatibility on the restriction filters. Applying the equivalence on the right-hand side. · LinearEquiv.restrictedProductCongrLeft'

restrictedProductCongrLeft' def

The multiplicative monoid isomorphism between restricted products on the same factors on different indices, when the indices are equivalent, with compatibility on the restriction filters. Applying the equivalence on the right-hand side. · MulEquiv.restrictedProductCongrLeft'

restrictedProductCongrLeft' def

The ring isomorphism between restricted products on the same factors on different indices, when the indices are equivalent, with compatibility on the restriction filters. Applying the equivalence on the right-hand side. · RingEquiv.restrictedProductCongrLeft'

restrictedProductCongrRight def

def ContinuousMulEquiv.restrictedProductCongrRight (φ : (i : ι) → G i ≃ₜ* H i) (hφ : ∀ᶠ i in ℱ, Set.BijOn (φ i) (A i) (B i)) : (Πʳ i, [G i, A i]_[ℱ]) ≃ₜ* (Πʳ i, [H i, B i]_[ℱ]) · ContinuousMulEquiv.restrictedProductCongrRight

restrictedProductCongrRight def

The equivalence between restricted products on the same index, when each factor is equivalent, with compatibility on the restricted subsets. · Equiv.restrictedProductCongrRight

restrictedProductCongrRight def

The LinearEquiv between restricted products built from LinearEquivs on the factors. · LinearEquiv.restrictedProductCongrRight

restrictedProductCongrRight def

def MulEquiv.restrictedProductCongrRight (φ : (i : ι) → R₁ i ≃* R₂ i) (hφ : ∀ᶠ i in 𝓕, Set.BijOn (φ i) (A₁ i) (A₂ i)) : (Πʳ i, [R₁ i, A₁ i]_[𝓕]) ≃* (Πʳ i, [R₂ i, A₂ i]_[𝓕]) · MulEquiv.restrictedProductCongrRight

restrictedProductCongrRight def

The ring isomorphism between restricted products on the same index, when each factor is equivalent, with compatibility on the restricted subsets. · RingEquiv.restrictedProductCongrRight

restrictedProductMatrix def

The monoid homeomorphism between a restricted product of n x n matrices, and n x n matrices of restricted products, when the products are with respect to open sets. · ContinuousMulEquiv.restrictedProductMatrix

restrictedProductMatrix def

The bijection between a restricted product of m x n matrices, and m x n matrices of restricted products. · Equiv.restrictedProductMatrix

restrictedProductMatrix def

The homeomorphism between a restricted product of m x n matrices, and m x n matrices of restricted products, when the products are with respect to open sets. · Homeomorph.restrictedProductMatrix

restrictedProductMatrixUnits def

The monoid homeomorphism between the matrix units over a restricted product and the restricted product of the matrix units over the factors, when the products are with respect to open submonoids. · ContinuousMulEquiv.restrictedProductMatrixUnits

restrictedProductPi def

def ContinuousMulEquiv.restrictedProductPi {ι : Type*} {n : Type*} [Fintype n] {A : n → ι → Type*} [∀ j i, TopologicalSpace (A j i)] [∀ j i, Group (A j i)] {C : (j : n) → (i : ι) → Subgroup (A j i)} … · ContinuousMulEquiv.restrictedProductPi

restrictedProductPi def

The bijection between a restricted product of finite products, and a finite product of restricted products. · Equiv.restrictedProductPi

restrictedProductPi def

The homeomorphism between a restricted product of finite products, and a finite product of restricted products, when the products are with respect to open subsets. · Homeomorph.restrictedProductPi

restrictedProductPi def

Canonical continuous linear equivalence between Π' R^n and (Π' R)^n · RestrictedProduct._root_.ContinuousLinearEquiv.restrictedProductPi

restrictedProductPi def

Canonical linear equivalence between Π' R^n and (Π' R)^n · RestrictedProduct._root_.LinearEquiv.restrictedProductPi

restrictedProductPiEquiv def

The continuous 𝔸 K-Linear equivalence between ∏'_v ∏_{w∣v} L_w and 𝔸 L given by reaindexing the elements. · IsDedekindDomain.FiniteAdeleRing.restrictedProductPiEquiv

restrictedProductPrincipal def

def ContinuousMulEquiv.restrictedProductPrincipal {ι : Type*} {R : ι → Type*} [∀ i, Monoid (R i)] [∀ i, TopologicalSpace (R i)] {S : ι → Type*} [∀ i, SetLike (S i) (R i)] [∀ i, SubmonoidClass (S i) … · ContinuousMulEquiv.restrictedProductPrincipal

restrictedProductPrincipal def

The canonical homeomorphism between a restricted product Πʳ i, [R i, A i]_[𝓟 J] over a principal filter, and the corresponding product (Π i : J, A i) × (Π i : Jᶜ, R i). · Homeomorph.restrictedProductPrincipal

restrictedProductProd def

The bijection between a restricted product of binary products, and the binary product of the restricted products. · Equiv.restrictedProductProd

restrictedProductProd def

The homeomorphism between restricted product of binary products, and the binary projuct of the restricted products, when the products are with respect to open subsets. · Homeomorph.restrictedProductProd

restrictedProductProdEquiv def

The B-linear isomorphism ∏'_v [∏_{w|v} L_w, ∏_{w|v} 𝓞_w] → 𝔸_L^∞ given by RestrictedProduct.flattenEquiv'. · IsDedekindDomain.FiniteAdeleRing.restrictedProductProdEquiv

restrictedProductTensorProductEquivRestrictedProductProd def

The B-linear isomorphism ∏'_v [B ⊗[A] K_v, B ⊗[A] 𝓞_v] ≅ ∏'_v [∏_{w|v} L_w, ∏_{w|v} 𝓞_w] given by adicCompletionComapIntegerLinearEquiv. · IsDedekindDomain.FiniteAdeleRing.restrictedProductTensorProductEquivRestrictedProductProd

restrictedProductUnits def

The monoid homeomorphism between the units of a restricted product of topological monoids and the restricted product of the units of the monoids, when the products are with respect to open submonoids. · ContinuousMulEquiv.restrictedProductUnits

restrictedProductUnits def

The isomorphism between the units of a restricted product of monoids, and the restricted product of the units of the monoids. · MulEquiv.restrictedProductUnits

restrictScalars def

Restrict the scalars of semialgebra map f : A →ₛₐ[ψ] B where ψ : R' →ₛₐ[φ] S', to φ : R →+* S. · SemialgHom.restrictScalars

rest₁ abbrev

The restriction of ringHaarCharKer D_𝔸 to (D ⊗ 𝔸_K^∞)ˣ via D𝔸_iso_prod_units. · NumberField.AdeleRing.DivisionAlgebra.Aux.rest₁

rightBaseChange def

def Module.Basis.rightBaseChange [DecidableEq ι] (b : Module.Basis ι R A) : Module.Basis ι B (A ⊗[R] B) · Module.Basis.rightBaseChange

ringHaarChar def

ringHaarChar : Rˣ →ₜ* ℝ≥0 is the function sending a unit of a locally compact topological ring R to the positive real factor which left multiplication by the unit scales additive Haar measure by. · MeasureTheory.ringHaarChar

ringHaarCharKer def

The kernel of the ringHaarChar : Rˣ → ℝ≥0, namely the units of a locally compact topological ring such that left multiplication by them does not change additive Haar measure. · MeasureTheory.ringHaarCharKer

ringHomEquivOfIsDomain def

def Pi.ringHomEquivOfIsDomain {ι S : Type*} {R : ι → Type*} [Finite ι] [DecidableEq ι] [∀ i, Ring (R i)] [Ring S] [IsDomain S] : ((Π i, R i) →+* S) ≃ Σ i, R i →+* S · Pi.ringHomEquivOfIsDomain

ringSMul def

The scalar action on the space of weight 2 automorphic forms on a totally definite quaternion algebra. · TotallyDefiniteQuaternionAlgebra.WeightTwoAutomorphicForm.ringSMul

rootable def

def Group.rootable (A : Type*) [CommGroup A] [TopologicalSpace A] [IsTopologicalGroup A] [ConnectedSpace A] [CompactSpace A] [T2Space A] : RootableBy A ℕ · Group.rootable

rootDiscrBound def

Minkowski's lower bound for the root discriminant (that is, the nth root of the absolute value of the discriminant) of a totally complex number field of degree n. · rootDiscrBound

rTensor def

The base extension of an R-algebra homomorphism f : N → P to an f-semilinear map N ⊗[R] M → P ⊗[R] M. · AlgHom.rTensor

rTensor' def

The continuous R-linear map M ⊗[R] V → N ⊗[R] V induced by a continuous R-linear map M → N. · ContinuousLinearMap.rTensor'

S

s abbrev

An auxiliary "size" function on invertible real matrices used in the slowly increasing condition; namely tr(MMᵀ) + tr(M⁻¹(M⁻¹)ᵀ). · AutomorphicForm.GLn.s

s def

The power series sₖ = ∑_{n ≥ 1} σₖ(n)qⁿ ∈ ℚ(u)⟦q⟧ (where σₖ(n) is the sum of the kth powers of the positive divisors of n). Up to a normalising constant, these are the q-expansions of the Eisenstein series of weight k + 1. · TateCurve.s

sAn def

The convergent power series sₖ(q) = ∑_{n ≥ 1} σₖ(n)qⁿ, for ‖q‖ < 1 (junk value otherwise); the evaluation of the formal series TateCurve.s k at q. Convergence follows from the crude estimate σₖ(n) ≤ n^(k+1). · TateCurve.Blueprint.sAn

self def

𝓞 as a proartinian local algebra. · Deformation.ProartinianCat.self

semialgebraMap def

The map (R,v) → (S,w) as a semialgebra map over R → S (which is the same map!). · IsDedekindDomain.HeightOneSpectrum.Extension._root_.WithVal.semialgebraMap

SemialgHom structure

Let φ : R →+* S be a ring homomorphism, let A be an R-algebra and let B be an S-algebra. Then SemialgHom φ A B or A →ₛₐ[φ] B is the ring homomorphisms ψ : A →+* B making lying above φ (i.e. such that `ψ (r • a) = φ r • ψ … · SemialgHom

semialgHom def

A family of semialgebra homomorphisms g i : A →ₛₐ[φ] f i defines a single semialgebra homomorphism A →ₛₐ[φ] (i : I) → f i to the product algebra. · Pi.semialgHom

SemialgHomClass class

SemialgHomClass F φ A B states that F is a type of φ-semialgebra homomorphisms from A to B, where A is an R-algebra, B is an S-algebra and φ : R →+* S. · SemialgHomClass

semialgHomPi def

The canonical map K_v → ∏_{w|v} L_w extending K → L. · IsDedekindDomain.HeightOneSpectrum.adicCompletion.semialgHomPi

semialgHomPi def

Given a reindexing r : I → J and a family of semialgebra homs p i : g (r i) →ₛₐ[φ] f i, build a semialgebra hom from the product over J of the g j to the product over I of the f i. · Pi.semialgHomPi

sigmaRangeQuotientStabilizer def

Given a representative for each orbit of X under G, and for each x : X a choice of σ that sends x to the representative, we obtain a bijection between X and ∐ G/stab(x) where the disjoint union runs through the … · MulAction.sigmaRangeQuotientStabilizer

single def

def NonUnitalRingHom.single {ι : Type*} (R : ι → Type*) [DecidableEq ι] [∀ i, NonUnitalNonAssocSemiring (R i)] (i) : R i →ₙ+* Π i, R i · NonUnitalRingHom.single

singleContinuousAddMonoidHom def

The inclusion from a factor into the restricted product of topological additive groups, as a continuous group homomorphism. · RestrictedProduct.singleContinuousAddMonoidHom

singleContinuousLinearMap def

The continuous K-linear inclusion Kᵥ → 𝔸_K^f from a completion to the finite K-adeles. · IsDedekindDomain.FiniteAdeleRing.singleContinuousLinearMap

singleLinearMap def

The continuous K-linear inclusion Kᵥ → 𝔸_K^f from a completion to the finite K-adeles. · IsDedekindDomain.FiniteAdeleRing.singleLinearMap

singleMulHom def

The continuous K-linear inclusion Kᵥ → 𝔸_K^f from a completion to the finite K-adeles. · IsDedekindDomain.FiniteAdeleRing.singleMulHom

sInt def

The formal series sₖ(q) = ∑_{n≥1} σₖ(n)qⁿ ∈ ℤ⟦q⟧ (integer-coefficient version of TateCurve.s; recall σₖ(0) = 0). · TateCurve.sInt

SL2F3 abbrev

The special linear group SL₂(𝔽₃). · SL2F3

sl2F3ToPermHom def

The permutation representation SL₂(𝔽₃) → S₄ induced by the action on ℙ¹(𝔽₃). · sl2F3ToPermHom

SL2ToPGL def

The natural homomorphism SL₂(F) → PGL₂(F) sending a matrix to the class of its image in GL₂(F). · SL2ToPGL

SLiftFunctor def

The functor of S-lifts of ρ, consisting of representations of GL₂ satisfying: 1. It is a lift of ρ. 2. Its determinant is equal to εₗ, the l-adic cyclotomic character. 3. It is unramified outside l and S. 4. Its trace is … · Deformation.SLiftFunctor

smul def

smul as a ContinuousAddEquiv. · ContinuousAddEquiv.smul

smulData class

Compatibility data between the local rings R i and modules M i and the open ideals of Λ: consists of an antitone function f : OpenIdeals Λ → ℕ such that m(R i)^(f α) • M i ⊆ α • M i for all i. · PatchingAlgebra.smulData

Space def

The underlying space of a galois rep. This is a type class synonym that allows G to act on it via ρ. · GaloisRep.Space

structureMap abbrev

The structure map Π 𝒪ᵥ → 𝔸ᶠ as a ring hom. · IsDedekindDomain.FiniteAdeleRing.structureMap

structureMapMonoidHom def

def structureMapMonoidHom {ι : Type*} (M : ι → Type*) [(i : ι) → Monoid (M i)] {S : ι → Type*} [∀ i, SetLike (S i) (M i)] [∀ i, SubmonoidClass (S i) (M i)] (A : Π i, S i) (𝓕 : Filter ι) : ((i : ι) → … · RestrictedProduct.structureMapMonoidHom

structureMapRingHom def

The structure map for a restricted product of ring. · RestrictedProduct.structureMapRingHom

structureSubring def

The subring ∏ i, A i inside Πʳ i, [R i, A i]_[𝓕]. · RestrictedProduct.structureSubring

subalgebra def

The patching algebra as a Λ-subalgebra of the product of components. · PatchingAlgebra.subalgebra

subalgebraEquiv def

There is a correspondence between K-subalgebras of Kⁿ and partitions of n, where for each set in the partition we take the diagonal subalgebra. · TotallyDefiniteQuaternionAlgebra.HeckeAlgebra.Pi.subalgebraEquiv

submodule def

FixedPoints as a submodule. · FixedPoints.submodule

submodule def

The patching module as a submodule of the product of components: those families compatible with the transition maps as α ≤ β ranges over open ideals. This is just an explicit construction of the patching module (a projective limit of … · PatchingModule.submodule

subring def

The patching algebra is an inverse limit of components; here we construct it explicitly as a subring of the product of components: those families that are compatible under the transition maps. · PatchingAlgebra.subring

sylowFixedPoint def

The unique fixed point on the projective line ℙ¹(𝔽̄_p) of a Sylow p-subgroup P. · Dickson.sylowFixedPoint

sylowMap def

The image of the Sylow p-subgroup P under conjugation by k₀, as a Sylow p-subgroup of the conjugate group k₀ G k₀⁻¹. · Dickson.sylowMap

T

T def

An auxiliary set T used in the proof of Fukisaki's lemma. Defined as Y ∩ Dˣ. · NumberField.AdeleRing.DivisionAlgebra.Aux.T

T def

The Hecke operator Tᵥ as an element of the Hecke algebra. · TotallyDefiniteQuaternionAlgebra.HeckeAlgebra.T

T def

The Hecke operator T_v as an R-linear map from M-valued quaternionic weight 2 automorphic forms of level U_1(S₀). · TotallyDefiniteQuaternionAlgebra.HeckeOperator.T

tateA₄ def

The coefficient a₄(q) = -5s₃(q) of the Tate curve, where sₖ(q) = ∑_{n≥1} nᵏqⁿ/(1-qⁿ) (Silverman, ATAEC V.3). · WeierstrassCurve.tateA₄

tateA₆ def

The coefficient a₆(q) = -(5s₃(q) + 7s₅(q))/12 of the Tate curve, where sₖ(q) = ∑_{n≥1} nᵏqⁿ/(1-qⁿ); the integrality 12 ∣ 5n³ + 7n⁵ makes sense of the division by 12 in every characteristic (Silverman, ATAEC V.3). · WeierstrassCurve.tateA₆

tateCurve def

The Tate curve E_q : y² + xy = x³ + a₄(q)x + a₆(q) (Silverman, ATAEC V.3). · WeierstrassCurve.tateCurve

tateCurveEquiv def

Tate's uniformisation of the Tate curve E_q, given by the explicit power series x = X(u, q), y = Y(u, q) of Silverman, ATAEC V.3. Unlike tateEquiv below, this involves no choices at all: it commutes on the nose with every valuative … · WeierstrassCurve.tateCurveEquiv

tateEquiv def

Tate's uniformization theorem: if E/k is an elliptic curve with split multiplicative reduction then E(k) is isomorphic to kˣ/⟨q⟩. · WeierstrassCurve.tateEquiv

tateEquivSepClosure def

Tate's uniformisation over a separable closure Ω of k: the union of the uniformisations of the E(l) over the finite subextensions l/k of Ω. Its sign is pinned to that of tateEquiv by tatePoint_baseChange. · WeierstrassCurve.tateEquivSepClosure

tateParameter def

The inverse of q ↦ j(q) (Silverman, ATAEC V.5.2): for |j| > 1, the unique q with 0 < |q| < 1 and j(q) = j, namely the evaluation q = j⁻¹ + 744j⁻² + 750420j⁻³ + ⋯ at j⁻¹ of the integral power series TateCurve.jInvReverse. … · WeierstrassCurve.tateParameter

tatePoint def

The point of E(Ω) corresponding to a unit x ∈ Ωˣ under Tate's uniformisation. · WeierstrassCurve.tatePoint

tensorAdicCompletionIntegersTo def

The canonical B-algebra map B ⊗[A] 𝓞_v → L ⊗[K] K_v · IsDedekindDomain.HeightOneSpectrum.tensorAdicCompletionIntegersTo

tensorAdicCompletionIntegersToAdicCompletion def

The map B ⊗ 𝓞_v → L_w for w an extension of v given by the algebra maps. · IsDedekindDomain.HeightOneSpectrum.Extension.tensorAdicCompletionIntegersToAdicCompletion

tensorAdicCompletionIntegersToPiRight def

The O_v-linear map from B ⊗[A] 𝓞ᵥ to Π v ∣ w, L_w · IsDedekindDomain.HeightOneSpectrum.tensorAdicCompletionIntegersToPiRight

tensorCoe def

The canonical B-linear map B ⊗[A] 𝓞_v → B ⊗[A] K_v. · IsDedekindDomain.HeightOneSpectrum.adicCompletionIntegers.tensorCoe

tensorEquivPi def

The complex anemic Hecke algebra is isomorphic to a product of copies of ℂ's, one for each eigenform. · TotallyDefiniteQuaternionAlgebra.HeckeAlgebra.tensorEquivPi

tensorEquivRestrictedProduct def

The B-linear isomorphism φ : B ⊗[K] 𝔸_K^∞ ≅ ∏'_v [B ⊗[A] K_v, B ⊗[A] 𝓞_v] given by φ (b ⊗ x) v = b ⊗ (x v). · IsDedekindDomain.FiniteAdeleRing.tensorEquivRestrictedProduct

tensorEquivTensor def

The canonical linear isomorphism L ⊗[K] 𝔸_K^∞ ≅ B ⊗[A] 𝔸_K^∞. · IsDedekindDomain.FiniteAdeleRing.tensorEquivTensor

tensorPiEquivFinitefreeModule def

The isomorphism Πᵢ ((B →₀ R) ⊗ Nᵢ) ≅ Πᵢ (M ⊗ Nᵢ) where M is assumed free and B is the basis of M given by Lean's global axiom-of-choice operator. This is an auxiliary definition. · tensorPiEquivFinitefreeModule

tensorPiEquivPiTensor def

Tensoring with a finite free module commutes with arbitrary products. · tensorPiEquivPiTensor

tensorPiEquivPiTensor' def

Tensoring with a finitely-presented module commutes with arbitrary products. To prove this, we consider the following commutative diagram. The goal is to show that i₃ is an isomorphism, which we do using the five lemma: · tensorPiEquivPiTensor'

tensorProductEquivPi abbrev

A continuous K-linear isomorphism L ⊗[K] 𝔸_K = (𝔸_K)ⁿ for n = [L:K] · NumberField.AdeleRing.tensorProductEquivPi

tmulEquivRangeLTensor def

R-Linear isomorphism between M ⊗_R (L i) and rangeLTensor R M N L i. · RestrictedProduct.tmulEquivRangeLTensor

toAdicCompletion def

The canonical ring homomorphism from the finite adele ring to a nonarchimedean local factor. · FiniteAdeleRing.toAdicCompletion

toAdicCompletion def

The canonical group homomorphism from GL_2(𝔸_F^∞) to the local component GL_2(F_v) for v a finite place. · IsDedekindDomain.FiniteAdeleRing.GL2.toAdicCompletion

toAdicCompletion def

def IsDedekindDomain.FiniteAdeleRing.toAdicCompletion (v : HeightOneSpectrum (𝓞 F)) : FiniteAdeleRing (𝓞 F) F →ₐ[F] HeightOneSpectrum.adicCompletion F v · IsDedekindDomain.FiniteAdeleRing.toAdicCompletion

toAdjoin' def

def Minpoly.toAdjoin' (R : Type*) {S : Type*} [CommRing R] [Ring S] [Algebra R S] (x : S) : AdjoinRoot (minpoly R x) →ₐ[R] adjoin R ({x} : Set S) · Minpoly.toAdjoin'

toComponent def

toComponent G f i is the canonical function from the inverse limit of the G_j to G_i. For the monoid homomorphism see toComponentMonoidHom, for the ring homomorphism see toComponentRingHom and for the linear map see … · InverseLimit.toComponent

toComponentLinearMap def

LinearMap version of toComponent G f i · InverseLimit.toComponentLinearMap

toComponentMonoidHom def

MonoidHom version of toComponent G f i · InverseLimit.toComponentMonoidHom

toComponentRingHom def

RingHom version of toComponent G f i · InverseLimit.toComponentRingHom

toConst def

The natural map from a fixed module M to the patching module of the constant family fun _ ↦ M. · PatchingModule.toConst

toContinuousAlgEquiv def

Build a ContinuousAlgEquiv from an isomorphism in the category ProartinianCat R. · Deformation.ProartinianCat._root_.CategoryTheory.Iso.toContinuousAlgEquiv

toContinuousLinearEquiv def

Given M : Matrix ι ι F, b : Module.Basis ι F V and h : M.det ≠ 0, this is the continuous linear equivalence arising from Matrix.toLinearEquiv b M (Ne.isUnit h) · Matrix.toContinuousLinearEquiv

toContinuousMonoidHom def

Coerce a ContinuousAlgHom to ContinuousMonoidHom. · ContinuousAlgHom.toContinuousMonoidHom

toContinuousMulEquiv def

smul as a ContinuousMulEquiv. · MulDistribMulAction.toContinuousMulEquiv

toContinuousSemialgHom def

Turn an element of F which satisfies ContinuousSemialgHomClass F φ A B to a ContinuousSemialgHom. · ContinuousSemialgHom._root_.ContinuousSemialgHomClass.toContinuousSemialgHom

toExtension abbrev

Any infinite place w of L is an extension of its restriction to K. · NumberField.InfinitePlace.toExtension

toFramedGaloisRep def

def toFramedGaloisRep {R} (ρ : (repnFunctor n (Γ K) 𝓞).obj R) : FramedGaloisRep K R n · Deformation.toFramedGaloisRep

toFun def

The Hecke operator T_g = [UgV] : A^V → A^U associated to the double coset UgV. · AbstractHeckeOperator.heckeOperator.toFun

toFunAlgHom def

The coercion from MulActionHom to functions as an AlgHom. · MulActionHom.toFunAlgHom

toHeightOneSpectrumInt def

The element of HeightOneSpectrum ℤ associated to a prime number. · Nat.Prime.toHeightOneSpectrumInt

toHeightOneSpectrumRingOfIntegersRat def

The element of HeightOneSpectrum (𝓞 ℚ) associated to a prime number. · Nat.Prime.toHeightOneSpectrumRingOfIntegersRat

toHomUnits def

Given a ContinuousMonoidHom from a group to a monoid, we may lift it to map into the group of units of the monoid. · ContinuousMonoidHom.toHomUnits

toIntContinuousLinearEquiv def

Reinterpret a continuous additive equivalence between additive groups as a continuous ℤ-linear equivalence. · ContinuousAddEquiv.toIntContinuousLinearEquiv

toIntegers abbrev

The induced map of an Eigenform from an hecke algebra to its integers. · TotallyDefiniteQuaternionAlgebra.HeckeAlgebra.Eigenform.toIntegers

toLocal abbrev

abbrev GaloisRep.toLocal (ρ : GaloisRep K A M) (v : Ω K) : GaloisRep (v.adicCompletion K) A M · GaloisRep.toLocal

toMapIdPreimage def

def DoubleCoset.toMapIdPreimage {G : Type*} [Group G] (H K₁ K₂ : Subgroup G) (eK : K₁ ≤ K₂) (g : G) : K₂ ⧸ K₁.subgroupOf K₂ → DoubleCoset.map H K₁ H K₂ (.id _) le_rfl eK ⁻¹' {DoubleCoset.mk _ _ g} · DoubleCoset.toMapIdPreimage

TopologicalAlgebraTypeCardLT def

The type of all finite Hausdorff topological R-algebras of cardinality less than N, with continuous scalar multiplication. · TopologicalAlgebraTypeCardLT

TopologicallyFG class

An R-algebra S is topologically finitely generated if there is a finite subset s ⊆ S such that the R-subalgebra generated by s is dense in S. · Algebra.TopologicallyFG

TopologicalModuleTypeCardLT def

The type of all finite Hausdorff topological R-modules of cardinality less than N, with continuous scalar multiplication. · TopologicalModuleTypeCardLT

toProdEigenform def

The embedding of the anemic Hecke algebra into a product of domains, indexed by eigenforms. · TotallyDefiniteQuaternionAlgebra.HeckeAlgebra.toProdEigenform

toQuaternion def

The embedding of the Hurwitz integers into the rational quaternions. · Hurwitz.toQuaternion

toQuot abbrev

The map from ringHaarCharKer D_𝔸 to the quotient Dˣ \ ringHaarCharKer D_𝔸. · NumberField.AdeleRing.DivisionAlgebra.Aux.toQuot

toRamifiedExtension def

Construct a v.RamifiedExtension L term from a w : v.Extension L such that w.1.IsRamified K. · NumberField.InfinitePlace.Extension.toRamifiedExtension

toRepnQuot def

def toRepnQuot : repnFunctor n G 𝓞 ⟶ repnQuotFunctor n G 𝓞 · Deformation.toRepnQuot

toRepresentation def

Turn an element in repnFunctor into an actual Representation. · Deformation.toRepresentation

toRepresentation def

A Galois representation is a representation (note that we are forgetting topological information here). · GaloisRep.toRepresentation

toResidueField def

def toResidueField (R : ProartinianCat 𝓞) : R ⟶ residueField · Deformation.ProartinianCat.toResidueField

toSemialgHom def

An algebra map defines a semi-algebra map using RingHom.id · AlgHom.toSemialgHom

toSemialgHom def

Promote a ring hom f : A →+* B which is φ-semilinear to a semi-algebra map. · RingHom.toSemialgHom

toSemialgHom def

Turn an element of F which satisfies SemialgHomClass F φ A B to a SemialgHom. · SemialgHomClass.toSemialgHom

toStruct def

The LevelStruct constructed via a LocalLevelStruct. · TotallyDefiniteQuaternionAlgebra.WeightTwoAutomorphicForm.LocalLevelStruct.toStruct

toSubmodule def

If S is a subring of R, then S can be viewed as an S-submodule of R. · Subring.toSubmodule

toUnramifiedExtension def

Construct a v.UnramifiedExtension L term from a w : v.Extension L such that w.1.IsUnramified K. · NumberField.InfinitePlace.Extension.toUnramifiedExtension

toZMod def

The canonical "reduce mod M" map from ZHat to ℤ/Mℤ. · ZHat.toZMod

traceConditionFunctor def

The subfunctor of representations whose trace is 2 on ker(Iᵥ → k(v)ˣ). · Deformation.traceConditionFunctor

translationGL def

The translation x ↦ x + b as the element !![1, b; 0, 1] of GL₂(K p). · Dickson.translationGL

translationPGL def

The translation x ↦ x + b as an element of PGLOf (K p) = PGL₂(𝔽̄_p). · Dickson.translationPGL

translationSet def

The set of b : K p for which the translation x ↦ x + b lies in the subgroup H. · Dickson.translationSet

transposeContinuousMulEquiv def

For any ring R, we have ring isomorphism Matₙₓₙ(Rᵒᵖ) ≅ (Matₙₓₙ(R))ᵒᵖ given by transpose. · MeasureTheory.Matrix.transposeContinuousMulEquiv

U

U def

The Hecke operator Uᵥ,ₐ as an element of the Hecke algebra. · TotallyDefiniteQuaternionAlgebra.HeckeAlgebra.U

U def

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 ∈ … · TotallyDefiniteQuaternionAlgebra.HeckeOperator.U

UA abbrev

U 𝔸ᶠˣ of a LevelStruct. · TotallyDefiniteQuaternionAlgebra.WeightTwoAutomorphicForm.LevelStruct.UA

Uf def

An auxiliary compact subset of D_𝔸^f with nonempty interior · NumberField.AdeleRing.DivisionAlgebra.Aux.Uf

Ui def

An auxiliary compact subset of D_∞ with nonempty interior · NumberField.AdeleRing.DivisionAlgebra.Aux.Ui

UltraProduct def

The ultraproduct of a family of additive groups M i along a filter F: the quotient of Π i, M i by tuples that are zero F-eventually. · UltraProduct

unframe def

def FramedGaloisRep.unframe (ρ : FramedGaloisRep K A n) (b : Module.Basis n A M) : GaloisRep K A M · FramedGaloisRep.unframe

UniformlyBoundedRank class

A family of local rings R i has uniformly bounded rank if for every k there exists a uniform bound on |R i / m(R i)^k| over all i. · Algebra.UniformlyBoundedRank

UniformlyBoundedRank class

A family of R-modules M i has uniformly bounded rank if there exists a single bound n : ℕ such that for every i, the rank of M i over R / Ann (M i) is less than n. · Module.UniformlyBoundedRank

unipotent def

The unipotent matrix element !![1, t; 0, 1]. · Matrix.GeneralLinearGroup.GL2.unipotent

unipotentMulDiag def

The matrix element (unipotent t) * (diag α hα) = !![α, t; 0, 1]. · TotallyDefiniteQuaternionAlgebra.WeightTwoAutomorphicForm.HeckeOperator.Local.GL2.unipotentMulDiag

unipotentMulDiagU1 def

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

unitBallPositiveCompact def

The unit ball as a compact set with nonempty interior. · Padic.unitBallPositiveCompact

unitsContinuousMulEquivUnitsType def

def Submonoid.unitsContinuousMulEquivUnitsType {M : Type*} [TopologicalSpace M] [Monoid M] {S : Submonoid M} (hS : IsOpen (S : Set M)) : S.units ≃ₜ* Sˣ · Submonoid.unitsContinuousMulEquivUnitsType

unitsIncl abbrev

Given a rigidification, we get an embedding Dˣ ↪ GL₂(𝔸_F). · IsQuaternionAlgebra.NumberField.WithRigidification.unitsIncl

unitsratsub abbrev

The image of ℚˣ inside ℚ̂ˣ as a subgroup. · QHat.unitsratsub

unitszHatsub abbrev

The image of ℤ̂ˣ inside ℚ̂ˣ as a subgroup. · QHat.unitszHatsub

unitszsub abbrev

The image of ℤˣ inside ℚ̂ˣ as a subgroup. · QHat.unitszsub

UnramifiedExtension abbrev

For a given infinite place v of K, UnramifiedExtension L v are all the infinite places of L / K that extend v and are unramified over K. · NumberField.InfinitePlace.UnramifiedExtension

unramifiedFunctor def

The subfunctor of unramified (at v) representations. · Deformation.unramifiedFunctor

U₁ def

def U₁ (𝒮 : U₁Data F R p) : WeightTwoAutomorphicForm.LocalLevelStruct F R · TotallyDefiniteQuaternionAlgebra.U₁

U₁ def

The upper elementary generator !![1, 1; 0, 1] of SL₂(𝔽₃). · U₁

U₁Data structure

The U₁ we will be considering needs the following input: · TotallyDefiniteQuaternionAlgebra.U₁Data

V

vanishingFilter def

The vanishing filter of an ideal p of the product ring Πᵢ Rᵢ over an index set ι: a set s ⊆ ι is in the vanishing filter if the element of Πᵢ Rᵢ which is 0 on s and 1 outside s lies in p. · vanishingFilter

vanishingFilterGI def

The Galois insertion between filters on ι and ideals of Π i, R i (for nontrivial R i) formed by vanishingFilter and eventuallyProd ⊥. · vanishingFilterGI

vanishingUltrafilter def

The vanishing ultrafilter of a prime ideal p of the product ring. See vanishingFilter for definition of a vanishing filter of an ideal of Πᵢ Rᵢ; if p is prime then this is an ultrafilter. · vanishingUltrafilter

W

Weight structure

A weight for GLₙ: a preweight whose associated O(n)-representation is simple. · AutomorphicForm.GLn.Weight

WeightTwoAutomorphicForm structure

This definition is made in mathlib-generality but is not the definition of a weight 2 automorphic form unless Dˣ is compact mod centre at infinity. This hypothesis will be true if D is a totally definite quaternion algebra over a … · TotallyDefiniteQuaternionAlgebra.WeightTwoAutomorphicForm

weilPairing def

The Weil pairing on the n-torsion of an elliptic curve E over a separably closed field k, a bilinear pairing with values in the n-th roots of unity of k. · WeierstrassCurve.weilPairing

withIdeal abbrev

The default WithIdeal structure on a local ring R, picking out the maximal ideal. · IsLocalRing.withIdeal

WithRigidification class

A rigidification of a quaternion algebra D over a number field F is a fixed choice of 𝔸_F^∞-algebra isomorphism D ⊗[F] 𝔸_F^∞ = M₂(𝔸_F^∞). In other words, it is a choice of splitting of D ⊗[F] Fᵥ (i.e. an isomorphism to M₂(Fᵥ)) for … · IsQuaternionAlgebra.NumberField.WithRigidification

X

X def

An auxiliary set X used in the proof of Fukisaki's lemma. Defined as E - E. · NumberField.AdeleRing.DivisionAlgebra.Aux.X

X def

The power series X(u,q) = u/(1-u)² + ∑_{n ≥ 1} (∑_{d ∣ n} d(uᵈ + u⁻ᵈ - 2)) qⁿ ∈ ℚ(u)⟦q⟧, the x-coordinate of the uniformisation kˣ/qᶻ ≃ E_q(k) of the Tate curve. · TateCurve.X

XAn def

The analytic function Xₐ(u, q) = ∑_{n : ℤ} qⁿu/(1 - qⁿu)² - 2s₁(q), defined for 0 < ‖q‖ < 1 and u ∉ qᶻ (junk value otherwise). This is the function called X(u, q) in [Silverman, Advanced topics, Theorem V.1.1]. The sum converges … · TateCurve.Blueprint.XAn

Y

Y def

An auxiliary set Y used in the proof of Fukisaki's lemma. Defined as X * X. · NumberField.AdeleRing.DivisionAlgebra.Aux.Y

Y def

The power series Y(u,q) = u²/(1-u)³ + ∑_{n ≥ 1} (∑_{d ∣ n} ((d choose 2)uᵈ - (d+1 choose 2)u⁻ᵈ + d)) qⁿ in ℚ(u)⟦q⟧, the y-coordinate of the uniformisation kˣ/qᶻ ≃ E_q(k) of the Tate curve. · TateCurve.Y

YAn def

The analytic function Yₐ(u, q) = ∑_{n : ℤ} (qⁿu)²/(1 - qⁿu)³ + s₁(q), defined for 0 < ‖q‖ < 1 and u ∉ qᶻ (junk value otherwise). This is the function called Y(u, q) in [Silverman, Advanced topics, Theorem V.1.1]. · TateCurve.Blueprint.YAn

Z

Z def

The centre of the universal enveloping algebra Alg G E. · AutomorphicForm.GLn.Z

Z2bar abbrev

Z2bar is the ring of integers of ℚ_[2]ᵃˡᵍ. · GaloisRepresentation.Z2bar

zero def

The Hurwitz number 0 · Hurwitz.zero

zero def

The zero automorphic form for a totally definite quaterion algebra. · TotallyDefiniteQuaternionAlgebra.WeightTwoAutomorphicForm.zero

ZHat def

We define the profinite completion of ℤ explicitly as compatible elements of ℤ/Nℤ for all positive integers N. We declare it as a subring of ∏_{N ≥ 1} (ℤ/Nℤ), and then promote it to a type. · ZHat

zHatsub abbrev

The image of ℤ̂ inside ℚ̂ as an additive subgroup. · QHat.zHatsub

zsub abbrev

The image of ℤ inside ℚ̂ as an additive subgroup. · QHat.zsub

Other

Δ def

Δ_g := U 𝔸ˣ ∩ g⁻¹ Dˣ g · TotallyDefiniteQuaternionAlgebra.WeightTwoAutomorphicForm.LevelStruct.Δ

ΔFormal def

The formal discriminant Δ(q) = q∏_{n≥1}(1 - qⁿ)²⁴ ∈ ℤ⟦q⟧ of the Tate curve: the q-expansion of the modular discriminant, ∑ τ(n)qⁿ with τ Ramanujan's tau. The product is a tprod in the X-adic topology, multipliable by … · TateCurve.ΔFormal

ΔIndex def

The index [U 𝔸ˣ ∩ g⁻¹ Dˣ g : Fˣ] as a function on Dˣ\GL₂(𝔸)/U. · TotallyDefiniteQuaternionAlgebra.WeightTwoAutomorphicForm.LevelStruct.ΔIndex

π def

The projection from the patching module onto its α-th component, for an open ideal α of R. · PatchingModule.π

π def

The canonical projection from the product Π i, R i to the ultraproduct as a ring homomorphism. · UltraProduct.π

πₗ def

The canonical projection from the product Π i, M i of R i-modules to the ultraproduct as a Π i, R i-linear map. · UltraProduct.πₗ

σ def

An arbitrary section of G → H＼G／K. · DoubleCoset.σ

σLeft def

An arbitrary choice of h such that h * σ(g) * K = g. · DoubleCoset.σLeft

σRight def

An arbitrary choice of k such that h * σ(g) * K = g. · DoubleCoset.σRight

φLocalKvLinear def

TensorProduct.localcomponent φ as v.adicCompletion K-linear map · φLocalKvLinear

χA def

The character extended onto U 𝔸ᶠˣ · TotallyDefiniteQuaternionAlgebra.WeightTwoAutomorphicForm.LevelStruct.χA

Terms from the explanations

Words defined in the explanations on this site (Lean4 Domain Explanation Language term lines). Where they appear, they link here.

Frey package

a normalised hypothetical counterexample (a, b, c, p) to Fermat's Last Theorem with p a prime at least 5 · FreyPackage

knownin1980s

a project tactic that closes any goal like sorry, reserved for results believed to follow from literature known before 1990 · FreyPackage.mazur

sorryAx

the axiom behind Lean's sorry; a theorem whose axioms include it has an unfinished proof somewhere below it · flt

Types

What kind of object something is. The Reading says these in words wherever they appear.

Bool

true or false

Equiv.Perm

Equiv.Perm α — a permutation (reordering) of α

EReal

a real number or ±∞

EuclideanSpace

EuclideanSpace ℝ (Fin n) — a point in n-dimensional space

Fin

Fin n — a number from 0 up to n − 1

Finset

Finset α — a finite set of elements of α

Ideal

Ideal R — a ideal (Ideal R)

IntermediateField

IntermediateField K L — a intermediate field (IntermediateField K L)

List

List α — a list of elements of α

Matrix

Matrix m n R — a matrix with rows m, columns n and entries in R

Measure

Measure α — a measure on α (a way to give sets a size)

Multiset

Multiset α — a finite collection of elements of α, repeats allowed

Option

Option α — either nothing or an element of α

Polynomial, R[X]

Polynomial R — a polynomial with coefficients in R

Prop

a statement (something true or false)

Set

Set α — a set of elements of α

SimpleGraph

SimpleGraph V — a graph whose vertices are the elements of V

String

a piece of text

Subfield

Subfield K — a subfield (Subfield K)

Subgroup

Subgroup G — a subgroup (Subgroup G)

Submodule

Submodule R M — a submodule (Submodule R M)

Subring

Subring R — a subring (Subring R)

Type, Type*, Type _, Type u, Type v, Sort*

a type (a collection of objects)

ZMod

ZMod n — an integer modulo n

× (pair type)

α × β — a pair (α, β)

ℂ, Complex

a complex number

ℕ+

a positive whole number

ℕ, Nat

a natural number (0, 1, 2, …)

ℚ, Rat

a rational number (a fraction)

ℝ, Real

a real number

ℝ≥0, NNReal

a real number that is at least 0

ℝ≥0∞, ENNReal

a number from 0 to ∞, ∞ included

ℤ, Int

an integer

→ (function type)

α → β — a function that takes α and gives β

Structures a type can have

Written in square brackets, such as [Field K]. Lean finds them by itself (they are type classes).

AddCommGroup

[AddCommGroup G] — G is a commutative group under addition

AddGroup

[AddGroup G] — G is a group under addition

CharZero

[CharZero α] — in α, 1 + 1 + … + 1 is never 0

CommGroup

[CommGroup G] — G is a commutative group

CommRing

[CommRing R] — R is a commutative ring: you can add, subtract and multiply, and order of multiplication does not matter

CommSemiring

[CommSemiring R] — R has addition and commutative multiplication

Countable

[Countable α] — α is countable

DecidableEq

[DecidableEq α] — equality between elements of α can be checked

DecidablePred

[DecidablePred p] — whether p holds can be checked

Fact

[Fact (Nat.Prime p)] — it is known that Nat.Prime p

Field

[Field K] — K is a field: you can add, subtract, multiply and divide (except by 0)

Finite

[Finite α] — α has finitely many elements

Fintype

[Fintype α] — α has finitely many elements

Group

[Group G] — G is a group: you can multiply and undo multiplication

Inhabited

[Inhabited α] — α has a chosen default element

InnerProductSpace

[InnerProductSpace ℝ E] — E has angles and lengths (an inner product)

LinearOrder

[LinearOrder α] — any two elements of α can be compared

MeasurableSpace

[MeasurableSpace X] — X has measurable sets

MetricSpace

[MetricSpace X] — X has a distance between any two points

Module

[Module R M] — M is a module (a vector space when the scalars form a field)

Monoid

[Monoid M] — M has a multiplication with a 1

NeZero

[NeZero n] — n is not 0

Nonempty

[Nonempty α] — α has at least one element

Nontrivial

[Nontrivial α] — α has at least two different elements

NormedAddCommGroup

[NormedAddCommGroup E] — E has a length (norm) for its elements

NormedSpace

[NormedSpace ℝ E] — E is a vector space with lengths

PartialOrder

[PartialOrder α] — α has an order (some pairs may be incomparable)

Ring

[Ring R] — R is a ring: you can add, subtract and multiply

Semiring

[Semiring R] — R has addition and multiplication

TopologicalSpace

[TopologicalSpace X] — X has a notion of nearness (open sets)

Properties

Statements about functions, numbers and sets that the Reading puts in words, each shown on a sample use.

AEMeasurable

AEMeasurable f — f is measurable, apart from a set of measure zero

AEStronglyMeasurable

AEStronglyMeasurable f — f is (strongly) measurable, apart from a set of measure zero

Antitone

Antitone f — f never increases

BddAbove

BddAbove S — S is bounded above

BddBelow

BddBelow S — S is bounded below

Bijective

Bijective f — f is a bijection: a perfect one-to-one pairing

BijOn

BijOn f s t — f pairs s one-to-one with t

Collinear

Collinear ℝ S — the points S lie on one line

Colorable

Colorable G n — the graph can be colored with n colors so that neighbors get different colors

Commute

Commute a b — a and b commute: their product is the same in either order

Computable

Computable f — f is computable

ConcaveOn

ConcaveOn ℝ s f — f is concave on s: its graph bends downward

ContDiff

ContDiff ℝ n f — f is smooth: it can be differentiated n times, continuously

ContDiffAt

ContDiffAt ℝ n f x — f is smooth at x

Continuous

Continuous f — f is continuous: no jumps or breaks

ContinuousAt

ContinuousAt f x — f is continuous at x

ContinuousOn

ContinuousOn f s — f is continuous on s

ContinuousWithinAt

ContinuousWithinAt f s x — f is continuous at x within s

Convex

Convex ℝ s — s is convex: it contains the segment between any two of its points

ConvexOn

ConvexOn ℝ s f — f is convex on s: its graph bends upward

Coprime

Coprime a b — a and b are coprime: no common factor bigger than 1

Countable

Countable S — S is countable

Dense

Dense S — S is dense: it comes arbitrarily close to every point

Differentiable

Differentiable ℝ f — f is differentiable: it has a derivative everywhere

DifferentiableAt

DifferentiableAt ℝ f x — f has a derivative at x

DifferentiableOn

DifferentiableOn ℝ f s — f has a derivative at every point of s

Disjoint

Disjoint s t — s and t have nothing in common

Even

Even n — n is even

Finite

Finite S — S is finite

HasDerivAt

HasDerivAt f f' x — f has derivative f' at x

HasSum

HasSum a s — the terms a add up to s

IdentDistrib

IdentDistrib X Y — X and Y have the same distribution

iIndepFun

iIndepFun m X μ — the random variables X are independent

IndepFun

IndepFun X Y — the random variables X and Y are independent

Infinite

Infinite S — S is infinite

Injective

Injective f — f is injective: different inputs always give different outputs

InjOn

InjOn f s — f is injective on s: different inputs there give different outputs

Integrable

Integrable f — f is integrable (its integral is finite)

IntegrableOn

IntegrableOn f s — f is integrable on s

IntervalIntegrable

IntervalIntegrable f volume a b — f can be integrated from a to b

Involutive

Involutive f — applying f twice gives back the input

Irrational

Irrational x — x is irrational: not a fraction of two integers

Irreducible

Irreducible p — p is irreducible: it cannot be factored into smaller non-units

IsAlgebraic

IsAlgebraic ℤ x — x is algebraic: a root of a nonzero polynomial

IsBigO

IsBigO l f g — f is at most a constant times g (big O)

IsClosed

IsClosed F — F is a closed set

IsCompact

IsCompact K — K is compact (closed and bounded, in ℝⁿ)

IsConnected

IsConnected S — S is connected: it is all in one piece

IsCoprime

IsCoprime a b — a and b are coprime

IsGLB

IsGLB S m — m is the greatest lower bound of S

IsGreatest

IsGreatest S m — m is the greatest element of S

IsLeast

IsLeast S m — m is the least element of S

IsLittleO

IsLittleO l f g — f is negligible compared with g (little o)

IsLUB

IsLUB S m — m is the least upper bound of S

IsOpen

IsOpen U — U is an open set

IsProbabilityMeasure

IsProbabilityMeasure μ — μ is a probability measure: the whole space has size 1

IsSquare

IsSquare n — n is a perfect square

IsUnit

IsUnit a — a has a multiplicative inverse

LeftInverse

LeftInverse g f — g undoes f: applying f then g gives back the input

LinearIndependent

LinearIndependent K v — the vectors v are linearly independent

LipschitzWith

LipschitzWith K f — f never stretches distances by more than a factor K

MapsTo

MapsTo f s t — f sends every element of s into t

Measurable

Measurable f — f is measurable

MeasurableSet

MeasurableSet S — S is a measurable set (one that has a size)

MeasurePreserving

MeasurePreserving f — f preserves the measure: sets keep their size

MemLp

MemLp f p — f is in Lᵖ for p = p (the p-th power of |f| has a finite integral)

Monotone

Monotone f — f never decreases: a bigger input gives an output at least as big

MonotoneOn

MonotoneOn f s — f never decreases on s

Nonempty

Nonempty S — S is not empty

Odd

Odd n — n is odd

Pairwise

Pairwise r — every two different elements are related by r

Periodic

Periodic f c — f repeats every c

Perm

Perm l₁ l₂ — l₁ is a rearrangement of l₂

Prime

Prime p — p is a prime number

Primrec

Primrec f — f is primitive recursive (computable by a simple kind of program)

Reachable

Reachable u v — there is a path from u to v

RightInverse

RightInverse g f — g is a right inverse of f

Sbtw

Sbtw ℝ x y z — y lies strictly between x and z

Squarefree

Squarefree n — n is squarefree: no square bigger than 1 divides it

StrictAnti

StrictAnti f — f is strictly decreasing

StrictMono

StrictMono f — f is strictly increasing: a bigger input gives a bigger output

StronglyMeasurable

StronglyMeasurable f — f is strongly measurable

Summable

Summable a — the series of the terms a adds up to a finite value

Surjective

Surjective f — f is surjective: every possible output is reached

SurjOn

SurjOn f s t — f maps s onto all of t

Tendsto

Tendsto f atTop (𝓝 0) — f tends to 0 as the input grows without bound

Transcendental

Transcendental ℤ x — x is transcendental: not a root of any nonzero polynomial with integer coefficients

UniformContinuous

UniformContinuous f — f is uniformly continuous

Wbtw

Wbtw ℝ x y z — y lies between x and z

Symbols

Notation a newcomer may not know. A Reading lists the ones its statement uses.

#s, card

the number of elements

%

remainder after division

.Finite

the set has finitely many elements

.Infinite

the set has infinitely many elements

/

division; on ℕ and ℤ it rounds down

^

a power

A × B

pairs (a, b) with a from A and b from B

answer(…)

marks the answer the problem asks for; answer(sorry) means the answer is not filled in

atTop

“as the input goes to infinity”

choose

binomial coefficient: the number of ways to pick k things from n

deriv

the derivative

exp

the exponential function eˣ

f '' s

the image: all outputs f gives on s

f =O[l] g

big O: f is at most a constant times g, along l

f =o[l] g

little o: f is negligible compared with g, along l

f ⁻¹' s

the preimage: all inputs that f sends into s

f ∘ g

composition: first g, then f

f ≪ g

f is at most a constant times g (for large inputs)

Finset.range n

the numbers 0, 1, …, n − 1

fun x ↦ …

a function: send x to …

gcd

greatest common divisor

lcm

least common multiple

log

the natural logarithm

n !

factorial: 1 · 2 · … · n

Set.Icc a b

the closed interval [a, b]

Set.Ioo a b

the open interval (a, b)

sᶜ

the complement: everything not in s

x⁻¹

the inverse, 1 / x for numbers

{x | p x}

the set of all x with property p

|x|

absolute value

¬

“not”

π

pi

‖x‖

the norm (length) of x

ℂ

the complex numbers

ℕ

the natural numbers 0, 1, 2, … (in Lean ℕ starts at 0)

ℚ

the rational numbers (fractions)

ℝ

the real numbers

ℤ

the integers …, −2, −1, 0, 1, 2, …

↑x

x viewed in a bigger number system, such as a natural number as a real number

→

“implies”, or for functions “to”

↔

“if and only if”: both directions hold

∀

“for every”

∃

“there exists”

∃!

“there is exactly one”

∏

a product over a range or a finite set

∑

a sum over a range or a finite set

√

square root

∣

“divides”: a ∣ b means b is a multiple of a

∧

“and”

∨

“or”

∩

intersection: what both sets have in common

∪

union: everything in either set

∫

an integral

≡ [MOD n]

same remainder when divided by n

⌈x⌉

ceiling: the smallest integer at least x

⌊x⌋

floor: the largest integer at most x

𝓝 x

“near x”: used for limits

Tactics

Steps inside a proof that starts with by. Each says what the tactic does in general; the goal it leaves depends on the proof.

abel

Both sides are equal by rearranging sums (abel: algebra in commutative groups).

absurd

absurd h h' — Two facts contradict each other: h h'.

admit

Not proved yet: admit is a placeholder, so this proof is unfinished.

aesop

Search automatically for a proof using many small rules (aesop).

all_goals

all_goals simp — On every remaining goal: Simplify with Lean's standard simplification rules.

and_intros

Split the “and” goal into its parts.

any_goals

any_goals simp — On every goal where it works: Simplify with Lean's standard simplification rules.

apply

apply h — Work backwards with h: it gives the goal once its own conditions hold, so those conditions become the new goals.

apply_fun

apply_fun f at h — Apply f to both sides in h.

assumption

The goal is exactly one of the assumptions.

bound

Prove the bound by combining standard inequalities.

by_cases

by_cases h : x = 0 — Split into two cases: x = 0 is true, or it is false.

by_contra

Proof by contradiction: assume the opposite and reach something false.

by_contra!

Proof by contradiction, with the assumed opposite already simplified.

calc

A chain of steps, each one justified on its own line.

case

case zero => simp — The case zero.

cases

cases h — Split into cases on how h can be built.

cases'

cases' h with x hx — Split into cases on how h can be built.

change

change a + 0 = a — Restate the goal as a + 0 = a (the same thing, written differently).

choose

choose f hf using h — From “for every x there is a y”, pick a function giving such a y: f hf using h.

classical

Allow classical reasoning from here on (every statement is true or false, even if we cannot compute which).

clear

clear h — Forget the assumptions h; they are not needed any more.

congr

Reduce to showing the matching parts of both sides are equal.

constructor

constructor function Object() { [native code] } — Split the goal into its parts: for “A and B” prove A and B, for “A iff B” prove both directions.

constructorm

Split every “and”-like assumption or goal into its parts.

continuity

Built automatically from the rules for continuous functions.

contradiction

Two assumptions contradict each other, so this case is done.

contrapose

Prove the contrapositive: if the conclusion fails, then so does the assumption.

contrapose!

Prove the contrapositive, with the negations pushed inward.

conv

Rewrite inside one chosen part of the goal.

conv_lhs

Rewrite inside the left-hand side only.

conv_rhs

Rewrite inside the right-hand side only.

convert

convert h using 1 — Close the goal with h, which almost matches; any differences become new goals.

decide

Lean checks it by direct computation (decide).

delta

delta f — Expand the definition of f.

dsimp

Simplify by unfolding definitions.

erw

erw [h] — Rewrite using h, matching up to unfolding definitions.

exact

exact h — Finish: h is exactly what is needed.

exact_mod_cast

exact_mod_cast h — Finish with h, ignoring conversions between number systems.

exacts

exacts [h₁, h₂] — Finish each remaining goal with [h₁, h₂].

exfalso

Switch to proving False: this case is impossible.

exists

exists 2 — Give 2 as the example that exists.

existsi

existsi 2 — Give 2 as the example that exists.

ext

Two functions (or sets) are equal when they agree at every input.

ext1

Two functions (or sets) are equal when they agree at every input.

field

Both sides are equal by algebra with division (field).

field_simp

Clear the denominators.

filter_upwards

Reduce a statement about “eventually” or “almost everywhere” to one about each point.

fin_cases

fin_cases i — Try each of the finitely many values of i, one case each.

finiteness

The quantity is finite (not ∞), checked automatically (finiteness).

first

first | simp | ring — Try these in order until one works: simp, ring

focus

Work on the first goal only.

fun_prop

Built automatically from the rules for continuity, differentiability or measurability (fun_prop).

funext

Two functions are equal when they agree at every input.

gcongr

Compare the two sides piece by piece: if each part on the left is at most the matching part on the right, so is the whole (gcongr).

generalize

generalize e : f x = y — Replace a specific expression by a general variable: e : f x = y.

grind

Automated reasoning that combines equalities, cases and arithmetic (grind).

group

Both sides are equal by the rules of a group (group).

grw

grw [h] — Rewrite with an inequality (or another relation) instead of an equation: h.

have

have h : 0 < 2 := by norm_num — Establish an intermediate fact h: 0 is less than 2. Proved by: Do the arithmetic: norm_num proves number facts such as 2 + 2 = 4, 7 ≠ 0 or that 13 is prime.

have'

have' h : 0 < 2 := by norm_num — Establish an intermediate fact h: 0 is less than 2. Proved by: Do the arithmetic: norm_num proves number facts such as 2 + 2 = 4, 7 ≠ 0 or that 13 is prime.

haveI

haveI h : 0 < 2 := by norm_num — Establish an intermediate fact h: 0 is less than 2. Proved by: Do the arithmetic: norm_num proves number facts such as 2 + 2 = 4, 7 ≠ 0 or that 13 is prime.

if

Split on a condition, if-then-else.

induction

induction n with — Prove it by induction on n: first a starting case, then a step from each case to the next.

induction'

induction' n with n ih — Prove it by induction on n: a starting case, then the step to the next case.

infer_instance

Lean finds this automatically from known structures.

interval_cases

interval_cases n — Try every possible value of n in its known range, one case each.

intro

Move the next variable or assumption of the goal into view.

intros

Introduce everything the goal starts with.

left

Prove the left side of the “or”.

let

let y := x + 1 — Give a name to a value: y := x + 1.

letI

letI inst := Classical.decEq α — Give a name to a structure for Lean to use: inst := Classical.decEq α.

lia

Whole-number arithmetic, decided automatically (lia: linear integer arithmetic).

lift

lift n to ℕ using hn — Treat n to ℕ using hn as a value of a smaller number system, since it is known to fit.

linarith

It follows by adding up the linear inequalities in the assumptions (linarith).

linear_combination

linear_combination h₁ - h₂ — The goal is exactly this combination of the assumptions: h₁ - h₂.

match

match n with — Split on the shape of n, one case per pattern.

measurability

Built automatically from the rules for measurable functions.

module

Both sides are equal by algebra with vectors and scalars (module).

native_decide

Checked by running compiled code (native_decide). This also trusts the compiler, an extra axiom.

next

The next case.

nlinarith

Like linarith, but also multiplies assumptions together, which handles squares and products.

nofun

No case can occur, so there is nothing to prove.

nomatch

nomatch h — No case of h can occur.

noncomm_ring

Both sides are equal by algebra where multiplication need not commute (noncomm_ring).

norm_cast

Move the statement between number systems (ℕ, ℤ, ℚ, ℝ) to where it is simplest.

norm_num

Do the arithmetic: norm_num proves number facts such as 2 + 2 = 4, 7 ≠ 0 or that 13 is prime.

norm_num1

Do the arithmetic.

nth_rewrite

nth_rewrite 2 [h] — Rewrite one chosen occurrence using h.

nth_rw

nth_rw 2 [h] — Rewrite one chosen occurrence using h.

obtain

obtain ⟨x, hx⟩ := h — Unpack h into its pieces ⟨x, hx⟩.

omega

Whole-number arithmetic with +, −, constants and comparisons, decided automatically (omega).

on_goal

on_goal 2 => simp — On one chosen goal: 2 => simp.

order

It follows from the order facts in the assumptions (order).

peel

peel h with x hx — Strip matching quantifiers from both sides: h with x hx.

polyrith

The goal is a combination of the equations in the assumptions (polyrith).

positivity

The expression is positive (or at least 0), checked term by term (positivity).

push

Push the operation inward.

push_cast

Push the number-system conversions (↑) inward.

push_neg

Push the “not” inward: not-for-every becomes there-is-a-counterexample, and so on.

qify

Move the statement to ℚ, where division behaves normally.

rcases

rcases h with ⟨x, hx⟩ — Unpack h into its pieces ⟨x, hx⟩, one case per alternative.

refine

refine ⟨?_, ?_⟩ — Fill in the goal with ⟨?_, ?_⟩; every ?_ hole becomes a new goal.

refine'

refine' ⟨_, _⟩ — Fill in the goal with ⟨_, _⟩; every _ hole becomes a new goal.

rename_i

rename_i x y — Name the unnamed variables x, y.

repeat

repeat rw [h] — Repeat as long as it works: Rewrite using h.

replace

replace h : 0 < x := by linarith — Replace an assumption with a stronger form: the fact h: 0 is less than x. Proved by: It follows by adding up the linear inequalities in the assumptions (linarith).

revert

revert x — Put x back into the goal, so the goal is about every possible value of it.

rewrite

rewrite [h] — Rewrite using h.

rfl

Both sides are the same by definition (rfl).

right

Prove the right side of the “or”.

ring

Both sides are equal by algebra: expand and collect like terms (ring).

ring_nf

Put the expressions into a standard algebraic form.

rintro

rintro ⟨x, hx⟩ — Introduce and unpack in one go: ⟨x, hx⟩.

rotate_left

Change the order of the goals.

rw

rw [h] — Rewrite using h.

rwa

rwa [h] at h₁ — Rewrite using h in h₁, and then the goal is one of the assumptions.

set

set y := x + 1 with hy — Give a name to an expression and use the name from now on: y := x + 1.

show

show a + 0 = a — Restate the goal as a + 0 = a.

simp

Simplify with Lean's standard simplification rules.

simp_all

Simplify the goal and all the assumptions together.

simp_arith

Simplify, including arithmetic on natural numbers.

simp_rw

simp_rw [h] — Rewrite using h, also inside “for every” and “there is”.

simpa

Simplify, and the goal closes.

sorry

Not proved yet: sorry is a placeholder, so this proof is unfinished.

specialize

specialize h 2 — Use the assumption h for the specific 2.

split

Split into one case for each branch of the if-then-else or match.

split_ifs

Split into a case for each branch of every if-then-else.

subst

subst h — Replace h by what it equals, everywhere.

suffices

suffices h : 0 < x by linarith — It is enough to prove 0 < x; that is shown next, then used to finish.

swap

Work on the second goal first.

symm

Swap the two sides.

tauto

Pure logic: it follows from the assumptions by the rules of and, or, not and implies (tauto).

trans

trans b — Go through a middle point b.

trivial

This goal is immediate.

try

try linarith — Try this, and carry on if it fails: It follows by adding up the linear inequalities in the assumptions (linarith).

unfold

unfold f — Expand the definition of f.

use

use 2 — Give 2 as the example that exists; what remains is to check it works.

wlog

wlog h : a ≤ b with H — Without loss of generality, h : a ≤ b; the other case follows the same way.

zify

Move the statement from ℕ to ℤ, where subtraction behaves normally.