← all areas

Namespace MvFormalGroup 166 theorems

— 86 · ArtinHasse 3 · BigWittLaw 12 · CartierModule 47 · Deformation 7 · End 1 · Hom 6 · IsSymmTwoCocycle 1 · Points 1 · WittLaw 2

directly in MvFormalGroup 86

• Integral rescaled exponential under a local Cartier dual MvFormalGroup.exists_rescaledExp_tendsto_zero_of_isLocalRing_cartierDual 25 below · cited by 1 · depth 21
• Existence of a rescaled logarithm over p-adically complete rings MvFormalGroup.exists_rescaledLog_of_isAdicComplete 2 below · cited by 1 · depth 21
• Box truncations of the logarithm lie in p^vY at w' MvFormalGroup.eventually_aeval_boxTrunc_mem_of_forall_adicEval_scaledLogTrunc_mem 0 below · cited by 1 · depth 22
• Integral rescaled exponential for unipotent p^v-torsion, case p=2 MvFormalGroup.exists_rescaledExp_tendsto_zero_of_isLocalRing_cartierDual_of_eq_two 22 below · cited by 1 · depth 22
• Rescaled exponential with p-adically vanishing coefficients, p odd MvFormalGroup.exists_rescaledExp_tendsto_zero_of_ne_two 2 below · cited by 1 · depth 22
• Integrality of the rescaled logarithm of a commutative formal group MvFormalGroup.natCast_mul_coeff_add_single_mem_span_pow_degree_of_subst_rescale_eq_add 0 below · cited by 9 · depth 22
• Mod p congruence between iterated-law and [p] coefficients MvFormalGroup.coeff_iterate_sum_single_sub_coeff_nthSeries_single_mem_span 0 below · cited by 2 · depth 23
• Mixed quadratic coefficients of F and its rescaled logarithm MvFormalGroup.coeff_mul_natCast_add_two_mul_coeff_rescaledLog_eq_zero 0 below · cited by 1 · depth 23
• Rescaled logarithm modulo p: degree ≥ 3 and mixed quadratic coefficients MvFormalGroup.coeff_rescaledLog_mem_span_of_three_le_degree 1 below · cited by 1 · depth 23
• Sub-unit slope bound for the logarithm under nilpotent Hasse–Witt MvFormalGroup.exists_coeff_mem_span_pow_sub_log_of_isNilpotent_hasseWitt 4 below · cited by 2 · depth 23
• Formal inverse function theorem over a commutative ring MvFormalGroup.exists_subst_eq_X_of_linearPart_eq_one 0 below · cited by 16 · depth 23
• Nilpotence of the Hasse–Witt matrix of [p]_F MvFormalGroup.isNilpotent_hasseWittMatrix_nthSeries_of_isLocalRing_cartierDual 11 below · cited by 2 · depth 23
• Denominators of the formal exponential divide m! MvFormalGroup.prod_factorial_mul_coeff_mem_span_pow_of_subst_eq_X 0 below · cited by 1 · depth 23
• Algebra maps into J-adically complete rings are adic evaluation MvFormalGroup.algHom_apply_eq_adicEval_of_forall_apply_X_mem_radical 0 below · cited by 22 · depth 24
• Additivity defect of the truncated logarithm covector MvFormalGroup.coeff_map_subst_sub_map_sub_map_mem_of_forall_coeff_ghostComponent_eq_logCovector 9 below · cited by 1 · depth 24
• Top-window stability of truncated logarithm covectors MvFormalGroup.coeff_sub_coeff_mem_of_forall_coeff_ghostComponent_eq_logCovector_of_le 8 below · cited by 1 · depth 24
• Hasse–Witt relation for point derivations on the Cartier dual MvFormalGroup.exists_cartierDual_derivation_pow_eq_sum_hasseWitt_smul 9 below · cited by 1 · depth 24
• Nilpotent Hasse–Witt matrix kills low-degree coefficients of [p^A]_F MvFormalGroup.exists_forall_coeff_nthSeries_pow_mem_span_of_isNilpotent_hasseWitt 2 below · cited by 1 · depth 24
• Cocommutativity from a commutative formal group law MvFormalGroup.isCocomm_of_comul_eq_adicEval_toPowerSeries 1 below · cited by 1 · depth 24
• Uniqueness of a point derivation from its values on coordinates MvFormalGroup.cartierDual_eq_of_forall_apply_tmul_eq_of_map_mul 0 below · cited by 1 · depth 25
• Convolution powers of a point derivation as iterated invariant derivatives MvFormalGroup.cartierDual_pow_apply_tmul_eq_algebraMap_constantCoeff_iterate 3 below · cited by 1 · depth 25
• Far Witt components of the logarithm lie in (p)+(X)^E MvFormalGroup.coeff_mem_span_sup_pow_of_forall_coeff_ghostComponent_eq_logCovector_of_slope 7 below · cited by 1 · depth 25
• Multiplication by p^ν when the Hasse–Witt matrix is ν-nilpotent MvFormalGroup.coeff_nthSeries_pow_eq_zero_of_hasseWitt_pow_eq_zero_zmodp 1 below · cited by 1 · depth 25
• Iterated invariant derivation at the origin as a multilinear coefficient MvFormalGroup.coeff_subst_iterate_sum_single_eq_constantCoeff_invariantDerivation_iterate 0 below · cited by 1 · depth 25
• Vanishing of the counit on formal group coordinates MvFormalGroup.counit_apply_eq_zero_of_comul_eq_adicEval 0 below · cited by 3 · depth 25
• Coordinate point derivations in the Cartier dual of 𝔽ₚ ⊗ R MvFormalGroup.exists_cartierDual_apply_tmul_eq_and_map_mul_of_ker_eq_span_nthSeries 3 below · cited by 1 · depth 25
• Additivity defect of a scaled logarithm truncation MvFormalGroup.lt_degree_and_natCast_mul_coeff_subst_sub_sub_mem_of_scaledLogTrunc 2 below · cited by 1 · depth 25
• Characteristic p: homomorphism with zero differential is a series in Xᵖ MvFormalGroup.coeff_eq_zero_of_linearPart_eq_zero_of_subst_eq_charP 0 below · cited by 9 · depth 26
• Natural group laws on p-adic test algebras come from a unique commutative formal group MvFormalGroup.existsUnique_isComm_and_apply_eq_adicEval_toPowerSeries_of_natural_of_mem_radical 1 below · cited by 1 · depth 26
• Nilpotent tuples lie in ker[p^v] for large v MvFormalGroup.exists_algHom_apply_eq_of_isNilpotent_of_ker_eq_span_nthSeries 0 below · cited by 1 · depth 26
• Twisted tower from a formal group and a 2-cocycle MvFormalGroup.exists_pDivisibleTower_of_cocycle 29 below · cited by 1 · depth 26
• Functorial group law on nilpotents is a unique commutative formal group MvFormalGroup.existsUnique_isComm_and_apply_eq_adicEval_toPowerSeries_of_natural 0 below · cited by 1 · depth 27
• One level of the cocycle-twisted p-divisible tower MvFormalGroup.exists_hopfAlgebra_presentation_comul_eq_of_cocycle_of_powerDefect 24 below · cited by 1 · depth 27
• Linear re-coordinatisation of a formal-group presentation MvFormalGroup.exists_isComm_comp_substAlgHom_of_isUnit_matrix 0 below · cited by 1 · depth 27
• Power defects of a symmetric 2-cocycle over a p-divisible tower MvFormalGroup.exists_powerDefect_map_comul_eq_adicEval_of_cocycle 1 below · cited by 1 · depth 27
• Transition maps for the twisted Tate tower of height h+hₑ MvFormalGroup.exists_transition_ker_eq_torsionIdeal_of_presentation_of_powerDefect 4 below · cited by 1 · depth 27
• First-order Taylor expansion for adic evaluation of power series MvFormalGroup.adicEval_add_sub_adicEval_sub_sum_mul_mem_span_sq 0 below · cited by 4 · depth 28
• Fibres of [p^v]_Φ are free of rank p^{vh} MvFormalGroup.free_and_finrank_quotient_span_nthSeries_sub_C_eq_pow_of_nontrivial 21 below · cited by 1 · depth 28
• Descent of kernel-invariant power series along an isogeny over a field MvFormalGroup.exists_eq_subst_of_subst_toPowerSeries_sub_mem_span_of_X_pow_mem_span_of_field 10 below · cited by 1 · depth 29
• Freeness of 𝒪[[X]] under [p^v]_Φ-substitution MvFormalGroup.exists_forall_existsUnique_eq_sum_subst_nthSeries_mul_of_finrank_eq_pow 18 below · cited by 1 · depth 29
• Functorial nilpotent-point criterion for ideal membership in B[[X]] MvFormalGroup.mem_span_of_forall_nilEval_eq_zero 1 below · cited by 15 · depth 29
• Truncated evaluation of a coordinate Xᵢ on a nilpotent tuple MvFormalGroup.nilEval_X_of_mem 0 below · cited by 20 · depth 29
• Truncated and J-adic evaluation agree when Jⁿ⁺¹=0 MvFormalGroup.nilEval_eq_adicEval_of_pow_succ_eq_bot 0 below · cited by 27 · depth 29
• Nil-evaluation of the [m]-series as an iterated formal sum MvFormalGroup.nilEval_nthSeries_eq_iterate_nilMul 2 below · cited by 4 · depth 29
• Truncated evaluation at nilpotents commutes with substitution MvFormalGroup.nilEval_subst_of_mem 0 below · cited by 48 · depth 29
• Natural additive maps on nilpotent points come from a unique homomorphism MvFormalGroup.existsUnique_hom_apply_eq_adicEval_of_natural_of_isNilpotent 0 below · cited by 6 · depth 30
• Finite freeness of rank p^{vh} of 𝒪[[X]]/([p^v]_F) MvFormalGroup.finite_free_finrank_quotient_span_nthSeries_of_finrank_eq_pow 11 below · cited by 1 · depth 30
• Rank of [p^v]_F is p^{vh} for a formal group of height h MvFormalGroup.finrank_quotient_span_nthSeries_pow_eq_pow 6 below · cited by 5 · depth 30
• Yoneda: natural group laws on nilpotent ideals are formal group laws MvFormalGroup.existsUnique_isComm_and_apply_eq_adicEval_of_natural_of_isNilpotent 0 below · cited by 1 · depth 31
• Finite p-power codimension of the [p]-series forces characteristic p MvFormalGroup.charP_of_finrank_quotient_span_nthSeries_eq_pow 3 below · cited by 1 · depth 32
• Rigidity of formal group laws along a nilpotent thickening MvFormalGroup.subst_nthSeries_eq_of_map_eq_and_exists_hom_of_ker_pow_eq_bot 0 below · cited by 4 · depth 32
• Symmetric 2-cocycles span: at most h-n classes modulo coboundaries MvFormalGroup.exists_isSymmTwoCocycle_span_of_finrank_quotient_span_nthSeries_eq_pow 31 below · cited by 3 · depth 33
• Glueing formal group laws along a cartesian square of rings MvFormalGroup.exists_map_eq_and_existsUnique_hom_of_pullback_of_surjective 1 below · cited by 4 · depth 33
• First-order deformations of a commutative formal group are ε-translates by symmetric 2-cocycles MvFormalGroup.exists_toPowerSeries_eq_subst_eps_smul_and_exists_isSymmTwoCocycle_of_map_fstHom_eq 0 below · cited by 4 · depth 33
• Injectivity of substitution along an isogeny, and descent MvFormalGroup.subst_injective_and_exists_eq_subst_of_subst_toPowerSeries_sub_mem_span_of_X_pow_mem_span 23 below · cited by 3 · depth 33
• First-order deformations in translation form: uniqueness, additivity, coboundaries MvFormalGroup.translate_injective_and_exists_hom_iff_exists_addCoboundary 0 below · cited by 3 · depth 33
• No nonzero homomorphism from a finite-height formal group to Gₐ MvFormalGroup.eq_zero_of_addCoboundary_eq_zero_of_finrank_quotient_span_nthSeries_eq_pow 6 below · cited by 2 · depth 34
• Descent of translation-invariant power series along a formal isogeny MvFormalGroup.exists_eq_subst_of_subst_toPowerSeries_sub_mem_span_of_X_pow_mem_span 19 below · cited by 2 · depth 34
• At most h symmetric 2-cocycles span the rigidified ones MvFormalGroup.exists_isSymmTwoCocycle_rigidified_span_of_finrank_quotient_span_nthSeries_eq_pow 29 below · cited by 1 · depth 34
• At most h-n independent primitives modulo [p]_F MvFormalGroup.exists_add_le_and_forall_exists_sub_sum_smul_mem_span_nthSeries_of_addCoboundary_mem_span 26 below · cited by 1 · depth 35
• Descent along an isogeny of formal groups: local Noetherian base MvFormalGroup.exists_eq_subst_of_subst_toPowerSeries_sub_mem_span_of_X_pow_mem_span_of_isLocalRing 15 below · cited by 1 · depth 35
• Tangent space bound d(h-d) for first-order deformations MvFormalGroup.finrank_firstOrderDeformations_le_mul_sub 39 below · cited by 1 · depth 35
• Unique descent of F[m]-invariant power series along [m]_F MvFormalGroup.existsUnique_eq_subst_nthSeries_of_sub_mem_span 6 below · cited by 1 · depth 36
• Arbitrary structure constants arise from a Cartier-module V-basis MvFormalGroup.exists_cartierModule_vBasis_of_frobenius_expansion 13 below · cited by 2 · depth 36
• Spanning first-order deformations of a formal group of height h MvFormalGroup.exists_deformations_dualNumber_span_of_finrank_quotient_span_nthSeries_eq_pow 34 below · cited by 1 · depth 36
• Normalising tangents of a V-basis by coordinate change MvFormalGroup.exists_hom_comp_eq_id_tangent_map_eq_of_isUnit_det 0 below · cited by 2 · depth 36
• Transport of a formal group law along a square-zero coordinate change MvFormalGroup.exists_hom_toPowerSeries_eq_add_sum_smul_of_mul_eq_zero 3 below · cited by 3 · depth 36
• Hopf algebra structure on the n-torsion of a formal group MvFormalGroup.exists_hopfAlgebra_ker_eq_span_nthSeries_comul_eq_adicEval_of_isAdicComplete 3 below · cited by 1 · depth 36
• Uniqueness of the quotient by a finite formal kernel MvFormalGroup.exists_isLawHom_comp_eq_of_span_range_eq_of_hasKernelOfDegree_of_isComm 28 below · cited by 1 · depth 36
• Tate's inequality dim_k P(𝒪(F[p])) + n ≤ h MvFormalGroup.finrank_primitives_add_le_of_ker_eq_span_nthSeries_of_finrank_eq_pow 23 below · cited by 1 · depth 36
• Multiples of a J^k-point of a formal group MvFormalGroup.iterate_nilMul_sub_natCast_mul_mem_pow 0 below · cited by 1 · depth 36
• Explicit description of first-order deformation coboundaries MvFormalGroup.mem_firstOrderCoboundaries_iff 4 below · cited by 2 · depth 36
• First-order cocycles as symmetric solutions of linearised associativity MvFormalGroup.mem_firstOrderCocycles_iff 3 below · cited by 2 · depth 36
• Primitive series modulo p-th powers for a formal group law MvFormalGroup.mem_span_X_pow_of_addCoboundary_mem_span_of_coeff_single_eq_zero 1 below · cited by 1 · depth 36
• Frobenius on the Cartier dual is dual to Verschiebung MvFormalGroup.cartierDual_pow_apply_eq_finsum_coeff_subst_mul_apply_pow 0 below · cited by 1 · depth 37
• Universal p-typical law with variables as structure constants MvFormalGroup.exists_cartierModule_vBasis_mvPolynomial_X 12 below · cited by 1 · depth 37
• Deformations over dual numbers spanned by nr explicit ones MvFormalGroup.exists_deformations_dualNumber_span_of_forall_isSymmTwoCocycle 1 below · cited by 1 · depth 37
• Endomorphisms with vanishing linear part factor through Frobenius MvFormalGroup.exists_eq_subst_X_pow_of_linearPart_eq_zero 1 below · cited by 1 · depth 37
• Descent of symmetric 2-cocycles along a finite endomorphism MvFormalGroup.exists_eq_subst_and_eq_addCoboundary_of_subst_eq_addCoboundary_of_mem_span 6 below · cited by 1 · depth 37
• Vanishing in Q ⊗_S Q versus membership in (I(x), I(y)) MvFormalGroup.map_mkQ_adicEval_sumElim_tmul_eq_zero_iff_mem_span_image_subst 0 below · cited by 1 · depth 37
• V-basis with variable structure constants from a functional-equation logarithm MvFormalGroup.exists_cartierModule_vBasis_mvPolynomial_X_of_log 7 below · cited by 1 · depth 38
• Truncated formal group law as a finite Hopf algebra, nilpotent case MvFormalGroup.exists_hopfAlgebra_surjective_ker_eq_span_nthSeries_comul_eq_adicEval_bot_of_isNilpotent 1 below · cited by 1 · depth 38
• Commutative law with functional-equation logarithm over ℚₚ[V] MvFormalGroup.exists_isComm_log_mvPolynomial_padic 1 below · cited by 1 · depth 38
• Functional-equation integrality for the universal p-typical law MvFormalGroup.exists_map_padicInt_eq_of_log 0 below · cited by 1 · depth 38
• Commutativity of a formal group law descends along injective base change MvFormalGroup.isComm_of_isComm_map_of_injective 0 below · cited by 1 · depth 38
• Last-factor form of the logarithm recursion over ℚₚ MvFormalGroup.smul_logCoeff_eq_sum_mul_map_iterate_of_smul_logCoeff_eq_sum_map_iterate_mul 0 below · cited by 1 · depth 39

