← all areas

Namespace PDivisibleGroup 138 theorems

— 97 · CartierDuality 26 · Hopf 6 · IsCartierDual 1 · Tower 8

directly in PDivisibleGroup 97

• Connected component of a level as formal group p^v-torsion PDivisibleGroup.exists_connectedComponent_mvFormalGroup_of_isLocalRing_cartierDual 77 below · cited by 1 · depth 21
• Inertia-invariant forms kill points reducing to the identity PDivisibleGroup.forall_dual_apply_eq_zero_of_forall_valuation_sub_counit_lt_one_of_forall_inertia 219 below · cited by 4 · depth 21
• Transport of Tate modules along an embedding ℚ̄→ℚ̄ₚ PDivisibleGroup.exists_linearEquiv_tateModule_baseChange_ringOfIntegers_of_ringHom_padicAlgCl 10 below · cited by 1 · depth 22
• Tate module map induced by an equivariant points dictionary PDivisibleGroup.exists_linearMap_tateModule_jOne_apply_injective_range_galois_of_injective_of_forall_iff 1 below · cited by 1 · depth 22
• Connected part of a unipotent p-divisible tower as a formal group PDivisibleGroup.exists_mvFormalGroup_connectedComponent_tower_of_isLocalRing_cartierDual 76 below · cited by 1 · depth 22
• Inertia-invariant functionals vanish on unit-section Tate vectors PDivisibleGroup.forall_dual_apply_eq_zero_of_forall_norm_sub_counit_lt_one_of_forall_inertia_of_ringOfIntegers 210 below · cited by 1 · depth 22
• Compatible coordinates on the special fibres of a connected p-divisible group PDivisibleGroup.exists_compatible_specialFibre_coordinates_of_isLocalRing 54 below · cited by 1 · depth 23
• Connected components of a unipotent p-divisible tower PDivisibleGroup.exists_connectedComponent_tower_of_isLocalRing_cartierDual 17 below · cited by 1 · depth 23
• Formal group law from coordinates on a Hopf-algebra tower PDivisibleGroup.exists_mvFormalGroup_comul_eq_adicEval_of_specialFibre_coordinates 5 below · cited by 1 · depth 23
• Tate's Proposition 12, quotient form, over mathcal O_K PDivisibleGroup.exists_pDivisibleGroup_bialgHom_linearMap_tateModule_ker_eq_of_forall_smul_mem_of_ringOfIntegers 96 below · cited by 1 · depth 23
• Counting L-points of the levels of a p-divisible group in characteristic 0 PDivisibleGroup.finite_point_and_natCard_point_eq_pow 9 below · cited by 14 · depth 23
• Points near the unit section push forward along Tψ PDivisibleGroup.forall_exists_norm_sub_counit_lt_one_map_of_forall_exists_norm_sub_counit_lt_one 0 below · cited by 1 · depth 23
• Unramified Tate module forces formal étaleness of all levels PDivisibleGroup.forall_formallyEtale_level_of_forall_inertia_tateModuleRep_eq_of_ringOfIntegers 135 below · cited by 1 · depth 23
• Kernels of quasi-inverse isogenies: freeness and degree product p^{wh} PDivisibleGroup.free_quotient_map_ker_counit_of_comp_eq_nsmulAlgHom 39 below · cited by 1 · depth 23
• Kernel of the formal coordinates is the [p^v]-series ideal PDivisibleGroup.ker_eq_span_range_nthSeries_of_comul_eq_adicEval 8 below · cited by 1 · depth 23
• Point congruent to the counit on a formally étale level is trivial PDivisibleGroup.point_eq_one_of_forall_norm_sub_counit_lt_one_of_formallyEtale_of_ringOfIntegers 0 below · cited by 1 · depth 23
• Hopf quotient system cutting out a saturated Galois-stable submodule PDivisibleGroup.exists_hopf_quotient_system_points_iff_mem_of_forall_smul_mem_of_ringOfIntegers 20 below · cited by 2 · depth 24
• Existence of the Cartier dual p-divisible group PDivisibleGroup.exists_isCartierDual 6 below · cited by 5 · depth 24
• Functoriality of the Tate module in transition-compatible level maps PDivisibleGroup.exists_linearMap_tateModule_of_comp_transition_eq 0 below · cited by 3 · depth 24
• Polynomial coordinates on the special fibre of a connected p-divisible group PDivisibleGroup.exists_mvPolynomial_specialFibre_coordinates_of_isLocalRing 53 below · cited by 1 · depth 24
• Saturated Galois-stable submodule realised by a p-divisible group PDivisibleGroup.exists_pDivisibleGroup_bialgHom_linearMap_tateModule_injective_range_eq_of_hopf_quotient_system_of_ringOfIntegers 76 below · cited by 2 · depth 24
• Rank of the connected component multiplies along [p] PDivisibleGroup.finrank_connectedComponent_succ_eq_mul_of_ker_eq_span_one_sub 6 below · cited by 1 · depth 24
• Kernels of a p^w-isogeny pair of p-divisible towers PDivisibleGroup.finrank_quotient_map_ker_counit_mul_eq_pow_of_comp_eq_nsmulAlgHom 38 below · cited by 1 · depth 24
• Dimension zero p-divisible groups have formally étale levels PDivisibleGroup.formallyEtale_level_of_hasDimension_zero 1 below · cited by 1 · depth 24
• Unramified Tate module forces dimension zero (Tate) PDivisibleGroup.hasDimension_zero_of_forall_inertia_tateModuleRep_eq_self_of_ringOfIntegers 132 below · cited by 1 · depth 24
• Multiplication by p on a p-divisible tower is an isogeny of degree p^h PDivisibleGroup.exists_algEquiv_range_nsmulAlgHom_and_finite_projective_rankAtStalk_of_ker_eq_torsionIdeal 5 below · cited by 5 · depth 25
• Galois-stable Tate submodules cut out Hopf quotient systems over K' PDivisibleGroup.exists_baseChange_hopf_quotient_system_points_iff_mem_of_forall_smul_mem 15 below · cited by 1 · depth 25
• Hodge–Tate decomposition of the Tate module of a p-divisible group PDivisibleGroup.exists_basis_padicComplex_tateModule_eq_cyclotomicCharacter_pow_smul_of_hasDimension_of_ringOfIntegers 100 below · cited by 2 · depth 25
• Multiplication by p along a Hopf quotient tower stabilises PDivisibleGroup.exists_bialgHom_comp_eq_nsmulBialgHom_and_bijOn_hopfKer_of_hopf_quotient_system_of_ringOfIntegers 30 below · cited by 1 · depth 25
• Tate's Proposition 12: maps onto the subquotient tower PDivisibleGroup.exists_bialgHom_comp_transition_eq_and_injective_of_hopf_quotient_system_of_tower_of_ringOfIntegers 9 below · cited by 1 · depth 25
• Existence of a dimension for a p-divisible group PDivisibleGroup.exists_hasDimension 28 below · cited by 3 · depth 25
• Transition-compatible level endomorphisms induce a Tate-module endomorphism PDivisibleGroup.exists_moduleEnd_tateModule_apply_eq_pointsMkAdd_comp_of_comp_transition_eq 0 below · cited by 4 · depth 25
• Cyclotomic inertia action on U^N of the connected Tate module PDivisibleGroup.exists_rep_pow_sub_smul_eq_cyclotomicCharacter_smul_of_reduction_pow_eq_frobenius_conv_verschiebung 111 below · cited by 1 · depth 25
• Reduction-trivial Tate vectors: a p-saturated, inertia-stable submodule PDivisibleGroup.exists_submodule_tateModule_reduction_and_rep_sub_mem_of_mem_inertiaSubgroupIn 0 below · cited by 4 · depth 25
• Ranks in a Hopf quotient system: p^{vr} and p^r PDivisibleGroup.finrank_eq_pow_mul_finrank_and_finrank_hopfKer_eq_of_hopf_quotient_system_of_ringOfIntegers 24 below · cited by 2 · depth 25
• Levelwise criterion for injectivity and image of a Tate-module map PDivisibleGroup.injective_and_range_eq_of_forall_injective_of_forall_iff_exists_mem 12 below · cited by 1 · depth 25
• Stabilisers of points of a p-divisible group are open PDivisibleGroup.isOpen_setOf_restrictScalars_smul_points_eq 0 below · cited by 2 · depth 25
• Frobenius-kernel coordinates of a connected p-divisible group over mathbb Fₚ PDivisibleGroup.ker_aeval_quotient_span_pow_augIdeal_eq_span_X_pow_of_isLocalRing 50 below · cited by 2 · depth 25
• Order of the pⁿ-torsion of points of a p-divisible group PDivisibleGroup.natCard_torsionBy_points_eq_pow 10 below · cited by 1 · depth 25
• Tate module of a height-h p-divisible group is free of rank h PDivisibleGroup.nonempty_basis_tateModule_points 11 below · cited by 6 · depth 25
• Special fibre of an explicit p-divisible tower stays local PDivisibleGroup.specialFibre_tower_of_isLocalRing 1 below · cited by 1 · depth 25
• Dimensions of a p-divisible group and its Cartier dual sum to the height PDivisibleGroup.add_eq_height_of_hasDimension_of_cartierDuality 17 below · cited by 1 · depth 26
• A Frobenius–Verschiebung identity for φ^∨ on the special fibre PDivisibleGroup.cartierDualMap_pow_eq_frobenius_conv_verschiebung_of_multiplicative_sub_of_verschiebung_sub_frobenius_quotient 6 below · cited by 1 · depth 26
• Base change of the cotangent space of a p-divisible group PDivisibleGroup.cotangentBaseChange_bijective 0 below · cited by 3 · depth 26
• Points over ℚ̄ separate elements of a level PDivisibleGroup.eq_of_forall_point_toAlgHom_apply_eq 8 below · cited by 4 · depth 26
• Compatible normalised lifts of Dieudonné covector components PDivisibleGroup.exists_compatible_lift_coeff_eq_of_surjective_tower_zmodp 0 below · cited by 1 · depth 26
• Étale p-divisible towers over 𝔽ₚ lift to 𝒪 PDivisibleGroup.exists_formallyEtale_tower_bijective_baseChange_zmodp 9 below · cited by 1 · depth 26
• Tate module functoriality for a surjection of p-divisible groups PDivisibleGroup.exists_linearMap_tateModule_injective_of_surjective_comp_transition 0 below · cited by 1 · depth 26
• Complementary idempotents split a p-divisible group PDivisibleGroup.exists_pDivisibleGroup_surjective_bijective_tensorProduct_of_comp_eq_self 11 below · cited by 1 · depth 26
• Unit-root points factor through the maximal multiplicative quotient PDivisibleGroup.exists_point_toAlgHom_eq_comp_of_etale_cartierDual_of_forall_comp_eq_of_reduction_pow_eq_frobenius_conv_verschiebung 72 below · cited by 1 · depth 26
• Tate module of the points of a p-divisible group PDivisibleGroup.exists_tateModule_apply_eq_and_apply_eq_zero_iff_and_free_finrank_of_natCard_point_eq 0 below · cited by 8 · depth 26
• Connected–étale splitting of a p-divisible tower over Fₚ PDivisibleGroup.exists_tower_isLocalRing_isReduced_bijective_tensorProduct_comul_zmodp 39 below · cited by 3 · depth 26
• Frobenius kernels of a connected p-divisible group have order pⁿᵈ PDivisibleGroup.finrank_quotient_span_pow_augIdeal_eq_pow_of_isLocalRing 49 below · cited by 1 · depth 26
• Ordinarity of a p-divisible tower detected at level one PDivisibleGroup.forall_exists_bijective_tensorProduct_isReduced_cartierDual_of_level_one_zmodp 50 below · cited by 2 · depth 26
• Polynomials in U preserve S and commute with Galois PDivisibleGroup.forall_mem_adjoin_tateModule_apply_mem_and_comp_tateModuleRep_eq 1 below · cited by 1 · depth 26
• Freeness of the cotangent module of a p-divisible group PDivisibleGroup.free_cotangent_of_isArtinianRing_of_pow_eq_zero 27 below · cited by 1 · depth 26
• Kernel of the cotangent transition map and p^v-torsion PDivisibleGroup.ker_cotangentMap_eq_smul_top_and_smul_top_eq_bot 0 below · cited by 3 · depth 26
• pⁿ-torsion in G(L) is Gₙ(L) PDivisibleGroup.nsmul_eq_zero_iff_exists_pointsMkAdd_eq 0 below · cited by 1 · depth 26
• Base change of a p-divisible tower over a nonzero algebra PDivisibleGroup.surjective_and_finrank_and_ker_tensorProduct_map_transition 1 below · cited by 3 · depth 26
• Tate-module endomorphisms induced by families of level endomorphisms PDivisibleGroup.tateModule_induced_mem_and_comm_and_add_and_comp 0 below · cited by 2 · depth 26
• Formal group coordinates on a connected p-divisible tower over 𝔽ₚ PDivisibleGroup.exists_mvFormalGroup_ker_eq_span_nthSeries_jointly_injective_surjective_of_isLocalRing_zmodp 58 below · cited by 1 · depth 27
• Splitting a p-divisible group by complementary idempotents PDivisibleGroup.exists_surjective_injective_ker_eq_map_of_comp_eq_self_of_field 38 below · cited by 1 · depth 27
• Constancy of the cotangent dimension along the levels PDivisibleGroup.finrank_cotangent_augIdeal_eq_of_isLocalRing 1 below · cited by 1 · depth 27
• Order p^{vdim G} of the Frobenius kernel ker F^v PDivisibleGroup.finrank_level_quotient_span_pow_eq_pow_mul_finrank_cotangent_one 21 below · cited by 1 · depth 27
• Ordinarity of the ε-part of every level of the special fibre PDivisibleGroup.forall_exists_bijective_tensorProduct_isReduced_cartierDual_of_comp_eq_idempotent_of_reduction_pow_eq_frobenius_conv_verschiebung 62 below · cited by 1 · depth 27
• Frobenius descent: aᵖ∈ Jₙ₊₁ implies a∈ Jₙ PDivisibleGroup.mem_span_pow_augIdeal_of_pow_mem_of_isLocalRing 8 below · cited by 1 · depth 27
• Cotangent module of a p-divisible group is free of rank n PDivisibleGroup.nonempty_basis_cotangentModule_of_hasDimension 0 below · cited by 3 · depth 27
• Points of a p-divisible group are integral, Galois-equivariantly PDivisibleGroup.bijective_pointsMap_val_integralClosure_and_exists_tateModule_equiv 0 below · cited by 2 · depth 28
• Quotient of a p-divisible group by a closed subgroup PDivisibleGroup.exists_pDivisibleGroup_bialgHom_injective_range_eq_hopfKer_of_surjective_of_comp_eq_of_isPrincipalIdealRing 86 below · cited by 1 · depth 28
• Splitting a p-divisible group by complementary bialgebra idempotents over a field PDivisibleGroup.exists_pDivisibleGroup_surjective_bijective_tensorProduct_of_comp_eq_self_of_field 37 below · cited by 1 · depth 28
• Transfer of splitness between two quotient witnesses of a p-divisible group PDivisibleGroup.exists_retraction_of_points_ker_iff_of_points_surjective_of_retraction_of_isDiscreteValuationRing_of_liesOverPrime 239 below · cited by 1 · depth 28
• Power-series coordinates on a connected p-divisible tower over 𝔽ₚ PDivisibleGroup.exists_surjective_mvPowerSeries_comp_eq_of_isLocalRing_zmodp 53 below · cited by 1 · depth 28
• Frobenius kernel lies in the Verschiebung image on G[p] PDivisibleGroup.mem_span_pow_of_forall_pow_apply_eq_zero 6 below · cited by 1 · depth 28
• Residue-field points of a p-divisible level equal the counit PDivisibleGroup.ringHom_apply_eq_residue_counit_of_forall_point_valuation_sub_lt_one 1 below · cited by 1 · depth 28
• p Gⁱ⊆ Gⁱ⁺¹ on completed points of G PDivisibleGroup.cpointsProj_succ_nsmul_eq_zero_of_cpointsProj_eq_zero 1 below · cited by 1 · depth 29
• Tate full faithfulness over a henselian place ring of ℚ̄ PDivisibleGroup.existsUnique_bialgHom_family_of_addMonoidHom_points_levelPreserving_galois_of_isDiscreteValuationRing_of_liesOverPrime 238 below · cited by 1 · depth 29
• Galois descent for completed points: Tate's Proposition 11, Step 3 PDivisibleGroup.existsUnique_cpointsMap_ofId_eq_of_forall_smul_eq_of_forall_mem_range_iff 3 below · cited by 1 · depth 29
• Transitions map Hopf kernels onto Hopf kernels, over a local PID PDivisibleGroup.surjOn_transition_hopfKer_of_surjective_of_comp_eq_of_isPrincipalIdealRing 36 below · cited by 1 · depth 29
• Kernel of transition on Hopf kernel is p^v-torsion ideal PDivisibleGroup.transition_apply_eq_zero_iff_mem_torsionIdeal_hopfKer_of_surjective_of_comp_eq_of_isPrincipalIdealRing 63 below · cited by 1 · depth 29
• Tate's full faithfulness over a characteristic-zero field, points form PDivisibleGroup.existsUnique_bialgHom_family_of_addMonoidHom_points_levelPreserving_galois_of_field 12 below · cited by 1 · depth 30
• Tate's full faithfulness over mathcal O_K, points form PDivisibleGroup.existsUnique_bialgHom_family_of_addMonoidHom_points_levelPreserving_galois_of_ringOfIntegers 220 below · cited by 1 · depth 30
• Multiplication by p from level w+1 to level w PDivisibleGroup.exists_bialgHom_comp_transition_eq_nsmulBialgHom_and_injective_and_map_ker_counit_eq_torsionIdeal_and_faithfullyFlat 6 below · cited by 1 · depth 30
• Geometric points of a p-divisible group under field extension PDivisibleGroup.exists_mulEquiv_point_addEquiv_points_eq_pointMap_of_isAlgClosed 0 below · cited by 1 · depth 30
• Geometric points of a p-divisible group commute with base change PDivisibleGroup.exists_mulEquiv_point_baseChange_and_addEquiv_points_baseChange 0 below · cited by 1 · depth 30
• Kernel of reduction in G(𝒪) is p-divisible PDivisibleGroup.exists_nsmul_eq_of_forall_isNilpotent_cpointsProj_one_of_isIntegral_iff 9 below · cited by 1 · depth 30
• p^k-torsion completed points come from level-k points PDivisibleGroup.exists_toCPoints_pointsMkAdd_eq_of_nsmul_eq_zero_of_isIntegral_iff 0 below · cited by 1 · depth 30
• Transitions are surjective on Hopf kernels of a quotient map PDivisibleGroup.surjOn_transition_hopfKer_of_surjective_of_comp_eq 35 below · cited by 1 · depth 30
• Geometric points determine bialgebra maps of p-divisible groups PDivisibleGroup.eq_of_forall_toAlgHom_comp_eq_of_ringOfIntegers 10 below · cited by 1 · depth 31
• Multiplication by p on a p-divisible group is an isogeny of degree p^h PDivisibleGroup.exists_algEquiv_range_nsmulAlgHom_and_finite_projective_rankAtStalk 5 below · cited by 2 · depth 31
• Splitting of the Tate module of a height-h+h' group PDivisibleGroup.exists_linearEquiv_tateModule_prod_of_bialgHom_comp_transition_of_bijective_points 1 below · cited by 1 · depth 31
• Functoriality of Tate modules under additive maps of points PDivisibleGroup.exists_linearMap_tateModule_apply_eq_of_addMonoidHom_points 0 below · cited by 1 · depth 31
• Existence of the product of two p-divisible groups PDivisibleGroup.exists_prod_bialgHom_bijective_points 0 below · cited by 1 · depth 31
• Tate module bijectivity implies bijectivity at every level PDivisibleGroup.forall_bijective_of_bijective_linearMap_tateModule_of_ringOfIntegers 172 below · cited by 1 · depth 31
• Discriminant of a level of a p-divisible group over mathcal O_K PDivisibleGroup.associated_discr_level_of_hasDimension_of_ringOfIntegers 73 below · cited by 1 · depth 32
• Tate module determines the dimension of a p-divisible group PDivisibleGroup.eq_of_hasDimension_of_linearEquiv_tateModule_of_ringOfIntegers 103 below · cited by 1 · depth 32
• Jacobian determinant of a square presentation of Gᵥ PDivisibleGroup.associated_jacobianDet_pow_of_hasDimension_of_ringOfIntegers 3 below · cited by 1 · depth 33
• Square polynomial presentations of the levels of a p-divisible group over mathcal O_K PDivisibleGroup.exists_square_presentation_level_of_ringOfIntegers 50 below · cited by 1 · depth 33

