← all areas

Namespace FormalGroup 78 theorems

— 35 · IsBaseChange 6 · IsDrinfeldBasisAdic 28 · LawHom 8 · LawIso 1

directly in FormalGroup 35

• Adic formal linear combinations modulo I and I² FormalGroup.linCombAdic_mem_and_sub_natCast_mul_add_mem_sq_and_linCombAdic_zero 0 below · cited by 3 · depth 32
• Linear coefficient of the [n]-series equals n FormalGroup.coeff_one_nthSeries 0 below · cited by 8 · depth 33
• Evaluating the n-series at a topologically nilpotent point FormalGroup.evalSeries_nthSeries 0 below · cited by 4 · depth 33
• [n](T) = nT + T²G(T) for formal group n-series FormalGroup.exists_nthSeries_eq_smul_add_sq_mul 1 below · cited by 1 · depth 33
• Adic evaluation of power series as a ring homomorphism FormalGroup.exists_ringHom_evalSeries_eq 0 below · cited by 15 · depth 33
• Frobenius factorisation of [q]_F in characteristic q FormalGroup.nthSeries_eq_zero_or_exists_eq_mul_X_pow_pow 5 below · cited by 1 · depth 33
• Base change of a formal group law along a ring map FormalGroup.exists_isBaseChange 0 below · cited by 1 · depth 34
• Isomorphic formal groups: Hasse coefficients agree up to a unit mod q FormalGroup.exists_isUnit_coeff_nthSeries_sub_mul_coeff_nthSeries_mem_span_of_lawIso 4 below · cited by 2 · depth 34
• Rigidity: [q]_G is a homomorphism between square-zero lifts FormalGroup.exists_lawHom_series_eq_nthSeries_of_isBaseChange_of_ker_sq_eq_bot 1 below · cited by 3 · depth 34
• The identity endomorphism X is an automorphism of a formal group law FormalGroup.exists_lawIso_refl_appAdic_eq_of_mem 0 below · cited by 4 · depth 34
• (0,0) is a Drinfeld basis iff [q]_F = u X^{q^2} FormalGroup.isDrinfeldBasisAdic_zero_zero_iff 0 below · cited by 22 · depth 34
• Coefficient of Tᵖ in [p] versus invariant differential FormalGroup.coeff_nthSeries_eq_coeff_invDiff_of_isBaseChange 4 below · cited by 2 · depth 35
• The variable-change series defines a formal group law homomorphism FormalGroup.exists_lawHom_series_eq_variableChangeSeries 5 below · cited by 4 · depth 35
• Adic limit of compatible isomorphisms of formal group laws FormalGroup.exists_lawIso_of_forall_isBaseChange_mk_pow 0 below · cited by 1 · depth 35
• q-fold decomposition [q](T)=qT+qT²h+T^qg FormalGroup.exists_nthSeries_eq_qfold_of_isUnit 1 below · cited by 3 · depth 35
• Star-isomorphic lifts share the q-th coefficient of [q] FormalGroup.coeff_nthSeries_eq_of_lawIso_of_sq_maximalIdeal_eq_bot 3 below · cited by 1 · depth 36
• Rigidity of square-zero lifts with equal q-series coefficient FormalGroup.exists_lawIso_of_coeff_nthSeries_eq_of_sq_maximalIdeal_eq_bot 13 below · cited by 2 · depth 36
• Invariance of the invariant differential under [n] FormalGroup.subst_nthSeries_invDiff_mul_derivative 0 below · cited by 3 · depth 36
• Zeros of the [q]-series in mathfrak m_V are simple FormalGroup.derivative_eval_ne_zero_of_nthSeries_eq_mul 3 below · cited by 1 · depth 37
• Drinfeld basis of level q from q² distinct roots of [q] FormalGroup.exists_isDrinfeldBasisAdic_of_nthSeries_eq_prod_mul_of_injective 2 below · cited by 1 · depth 37
• Weierstrass preparation of the [q]-series in the height-one case FormalGroup.exists_monic_isUnit_nthSeries_eq_X_mul_mul_of_map_residue_eq_mul_X_pow 1 below · cited by 2 · depth 37
• Adic evaluation of two-variable power series at ideal elements FormalGroup.exists_ringHom_mvPowerSeries_eval_of_mem 0 below · cited by 1 · depth 37
• Kernel of evaluation at a is (X - C a) FormalGroup.ker_evalSeries_eq_span 1 below · cited by 2 · depth 37
• Invariance of the q-th coefficient of [q] under I-trivial isomorphisms FormalGroup.coeff_nthSeries_eq_of_lawIso_of_mul_maximalIdeal_eq_bot 3 below · cited by 3 · depth 38
• Adic evaluation of a mapped power series is substitution FormalGroup.evalSeries_map_algebraMap_eq_subst 1 below · cited by 2 · depth 38
• Derivative of [n] on a formal group is n times a unit FormalGroup.exists_isUnit_derivative_nthSeries_eq_natCast_mul 1 below · cited by 1 · depth 38
• Transport of a formal group law along an invertible series FormalGroup.exists_lawIso_series_eq_of_isUnit_coeff_one 0 below · cited by 3 · depth 38
• Adic linear combination at (q,0) is the q-series FormalGroup.linCombAdic_map_X_eq_nthSeries 4 below · cited by 1 · depth 38
• Congruent lifts with equal [q]-coefficient are I-trivially isomorphic FormalGroup.exists_lawIso_of_coeff_nthSeries_eq_of_mul_maximalIdeal_eq_bot 14 below · cited by 2 · depth 39
• Full set of q-torsion points over a domain FormalGroup.X_mul_eq_prod_X_sub_C_evalNSMul_of_eval_eq_zero_of_isDomain 6 below · cited by 2 · depth 40
• Repackaging [q]_F = X g v as a unit times prod (X - cₐ) FormalGroup.exists_isUnit_nthSeries_eq_mul_prod_of_X_mul_eq_prod 0 below · cited by 2 · depth 40
• Roots of the Igusa factor are [q]_F-torsion FormalGroup.evalNSMul_mul_eq_zero_of_eval_eq_zero 1 below · cited by 1 · depth 41
• Product-form generator of ker[q] is a root of the distinguished factor FormalGroup.eval_eq_zero_of_nthSeries_eq_mul_prod_X_sub_C_evalNSMul 0 below · cited by 1 · depth 41
• Unit times X^q criterion for [q]_F via g(0)=0 FormalGroup.exists_nthSeries_eq_mul_X_pow_iff_eval_zero_eq_zero 3 below · cited by 1 · depth 41
• Adic linear combination with b=0: F([a]x,[0]y)=[a]x FormalGroup.linCombAdic_zero_right 0 below · cited by 2 · depth 42