MvFormalGroup.ArtinHasse 3

• Artin–Hasse family carries Witt addition to big Witt addition MvFormalGroup.ArtinHasse.subst_addFam_fam 1 below · cited by 1 · depth 32
• Artin–Hasse series equals expbigl(sum_m X^{p^m}/p^mbigr) MvFormalGroup.ArtinHasse.map_series_eq_map_exp_subst 0 below · cited by 6 · depth 33
• Artin–Hasse coordinates are additive over a ℤₚ-algebra MvFormalGroup.ArtinHasse.subst_addFam_map_coord 1 below · cited by 3 · depth 36

MvFormalGroup.BigWittLaw 12

• Every curve arises from a big Witt homomorphism MvFormalGroup.BigWittLaw.exists_hom_subst_curveFam_eq 0 below · cited by 4 · depth 32
• Low-weight coefficients vanish for big-Witt homomorphisms MvFormalGroup.BigWittLaw.coeff_eq_zero_of_coeff_subst_pow_eq_zero 0 below · cited by 1 · depth 36
• Cartier's first theorem, ω-curve form MvFormalGroup.BigWittLaw.exists_hom_subst_pow_eq 1 below · cited by 1 · depth 36
• Cartier splitting of the big Witt law over a ℤₚ-algebra MvFormalGroup.BigWittLaw.exists_proj_trunc_genSeries_eq_trunc_prod_of_algebra_padicInt 2 below · cited by 1 · depth 36
• Frobenius family mathbf Fₙ is additive for the big Witt law MvFormalGroup.BigWittLaw.subst_addFam_frobFam 0 below · cited by 1 · depth 36
• Additivity of `projFam` and splitting of Artin–Hasse MvFormalGroup.BigWittLaw.subst_addFam_projFam_and_subst_artinHasse_projFam 2 below · cited by 1 · depth 36
• Verschiebung commutes with the big Witt addition law MvFormalGroup.BigWittLaw.subst_addFam_verschiebungFam 0 below · cited by 1 · depth 36
• Artin–Hasse coordinates intertwine the big Witt and Witt Frobenii MvFormalGroup.BigWittLaw.subst_artinHasse_frobFam 1 below · cited by 1 · depth 36
• Artin–Hasse projector kills non-p-power Frobenii, commutes with mathbf Fₚ MvFormalGroup.BigWittLaw.subst_artinHasse_projFam_frobFam 1 below · cited by 1 · depth 36
• Difference of two big Witt homomorphisms agreeing to order n MvFormalGroup.BigWittLaw.subst_elim_negSeries_hom_and_coeff_eq_zero 0 below · cited by 1 · depth 36
• Frobenius mathbf Fₙ of the big Witt law on ω-curves MvFormalGroup.BigWittLaw.subst_pow_subst_frobFam 0 below · cited by 1 · depth 36
• The ω-curve of f∘π is the standard curve of f MvFormalGroup.BigWittLaw.subst_pow_subst_projFam 0 below · cited by 1 · depth 36

