feat(RingTheory/Perfectoid): Fontaine's theta map

[jjdishere]

In this PR, we define the Fontaine's theta map and show it is surjective.

---

• depends on: [Merged by Bors] - feat(RingTheory/Perfectoid): define the untilt map and generalize pretilt #21563 [untilt map]
• depends on: feat(RingTheory/AdicCompletion): more APIs for IsAdicComplete #21582
  

[github-actions]

PR summary 59985ff44b

Import changes for modified files

No significant changes to the import graph

Import changes for all files

Files	Import difference
Mathlib.RingTheory.Perfectoid.IntergalPerfectoid (new file)	1856
Mathlib.RingTheory.Perfectoid.FontaineTheta (new file)	1915

---

Declarations diff

+ BDeRham
+ BDeRhamPlus
+ Ideal.Quotient.eq_factor_of_eq_factor_succ
+ IntegralPerfectoid
+ IsAdicComplete.surjective_of_surjective_mkQ_comp
+ IsHausdorff.map
+ IsPerfectoidPsU
+ MonoidHom.map_frobeniusEquiv_symm
+ MonoidHom.map_iterate_frobeniusEquiv_symm
+ Perfection.coeff_frobeniusEquiv_symm
+ Perfection.coeff_iterate_frobeniusEquiv_symm
+ PreTilt.coeff_frobenius
+ PreTilt.coeff_frobeniusEquiv_symm
+ PreTilt.coeff_frobenius_pow
+ PreTilt.coeff_iterate_frobeniusEquiv_symm
+ PreTilt.untilt_frobeniusEquiv_symm_pow_pow
+ RingAut.coe_one
+ RingAut.coe_pow
+ RingAut.inv_apply
+ RingAut.mul_apply
+ RingAut.one_apply
+ RingAut.one_eq_refl
+ RingHom.eq_liftOfSurjective
+ RingHom.liftOfSurjective_comp
+ RingHom.liftOfSurjective_comp_apply
+ RingHom.map_frobeniusEquiv_symm
+ RingHom.map_iterate_frobeniusEquiv_symm
+ SModEq.of_toAddSubgroup_le
+ Submodule.eq_factor_of_eq_factor_succ
+ Submodule.toAddSubgroup_toAddSubmonoid
+ Tilt
+ WittVector.map_id
+ _root_.isHausdorff_iff
+ _root_.isPrecomplete_iff
+ coe_frobenius_comp_coe_frobeniusEquiv
+ coeff_sum_of_disjoint
+ dvd_sub_sum_teichmuller_iterateFrobeniusEquiv_coeff
+ eq_iff_smodEq
+ eq_iff_smodEq'
+ eq_iff_smodEq_of_strictMono
+ eq_iff_smodEq_of_strictMono'
+ eq_of_apply_teichmuller_eq
+ eq_of_smodEq
+ eq_of_smodEq'
+ eq_one
+ eq_zero
+ eq_zero'
+ exists_pow_dvd
+ factorPowSucc_comp_fontaineThetaModPPow
+ factorPowSucc_fontaineThetaModPPow_eq
+ factor_eq_factor
+ fontaineTheta
+ fontaineThetaInvertP
+ fontaineThetaModPPow
+ fontaineThetaModPPow_teichmuller
+ fontaineTheta_teichmuller
+ frobeniusEquiv_symm_pow_pow_p_pow
+ function_of_eq_factorPow
+ function_of_eq_factorPow'
+ ghostComponentModPPow
+ ghostComponentModPPow'
+ ghostComponentModPPow_teichmuller_coeff
+ haus
+ instance : CommRing (BDeRhamPlus O p) := AdicCompletion.instCommRing _
+ instance : CommRing (Tilt A p) := Perfection.commRing p (A ⧸ Ideal.span {(p : A)}) -- p is not invertible in integral perfectoid case
+ instance : PerfectRing (PreTilt O p) p
+ ker_map_le_ker_mk_comp_ghostComponent
+ limLinearMap
+ limRingHom
+ map_add
+ map_add'
+ map_eq_zero_iff
+ map_mk_teichmuller_frobeniusEquiv_symm_pow_untilt
+ map_mul
+ map_smul
+ mkQ_comp_limLinearMap
+ mk_comp_limRingHom
+ mk_fontaineTheta
+ mk_limLinearMap
+ mk_limRingHom
+ mk_out
+ mk_pow_fontaineTheta
+ of_SModEq_succ
+ of_eq_factorPow
+ of_eq_factorPow'
+ of_eq_factorPowSucc
+ of_eq_factorPowSucc'
+ pow_dvd_ghostComponent_of_dvd_coeff
+ prec
+ quotEquivOfEq_eq_factor
+ quotEquivOfEq_ghostComponentModPPow
+ sharp
+ sharp_p_pow
+ surjective_fontaineTheta
+ teichmuller_mul_pow_coeff
+ teichmuller_mul_pow_coeff_of_ne
++ _
- IsHausdorff.eq_iff_smodEq
- IsHausdorff.haus
- IsPrecomplete.prec
- isHausdorff_iff
- isPrecomplete_iff

You can run this locally as follows

## summary with just the declaration names:
./scripts/declarations_diff.sh <optional_commit>

## more verbose report:
./scripts/declarations_diff.sh long <optional_commit>

The doc-module for script/declarations_diff.sh contains some details about this script.

---

No changes to technical debt.

You can run this locally as

./scripts/technical-debt-metrics.sh pr_summary

• The relative value is the weighted sum of the differences with weight given by the inverse of the current value of the statistic.
• The absolute value is the relative value divided by the total sum of the inverses of the current values (i.e. the weighted average of the differences).

[mathlib4-dependent-issues-bot]

This PR/issue depends on:

• [Merged by Bors] - feat(RingTheory/Perfectoid): define the untilt map and generalize pretilt #21563
• feat(RingTheory/AdicCompletion): more APIs for IsAdicComplete #21582
  By Dependent Issues (🤖). Happy coding!