PDivisibleGroup.CartierDuality 26

• Annihilator of a saturated Galois-stable submodule under a Tate pairing PDivisibleGroup.CartierDuality.exists_submodule_annihilator_stable_saturated_and_forall_mem_iff 15 below · cited by 1 · depth 24
• Galois-equivariant Tate module pairing from Cartier duality PDivisibleGroup.CartierDuality.exists_tateModule_pairing_eq_pair 1 below · cited by 4 · depth 24
• Cartier duality of p-divisible groups is symmetric PDivisibleGroup.CartierDuality.isCartierDual_symm 0 below · cited by 2 · depth 24
• Adjointness of Tate-module maps under Cartier pairings PDivisibleGroup.CartierDuality.tateModule_pairing_adjoint_and_ker_iff_and_surjective_of_pair_comp_eq 15 below · cited by 1 · depth 24
• Cartier duality of a morphism: transitions and pairing adjointness PDivisibleGroup.CartierDuality.transpose_comp_transition_eq_and_pair_comp_eq_pair_comp_transpose 0 below · cited by 1 · depth 24
• Perfectness of the Cartier pairing on Tate modules PDivisibleGroup.CartierDuality.bijective_tateModule_pairing_of_isAlgClosed 13 below · cited by 6 · depth 25
• Tate's period functionals: n invariant ℂₚ-functionals on the dual Tate module PDivisibleGroup.CartierDuality.exists_linearIndependent_invariant_dual_padicComplex_tateModule_of_hasDimension_of_ringOfIntegers 44 below · cited by 1 · depth 26
• Cartier-transpose Frobenius twist forces A to act by a scalar PDivisibleGroup.CartierDuality.moduleEnd_tateModuleRep_eq_smul_of_forall_point_comp_cartierTranspose_valuation_sub_pow_lt_one 16 below · cited by 1 · depth 26
• Cartier pairing equals 1 on étale-dual factors and formal points PDivisibleGroup.CartierDuality.pair_eq_one_of_eq_comp_of_etale_cartierDual_of_forall_valuation_sub_counit_lt_one 4 below · cited by 1 · depth 26
• Formal points pair trivially at an ordinary level PDivisibleGroup.CartierDuality.pair_eq_one_of_forall_valuation_sub_counit_lt_one_of_bijective_tensorProduct_isReduced 38 below · cited by 1 · depth 26
• Inertia acts on formal Tate vectors by the cyclotomic character PDivisibleGroup.CartierDuality.tateModuleRep_eq_cyclotomicCharacter_smul_of_mem_inertiaSubgroupIn_of_forall_pair_eq_one 17 below · cited by 1 · depth 26
• Frobenius on the ε-part of a Tate module via Cartier duality PDivisibleGroup.CartierDuality.tateModule_pairing_rep_eq_cyclotomicCharacter_smul_pairing_of_isFrobeniusAt_of_comp_transition_of_forall_comp_eq_of_forall_valuation_sub_pow_lt_one 2 below · cited by 1 · depth 26
• Existence of Tate's period maps dαⱼ over 𝒪_K PDivisibleGroup.CartierDuality.exists_addMonoidHom_tateModule_padicComplex_smul_eq_and_norm_sub_le_of_ringOfIntegers 6 below · cited by 1 · depth 27
• Tate's relation dim G+dim G'=h under Cartier duality PDivisibleGroup.CartierDuality.finrank_cotangent_one_add_finrank_cotangent_one_eq_height 13 below · cited by 2 · depth 27
• Cartier transpose as Frobenius on integral ε-supported points PDivisibleGroup.CartierDuality.forall_point_valuation_cartierTranspose_sub_pow_lt_one_of_comp_eq_comp_verschiebung_of_bijective_tensorProduct_zmodp 7 below · cited by 1 · depth 27
• Independence over K of Hodge–Tate period coordinates PDivisibleGroup.CartierDuality.linearIndependent_tateModule_padicComplex_of_norm_sub_le_of_ringOfIntegers 40 below · cited by 1 · depth 27
• Cartier transpose is adjoint for the Cartier pairing on points PDivisibleGroup.CartierDuality.pair_comp_eq_pair_comp_cartierTranspose 0 below · cited by 1 · depth 27
• Triviality of all Cartier pairings forces a completed point to vanish PDivisibleGroup.CartierDuality.cpoints_eq_zero_of_forall_pair_eq_one_of_forall_mem_range_iff 36 below · cited by 1 · depth 28
• Exponential of a p-divisible group and the Cartier pairing PDivisibleGroup.CartierDuality.exists_addMonoidHom_tangentSpace_cpoints_pair_eq_sum_pow_of_ker_cotangentModuleProj_eq 1 below · cited by 1 · depth 28
• Hodge–Tate family attached to Tate-module points of the Cartier dual PDivisibleGroup.CartierDuality.exists_addMonoidHom_tateModule_apply_eq_charDiff 1 below · cited by 1 · depth 28
• Character element of a dual point: multiplicativity, naturality, tower compatibility PDivisibleGroup.CartierDuality.charElem_mul_and_charDiff_mul_and_lTensor_cotangentMap_charDiff 0 below · cited by 1 · depth 29
• Tate's pairing kernel: torsion-free and p-divisible part PDivisibleGroup.CartierDuality.nsmul_mem_and_eq_zero_and_exists_nsmul_eq_of_forall_pair_eq_one_of_isIntegral_iff 28 below · cited by 1 · depth 29
• Cartier pairing is perfect on K-points, K algebraically closed of characteristic 0 PDivisibleGroup.CartierDuality.eq_one_of_forall_pair_eq_one_and_exists_pair_eq_of_isAlgClosed 12 below · cited by 2 · depth 30
• Tate's map α from points to dual Tate module characters PDivisibleGroup.CartierDuality.exists_points_tateModule_pairing_eq_pair 1 below · cited by 1 · depth 30
• Double annihilators and Tate-module lifting for Cartier-dual pairings PDivisibleGroup.CartierDuality.mem_of_forall_pair_eq_one_and_exists_tateModule_forall_pair_eq_one 13 below · cited by 1 · depth 30
• Points reducing to the identity mod pⁱ pair trivially PDivisibleGroup.CartierDuality.pair_pointMap_eq_one_of_forall_isNilpotent_of_isIntegral_iff 11 below · cited by 1 · depth 30