MvFormalGroup.CartierModule 47

• Faithfulness of the Cartier module functor in characteristic p MvFormalGroup.CartierModule.eq_of_map_eq 5 below · cited by 5 · depth 30
• Fullness of the Cartier module functor over a perfect field MvFormalGroup.CartierModule.exists_hom_map_eq_of_perfectRing 10 below · cited by 3 · depth 30
• Degree formula: colength of the Cartier module of an isogeny MvFormalGroup.CartierModule.length_quotient_range_mapLinear_eq_of_finrank_eq_pow 22 below · cited by 4 · depth 30
• Injectivity on Cartier modules for finite-kernel homomorphisms MvFormalGroup.CartierModule.map_injective_of_finite_quotient 0 below · cited by 16 · depth 30
• Kernel of the tangent map is V M in characteristic p MvFormalGroup.CartierModule.tangent_eq_zero_iff_exists_verschiebung_eq 1 below · cited by 13 · depth 30
• Unique finite V-expansion along a tangent basis MvFormalGroup.CartierModule.existsUnique_eq_sum_verschiebung_homothety_add 2 below · cited by 3 · depth 31
• V-adic completeness of the Cartier module of a formal group MvFormalGroup.CartierModule.existsUnique_forall_eq_sum_range_verschiebung_iterate_add 0 below · cited by 3 · depth 31
• Approximate exactness of the Cartier presentation map MvFormalGroup.CartierModule.exists_forall_le_order_coeff_sub_of_forall_le_order_presPi 1 below · cited by 1 · depth 31
• Cokernel of π_* on Cartier modules has rank rank dρ MvFormalGroup.CartierModule.nonempty_basis_quotient_span_range_map_of_comp_eq_X_pow 7 below · cited by 2 · depth 31
• Surjectivity of the tangent map of a Cartier module MvFormalGroup.CartierModule.tangent_surjective 3 below · cited by 7 · depth 31
• V-adic completeness and separatedness of the Cartier module MvFormalGroup.CartierModule.existsUnique_forall_eq_sum_range_verschiebungInt_iterate_add 0 below · cited by 22 · depth 32
• Cartier relation points lie in the kernel of Pi_f MvFormalGroup.CartierModule.presPi_verPt_sub_sum_teichPt_frobPt_eq_presPi_frobPt_iterate 0 below · cited by 1 · depth 32
• Freeness of the Cartier module of a height-h formal group MvFormalGroup.CartierModule.nonempty_basis_of_finrank_eq_pow 29 below · cited by 1 · depth 33
• Faithfulness of the Cartier module functor over ℤₚ-algebras MvFormalGroup.CartierModule.eq_of_forall_map_eq_of_algebra_padicInt 7 below · cited by 7 · depth 34
• Unique finite V-expansion along a tangent basis MvFormalGroup.CartierModule.existsUnique_eq_sum_verschiebungInt_iterate_homothety_add 17 below · cited by 11 · depth 34
• Cartier module modulo p is free of rank h MvFormalGroup.CartierModule.nonempty_basis_quotient_smul_top_of_finrank_eq_pow 25 below · cited by 2 · depth 34
• V-reducedness of the Cartier module over a ℤₚ-algebra MvFormalGroup.CartierModule.tangent_eq_zero_iff_exists_verschiebungInt_eq 15 below · cited by 3 · depth 34
• Cartier's tangent map: surjectivity and kernel VM MvFormalGroup.CartierModule.tangent_surjective_and_tangent_eq_zero_iff_exists_verschiebung_eq 6 below · cited by 2 · depth 34
• Surjectivity of the tangent map of a Cartier module MvFormalGroup.CartierModule.tangent_surjective_of_algebra_padicInt 2 below · cited by 5 · depth 34
• Height equals dimension plus codimension, Cartier module form MvFormalGroup.CartierModule.exists_add_eq_and_nonempty_basis_quotient_span_frobenius_of_finrank_eq_pow 24 below · cited by 1 · depth 35
• Zero tangent vector implies being a Verschiebung value MvFormalGroup.CartierModule.exists_verschiebungInt_eq_of_tangent_eq_zero_of_algebra_padicInt 14 below · cited by 4 · depth 35
• Frobenius image in M/pM is free of rank d MvFormalGroup.CartierModule.nonempty_basis_span_frobenius_of_finite_quotient 7 below · cited by 2 · depth 35
• Homomorphisms agreeing on p-typical curves agree on all curves MvFormalGroup.CartierModule.subst_curve_eq_of_forall_map_eq_of_algebra_padicInt 5 below · cited by 1 · depth 35
• Cartier module over a ℤₚ-algebra is reduced MvFormalGroup.CartierModule.verschiebungInt_injective_and_tangent_surjective_and_ker_and_complete_of_algebra_padicInt 19 below · cited by 4 · depth 35
• Injectivity of Verschiebung over a ℤₚ-algebra MvFormalGroup.CartierModule.verschiebungInt_injective_of_algebra_padicInt 1 below · cited by 13 · depth 35
• Cartier module elements are determined by their curves MvFormalGroup.CartierModule.curve_injective_of_algebra_padicInt 0 below · cited by 1 · depth 36
• Cartier modules: maps determined by a V-basis MvFormalGroup.CartierModule.existsUnique_addMonoidHom_apply_eq_of_frobenius_expansion 25 below · cited by 7 · depth 36
• Unique finite V-adic expansion in characteristic p MvFormalGroup.CartierModule.existsUnique_eq_sum_verschiebungInt_iterate_homothety_add_of_charP 2 below · cited by 2 · depth 36
• Weight-adic convergence of sums in the Cartier module MvFormalGroup.CartierModule.exists_forall_coeff_sub_sum_eq_zero 0 below · cited by 1 · depth 36
• Cartier module maps commuting with F, V, ⟨ a⟩ are induced MvFormalGroup.CartierModule.exists_hom_forall_map_eq_of_algebra_padicInt 22 below · cited by 7 · depth 36
• Cartier presentation: a homomorphism matching prescribed curves MvFormalGroup.CartierModule.exists_hom_forall_map_eq_of_forall_frobenius_eq_sum_verschiebungInt_iterate_smul 3 below · cited by 2 · depth 36
• Graded Frobenius expansion yields a ℤ_{p²}-action on Φ MvFormalGroup.CartierModule.exists_zp2Action_of_graded_frobenius_expansion 9 below · cited by 1 · depth 36
• Cokernel of a degree p^e isogeny on Cartier modules MvFormalGroup.CartierModule.nonempty_basis_quotient_span_range_map_of_finrank_eq_pow 22 below · cited by 1 · depth 36
• The varpi-relation passes to varpi f, and varpi g ≡ p f MvFormalGroup.CartierModule.varpiTuple_rel_and_sum_eq_of_rel 0 below · cited by 1 · depth 36
• Cartier presentation: relations to every order over arbitrary base MvFormalGroup.CartierModule.exists_forall_le_order_coeff_sub_and_frobIntPt_iterate_of_forall_le_order_presPi 1 below · cited by 1 · depth 37
• Homomorphism of formal groups from matching V-adic expansions MvFormalGroup.CartierModule.exists_hom_forall_map_eq_of_forall_frobenius_eq_sum_verschiebungInt_iterate_homothety_add 4 below · cited by 3 · depth 37
• Universal Teichmüller-digit normal form in Cartier modules MvFormalGroup.CartierModule.exists_sum_verschiebungInt_iterate_smul_eq_sum_homothety_teichmuellerDigit_add 0 below · cited by 1 · depth 37
• Twisting a graded F-expansion by Frobenius-exchanged Witt scalars MvFormalGroup.CartierModule.frobenius_smul_eq_of_graded_frobenius_expansion_of_frobenius_eq 0 below · cited by 1 · depth 37
• Base change of a V-basis with structure constants MvFormalGroup.CartierModule.isUnit_det_tangent_and_frobenius_expansion_baseChange 0 below · cited by 2 · depth 37
• Presentation map kills Cartier relation points up to remainder MvFormalGroup.CartierModule.presPi_verPt_sub_sum_wittSMulPt_frobIntPt_eq_presPi_frobIntPt_iterate 0 below · cited by 1 · depth 38
• Descent of a Cartier element with ghost logarithm MvFormalGroup.CartierModule.exists_baseChange_eq_of_coeff_subst_eq_ghost_of_functionalEquation 1 below · cited by 1 · depth 39
• Verschiebung is topologically nilpotent in finite height MvFormalGroup.CartierModule.exists_forall_iterate_verschiebung_eq_smul_of_finrank_eq_pow 15 below · cited by 1 · depth 39
• Cartier module elements with prescribed ghost logarithm MvFormalGroup.CartierModule.exists_tangent_eq_and_coeff_subst_eq_ghost_of_log 1 below · cited by 1 · depth 39
• Injectivity of Verschiebung when p is nilpotent MvFormalGroup.CartierModule.verschiebungInt_injective_of_isNilpotent 0 below · cited by 3 · depth 39
• Base change of Cartier modules along a surjection is surjective MvFormalGroup.CartierModule.baseChange_surjective_of_surjective 18 below · cited by 2 · depth 41
• Cartier modules are exact along a Milnor square of base rings MvFormalGroup.CartierModule.exists_baseChangeEq_eq_and_of_baseChangeEq_eq_of_milnor 0 below · cited by 1 · depth 41
• Cartier curves with Fγ=Vγ descend to a one-dimensional law MvFormalGroup.CartierModule.exists_hom_map_eq_of_frobenius_eq_verschiebungInt 41 below · cited by 1 · depth 44

