Isocrystal

📁 Source: Mathlib/RingTheory/WittVector/Isocrystal.lean

Statistics

Metric	Count
Definitions «termK(_,_)»»), «term_→ᶠˡ[_,_]_», «term_→ᶠⁱ[_,_]_», «term_≃ᶠˡ[_,_]_», «term_≃ᶠⁱ[_,_]_», «termΦ(_,_)»»), «termφ(_,_)»»), frobenius, frobeniusRingHom, Isocrystal, frob, frobenius, toModule, IsocrystalEquiv, toLinearEquiv, IsocrystalHom, toLinearMap, StandardOneDimIsocrystal, instAddCommGroupStandardOneDimIsocrystal, instIsocrystalStandardOneDimIsocrystal, instModuleFractionRingStandardOneDimIsocrystal	21
Theorems frob_equivariant, frob_equivariant, frobenius_apply, inv_pair₁, inv_pair₂, isocrystal_classification	6
Total	27

Isocrystal

Definitions

Name	Category	Theorems
«termK(_,_)» 📖» "API Documentation")	CompOp	—
«term_→ᶠˡ[_,_]_» 📖	CompOp	—
«term_→ᶠⁱ[_,_]_» 📖	CompOp	—
«term_≃ᶠˡ[_,_]_» 📖	CompOp	—
«term_≃ᶠⁱ[_,_]_» 📖	CompOp	—
«termΦ(_,_)» 📖» "API Documentation")	CompOp	—
«termφ(_,_)» 📖» "API Documentation")	CompOp	—

WittVector

Definitions

