← all areas

Namespace WittVector 32 theorems

• Lifting a residue-field map to W(k₀)→𝒪 WittVector.exists_ringHom_isLocalHom_and_residue_comp_eq_comp_constantCoeff 0 below · cited by 2 · depth 11
• W(k₀) is a complete DVR with residue field k₀ WittVector.isDiscreteValuationRing_and_isAdicComplete_and_charZero_and_finite_residueField_and_nonempty_residueField_equiv 0 below · cited by 2 · depth 11
• Witt lift into a valuation ring with a transcendental element WittVector.exists_valuationSubring_lift_with_transcendental 0 below · cited by 2 · depth 16
• Valuation subring of an algebraic extension of W(k) dominating W(k) WittVector.exists_valuationSubring_residueField_equiv_of_isAlgebraic 0 below · cited by 3 · depth 23
• Dwork's lemma: existence of prescribed ghost components WittVector.exists_forall_ghostComponent_eq_of_sub_frobeniusLift_mem 0 below · cited by 8 · depth 24
• Carry estimate for Witt addition with slope p-1 WittVector.add_coeff_sub_coeff_mem_pow_of_forall_coeff_mem_pow 1 below · cited by 1 · depth 25
• Witt coefficients mod p from a ghost component mod p^N WittVector.coeff_mem_span_of_ghostComponent_mem_span_pow_of_isReduced 0 below · cited by 3 · depth 25
• Adding a Witt vector with vanishing initial coefficients WittVector.add_coeff_eq_of_forall_coeff_eq_zero 0 below · cited by 1 · depth 26
• Ghost components determine Witt coefficients when p is regular WittVector.coeff_eq_coeff_of_forall_ghostComponent_eq 0 below · cited by 11 · depth 26
• Ghost divisibility forces coefficient divisibility for Witt vectors WittVector.coeff_mem_span_pow_sub_of_forall_ghostComponent_mem_span_pow 0 below · cited by 1 · depth 26
• Witt structure polynomials are weighted homogeneous WittVector.isWeightedHomogeneous_wittStructureInt 0 below · cited by 1 · depth 26
• W(mathbb F_{p²}) as mathbb Zₚ[ω] with σω = t-ω WittVector.exists_ringHom_padicInt_and_root_of_forall_sq_sub_mul_add_ne_zero 0 below · cited by 2 · depth 28
• Witt vectors as the unique strict p-ring with residue ring k WittVector.exists_ringEquiv_comp_eq_constantCoeff_of_isAdicComplete 0 below · cited by 2 · depth 29
• Lubin–Tate lemma for f(T)=pT+T^q over W(k) WittVector.existsUnique_mvPowerSeries_coeff_single_eq_and_C_mul_add_pow_card_eq_subst 0 below · cited by 2 · depth 30
• Ring maps W(F)→ W(k) commute with Frobenius WittVector.ringHom_map_frobenius_of_finite 0 below · cited by 8 · depth 30
• Unique lifting of W(k) along square-zero surjections WittVector.existsUnique_ringHom_comp_eq_of_surjective_of_mul_eq_zero_of_isNilpotent 1 below · cited by 2 · depth 31
• Existence of W(k) and a ramified quadratic extension W(k)[√ p] WittVector.exists_isDiscreteValuationRing_charZero_residueField_ringEquiv_and_sq_eq_of_isAlgClosed 0 below · cited by 1 · depth 31
• M₂(mathbb Zₚ) as a crossed product of W(mathbb F_{p²}) WittVector.exists_ringHom_matrix_padicInt_mul_eq_frobenius_mul_and_forall_exists_eq_add_mul 1 below · cited by 1 · depth 31
• Teichmüller lifts of a basis form a W(k)-basis of W(l) WittVector.bijective_sum_map_mul_teichmuller_basis_of_perfectRing 0 below · cited by 2 · depth 32
• Unique ring map W(k)→ B when kerρ is nilpotent WittVector.existsUnique_ringHom_comp_eq_constantCoeff_of_isNilpotent_ker 0 below · cited by 3 · depth 32
• Witt rigidity: Frobenius lifts commute with maps out of W(k) WittVector.ringHom_comp_eq_comp_frobenius_of_sub_pow_mem_of_isHausdorff 2 below · cited by 1 · depth 32
• Dwork's lemma: a Frobenius lift gives a section R → W(R) WittVector.exists_ringHom_forall_ghostComponent_eq_iterate_of_frobeniusLift 2 below · cited by 3 · depth 33
• Frobenius-fixed Witt vectors form a copy of ℤₚ WittVector.exists_ringHom_padicInt_injective_frobenius_eq_iff_mem_range 0 below · cited by 11 · depth 33
• W(k)/pW(k)≅ k for perfect k of characteristic p WittVector.nonempty_ringEquiv_quotient_pIdeal_of_perfectRing 0 below · cited by 14 · depth 33
• Ring maps W(𝔽_{p²})→ W(k) differ by Frobenius WittVector.eq_or_eq_comp_frobenius_of_ringHom_galoisField_two 1 below · cited by 1 · depth 35
• Ring maps from W(𝔽_{p²}) agree up to Frobenius WittVector.eq_or_eq_comp_frobenius_of_ringHom_galoisField_two_of_charP 0 below · cited by 1 · depth 37
• p-adic valuation of detγ as Witt-vector colength WittVector.exists_det_eq_mul_pow_iff_length_quotient_range_mulVecLin_eq 0 below · cited by 3 · depth 37
• Existence of W(k) and a ramified quadratic extension W(k)[√ p ] WittVector.exists_isDiscreteValuationRing_charZero_residueField_ringEquiv_ringHom_and_sq_eq_of_isAlgClosed 0 below · cited by 2 · depth 37
• Frobenius-fixed Witt vectors map canonically when p is nilpotent WittVector.ringHom_apply_eq_algebraMap_of_frobenius_eq_of_isNilpotent 0 below · cited by 1 · depth 37
• Witt vectors over ̄ k as a Cohen ring with universal property WittVector.exists_isDiscreteValuationRing_charZero_isAdicComplete_residueField_equiv_forall_existsUnique_ringHom_of_isAlgClosed 1 below · cited by 1 · depth 38
• Truncated Teichmüller expansion of a Witt vector WittVector.exists_eq_sum_iterate_verschiebung_teichmuller_add 0 below · cited by 2 · depth 43
• Uniqueness of ring maps ℤₚ → W(R) in characteristic p WittVector.ringHom_ext_padicInt 0 below · cited by 2 · depth 43