Documentation Verification Report

FontaineTheta

📁 Source: Mathlib/RingTheory/Perfectoid/FontaineTheta.lean

Statistics

Metric	Count
Definitions `fontaineTheta`, `fontaineThetaModPPow`, `ghostComponentModPPow`	3
Theorems `factorPowSucc_comp_fontaineThetaModPPow`, `factorPowSucc_fontaineThetaModPPow_eq`, `fontaineThetaModPPow_teichmuller`, `fontaineTheta_teichmuller`, `ghostComponentModPPow_map_mk`, `ghostComponentModPPow_teichmuller_coeff`, `ker_map_le_ker_mk_comp_ghostComponent`, `mk_fontaineTheta`, `mk_pow_fontaineTheta`, `quotEquivOfEq_ghostComponentModPPow`, `surjective_fontaineTheta`	11
Total	14

WittVector

Definitions

Name	Category	Theorems
`fontaineTheta` 📖	CompOp	4 math math: `mk_pow_fontaineTheta`, `surjective_fontaineTheta`, `fontaineTheta_teichmuller`, `mk_fontaineTheta`
`fontaineThetaModPPow` 📖	CompOp	4 math math: `factorPowSucc_comp_fontaineThetaModPPow`, `factorPowSucc_fontaineThetaModPPow_eq`, `mk_pow_fontaineTheta`, `fontaineThetaModPPow_teichmuller`
`ghostComponentModPPow` 📖	CompOp	3 math math: `ghostComponentModPPow_teichmuller_coeff`, `quotEquivOfEq_ghostComponentModPPow`, `ghostComponentModPPow_map_mk`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`factorPowSucc_comp_fontaineThetaModPPow` 📖	mathematical	—	`RingHom.comp` `WittVector` `PreTilt` `HasQuotient.Quotient` `Ideal` `Ring.toSemiring` `CommRing.toRing` `Ideal.instHasQuotient` `Submodule.instPowNat` `Semiring.toModule` `IsScalarTower.left` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `DistribMulAction.toMulAction` `AddCommMonoid.toAddMonoid` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonAssocRing.toNonUnitalNonAssocRing` `Ring.toNonAssocRing` `Module.toDistribMulAction` `Ideal.span` `CommSemiring.toSemiring` `CommRing.toCommSemiring` `Set` `Set.instSingletonSet` `AddMonoidWithOne.toNatCast` `AddGroupWithOne.toAddMonoidWithOne` `Ring.toAddGroupWithOne` `Semiring.toNonAssocSemiring` `instCommRing` `PreTilt.instCommRing` `Ideal.Quotient.ring` `Ideal.IsTwoSided.instHPowNat` `Ideal.instIsTwoSided_1` `Ideal.Quotient.factorPowSucc` `fontaineThetaModPPow`	—	`eq_of_apply_teichmuller_eq` `PreTilt.instCharP` `PreTilt.instPerfectRing` `IsScalarTower.left` `Ideal.IsTwoSided.instHPowNat` `Ideal.instIsTwoSided_1` `IsScalarTower.right` `map_natCast` `RingHom.instRingHomClass` `map_pow` `MonoidWithZeroHomClass.toMonoidHomClass` `RingHomClass.toMonoidWithZeroHomClass` `Ideal.Quotient.eq_zero_iff_mem` `Ideal.pow_mem_pow` `Ideal.mem_span_singleton_self` `map_teichmuller` `expChar_prime` `PreTilt.coeff_iterate_frobeniusEquiv_symm` `zero_add` `PreTilt.coeff_frobeniusEquiv_symm` `ghostComponentModPPow_teichmuller_coeff`
`factorPowSucc_fontaineThetaModPPow_eq` 📖	mathematical	—	`DFunLike.coe` `RingHom` `HasQuotient.Quotient` `Ideal` `Ring.toSemiring` `CommRing.toRing` `Ideal.instHasQuotient` `Submodule.instPowNat` `Semiring.toModule` `IsScalarTower.left` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `DistribMulAction.toMulAction` `AddCommMonoid.toAddMonoid` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonAssocRing.toNonUnitalNonAssocRing` `Ring.toNonAssocRing` `Module.toDistribMulAction` `Ideal.span` `CommSemiring.toSemiring` `CommRing.toCommSemiring` `Set` `Set.instSingletonSet` `AddMonoidWithOne.toNatCast` `AddGroupWithOne.toAddMonoidWithOne` `Ring.toAddGroupWithOne` `Semiring.toNonAssocSemiring` `Ideal.Quotient.ring` `Ideal.IsTwoSided.instHPowNat` `Ideal.instIsTwoSided_1` `RingHom.instFunLike` `Ideal.Quotient.factorPowSucc` `WittVector` `PreTilt` `Ideal.instHasQuotient_1` `IsScalarTower.right` `Algebra.id` `instCommRing` `PreTilt.instCommRing` `Ideal.Quotient.semiring` `fontaineThetaModPPow`	—	`IsScalarTower.left` `Ideal.IsTwoSided.instHPowNat` `Ideal.instIsTwoSided_1` `IsScalarTower.right` `factorPowSucc_comp_fontaineThetaModPPow`
`fontaineThetaModPPow_teichmuller` 📖	mathematical	—	`DFunLike.coe` `RingHom` `WittVector` `PreTilt` `HasQuotient.Quotient` `Ideal` `CommSemiring.toSemiring` `CommRing.toCommSemiring` `Ideal.instHasQuotient_1` `Submodule.instPowNat` `Semiring.toModule` `IsScalarTower.right` `Algebra.id` `Ideal.span` `Set` `Set.instSingletonSet` `AddMonoidWithOne.toNatCast` `AddGroupWithOne.toAddMonoidWithOne` `Ring.toAddGroupWithOne` `CommRing.toRing` `Semiring.toNonAssocSemiring` `instCommRing` `PreTilt.instCommRing` `Ideal.Quotient.semiring` `RingHom.instFunLike` `fontaineThetaModPPow` `MonoidHom` `MulOneClass.toMulOne` `MulZeroOneClass.toMulOneClass` `NonAssocSemiring.toMulZeroOneClass` `MonoidHom.instFunLike` `teichmuller` `Ring.toSemiring` `Ideal.instHasQuotient` `Ideal.Quotient.ring` `Ideal.instIsTwoSided_1` `PreTilt.untilt`	—	`IsScalarTower.right` `Ideal.instIsTwoSided_1` `PreTilt.instPerfectRing` `map_teichmuller` `expChar_prime` `PreTilt.instCharP` `PreTilt.coeff_iterate_frobeniusEquiv_symm` `zero_add` `ghostComponentModPPow_teichmuller_coeff`
`fontaineTheta_teichmuller` 📖	mathematical	—	`DFunLike.coe` `RingHom` `WittVector` `PreTilt` `Semiring.toNonAssocSemiring` `CommSemiring.toSemiring` `CommRing.toCommSemiring` `instCommRing` `PreTilt.instCommRing` `RingHom.instFunLike` `fontaineTheta` `MonoidHom` `MulOneClass.toMulOne` `MulZeroOneClass.toMulOneClass` `NonAssocSemiring.toMulZeroOneClass` `MonoidHom.instFunLike` `teichmuller` `PreTilt.untilt`	—	`IsScalarTower.left` `IsHausdorff.eq_iff_smodEq` `IsAdicComplete.toIsHausdorff` `Ideal.mul_top` `Ideal.instIsTwoSided_1` `pow_zero` `Ideal.one_eq_top` `IsScalarTower.right` `mk_pow_fontaineTheta` `fontaineThetaModPPow_teichmuller`
`ghostComponentModPPow_map_mk` 📖	mathematical	—	`DFunLike.coe` `RingHom` `WittVector` `HasQuotient.Quotient` `Ideal` `CommSemiring.toSemiring` `CommRing.toCommSemiring` `Ideal.instHasQuotient_1` `Ideal.span` `Set` `Set.instSingletonSet` `AddMonoidWithOne.toNatCast` `AddGroupWithOne.toAddMonoidWithOne` `Ring.toAddGroupWithOne` `CommRing.toRing` `Submodule.instPowNat` `Semiring.toModule` `IsScalarTower.right` `Algebra.id` `Semiring.toNonAssocSemiring` `instCommRing` `ModP.commRing` `Ideal.Quotient.semiring` `RingHom.instFunLike` `ghostComponentModPPow` `Ring.toSemiring` `Ideal.instHasQuotient` `map` `Ideal.instIsTwoSided_1` `Ideal.Quotient.ring` `ghostComponent`	—	`RingHom.liftOfSurjective_comp_apply` `IsScalarTower.right` `ker_map_le_ker_mk_comp_ghostComponent`
`ghostComponentModPPow_teichmuller_coeff` 📖	mathematical	—	`DFunLike.coe` `RingHom` `WittVector` `HasQuotient.Quotient` `Ideal` `CommSemiring.toSemiring` `CommRing.toCommSemiring` `Ideal.instHasQuotient_1` `Ideal.span` `Set` `Set.instSingletonSet` `AddMonoidWithOne.toNatCast` `AddGroupWithOne.toAddMonoidWithOne` `Ring.toAddGroupWithOne` `CommRing.toRing` `Submodule.instPowNat` `Semiring.toModule` `IsScalarTower.right` `Algebra.id` `Semiring.toNonAssocSemiring` `instCommRing` `ModP.commRing` `Ideal.Quotient.semiring` `RingHom.instFunLike` `ghostComponentModPPow` `MonoidHom` `MulOneClass.toMulOne` `MulZeroOneClass.toMulOneClass` `NonAssocSemiring.toMulZeroOneClass` `MonoidHom.instFunLike` `teichmuller` `PreTilt` `ModP` `PreTilt.instCommRing` `PreTilt.coeff` `Ring.toSemiring` `Ideal.instHasQuotient` `Ideal.Quotient.ring` `Ideal.instIsTwoSided_1` `PreTilt.untilt`	—	`IsScalarTower.right` `Ideal.instIsTwoSided_1` `expChar_prime` `PreTilt.instCharP` `PreTilt.instPerfectRing` `RingAut.coe_pow` `map_teichmuller` `PreTilt.mk_untilt_eq_coeff_zero` `PreTilt.coeff_iterate_frobeniusEquiv_symm` `zero_add` `ghostComponent_teichmuller` `PreTilt.untilt_iterate_frobeniusEquiv_symm_pow`
`ker_map_le_ker_mk_comp_ghostComponent` 📖	mathematical	—	`Ideal` `WittVector` `CommSemiring.toSemiring` `CommRing.toCommSemiring` `instCommRing` `Preorder.toLE` `PartialOrder.toPreorder` `Submodule.instPartialOrder` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `Semiring.toModule` `RingHom.ker` `HasQuotient.Quotient` `Ring.toSemiring` `CommRing.toRing` `Ideal.instHasQuotient` `Ideal.span` `Set` `Set.instSingletonSet` `AddMonoidWithOne.toNatCast` `AddGroupWithOne.toAddMonoidWithOne` `Ring.toAddGroupWithOne` `RingHom` `ModP.commRing` `RingHom.instFunLike` `RingHom.instRingHomClass` `map` `Ideal.instIsTwoSided_1` `Submodule.instPowNat` `IsScalarTower.right` `Algebra.id` `Ideal.Quotient.ring` `RingHom.comp` `ghostComponent`	—	`RingHom.instRingHomClass` `Ideal.instIsTwoSided_1` `IsScalarTower.right` `Equiv.injective` `IsScalarTower.left` `Ideal.span_singleton_pow` `map_zero` `MonoidWithZeroHomClass.toZeroHomClass` `RingHomClass.toMonoidWithZeroHomClass` `RingEquivClass.toRingHomClass` `RingEquiv.instRingEquivClass` `pow_dvd_ghostComponent_of_dvd_coeff`
`mk_fontaineTheta` 📖	mathematical	—	`DFunLike.coe` `RingHom` `HasQuotient.Quotient` `Ideal` `Ring.toSemiring` `CommRing.toRing` `Ideal.instHasQuotient` `Ideal.span` `Set` `Set.instSingletonSet` `AddMonoidWithOne.toNatCast` `AddGroupWithOne.toAddMonoidWithOne` `Ring.toAddGroupWithOne` `Semiring.toNonAssocSemiring` `Ideal.Quotient.ring` `Ideal.instIsTwoSided_1` `RingHom.instFunLike` `WittVector` `PreTilt` `CommSemiring.toSemiring` `CommRing.toCommSemiring` `instCommRing` `PreTilt.instCommRing` `fontaineTheta` `ModP` `Ideal.Quotient.semiring` `PreTilt.coeff` `coeff`	—	`IsScalarTower.right` `Ideal.instIsTwoSided_1` `mk_pow_fontaineTheta` `IsScalarTower.left` `Ideal.span_singleton_pow` `pow_one` `PreTilt.instPerfectRing` `pow_zero` `map_id` `RingHomCompTriple.comp_eq` `RingHomCompTriple.ids` `quotEquivOfEq_ghostComponentModPPow` `wittPolynomial_zero` `MvPolynomial.aeval_X`
`mk_pow_fontaineTheta` 📖	mathematical	—	`DFunLike.coe` `RingHom` `HasQuotient.Quotient` `Ideal` `Ring.toSemiring` `CommRing.toRing` `Ideal.instHasQuotient` `CommSemiring.toSemiring` `CommRing.toCommSemiring` `Submodule.instPowNat` `Semiring.toModule` `IsScalarTower.right` `Algebra.id` `Ideal.span` `Set` `Set.instSingletonSet` `AddMonoidWithOne.toNatCast` `AddGroupWithOne.toAddMonoidWithOne` `Ring.toAddGroupWithOne` `Semiring.toNonAssocSemiring` `Ideal.Quotient.ring` `Ideal.instIsTwoSided_1` `RingHom.instFunLike` `WittVector` `PreTilt` `instCommRing` `PreTilt.instCommRing` `fontaineTheta` `Ideal.instHasQuotient_1` `Ideal.Quotient.semiring` `fontaineThetaModPPow`	—	`IsAdicComplete.StrictMono.mk_liftRingHom` `Order.succ_strictMono` `Nat.instNoMaxOrder` `factorPowSucc_comp_fontaineThetaModPPow`
`quotEquivOfEq_ghostComponentModPPow` 📖	mathematical	`Ideal` `CommSemiring.toSemiring` `CommRing.toCommSemiring` `Submodule.instPowNat` `Semiring.toModule` `IsScalarTower.right` `Algebra.id` `Ideal.span` `Set` `Set.instSingletonSet` `AddMonoidWithOne.toNatCast` `AddGroupWithOne.toAddMonoidWithOne` `Ring.toAddGroupWithOne` `CommRing.toRing`	`DFunLike.coe` `RingEquiv` `HasQuotient.Quotient` `Ring.toSemiring` `Ideal.instHasQuotient` `Distrib.toMul` `NonUnitalNonAssocSemiring.toDistrib` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonAssocRing.toNonUnitalNonAssocRing` `Ring.toNonAssocRing` `Ideal.Quotient.ring` `Ideal.instIsTwoSided_1` `Distrib.toAdd` `EquivLike.toFunLike` `RingEquiv.instEquivLike` `Ideal.quotEquivOfEq` `RingHom` `WittVector` `Ideal.instHasQuotient_1` `Semiring.toNonAssocSemiring` `instCommRing` `ModP.commRing` `Ideal.Quotient.semiring` `RingHom.instFunLike` `ghostComponentModPPow` `ghostComponent`	—	`IsScalarTower.right` `Ideal.instIsTwoSided_1` `map_surjective` `Ideal.Quotient.mk_surjective` `wittPolynomial_zero` `MvPolynomial.aeval_X`

(root)

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`surjective_fontaineTheta` 📖	mathematical	`ModP` `DFunLike.coe` `RingHom` `Semiring.toNonAssocSemiring` `CommSemiring.toSemiring` `Ideal.Quotient.commSemiring` `Ideal.span` `CommRing.toCommSemiring` `Set` `Set.instSingletonSet` `AddMonoidWithOne.toNatCast` `AddGroupWithOne.toAddMonoidWithOne` `Ring.toAddGroupWithOne` `CommRing.toRing` `RingHom.instFunLike` `frobenius` `expChar_prime` `AddCommMonoidWithOne.toAddMonoidWithOne` `NonAssocSemiring.toAddCommMonoidWithOne` `ModP.charP`	`WittVector` `PreTilt` `WittVector.instCommRing` `PreTilt.instCommRing` `WittVector.fontaineTheta`	—	`expChar_prime` `ModP.charP` `Ideal.map_span` `RingHom.instRingHomClass` `Set.image_singleton` `map_natCast` `IsAdicComplete.toIsHausdorff` `surjective_of_mk_map_comp_surjective` `IsAdicComplete.toIsPrecomplete` `WittVector.isAdicCompleteIdealSpanP` `PreTilt.instCharP` `PreTilt.instPerfectRing` `Ideal.instIsTwoSided_1` `WittVector.mk_fontaineTheta` `Perfection.coeff_surjective` `WittVector.coeff_surjective`

---

← Back to Index