← all areas

Namespace LT 50 theorems

Artin 1 · HeckeChar 1 · LatticeTree 34 · TwistedNorm 14

LT.Artin 1

• Abelian case: any arithmetic Frobenius at Q is the Artin element LT.Artin.eq_artinFrob_of_isArithFrobAt 0 below · cited by 3 · depth 16

LT.HeckeChar 1

• Hecke characters realising narrow ray class characters LT.HeckeChar.exists_heckeCharOfRayClassChar 0 below · cited by 2 · depth 16

LT.LatticeTree 34

• Vertices moved distance exactly n counted by double cosets LT.LatticeTree.card_orbitalBall_sdiff_eq_relIndex_mul_sum_relIndex_of_det_eq_mul_zpow 2 below · cited by 2 · depth 21
• Displacement counts for a GL₂ class swapping two adjacent vertices LT.LatticeTree.card_orbitalBall_sdiff_of_act_swap_of_isWithin_one 7 below · cited by 2 · depth 21
• Displacement sphere counts on the lattice tree for g with finite non-empty fixed set LT.LatticeTree.card_orbitalBall_sdiff_of_finite_fixedVertexSet_of_nonempty 7 below · cited by 3 · depth 21
• Counting vertices at twisted distance exactly n by double cosets LT.LatticeTree.card_twistedOrbitalBall_sdiff_eq_relIndex_mul_sum_relIndex_of_det_eq_mul_zpow 1 below · cited by 3 · depth 21
• Twisted displacement shells on the tree for a finite non-empty twisted fixed set LT.LatticeTree.card_twistedOrbitalBall_sdiff_of_finite_twistedFixedVertexSet_of_nonempty 6 below · cited by 3 · depth 21
• Twisted displacement counts for an exchanged adjacent pair LT.LatticeTree.card_twistedOrbitalBall_sdiff_of_twistedAct_swap_of_isWithin_one 6 below · cited by 3 · depth 21
• Parity of vertex displacement equals parity of orddet LT.LatticeTree.even_of_mem_fixedVertexSet_and_even_of_mem_orbitalBall_sdiff_of_det_eq_mul_zpow 2 below · cited by 3 · depth 21
• Parity of twisted displacement equals parity of ord(detδ) LT.LatticeTree.even_of_mem_twistedFixedVertexSet_and_even_of_mem_twistedOrbitalBall_sdiff_of_det_eq_mul_zpow 1 below · cited by 3 · depth 21
• Normal forms for elliptic conjugacy classes in GL₂(Kᵥ) LT.LatticeTree.exists_conj_eq_zpow_smul_of_not_isSquare_discr 0 below · cited by 4 · depth 21
• Fixed vertex or swapped adjacent pair descends from an iterate LT.LatticeTree.nonempty_fixedVertexSet_or_exists_swap_of_iterate_act 2 below · cited by 4 · depth 21
• Fixed vertex or swapped pair for a twisted tree action LT.LatticeTree.nonempty_twistedFixedVertexSet_or_exists_swap_of_iterate_twistedAct 1 below · cited by 3 · depth 21
• Twisted fixed-vertex count as an index-weighted double-coset sum LT.LatticeTree.twistedUnitOrbitalCount_eq_relIndex_mul_sum_relIndex_of_det_eq_algebraMap 1 below · cited by 3 · depth 21
• Twisted fixed vertices count equals fixed vertices, anisotropic unit case LT.LatticeTree.twistedUnitOrbitalCount_eq_unitOrbitalCount_of_sigmaNormPow_eq_of_anisotropic 0 below · cited by 2 · depth 21
• Unit twisted orbital count equals orbital count, ramified elliptic case LT.LatticeTree.twistedUnitOrbitalCount_eq_unitOrbitalCount_of_sigmaNormPow_eq_of_eisenstein 0 below · cited by 2 · depth 21
• Fixed vertices of a unit-determinant class as a weighted double-coset count LT.LatticeTree.unitOrbitalCount_eq_relIndex_mul_sum_relIndex_of_det_eq_algebraMap 2 below · cited by 3 · depth 21
• Non-vanishing unit orbital count for anisotropic classes LT.LatticeTree.unitOrbitalCount_ne_zero_of_anisotropic 0 below · cited by 3 · depth 21
• Non-vanishing of the unit orbital count for ramified classes LT.LatticeTree.unitOrbitalCount_ne_zero_of_eisenstein 0 below · cited by 3 · depth 21
• Lattice sandwiching depth equals distance on the Bruhat–Tits tree LT.LatticeTree.Vertex.isWithin_iff_dist_le 1 below · cited by 3 · depth 22
• Integral g moves the base vertex by at most v(det g) LT.LatticeTree.Vertex.isWithin_stdVertex_act_of_isInteger_of_det_eq 0 below · cited by 2 · depth 22
• GL₂(K) acts transitively on lattice-tree vertices LT.LatticeTree.exists_act_stdVertex_eq 0 below · cited by 20 · depth 22
• Vertices at distance exactly r+1 from a twisted fixed set LT.LatticeTree.finite_sdiff_setOf_exists_isWithin_and_card_eq_of_finite_twistedFixedVertexSet 4 below · cited by 1 · depth 22
• Finiteness and size of balls of radius d in the lattice tree LT.LatticeTree.finite_setOf_isWithin_and_card_eq 1 below · cited by 4 · depth 22
• Vertices within r of an edge number 2(1+q+…+q^r) LT.LatticeTree.finite_setOf_isWithin_or_isWithin_and_card_eq_of_isWithin_one 4 below · cited by 1 · depth 22
• Displacement sets of an edge-swapping twisted action on the lattice tree LT.LatticeTree.twistedFixedVertexSet_eq_empty_and_twistedOrbitalBall_eq_of_twistedAct_swap 3 below · cited by 1 · depth 22
• Odd twisted orbital balls collapse; even ones surround the fixed set LT.LatticeTree.twistedOrbitalBall_odd_eq_and_even_eq_setOf_exists_isWithin_of_nonempty 3 below · cited by 2 · depth 22
• Unique neighbour towards v of a vertex at distance exactly n+1 LT.LatticeTree.Vertex.exists_isWithin_one_and_isWithin_and_forall_not_isWithin_succ_of_isWithin_succ_of_not_isWithin 1 below · cited by 4 · depth 23
• Additivity of the varpi-sandwich relation on lattice classes LT.LatticeTree.Vertex.isWithin_add_of_isWithin_of_isWithin 0 below · cited by 4 · depth 23
• Upper-triangular normal form for full lattices in K² LT.LatticeTree.exists_eq_latticeMap_scalarGL_mul_triangular_stdLattice 0 below · cited by 3 · depth 31
• Fixed-vertex counts for a+varpi^m Y: two kinds LT.LatticeTree.unitOrbitalCount_eq_of_anisotropic_and_eq_of_eisenstein_of_depth 11 below · cited by 1 · depth 32
• Fixed vertices of 1+varpi^{j+1}Y as the 1-neighbourhood LT.LatticeTree.fixedVertexSet_eq_setOf_exists_isWithin_one_of_coe_eq_one_add_pow_succ_smul 1 below · cited by 1 · depth 33
• Vertices fixed by 1+varpi Y neighbour those fixed by b+Y LT.LatticeTree.fixedVertexSet_eq_setOf_exists_isWithin_one_of_coe_eq_one_add_smul_of_isUnit_det 1 below · cited by 1 · depth 33
• Fixed vertices at depth zero: one in the anisotropic case, two in the Eisenstein case LT.LatticeTree.unitOrbitalCount_eq_one_of_anisotropic_and_eq_two_of_eisenstein_of_depth_zero 0 below · cited by 1 · depth 33
• Submodules between π M and a rank-two lattice M coincide LT.LatticeTree.FullLattice.eq_of_forall_smul_mem_of_le_of_le 0 below · cited by 2 · depth 34
• Nested ℤₚ-lattices of equal determinant index coincide LT.LatticeTree.eq_of_le_of_hasDetIndex_padic 0 below · cited by 6 · depth 34