PDivisibleGroup.Hopf 6

• Multiplication by n on a bialgebra commutes with base change PDivisibleGroup.Hopf.map_id_nsmulAlgHom_eq_nsmulAlgHom_baseChange 0 below · cited by 5 · depth 23
• Iterated transitions in a p-divisible tower of Hopf algebras PDivisibleGroup.Hopf.exists_forall_comp_transition_surjective_ker_eq_torsionIdeal 0 below · cited by 7 · depth 24
• Multiplication by n acts as n on I/I² PDivisibleGroup.Hopf.nsmulAlgHom_sub_nsmul_mem_augIdeal_sq 0 below · cited by 5 · depth 25
• Existence of the Verschiebung over 𝔽ₚ PDivisibleGroup.Hopf.exists_verschiebung_algHom_zmodp 1 below · cited by 7 · depth 27
• Multiplication by p in coordinates: V∘ F formula PDivisibleGroup.Hopf.nsmulAlgHom_eq_sum_pow_apply_smul_pow 0 below · cited by 2 · depth 28
• Higher Leibniz rule for convolution powers of a primitive functional PDivisibleGroup.Hopf.convPow_apply_mul_eq_sum_of_apply_mul_eq 0 below · cited by 1 · depth 29

PDivisibleGroup.IsCartierDual 1