FormalGroup.IsBaseChange 6

• Commutativity is preserved by base change of formal group laws FormalGroup.IsBaseChange.isComm 0 below · cited by 11 · depth 34
• Base change commutes with the [n]-series of a formal group law FormalGroup.IsBaseChange.nthSeries_eq_map 0 below · cited by 36 · depth 34
• Weierstrass preparation of the q-series of a formal group lift FormalGroup.IsBaseChange.exists_monic_natDegree_eq_mul_self_nthSeries_eq_mul 4 below · cited by 3 · depth 35
• Frobenius twist commutes with base change FormalGroup.IsBaseChange.map_frobenius 0 below · cited by 1 · depth 35
• Invariant differential commutes with base change of formal groups FormalGroup.IsBaseChange.invDiff_eq_map 0 below · cited by 1 · depth 36
• Base change of adic formal linear combinations [a]x₀+[b]x₁ FormalGroup.IsBaseChange.apply_linCombAdic_eq_of_apply_mem 1 below · cited by 2 · depth 40

FormalGroup.IsDrinfeldBasisAdic 28

• Hasse parameter on a Drinfeld chart: purity of order q(q-1) FormalGroup.IsDrinfeldBasisAdic.exists_mem_pow_isUnit_homogeneous_of_coeff_nthSeries_of_ringEquiv_drinfeldChart 7 below · cited by 2 · depth 31
• Drinfeld basis gives a W[[X₀,X₁]]/(varpi v-fu) presentation FormalGroup.IsDrinfeldBasisAdic.exists_ringEquiv_mvPowerSeries_quotient_drinfeldForm_of_isRegularLocalRing 29 below · cited by 3 · depth 31
• Drinfeld basis forces q=u (x₀prod_c P_c)^{q-1} FormalGroup.IsDrinfeldBasisAdic.exists_natCast_eq_mul_prod_pow_sub_one_of_isAdicComplete 4 below · cited by 3 · depth 32
• Drinfeld chart over ramified constants at a Drinfeld-basis point FormalGroup.IsDrinfeldBasisAdic.exists_ringEquiv_mvPowerSeries_quotient_drinfeldForm_of_isRegularLocalRing_of_prime 28 below · cited by 2 · depth 32
• Drinfeld deformation rings are regular of dimension two FormalGroup.IsDrinfeldBasisAdic.isRegularLocalRing_and_ringKrullDim_eq_two_of_universal_of_isComm_of_lift 63 below · cited by 8 · depth 33
• Universal Drinfeld basis generates the maximal ideal FormalGroup.IsDrinfeldBasisAdic.maximalIdeal_eq_span_pair_of_universal_of_isComm 18 below · cited by 7 · depth 33
• A Lubin–Tate coordinate W₀[[X]] → R for a lift of F₀ FormalGroup.IsDrinfeldBasisAdic.exists_algHom_powerSeries_isBaseChange_lawIso 8 below · cited by 7 · depth 34
• Triviality of first-order lifts keeping (0,0) a Drinfeld basis FormalGroup.IsDrinfeldBasisAdic.exists_lawIso_trivial_of_sq_maximalIdeal_eq_bot_of_isComm 10 below · cited by 2 · depth 34
• Module-finiteness of the Drinfeld level-q deformation map FormalGroup.IsDrinfeldBasisAdic.finite_of_lawIso_isBaseChange_powerSeries_of_maximalIdeal_eq_span_pair_of_isComm 14 below · cited by 1 · depth 34
• Injectivity of the Lubin–Tate coordinate on the Drinfeld deformation ring FormalGroup.IsDrinfeldBasisAdic.injective_algHom_powerSeries_of_universal 26 below · cited by 5 · depth 34
• Reducedness of the special fibre of a Drinfeld-basis chart FormalGroup.IsDrinfeldBasisAdic.isReduced_quotient_span_of_isRegularLocalRing_of_pow_sub_one_eq_mul 35 below · cited by 1 · depth 34
• Drinfeld bases transport along base change of formal groups FormalGroup.IsDrinfeldBasisAdic.map_of_isBaseChange 1 below · cited by 4 · depth 34
• A Drinfeld basis of level q in I forces q∈ I^{q^2-1} FormalGroup.IsDrinfeldBasisAdic.natCast_mem_pow 1 below · cited by 1 · depth 34
• Generic lift over W₀[[t]] is universal FormalGroup.IsDrinfeldBasisAdic.universal_deformation_powerSeries_of_generic_lift 25 below · cited by 7 · depth 34
• Square-zero universality of a generic lift over W₀[[t]] FormalGroup.IsDrinfeldBasisAdic.existsUnique_algHom_powerSeries_of_sq_zero_of_coeff_nthSeries 17 below · cited by 1 · depth 35
• Transporting a Drinfeld basis along an isomorphism of formal group laws FormalGroup.IsDrinfeldBasisAdic.exists_maximalIdeal_eq_span_pair_and_eval_eq_zero_of_lawIso 6 below · cited by 1 · depth 35
• Representability of formal Drinfeld bases by a finite local algebra FormalGroup.IsDrinfeldBasisAdic.exists_moduleFinite_isLocalRing_represents_isDrinfeldBasisAdic 8 below · cited by 1 · depth 35
• Injectivity of the Lubin–Tate coordinate via a finite cover FormalGroup.IsDrinfeldBasisAdic.injective_algHom_powerSeries_of_universal_of_cover 7 below · cited by 1 · depth 35
• Injectivity of W₀llbracket trrbracket → C for a representing algebra FormalGroup.IsDrinfeldBasisAdic.injective_algebraMap_of_represents_isDrinfeldBasisAdic 15 below · cited by 1 · depth 35
• Reducedness of the special fibre of a Drinfeld-basis chart FormalGroup.IsDrinfeldBasisAdic.isReduced_quotient_span_of_isRegularLocalRing_of_pow_sub_one_eq_mul_of_prime 32 below · cited by 1 · depth 35
• Artinian universality from square-zero universality FormalGroup.IsDrinfeldBasisAdic.universal_of_universal_sq_zero 11 below · cited by 1 · depth 35
• Drinfeld basis members are roots of the [q]-series FormalGroup.IsDrinfeldBasisAdic.evalSeries_nthSeries_eq_zero 0 below · cited by 2 · depth 36
• Small-extension lifting step for the Lubin–Tate universal law FormalGroup.IsDrinfeldBasisAdic.existsUnique_algHom_powerSeries_lift_of_smallExtension_of_sqZero 9 below · cited by 1 · depth 36
• Existence of a Drinfeld basis after a finite base change FormalGroup.IsDrinfeldBasisAdic.exists_isDomain_injective_isDrinfeldBasisAdic 14 below · cited by 1 · depth 36
• Adic Drinfeld bases transport along isomorphisms of formal groups FormalGroup.IsDrinfeldBasisAdic.map_iso 3 below · cited by 3 · depth 36
• Uniqueness of deformation lifts along a small extension FormalGroup.IsDrinfeldBasisAdic.algHom_eq_of_smallExtension_of_sqZero 5 below · cited by 1 · depth 37
• Existence of a lift along a small extension FormalGroup.IsDrinfeldBasisAdic.exists_algHom_powerSeries_lift_of_smallExtension_of_sqZero 2 below · cited by 1 · depth 37
• Free rank q² basis of T[[X]]/([q]_F) at a Drinfeld basis FormalGroup.IsDrinfeldBasisAdic.exists_basis_quotient_span_nthSeries_eq_X_pow 0 below · cited by 1 · depth 37