MvFormalGroup.Deformation 7

• Two lifts differ by a unique first-order class MvFormalGroup.Deformation.existsUnique_isShiftBy 6 below · cited by 2 · depth 35
• First-order classes shift commutative lifts of formal group laws MvFormalGroup.Deformation.exists_isComm_isShiftBy 5 below · cited by 1 · depth 35
• Strict isomorphism of deformations is an equivalence relation MvFormalGroup.Deformation.isIso_equivalence 0 below · cited by 3 · depth 35
• Two shifts of a deformation by the same class are isomorphic MvFormalGroup.Deformation.isIso_of_isShiftBy_of_isShiftBy 7 below · cited by 1 · depth 35
• Shift relation invariant under strict isomorphism of deformations MvFormalGroup.Deformation.isShiftBy_of_isIso_of_isIso 8 below · cited by 3 · depth 35
• Zero and additivity of the shift relation MvFormalGroup.Deformation.isShiftBy_zero_and_isShiftBy_add 0 below · cited by 2 · depth 35
• Shift classes add under affine combinations of deformations MvFormalGroup.Deformation.isShiftBy_add_smul_of_toPowerSeries_eq_add_smul_sub 0 below · cited by 1 · depth 37

MvFormalGroup.End 1

• Faithfulness and commutant of a formal W(κ)-action MvFormalGroup.End.injective_and_forall_exists_eq_of_forall_commute_of_toPowerSeries_eq_X_pow_card 1 below · cited by 1 · depth 32