• Cartier duality of p-divisible groups is stable under base change PDivisibleGroup.IsCartierDual.baseChange 1 below · cited by 1 · depth 27

PDivisibleGroup.Tower 8

• Shifted Hopf-kernel tower is a p-divisible group of height h' PDivisibleGroup.Tower.exists_tower_hopfKer_transitionLE_of_bijOn_hopfKer 45 below · cited by 1 · depth 25
• Transitions map Hopf kernels onto Hopf kernels in a tower PDivisibleGroup.Tower.map_hopfKer_transitionLE_succ_eq 34 below · cited by 1 · depth 26
• Exactness of the Hopf-kernel tower: Γᵥ=Γᵥ₊₁[p^v] PDivisibleGroup.Tower.transition_apply_eq_zero_iff_mem_span_nsmulAlgHom_image_of_bijOn_hopfKer_of_isPrincipalIdealRing 37 below · cited by 1 · depth 26
• Reduced Cartier duals propagate up a p-divisible tower over 𝔽ₚ PDivisibleGroup.Tower.forall_isReduced_cartierDual_of_isReduced_cartierDual_one_zmodp 13 below · cited by 2 · depth 27
• Frobenius cancellation for endomorphisms of a p-divisible tower PDivisibleGroup.Tower.eq_of_frobenius_comp_eq_zmodp 9 below · cited by 1 · depth 28
• Split idempotent subtower of a p-divisible tower over 𝔽ₚ PDivisibleGroup.Tower.surjective_and_exists_finrank_eq_and_ker_eq_torsionIdeal_of_comp_eq_idempotent_zmodp 38 below · cited by 1 · depth 28
• Tate's sequence 0→ Gᵤ→ Gᵥ₊ᵤ→ Gᵥ→ 0 for towers PDivisibleGroup.Tower.exists_algEquiv_range_nsmulAlgHom_and_finite_projective_rankAtStalk 5 below · cited by 1 · depth 29
• Kernel of [p]^* equals kernel of the transition map PDivisibleGroup.Tower.nsmulAlgHom_apply_eq_zero_iff_transition_apply_eq_zero_zmodp 6 below · cited by 1 · depth 29