Name	Category	Theorems
Isocrystal 📖	CompData	—
IsocrystalEquiv 📖	CompData	1 math math: isocrystal_classification
IsocrystalHom 📖	CompData	—
StandardOneDimIsocrystal 📖	CompOp	2 math math: StandardOneDimIsocrystal.frobenius_apply, isocrystal_classification
instAddCommGroupStandardOneDimIsocrystal 📖	CompOp	2 math math: StandardOneDimIsocrystal.frobenius_apply, isocrystal_classification
instIsocrystalStandardOneDimIsocrystal 📖	CompOp	2 math math: StandardOneDimIsocrystal.frobenius_apply, isocrystal_classification
instModuleFractionRingStandardOneDimIsocrystal 📖	CompOp	—

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
inv_pair₁ 📖	mathematical	—	RingHomInvPair FractionRing WittVector instCommRing OreLocalization.instSemiring CommSemiring.toSemiring CommRing.toCommSemiring nonZeroDivisors Semiring.toMonoidWithZero OreLocalization.oreSetComm CommRing.toCommMonoid FractionRing.frobeniusRingHom RingHomClass.toRingHom RingEquiv OreLocalization.instMul CommMonoid.toMonoid OreLocalization.instAdd AddCommMonoid.toAddMonoid NonUnitalNonAssocSemiring.toAddCommMonoid NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing Module.toDistribMulAction Ring.toSemiring CommRing.toRing Semiring.toModule EquivLike.toFunLike RingEquiv.instEquivLike Semiring.toNonAssocSemiring RingEquivClass.toRingHomClass RingEquiv.instRingEquivClass RingEquiv.symm FractionRing.frobenius	—	expChar_prime RingHomInvPair.of_ringEquiv
inv_pair₂ 📖	mathematical	—	RingHomInvPair FractionRing WittVector instCommRing OreLocalization.instSemiring CommSemiring.toSemiring CommRing.toCommSemiring nonZeroDivisors Semiring.toMonoidWithZero OreLocalization.oreSetComm CommRing.toCommMonoid RingHomClass.toRingHom RingEquiv OreLocalization.instMul CommMonoid.toMonoid OreLocalization.instAdd AddCommMonoid.toAddMonoid NonUnitalNonAssocSemiring.toAddCommMonoid NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing Module.toDistribMulAction Ring.toSemiring CommRing.toRing Semiring.toModule EquivLike.toFunLike RingEquiv.instEquivLike Semiring.toNonAssocSemiring RingEquivClass.toRingHomClass RingEquiv.instRingEquivClass RingEquiv.symm FractionRing.frobenius	—	expChar_prime RingHomInvPair.of_ringEquiv
isocrystal_classification 📖	mathematical	Module.finrank FractionRing WittVector instCommRing EuclideanDomain.toCommRing Field.toEuclideanDomain OreLocalization.instSemiring CommSemiring.toSemiring CommRing.toCommSemiring nonZeroDivisors Semiring.toMonoidWithZero OreLocalization.oreSetComm CommRing.toCommMonoid AddCommGroup.toAddCommMonoid Isocrystal.toModule PerfectField.toPerfectRing IsAlgClosed.perfectField expChar_prime AddCommMonoidWithOne.toAddMonoidWithOne NonAssocSemiring.toAddCommMonoidWithOne Semiring.toNonAssocSemiring	IsocrystalEquiv StandardOneDimIsocrystal instAddCommGroupStandardOneDimIsocrystal instIsocrystalStandardOneDimIsocrystal instIsDomain Field.toSemifield	—	PerfectField.toPerfectRing IsAlgClosed.perfectField expChar_prime instIsDomain exists_ne Module.nontrivial_of_finrank_eq_succ FractionRing.instNontrivial instNontrivial IsLocalRing.toNontrivial Field.instIsLocalRing RingEquivClass.toRingHomClass RingEquiv.instRingEquivClass inv_pair₁ inv_pair₂ map_zero AddMonoidHomClass.toZeroHomClass DistribMulActionSemiHomClass.toAddMonoidHomClass SemilinearMapClass.distribMulActionSemiHomClass SemilinearEquivClass.instSemilinearMapClass LinearEquiv.instSemilinearEquivClass LinearEquiv.injective instNoZeroDivisorsOfCharP IsDomain.to_noZeroDivisors finrank_eq_one_iff_of_nonzero' zero_smul Localization.isLocalization exists_frobenius_solution_fractionRing RingHomInvPair.ids LinearMap.ker_eq_bot LinearMap.ker_toSpanSingleton instIsDomain instIsTorsionFreeOfIsDomainOfNoZeroSMulDivisors GroupWithZero.toNoZeroSMulDivisors RingHomSurjective.ids LinearMap.range_eq_top finrank_eq_one_iff_of_nonzero LinearMap.span_singleton_eq_range RingHomCompTriple.ids LinearEquiv.trans_apply LinearEquiv.smulOfNeZero_apply LinearEquiv.map_smul LinearEquiv.ofBijective_apply IsDomain.toNontrivial StandardOneDimIsocrystal.frobenius_apply LinearMap.toSpanSingleton_apply MulActionSemiHomClass.map_smulₛₗ SemilinearMapClass.toMulActionSemiHomClass Mathlib.Tactic.LinearCombination.eq_of_eq AddRightCancelSemigroup.toIsRightCancelAdd Mathlib.Tactic.LinearCombination.mul_const_eq Mathlib.Tactic.LinearCombination.eq_rearrange Mathlib.Tactic.Ring.of_eq Mathlib.Tactic.Ring.sub_congr Mathlib.Tactic.Ring.add_congr Mathlib.Tactic.Ring.mul_congr Mathlib.Tactic.Ring.atom_pf Mathlib.Tactic.Ring.add_mul Mathlib.Tactic.Ring.mul_add Mathlib.Tactic.Ring.mul_pf_left Mathlib.Tactic.Ring.mul_pf_right Mathlib.Tactic.Ring.one_mul Mathlib.Tactic.Ring.mul_zero Mathlib.Tactic.Ring.add_pf_add_zero Mathlib.Tactic.Ring.zero_mul Mathlib.Tactic.Ring.add_pf_add_lt Mathlib.Tactic.Ring.add_pf_zero_add Mathlib.Tactic.Ring.add_pf_add_gt Mathlib.Tactic.Ring.sub_pf Mathlib.Tactic.Ring.neg_add Mathlib.Tactic.Ring.neg_mul Mathlib.Tactic.Ring.neg_one_mul Mathlib.Meta.NormNum.IsInt.to_raw_eq Mathlib.Meta.NormNum.isInt_mul Mathlib.Meta.NormNum.IsInt.of_raw Mathlib.Meta.NormNum.IsNat.to_isInt Mathlib.Meta.NormNum.IsNat.of_raw Mathlib.Tactic.Ring.neg_zero Mathlib.Tactic.Ring.add_pf_add_overlap_zero Mathlib.Tactic.Ring.add_overlap_pf_zero Mathlib.Meta.NormNum.IsInt.to_isNat Mathlib.Meta.NormNum.isInt_add Mathlib.Tactic.Ring.cast_zero Mathlib.Meta.NormNum.isNat_ofNat Nat.cast_zero

WittVector.FractionRing

Definitions

Name	Category	Theorems
frobenius 📖	CompOp	5 math math: WittVector.IsocrystalHom.frob_equivariant, WittVector.IsocrystalEquiv.frob_equivariant, WittVector.inv_pair₂, WittVector.inv_pair₁, WittVector.StandardOneDimIsocrystal.frobenius_apply
frobeniusRingHom 📖	CompOp	4 math math: WittVector.IsocrystalHom.frob_equivariant, WittVector.IsocrystalEquiv.frob_equivariant, WittVector.inv_pair₁, WittVector.StandardOneDimIsocrystal.frobenius_apply

WittVector.Isocrystal

Definitions

Name	Category	Theorems
frob 📖	CompOp	—
frobenius 📖	CompOp	3 math math: WittVector.IsocrystalHom.frob_equivariant, WittVector.IsocrystalEquiv.frob_equivariant, WittVector.StandardOneDimIsocrystal.frobenius_apply
toModule 📖	CompOp	3 math math: WittVector.IsocrystalHom.frob_equivariant, WittVector.IsocrystalEquiv.frob_equivariant, WittVector.StandardOneDimIsocrystal.frobenius_apply

