Namespace Deformation 120 theorems
— 36 · DieudonneDatum 4 · DieudonneModule 39 · FontaineLift 3 · HondaSystem 28 · PLoc 3 · ProartinianCat 4 · TraceAlgebra 1 · TruncWitt 1 · WittKernel 1
directly in Deformation 36
- Corepresentable subfunctors have a weakly initial element
Deformation.exists_weakly_initial_of_corepresentableBy0 below · cited by 1 · depth 9 - Corepresentability of a conjugation-quotient deformation subfunctor
Deformation.isCorepresentable_conjQuotSubfunctor_of_descends4 below · cited by 1 · depth 9 - Conjugation stability of the lift subfunctor
Deformation.conjStable_liftFunctor0 below · cited by 1 · depth 10 - Conditioned lift descending to its trace algebra
Deformation.exists_cond_lift_traceAlgebra0 below · cited by 1 · depth 10 - Conjugate lifts are strictly equivalent, residually absolutely irreducible case
Deformation.exists_residuallyTrivial_conj_of_conj5 below · cited by 1 · depth 10 - Weak initiality descends to the conjugation quotient subfunctor
Deformation.exists_weaklyInitial_elements_conjQuotSubfunctor0 below · cited by 1 · depth 10 - Uniqueness from traces modulo strict equivalence
Deformation.hom_ext_of_mk_mapRepn_eq1 below · cited by 1 · depth 10 - Complete Noetherian local 𝒪-algebras are pro-Artinian
Deformation.isLocalProartinianAlgebra_of_isAdicComplete0 below · cited by 2 · depth 10 - The lift subfunctor is reflected along injective morphisms
Deformation.reflectedByInjective_liftFunctor0 below · cited by 1 · depth 10 - Schur's lemma for lifts of an absolutely irreducible representation
Deformation.exists_eq_smul_one_of_commute4 below · cited by 1 · depth 11 - Morphisms out of a trace-generated deformation are determined by traces
Deformation.hom_ext_of_traceSubalgebra_eq_top0 below · cited by 1 · depth 11 - Additivity of Hom(-, Wₙ) under convolution of bialgebra maps
Deformation.wittHomMap_convMul0 below · cited by 1 · depth 18 - Fontaine's criterion for lifting special-fibre points, residue field mathbf Fₚ
Deformation.exists_algHom_baseChange_eq_of_forall_map_mem_fontaineKer_zmodp279 below · cited by 1 · depth 19 - Length-one Witt homomorphisms are the primitive elements
Deformation.mem_wittHom_one_iff_coeff_mem_primitives0 below · cited by 6 · depth 19 - Witt shift is surjective when β(1)=0 forces β^{p^n}=0
Deformation.wittHomShift_surjective_of_forall_convPow_eq_zero1 below · cited by 3 · depth 19 - Convolution p-th powers shift Witt coordinates of a homomorphism
Deformation.convPow_prime_apply_coeff_of_mem_wittHom0 below · cited by 6 · depth 20 - Lifting Fontaine-compatible points of unipotent p-divisible groups over ℤₚ
Deformation.exists_algHom_baseChange_eq_of_forall_map_mem_fontaineKer_of_forall_ker_eq_torsionIdeal_zmodp169 below · cited by 4 · depth 20 - Fontaine's criterion descends along a bialgebra quotient
Deformation.exists_algHom_baseChange_eq_of_ker_eq_map_ker_counit0 below · cited by 2 · depth 20 - First Witt coordinates of homomorphisms into Wₙ₊₁
Deformation.exists_mem_wittHom_coeff_zero_eq_iff_of_forall_convPow_eq_zero33 below · cited by 1 · depth 20 - Fontaine's theorem: unipotent p-group schemes as kernels over ℤₚ
Deformation.exists_pDivisibleTower_surjective_ker_eq_map_of_isLocalRing_cartierDual_zmodp278 below · cited by 1 · depth 20 - Fontaine's membership criterion for truncated Witt covectors
Deformation.mem_wittHom_of_mem_fontaineKer_of_verschiebung_mem_wittHom0 below · cited by 3 · depth 20 - Primitivity criterion for Witt vectors concentrated in the last coordinate
Deformation.mem_wittHom_succ_iff_comul_eq_of_forall_coeff_eq_zero0 below · cited by 1 · depth 20 - Vanishing of a Witt-vector homomorphism after restriction
Deformation.wittHomMap_eq_zero_iff_forall_coeff_mem_hopfKer0 below · cited by 3 · depth 20 - Witt coordinates generate a unipotent finite Hopf algebra
Deformation.adjoin_coeff_wittHom_eq_top_of_isLocalRing_cartierDual49 below · cited by 3 · depth 21 - Fontaine's point criterion passes to extensions of group schemes
Deformation.exists_algHom_baseChange_eq_of_faithfullyFlat_of_ker_eq_map_ker_counit0 below · cited by 1 · depth 21 - Fontaine's lifting criterion for maps from F[p^v]
Deformation.exists_algHom_baseChange_eq_of_forall_map_mem_fontaineKer_of_mvFormalGroup40 below · cited by 1 · depth 21 - Extending a homomorphism to W_{m+1} over W_{m+2}
Deformation.exists_mem_wittHom_truncate_eq_of_forall_apply_coeff_last_eq_zero31 below · cited by 1 · depth 21 - Fontaine's fourth step for unipotent groups over mathbf Zₚ
Deformation.exists_pDivisibleTower_ker_eq_map_bijective_baseChange_of_isLocalRing_cartierDual_zmodp275 below · cited by 1 · depth 21 - Fontaine's fourth step for unipotent groups over 𝒪
Deformation.exists_pDivisibleTower_ker_eq_map_bijective_map_comp_mem_fontaineKer_of_isLocalRing_cartierDual_zmodp274 below · cited by 1 · depth 22 - Rescaled-logarithm Witt vectors lie in `wittHom` and `fontaineKer`
Deformation.exists_wittVector_ghostComponent_truncate_map_mem_wittHom_fontaineKer_of_mvFormalGroup37 below · cited by 1 · depth 22 - Truncated Witt homomorphisms killed by the exponent
Deformation.wittHom_nsmul_eq_zero_of_forall_convPow_eq_one0 below · cited by 1 · depth 22 - pⁿ-torsion abelian groups as 𝒪-modules
Deformation.exists_module_forall_exists_intCast_smul_eq_of_pow_smul_eq_zero0 below · cited by 1 · depth 23 - Scaled truncations of the logarithm land in p^N R
Deformation.map_scaledLogTrunc_mem_span_pow_of_mvFormalGroup1 below · cited by 1 · depth 23 - Truncated logarithm covectors are additive modulo p
Deformation.truncate_map_mem_wittHom_of_forall_coeff_ghostComponent_eq_logCovector35 below · cited by 1 · depth 23 - Far Witt components of the logarithm covector lie in pR
Deformation.map_coeff_mem_span_of_forall_coeff_ghostComponent_eq_logCovector26 below · cited by 1 · depth 24 - Bialgebras generated by Witt coordinates have local Cartier dual
Deformation.convPow_eq_zero_and_isLocalRing_cartierDual_of_adjoin_coeff_wittHom_eq_top1 below · cited by 2 · depth 26
Deformation.DieudonneDatum 4
- Free Dieudonné cover with injective, topologically nilpotent V
Deformation.DieudonneDatum.exists_free_cover_of_isNilpotent_V1 below · cited by 1 · depth 24 - Realising a Dieudonné datum by a p-divisible tower over Fₚ
Deformation.DieudonneDatum.exists_pDivisibleTower_zmod_dieudonneModule_of_range_pow_le71 below · cited by 1 · depth 24 - Free Dieudonné cover of a nilpotent Dieudonné datum
Deformation.DieudonneDatum.exists_free_cover_of_isNilpotent0 below · cited by 1 · depth 25 - Finite Dieudonné datum with nilpotent V comes from a Hopf algebra
Deformation.DieudonneDatum.exists_hopfAlgebra_zmod_addEquiv_dieudonneModule_of_isNilpotent69 below · cited by 1 · depth 25
Deformation.DieudonneModule 39
- Honda system of a unipotent k-vector space scheme over ℤₚ
Deformation.DieudonneModule.exists_hondaSystem_addEquiv_smul_eq_map_of_isLocalRing_cartierDual63 below · cited by 2 · depth 17 - Order of the Dieudonné module of a unipotent group scheme
Deformation.DieudonneModule.exists_finrank_eq_pow_and_natCard_eq_pow_of_isLocalRing_cartierDual53 below · cited by 12 · depth 18 - Fontaine's theorem: (L(G),M(G_k)) is a Honda system
Deformation.DieudonneModule.exists_hondaSystem_L_eq_fontaineHodge8 below · cited by 5 · depth 18 - Geometric point count and Dieudonné module order agree
Deformation.DieudonneModule.exists_natCard_algHom_eq_pow_and_natCard_baseChange_eq_pow_of_isLocalRing_cartierDual63 below · cited by 1 · depth 18 - Ring action on a Dieudonné module from convolution-additive bialgebra endomorphisms
Deformation.DieudonneModule.exists_ringHom_addMonoidEnd_apply_eq_map1 below · cited by 1 · depth 18 - Fontaine layer: ker M(π) surjects onto M(H_V)
Deformation.DieudonneModule.exists_surjective_ker_map_of_bottomLayer169 below · cited by 1 · depth 18 - The Dieudonné module functor sends convolution to addition
Deformation.DieudonneModule.map_apply_eq_add_of_toLinearMap_eq_mul_comp_map_comp_comul0 below · cited by 2 · depth 18 - Fontaine full faithfulness for unipotent p-group schemes
Deformation.DieudonneModule.map_baseChange_injective_and_exists_map_baseChange_eq280 below · cited by 2 · depth 18 - Exactness of Fontaine's functor along a Hopf-kernel extension
Deformation.DieudonneModule.map_baseChange_surjective_injective_fontaineHodge_of_range_eq_hopfKer57 below · cited by 3 · depth 18 - Rank symmetry of F and V under a cyclotomic pairing
Deformation.DieudonneModule.natCard_ker_frobenius_eq_natCard_quot_range_verschiebung_of_cyclotomicPairing161 below · cited by 1 · depth 18 - Verschiebung is injective on Fontaine's submodule L
Deformation.DieudonneModule.eq_zero_of_mem_fontaineHodge_of_verschiebung_eq_zero0 below · cited by 1 · depth 19 - Left exactness of the Dieudonné module functor
Deformation.DieudonneModule.exact_map_hopfKerVal_map1 below · cited by 3 · depth 19 - p-torsion of the Dieudonné module lies in L+ker V
Deformation.DieudonneModule.exists_mem_fontaineHodge_add_eq_of_smul_eq_zero2 below · cited by 1 · depth 19 - Frobenius on Fontaine's submodule lands in p L
Deformation.DieudonneModule.exists_mem_fontaineHodge_frobenius_eq_smul2 below · cited by 1 · depth 19 - Kernel of Frobenius lies in V(L)
Deformation.DieudonneModule.exists_mem_fontaineHodge_verschiebung_eq_of_frobenius_eq_zero2 below · cited by 2 · depth 19 - Stabilisation of the Dieudonné module over a perfect field
Deformation.DieudonneModule.exists_surjective_of0 below · cited by 10 · depth 19 - Fontaine's submodule is exact along a Hopf-algebra surjection
Deformation.DieudonneModule.fontaineHodge_map_surjective_and_exists_of_mem_range_of_surjective56 below · cited by 1 · depth 19 - Full faithfulness of the Dieudonné functor over Fₚ
Deformation.DieudonneModule.map_injective_and_exists_map_eq_of_isLocalRing_cartierDual60 below · cited by 5 · depth 19 - Surjectivity of M(π) for surjective π (right exactness)
Deformation.DieudonneModule.map_surjective_of_surjective57 below · cited by 2 · depth 19 - Self-dual local–local Dieudonné modules: #ker F=#cokerV
Deformation.DieudonneModule.natCard_ker_frobenius_eq_natCard_quot_range_verschiebung_of_nonempty_bialgEquiv_cartierDual_zmodp67 below · cited by 1 · depth 19 - Kernel of Verschiebung on the Dieudonné module is the primitives
Deformation.DieudonneModule.nonempty_ker_verschiebung_addEquiv_primitives1 below · cited by 3 · depth 19 - Faithfulness of the Dieudonné module map
Deformation.DieudonneModule.eq_of_map_eq_of_isLocalRing_cartierDual51 below · cited by 1 · depth 20 - Fullness of the Dieudonné module functor over 𝔽ₚ
Deformation.DieudonneModule.exists_map_eq_of_isLocalRing_cartierDual56 below · cited by 2 · depth 20 - Cokernel of Frobenius counts the Dieudonné module of B
Deformation.DieudonneModule.natCard_quot_range_frobenius_eq_natCard_of_ker_eq_map_frobenius_ker_counit_zmodp50 below · cited by 1 · depth 20 - Unipotent Hopf algebras: order p^L and Dieudonné module bound
Deformation.DieudonneModule.exists_finrank_eq_pow_and_natCard_le_pow_of_isLocalRing_cartierDual15 below · cited by 1 · depth 21 - Fontaine's submodule surjects along a Hopf algebra quotient
Deformation.DieudonneModule.exists_mem_fontaineHodge_map_eq_of_isLocalRing_cartierDual56 below · cited by 2 · depth 21 - Dimension bound for the Witt-coordinate subalgebra of a finite F,V-stable subgroup
Deformation.DieudonneModule.finrank_adjoin_coeff_le_natCard0 below · cited by 3 · depth 21 - Exactness of the Dieudonné module functor at a kernel
Deformation.DieudonneModule.map_surjective_and_exact_map_of_ker_eq_map_ker_counit49 below · cited by 4 · depth 21 - Verschiebung cokernel counts primitives modulo bialgebra endomorphisms
Deformation.DieudonneModule.natCard_quot_range_verschiebung_sup_iSup_range_map_eq_natCard_primitives_quot_of_pow_eq_one22 below · cited by 1 · depth 21 - Kernel of Verschiebung equals the primitives, equivariantly
Deformation.DieudonneModule.exists_ker_verschiebung_addEquiv_primitives_apply_of_eq_and_apply_map1 below · cited by 1 · depth 22 - Dieudonné isomorphisms over Fₚ come from bialgebra isomorphisms
Deformation.DieudonneModule.exists_bijective_map_eq_of_addEquiv_of_isLocalRing_cartierDual61 below · cited by 2 · depth 23 - Multiplication by n induces n on the Dieudonné module
Deformation.DieudonneModule.exists_coe_eq_nsmulAlgHom_and_map_eq_nsmul0 below · cited by 1 · depth 23 - Points of a unipotent group scheme as F,V-maps of Dieudonné modules
Deformation.DieudonneModule.eval_injective_and_exists_eval_eq_of_isLocalRing_cartierDual58 below · cited by 4 · depth 26 - Additivity of the Dieudonné module along a splitting
Deformation.DieudonneModule.bijective_prod_map_of_bijective_tensorProduct_comul1 below · cited by 2 · depth 27 - Frobenius is nilpotent on the Dieudonné module of a local bialgebra
Deformation.DieudonneModule.exists_frobenius_iterate_eq_zero_of_isLocalRing0 below · cited by 1 · depth 27 - Covector coordinates of a compatible Dieudonné family
Deformation.DieudonneModule.exists_mvPowerSeries_coeff_eq_apply_of_forall_map_eq0 below · cited by 1 · depth 27 - Frobenius is bijective on the Dieudonné module of a reduced bialgebra
Deformation.DieudonneModule.frobenius_bijective_of_isReduced0 below · cited by 2 · depth 27 - Additivity of the Dieudonné module on a tensor product
Deformation.DieudonneModule.exists_addEquiv_prod_apply_eq_map_of_tensorProduct0 below · cited by 2 · depth 28 - Dieudonné module modulo Frobenius is the cotangent space
Deformation.DieudonneModule.exists_addMonoidHom_cotangent_surjective_ker_eq_range_frobenius_of_isLocalRing_cartierDual59 below · cited by 1 · depth 28
Deformation.FontaineLift 3
- Fontaine's unique lifting of logarithm-type coordinates
Deformation.FontaineLift.existsUnique_sub_mem_and_wSeries_adicEval_eq_of_isUnit_linearPart9 below · cited by 1 · depth 26 - Convergence of Fontaine's w-series at nilpotent points
Deformation.FontaineLift.isPadicLimit_wPartialSum_adicEval0 below · cited by 6 · depth 26 - Continuity of the w-series in the evaluation point
Deformation.FontaineLift.wSeries_adicEval_sub_wSeries_adicEval_mem_powSub2 below · cited by 1 · depth 27
Deformation.HondaSystem 28
- Self-extensions exceed endomorphisms by at most one in rank two
Deformation.HondaSystem.finrank_selfExt_le_finrank_endHonda_add_one3 below · cited by 1 · depth 16 - Self-extensions of an étale Honda system: dim Ext¹ = dim End
Deformation.HondaSystem.finrank_selfExt_eq_finrank_endHonda_of_L_eq_bot0 below · cited by 1 · depth 17 - Self-extensions of a Honda system with ℓ=0 and L=D
Deformation.HondaSystem.finrank_selfExt_eq_finrank_endHonda_of_L_eq_top0 below · cited by 1 · depth 17 - Self-extensions of a rank-two Honda system over a field
Deformation.HondaSystem.finrank_selfExt_eq_one_add_finrank_endHonda0 below · cited by 1 · depth 17 - Length count: im F + L = D for finite-length Dieudonné data
Deformation.HondaSystem.range_sup_eq_top_of_isArtinian_of_isNoetherian0 below · cited by 1 · depth 19 - Free resolution of a finite Honda system with nilpotent V
Deformation.HondaSystem.exists_free_resolution_of_isNilpotent6 below · cited by 1 · depth 23 - Realising Honda systems by unipotent p-divisible towers
Deformation.HondaSystem.exists_pDivisibleTower_dieudonneModule_of_range_pow_le180 below · cited by 1 · depth 23 - Morphisms of Honda systems come from p-divisible towers
Deformation.HondaSystem.exists_towerHom_map_comp_eq_comp_of_map_L_le181 below · cited by 1 · depth 23 - Honda system of an isogeny kernel as a cokernel
Deformation.HondaSystem.map_comp_surjective_and_ker_and_fontaineHodge_eq_of_ker_eq_map_ker_counit62 below · cited by 1 · depth 23 - Equivariant injections of free Honda systems are strict on L
Deformation.HondaSystem.comap_L_eq_of_injective_of_map_L_le1 below · cited by 1 · depth 24 - Lifting Honda systems along equivariant surjections
Deformation.HondaSystem.exists_hondaSystem_lifts_of_equivariant_surjective0 below · cited by 1 · depth 24 - Fontaine lifting of a unipotent p-divisible tower over mathbf Fₚ
Deformation.HondaSystem.exists_pDivisibleTower_bijective_map_mem_fontaineHodge_of_pDivisibleTower_zmod159 below · cited by 1 · depth 24 - Unique split coordinates of a continuous point of Fontaine's functor
Deformation.HondaSystem.existsUnique_coords_of_mem_fontaineFunctor_of_splitCoordinates70 below · cited by 1 · depth 25 - Existence in Fontaine's functor with prescribed split coordinates
Deformation.HondaSystem.exists_mem_fontaineFunctor_of_coords_of_splitCoordinates61 below · cited by 1 · depth 25 - Lifted formal group law and its extension cocycle
Deformation.HondaSystem.exists_mvFormalGroup_cocycle_of_splitCoordinates66 below · cited by 1 · depth 25 - Fontaine's lifting theorem from split coordinates and a cocycle
Deformation.HondaSystem.exists_pDivisibleTower_bijective_map_mem_fontaineHodge_of_splitCoordinates_of_cocycle35 below · cited by 1 · depth 25 - Existence of lawful split coordinates in normal form
Deformation.HondaSystem.exists_splitCoordinates_lawful_normalForm111 below · cited by 1 · depth 25 - Reduction of Φ modulo p equals Φ₀
Deformation.HondaSystem.SplitCoordinates.map_eq_phi0_of_forall_exists_convMul_apply_kappa_X0 below · cited by 1 · depth 26 - Naturality of the Fontaine functor in the test algebra
Deformation.HondaSystem.SplitCoordinates.map_mem_fontaineFunctor_and_described2 below · cited by 1 · depth 26 - Special fibre of the twisted tower: Gᶜᵥ⊗ G^eᵥ≅𝔽ₚ⊗ Lᵥ
Deformation.HondaSystem.exists_bijective_tensorProduct_specialFibre_of_cocycle2 below · cited by 1 · depth 26 - Connected–étale splitting of a free Honda system
Deformation.HondaSystem.exists_isCompl_pow_F_le_and_L_inf_eq_bot0 below · cited by 1 · depth 26 - Coefficientwise lifting of normalised power series to 𝒪
Deformation.HondaSystem.exists_lift_linearPart_map_eq_one_of_coeff_eq0 below · cited by 1 · depth 26 - Fontaine's normalised coordinates on the connected factor
Deformation.HondaSystem.exists_mvFormalGroup_basis_coeff_eq_normalForm93 below · cited by 1 · depth 26 - Rank of the connected Fitting summand equals connected height
Deformation.HondaSystem.finrank_eq_of_isCompl_of_bijective_tensorProduct_comul59 below · cited by 1 · depth 26 - Fontaine–Hodge membership at a twisted Tate level
Deformation.HondaSystem.map_apply_basis_mem_fontaineHodge_of_cocycle3 below · cited by 1 · depth 26 - Fitting summands of a Honda system and the connected–étale splitting
Deformation.HondaSystem.map_eq_zero_of_mem_of_isCompl_of_bijective_tensorProduct2 below · cited by 2 · depth 26 - Linear-algebra core of Fontaine's normal form
Deformation.HondaSystem.exists_basis_isUnit_mulVec_eq_single_of_isNilpotent0 below · cited by 1 · depth 27 - Fontaine's linear parts λ₀,λ₁ with nilpotent C
Deformation.HondaSystem.exists_linearMap_surjective_mulVec_isNilpotent_coeff_eq65 below · cited by 1 · depth 27
Deformation.PLoc 3
- Convergence of Fontaine's w-series when c_k ∈ pg eventually
Deformation.PLoc.isPadicLimit_wPartialSum_wSeries_of_eventually_mem_span0 below · cited by 4 · depth 26 - Newton step for Fontaine's w-series at p=2
Deformation.PLoc.wPartialSum_adicEval_add_sub_sub_algebraMap_mul_add_mem_powSub_two2 below · cited by 1 · depth 27 - Newton linearisation of Fontaine's partial w-sums
Deformation.PLoc.wPartialSum_adicEval_add_sub_sub_algebraMap_mul_sum_mem_powSub2 below · cited by 1 · depth 27
Deformation.ProartinianCat 4
- Power series presentation of a pro-Artinian object
Deformation.ProartinianCat.exists_surjective_mvPowerSeriesLift0 below · cited by 1 · depth 9 - Noetherian pro-Artinian algebras are 𝔪-adically complete
Deformation.ProartinianCat.isAdicComplete_of_isNoetherianRing0 below · cited by 1 · depth 9 - Noetherian pro-Artinian algebras carry the 𝔪-adic topology
Deformation.ProartinianCat.isAdicTopology_of_isNoetherianRing0 below · cited by 1 · depth 9 - Limit-preserving functors on widehatC_𝒪 are corepresentable
Deformation.ProartinianCat.isCorepresentable_of_preservesLimits2 below · cited by 1 · depth 9
Deformation.TraceAlgebra 1
- Carayol's lemma: lifts descend to their trace subalgebra
Deformation.TraceAlgebra.descends4 below · cited by 2 · depth 9
Deformation.TruncWitt 1
- One-coordinate lift into the Fontaine kernel
Deformation.TruncWitt.exists_mem_fontaineKer_truncate_eq_of_frobeniusFun_mem_fontaineKer0 below · cited by 3 · depth 20