FormalGroup.LawHom 8

• Adic evaluation of a formal group law homomorphism at 0 FormalGroup.LawHom.appAdic_zero 0 below · cited by 1 · depth 34
• Frobenius factorisation of a law homomorphism with zero linear term FormalGroup.LawHom.exists_lawHom_map_frobenius_coeff_eq_of_coeff_one_eq_zero 1 below · cited by 3 · depth 34
• Composition of formal group law homomorphisms FormalGroup.LawHom.exists_comp_series_eq_subst 0 below · cited by 9 · depth 35
• Base change of a homomorphism of formal group laws FormalGroup.LawHom.exists_isBaseChange_series_eq_map 0 below · cited by 18 · depth 35
• Rigidity of homomorphisms between nilpotent-kernel lifts FormalGroup.LawHom.series_eq_of_map_series_eq_of_surjective_of_ker_pow_eq_bot 4 below · cited by 5 · depth 35
• Homomorphisms of formal group laws commute with [n]-series FormalGroup.LawHom.subst_nthSeries_series_eq 0 below · cited by 7 · depth 35
• Adic evaluation of a composite formal group law homomorphism FormalGroup.LawHom.exists_comp_appAdic_eq 1 below · cited by 4 · depth 36
• Transport of adic parameters along a homomorphism reducing to X FormalGroup.LawHom.appAdic_eq_of_lawIso_appAdic_eq_of_map_series_eq_X 9 below · cited by 2 · depth 37

FormalGroup.LawIso 1

• Isomorphisms of formal group laws admit two-sided inverses FormalGroup.LawIso.exists_symm_subst_eq_X 0 below · cited by 15 · depth 35