MvFormalGroup.Hom 6

• Degree of an isogeny of commutative formal groups is a power of p MvFormalGroup.Hom.exists_finrank_quotient_span_range_map_eq_prime_pow_of_isComm 16 below · cited by 3 · depth 30
• Factoring an isogeny of formal groups through Frobenius MvFormalGroup.Hom.exists_comp_eq_and_comp_eq_X_pow_and_finrank_eq_pow_mul 13 below · cited by 5 · depth 31
• Normal form of a formal group homomorphism in characteristic p MvFormalGroup.Hom.exists_subst_eq_X_and_coeff_subst_eq_zero_of_not_dvd 3 below · cited by 2 · depth 32
• Rigidity of homomorphisms of formal groups modulo a nilpotent ideal MvFormalGroup.Hom.eq_of_map_eq_of_ker_pow_eq_bot_of_finrank_eq_pow 8 below · cited by 4 · depth 33
• Homomorphisms of formal group laws are determined on curves MvFormalGroup.Hom.eq_of_forall_subst_curve_eq 0 below · cited by 1 · depth 35
• Degree of a formal group isogeny is a power of p MvFormalGroup.Hom.exists_finrank_quotient_span_range_eq_pow_of_finite 14 below · cited by 1 · depth 45

MvFormalGroup.IsSymmTwoCocycle 1

• Summed cocycle Φ and its coboundary for [p]_F MvFormalGroup.IsSymmTwoCocycle.addCoboundary_sum_subst_nthSeries_eq_and_exists_eq_addCoboundary_of_mem_span 7 below · cited by 2 · depth 35

MvFormalGroup.Points 1

• Integral logarithm criterion for p^v-torsion congruence MvFormalGroup.Points.exists_nsmul_eq_zero_and_sub_mem_iff_of_rescaledLog 0 below · cited by 1 · depth 22

MvFormalGroup.WittLaw 2

• Ghost read-out of Verschiebung, Frobenius and Teichmüller substitutions MvFormalGroup.WittLaw.coeff_subst_verFam_frobPolyFam_teichFam_of_coeff_eq_ghost 0 below · cited by 1 · depth 39
• Ghost series are additive for the Witt addition law MvFormalGroup.WittLaw.subst_addFam_eq_add_of_coeff_eq_ghost 0 below · cited by 1 · depth 40