← all areas

Namespace TateModule 20 theorems

• Order of the p-primary kernel via the Tate determinant TateModule.natCard_primaryComponent_ker_eq_pow_valuation_det 2 below · cited by 2 · depth 15
• Freeness of the p-adic Tate module from torsion counts TateModule.nonempty_basis_of_card_torsionBy 0 below · cited by 16 · depth 15
• A level-n coordinate map on R⊗_{mathbb Z_p}TₚM with kernel pⁿ TateModule.exists_baseChange_pi_torsionBy_ker_eq_pow_smul 0 below · cited by 1 · depth 18
• Equivariant isomorphism of rational Tate modules from equal torsion counts TateModule.exists_rationalTateModule_linearEquiv_comp_rationalGaloisRep_eq_of_injective_of_card_torsionBy_eq 2 below · cited by 1 · depth 18
• Reduction mod ℓ of a basis of the Tate module TateModule.exists_basis_toMatrix_eq_map_toZMod_of_card_torsionBy 0 below · cited by 1 · depth 19
• Functoriality of the p-adic Tate module in M TateModule.exists_linearMap_apply_eq_of_addMonoidHom 0 below · cited by 4 · depth 19
• Characteristic polynomial on the Tate module from kernel counts TateModule.charpoly_toMatrix_rep_eq_map_of_natCard_primaryComponent_ker_aeval 3 below · cited by 1 · depth 20
• Functoriality of the rational Tate module under a group isomorphism TateModule.exists_linearEquiv_rationalTateModule_comp_rationalGaloisRep_eq_of_addEquiv 1 below · cited by 1 · depth 21
• Tate module of ℓ-power torsion of order (ℓⁿ)ᵈ is free of rank d TateModule.finite_free_finrank_eq_of_natCard_torsionBy_pow_eq 0 below · cited by 3 · depth 23
• Fixing a tame generator suffices on the Tate module TateModule.forall_rep_eq_self_of_rep_eq_self_of_unipotent_of_forall_eq_pow_mul_pow_mul_pow 0 below · cited by 1 · depth 23
• A compatible filtration cuts out a line in a Tate module TateModule.exists_basis_span_eq_of_filtration 0 below · cited by 1 · depth 24
• Mittag-Leffler argument with level shift on Tate modules TateModule.exists_forall_apply_proj_eq_pow_smul_proj_of_forall_exists_torsionBy 0 below · cited by 1 · depth 24
• Dimension bound for subspaces of a rational Tate module TateModule.finrank_le_of_forall_proj_mem_of_card_le_pow 0 below · cited by 1 · depth 24
• Rank bound for Tate vectors with coboundary relations TateModule.add_one_le_finrank_span_tmul_add_of_forall_proj_rel_coboundary 0 below · cited by 1 · depth 27
• Tate module of a split torus: freeness and cyclotomic character TateModule.nonempty_basis_pi_units_and_eq_cyclotomicCharacter_smul_of_forall_apply_eq 1 below · cited by 2 · depth 27
• Rigidity of the Tate module under fixing the pᵃ-torsion TateModule.sub_one_pow_rep_eq_zero_of_pow_sub_one_pow_eq_zero_of_forall_torsionBy_smul_eq 1 below · cited by 4 · depth 28
• Homomorphisms from a saturated Tate submodule and its first projection TateModule.exists_addEquiv_addMonoidHom_map_proj_one_of_forall_smul_mem 0 below · cited by 1 · depth 29
• Functoriality of the Tate module: induced ℤₚ-linear map TateModule.exists_linearMap_forall_apply_eq 0 below · cited by 1 · depth 38
• Free Tate module of rank r and level surjectivity TateModule.nonempty_basis_and_forall_exists_proj_eq_of_natCard_torsionBy_eq_pow 1 below · cited by 6 · depth 38
• Level-one non-degeneracy mod p gives a perfect pairing TateModule.isPerfPair_of_forall_apply_one_ne_zero 1 below · cited by 1 · depth 39