LT.TwistedNorm 14

• Injectivity of the twisted norm on σ-conjugacy classes in GL₂ LT.TwistedNorm.exists_eq_sigmaConj_of_sigmaNormPow_eq_of_forall_mem_zpowers 0 below · cited by 3 · depth 25
• Injectivity of the twisted norm map over central classes LT.TwistedNorm.sigmaConjClasses_mk_eq_of_normClassMap_eq_mk_of_mem_centralCell 0 below · cited by 2 · depth 25
• Injectivity of the twisted norm map on elliptic classes LT.TwistedNorm.sigmaConjClasses_mk_eq_of_normClassMap_eq_mk_of_mem_ellipticCell 0 below · cited by 2 · depth 25
• Upper-triangular δ with central norm class is a scalar coboundary LT.TwistedNorm.exists_eq_scalar_mul_inv_mul_map_of_apply_one_zero_eq_zero_of_normClassMap_eq_mk 1 below · cited by 1 · depth 26
• Twisted elliptic norm classes re-indexed by scalars modulo norms LT.TwistedNorm.finsum_inv_card_mul_eq_finsum_inv_card_mul_of_normClassMap_eq_of_mem_ellipticCell 1 below · cited by 1 · depth 26
• Hyperbolic twisted classes parametrised by diagonal elements LT.TwistedNorm.setOf_exists_mem_center_subset_and_exists_and_eq_iff_of_diagonal 3 below · cited by 11 · depth 27
• Norms detect σ-twisted conjugacy of diagonal matrices in GL₂ LT.TwistedNorm.exists_eq_inv_mul_mul_map_iff_norm_eq_of_diagonal 0 below · cited by 3 · depth 28
• Hyperbolic norm class of an upper-triangular δ LT.TwistedNorm.exists_mem_hyperbolicCell_and_normClassMap_eq_iff_norm_div_ne_one 0 below · cited by 5 · depth 28
• Diagonal σ-conjugate when the norm class is hyperbolic LT.TwistedNorm.exists_sigmaConj_diagonal_of_mem_hyperbolicCell_of_normClassMap_eq 0 below · cited by 1 · depth 28
• Twisted stabiliser modulo centre of a diagonal GL₂ element LT.TwistedNorm.exists_subgroup_and_mul_mul_map_inv_mem_center_iff_of_diagonal_of_norm_div_ne_one 0 below · cited by 4 · depth 30
• Upper-triangular part of a hyperbolic twisted class: two cusp classes LT.TwistedNorm.setOf_exists_mem_center_inter_setOf_apply_one_zero_eq_zero_eq_union_and_disjoint 2 below · cited by 3 · depth 30
• Unipotent norm class for upper triangular δ LT.TwistedNorm.exists_mem_unipotentCell_and_normClassMap_eq_iff_exists_mul_eq_mul_map_and_trace_ne_zero_of_apply_one_zero_eq_zero 2 below · cited by 2 · depth 33
• Upper-triangular twisted conjugators for unipotent-type norm class LT.TwistedNorm.apply_one_zero_eq_zero_of_sigmaConj_upper_of_normClassMap_eq_mk_of_mem_unipotentCell 0 below · cited by 1 · depth 34
• Unipotent norm class iff σ-conjugate to ζ n(b), Tr(b)≠ 0 LT.TwistedNorm.exists_mem_unipotentCell_and_normClassMap_eq_iff_exists_mk_eq_mk_scalar_mul_unipotentGL2 0 below · cited by 1 · depth 34