WittVector.IsocrystalEquiv

Definitions

Name	Category	Theorems
toLinearEquiv 📖	CompOp	1 math math: frob_equivariant

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
frob_equivariant 📖	mathematical	—	DFunLike.coe LinearEquiv FractionRing WittVector WittVector.instCommRing OreLocalization.instSemiring CommSemiring.toSemiring CommRing.toCommSemiring nonZeroDivisors Semiring.toMonoidWithZero OreLocalization.oreSetComm CommRing.toCommMonoid WittVector.FractionRing.frobeniusRingHom RingHomClass.toRingHom RingEquiv OreLocalization.instMul CommMonoid.toMonoid OreLocalization.instAdd AddCommMonoid.toAddMonoid NonUnitalNonAssocSemiring.toAddCommMonoid NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing Module.toDistribMulAction Ring.toSemiring CommRing.toRing Semiring.toModule EquivLike.toFunLike RingEquiv.instEquivLike Semiring.toNonAssocSemiring RingEquivClass.toRingHomClass RingEquiv.instRingEquivClass RingEquiv.symm WittVector.FractionRing.frobenius WittVector.inv_pair₁ WittVector.inv_pair₂ AddCommGroup.toAddCommMonoid WittVector.Isocrystal.toModule DFinsupp.instEquivLikeLinearEquiv WittVector.Isocrystal.frobenius RingHom.id RingHomInvPair.ids toLinearEquiv	—	expChar_prime

WittVector.IsocrystalHom

Definitions

Name	Category	Theorems
toLinearMap 📖	CompOp	1 math math: frob_equivariant

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
frob_equivariant 📖	mathematical	—	DFunLike.coe LinearEquiv FractionRing WittVector WittVector.instCommRing OreLocalization.instSemiring CommSemiring.toSemiring CommRing.toCommSemiring nonZeroDivisors Semiring.toMonoidWithZero OreLocalization.oreSetComm CommRing.toCommMonoid WittVector.FractionRing.frobeniusRingHom RingHomClass.toRingHom RingEquiv OreLocalization.instMul CommMonoid.toMonoid OreLocalization.instAdd AddCommMonoid.toAddMonoid NonUnitalNonAssocSemiring.toAddCommMonoid NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing Module.toDistribMulAction Ring.toSemiring CommRing.toRing Semiring.toModule EquivLike.toFunLike RingEquiv.instEquivLike Semiring.toNonAssocSemiring RingEquivClass.toRingHomClass RingEquiv.instRingEquivClass RingEquiv.symm WittVector.FractionRing.frobenius WittVector.inv_pair₁ WittVector.inv_pair₂ AddCommGroup.toAddCommMonoid WittVector.Isocrystal.toModule DFinsupp.instEquivLikeLinearEquiv WittVector.Isocrystal.frobenius LinearMap RingHom.id LinearMap.instFunLike toLinearMap	—	expChar_prime

WittVector.StandardOneDimIsocrystal

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
frobenius_apply 📖	mathematical	—	DFunLike.coe LinearEquiv FractionRing WittVector WittVector.instCommRing OreLocalization.instSemiring CommSemiring.toSemiring CommRing.toCommSemiring nonZeroDivisors Semiring.toMonoidWithZero OreLocalization.oreSetComm CommRing.toCommMonoid WittVector.FractionRing.frobeniusRingHom RingHomClass.toRingHom RingEquiv OreLocalization.instMul CommMonoid.toMonoid OreLocalization.instAdd AddCommMonoid.toAddMonoid NonUnitalNonAssocSemiring.toAddCommMonoid NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing Module.toDistribMulAction Ring.toSemiring CommRing.toRing Semiring.toModule EquivLike.toFunLike RingEquiv.instEquivLike Semiring.toNonAssocSemiring RingEquivClass.toRingHomClass RingEquiv.instRingEquivClass RingEquiv.symm WittVector.FractionRing.frobenius WittVector.inv_pair₁ WittVector.inv_pair₂ WittVector.StandardOneDimIsocrystal AddCommGroup.toAddCommMonoid WittVector.instAddCommGroupStandardOneDimIsocrystal WittVector.Isocrystal.toModule WittVector.instIsocrystalStandardOneDimIsocrystal DFinsupp.instEquivLikeLinearEquiv WittVector.Isocrystal.frobenius OreLocalization.instSMul Monoid.toMulAction DivInvMonoid.toZPow DivisionRing.toDivInvMonoid OreLocalization.instDivisionRingNonZeroDivisors WittVector.instNontrivial IsDomain.toNontrivial WittVector.instNoZeroDivisorsOfCharP IsDomain.to_noZeroDivisors AddMonoidWithOne.toNatCast AddGroupWithOne.toAddMonoidWithOne Ring.toAddGroupWithOne OreLocalization.instRing RingHom RingHom.instFunLike	—	expChar_prime RingEquivClass.toRingHomClass RingEquiv.instRingEquivClass WittVector.inv_pair₁ WittVector.inv_pair₂

---

← Back to Index