Commit 2025-12-11 08:08 63a90fe8

View on Github →

feat(RingTheory/Perfectoid): Fontaine's theta map is surjective (#26384) This PR continues the work from #22332. Original PR: https://github.com/leanprover-community/mathlib4/pull/22332 In this file, we show that when R is p-adically complete and Frob : R/p -> R/p is surjective, Fontaine's theta map is surjective.

Estimated changes

Modified Mathlib.lean

Modified Mathlib/Algebra/Module/Submodule/Basic.lean

added theorem Submodule.toAddSubgroup_toAddSubmonoid

Modified Mathlib/LinearAlgebra/SModEq/Basic.lean

added theorem SModEq.of_toAddSubgroup_le

Created Mathlib/LinearAlgebra/SModEq/Pointwise.lean

added theorem SModEq.smul'

Modified Mathlib/RingTheory/AdicCompletion/Basic.lean

added theorem IsHausdorff.map_algebraMap_iff

added theorem IsHausdorff.of_map

Modified Mathlib/RingTheory/AdicCompletion/Functoriality.lean

added theorem AdicCompletion.exists_smodEq_pow_add_one_smul

added theorem AdicCompletion.exists_smodEq_pow_smul_top_and_mkQ_eq

added theorem AdicCompletion.exists_smodEq_pow_smul_top_and_smodEq_pow_add_one_smul_top

added theorem AdicCompletion.map_of

added theorem AdicCompletion.map_surjective_of_mkQ_comp_surjective

added theorem surjective_of_mkQ_comp_surjective

added theorem surjective_of_mk_map_comp_surjective

Modified Mathlib/RingTheory/Perfection.lean

added theorem Perfection.coeff_surjective

Modified Mathlib/RingTheory/Perfectoid/FontaineTheta.lean

added theorem surjective_fontaineTheta

Modified Mathlib/RingTheory/WittVector/Defs.lean

added theorem WittVector.coeff_surjective