Truncated

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

Statistics

Metric	Count
Definitions Truncated, Truncated, Truncated, TruncatedWittVector, coeff, hasIntScalar, hasNatPow, hasNatScalar, instAdd, instCommRing, instFintype, instIntCast, instMul, instNatCast, instNeg, instOne, instSub, instZero, mk, out, truncate, liftEquiv, liftFun, truncate, truncateFun, instInhabitedTruncatedWittVector, witt_truncateFun_tac	27
Theorems card, coeff_mk, coeff_out, coeff_truncate, coeff_zero, ext, ext_iff, iInf_ker_truncate, mk_coeff, out_injective, truncateFun_out, truncate_comp, truncate_comp_wittVector_truncate, truncate_surjective, truncate_truncate, truncate_wittVector_truncate, coeff_truncate, coeff_truncateFun, hom_ext, liftEquiv_apply, liftEquiv_symm_apply_coe, lift_unique, mem_ker_truncate, out_truncateFun, truncateFun_add, truncateFun_intCast, truncateFun_mul, truncateFun_natCast, truncateFun_neg, truncateFun_nsmul, truncateFun_one, truncateFun_pow, truncateFun_sub, truncateFun_surjective, truncateFun_zero, truncateFun_zsmul, truncate_comp_lift, truncate_lift, truncate_liftFun, truncate_mk', truncate_surjective	41
Total	68

CategoryTheory.CosimplicialObject

Definitions

Name	Category	Theorems
Truncated 📖	CompOp	8 math math: Truncated.whiskering_obj_obj_obj, Truncated.whiskering_map_app_app, Truncated.whiskering_obj_map_app, Truncated.instHasColimits, Truncated.instHasLimitsOfShape, Truncated.instHasColimitsOfShape, Truncated.instHasLimits, Truncated.whiskering_obj_obj_map

CategoryTheory.SimplicialObject

Definitions

Name	Category	Theorems
Truncated 📖	CompOp	22 math math: Truncated.instHasLimits, Truncated.whiskering_obj_obj_obj, Truncated.whiskering_map_app_app, Truncated.cosk.full, instIsRightKanExtensionOppositeTruncatedSimplexCategoryObjCoskAppTruncatedCounitCoskAdjTruncation, Truncated.instHasColimits, Truncated.cosk.faithful, Truncated.trunc_obj_obj, isoCoskOfIsCoskeletal_hom, Truncated.sk.full, instIsIsoAppUnitTruncatedCoskAdj, Truncated.trunc_obj_map, Truncated.trunc_map_app, Truncated.instHasLimitsOfShape, Truncated.whiskering_obj_obj_map, Truncated.cosk_reflective, Truncated.sk_coreflective, Truncated.sk.faithful, instIsLeftKanExtensionOppositeTruncatedSimplexCategoryObjSkAppTruncatedUnitSkAdjTruncation, isCoskeletal_iff_isIso, Truncated.instHasColimitsOfShape, Truncated.whiskering_obj_map_app

SSet

Definitions

Name	Category	Theorems
Truncated 📖	CompOp	88 math math: OneTruncation₂.nerveEquiv_apply, Truncated.HomotopyCategory.BinaryProduct.iso_inv_toFunctor, Truncated.tensor_map_apply_snd, oneTruncation₂_obj, OneTruncation₂.ofNerve₂.natIso_hom_app_map, CategoryTheory.nerve.instFullCatTruncatedOfNatNatNerveFunctor₂, Truncated.sk.full, Truncated.HomotopyCategory.descOfTruncation_comp, instIsDiscreteHomotopyCategoryObjTruncatedOfNatNatTruncationSimplexCategoryStdSimplexMk, oneTruncation₂_map, Truncated.Path.mk₂_arrow, Truncated.HomotopyCategory.BinaryProduct.inverse_map_mkHom_id_homMk, OneTruncation₂.nerveHomEquiv_id, CategoryTheory.nerve.functorOfNerveMap_map, Truncated.sk_coreflective, Truncated.Edge.map_fst, Truncated.HomotopyCategory.BinaryProduct.functorCompInverseIso_inv_app, Truncated.HomotopyCategory.BinaryProduct.functorCompInverseIso_hom_app, Edge.ofTruncated_edge, Truncated.HomotopyCategory.BinaryProduct.inverse_comp_mapHomotopyCategory_fst, OneTruncation₂.ofNerve₂.natIso_inv_app_obj_obj, Truncated.Edge.CompStruct.tensor_simplex_snd, Truncated.HomotopyCategory.BinaryProduct.inverse_comp_mapHomotopyCategory_snd, Truncated.Edge.id_tensor_id, CategoryTheory.Nerve.instIsStrictSegalObjCatTruncatedOfNatNatNerveFunctor₂, OneTruncation₂.ofNerve₂.natIso_hom_app_obj, Truncated.id_app, Truncated.HomotopyCategory.BinaryProduct.left_unitality, Truncated.Edge.CompStruct.tensor_simplex_fst, Truncated.hasColimits, Truncated.HomotopyCategory.BinaryProduct.inverseCompFunctorIso_inv_app, Truncated.Edge.map_associator_hom, OneTruncation₂.nerveEquiv_symm_apply_map, Truncated.HomotopyCategory.BinaryProduct.iso_hom_toFunctor, Truncated.Edge.map_whiskerLeft, Truncated.HomotopyCategory.BinaryProduct.inverse_map_mkHom_homMk_id, Truncated.HomotopyCategory.BinaryProduct.mapHomotopyCategory_prod_id_comp_inverse, Truncated.Edge.map_snd, Truncated.HomotopyCategory.BinaryProduct.functor_comp_inverse, Truncated.HomotopyCategory.descOfTruncation_map_homMk, Truncated.HomotopyCategory.BinaryProduct.inverse_map_mkHom_homMk_homMk, Truncated.hoFunctor₂_naturality, Truncated.HomotopyCategory.BinaryProduct.inverse_comp_functor, Truncated.HomotopyCategory.homToNerveMk_app_one, Truncated.comp_app_assoc, Truncated.Edge.map_tensorHom, Truncated.HomotopyCategory.BinaryProduct.associativity'Iso_hom_app, horn.spineId_vertex_coe, Truncated.tensor_map_apply_fst, Truncated.HomotopyCategory.BinaryProduct.functor_obj, horn.spineId_arrow_coe, Truncated.Edge.tensor_edge, Truncated.cosk.faithful, Subcomplex.liftPath_arrow_coe, Truncated.HomotopyCategory.BinaryProduct.square, Truncated.HomotopyCategory.BinaryProduct.inverseCompFunctorIso_hom_app, Truncated.HomotopyCategory.homToNerveMk_app_edge, OneTruncation₂.ofNerve₂.natIso_inv_app_map, Truncated.trunc_spine, Truncated.cosk.full, Truncated.HomotopyCategory.BinaryProduct.associativity, OneTruncation₂.nerveEquiv_symm_apply_obj, Subcomplex.liftPath_vertex_coe, OneTruncation₂.ofNerve₂.natIso_inv_app_obj_map, Truncated.HomotopyCategory.BinaryProduct.right_unitality, Truncated.cosk_reflective, CategoryTheory.nerve.functorOfNerveMap_nerveFunctor₂_map, Truncated.Path.mk₂_vertex, OneTruncation₂.nerveHomEquiv_apply, Truncated.HomotopyCategory.BinaryProduct.associativityIso_hom_app, Truncated.HomotopyCategory.homToNerveMk_app_zero, Truncated.Edge.map_whiskerRight, Truncated.comp_app, truncation_spine, Truncated.HomotopyCategory.homToNerveMk_comp, Truncated.HomotopyCategory.BinaryProduct.functor_map, CategoryTheory.nerve.functorOfNerveMap_obj, CategoryTheory.nerve.nerveFunctor₂_map_functorOfNerveMap, Truncated.HomotopyCategory.BinaryProduct.id_prod_mapHomotopyCategory_comp_inverse, Edge.toTruncated_id, Truncated.sk.faithful, StrictSegal.instIsStrictSegalObjTruncatedHAddNatOfNatTruncationOfIsStrictSegal, Truncated.HomotopyCategory.descOfTruncation_obj_mk, Truncated.HomotopyCategory.BinaryProduct.inverse_obj, Truncated.HomotopyCategory.homToNerveMk_comp_assoc, CategoryTheory.nerve.instFaithfulCatTruncatedOfNatNatNerveFunctor₂, Edge.toTruncated_edge, Truncated.hasLimits

TruncatedWittVector

Definitions

Name	Category	Theorems
coeff 📖	CompOp	8 math math: WittVector.coeff_truncate, coeff_out, coeff_zero, mk_coeff, WittVector.coeff_truncateFun, coeff_mk, ext_iff, coeff_truncate
hasIntScalar 📖	CompOp	1 math math: WittVector.truncateFun_zsmul
hasNatPow 📖	CompOp	1 math math: WittVector.truncateFun_pow
hasNatScalar 📖	CompOp	1 math math: WittVector.truncateFun_nsmul
instAdd 📖	CompOp	5 math math: WittVector.truncateFun_add, commutes_symm', zmodEquivTrunc_apply, commutes', commutes_symm
instCommRing 📖	CompOp	19 math math: WittVector.coeff_truncate, iInf_ker_truncate, truncate_wittVector_truncate, WittVector.truncate_surjective, commutes_symm', truncate_truncate, WittVector.mem_ker_truncate, truncate_comp_wittVector_truncate, charP_zmod, truncate_surjective, truncate_comp, WittVector.liftEquiv_symm_apply_coe, zmodEquivTrunc_apply, coeff_truncate, commutes, WittVector.truncate_mk', commutes', WittVector.zmodEquivTrunc_compat, commutes_symm
instFintype 📖	CompOp	2 math math: card, card_zmod
instIntCast 📖	CompOp	1 math math: WittVector.truncateFun_intCast
instMul 📖	CompOp	5 math math: commutes_symm', zmodEquivTrunc_apply, WittVector.truncateFun_mul, commutes', commutes_symm
instNatCast 📖	CompOp	1 math math: WittVector.truncateFun_natCast
instNeg 📖	CompOp	1 math math: WittVector.truncateFun_neg
instOne 📖	CompOp	1 math math: WittVector.truncateFun_one
instSub 📖	CompOp	1 math math: WittVector.truncateFun_sub
instZero 📖	CompOp	2 math math: WittVector.truncateFun_zero, coeff_zero
mk 📖	CompOp	—
out 📖	CompOp	4 math math: truncateFun_out, coeff_out, out_injective, WittVector.out_truncateFun
truncate 📖	CompOp	11 math math: truncate_wittVector_truncate, commutes_symm', truncate_truncate, truncate_comp_wittVector_truncate, truncate_surjective, truncate_comp, coeff_truncate, commutes, commutes', WittVector.zmodEquivTrunc_compat, commutes_symm

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
card 📖	mathematical	—	Fintype.card TruncatedWittVector instFintype Monoid.toNatPow Nat.instMonoid	—	Fintype.card_fun Fintype.card_fin
coeff_mk 📖	mathematical	—	coeff	—	—
coeff_out 📖	mathematical	—	WittVector.coeff out coeff	—	out.eq_1
coeff_truncate 📖	mathematical	—	coeff DFunLike.coe RingHom TruncatedWittVector Semiring.toNonAssocSemiring CommSemiring.toSemiring CommRing.toCommSemiring instCommRing RingHom.instFunLike truncate	—	WittVector.truncate_surjective truncate_wittVector_truncate WittVector.coeff_truncate
coeff_zero 📖	mathematical	—	coeff TruncatedWittVector instZero MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing	—	WittVector.coeff_truncateFun WittVector.zero_coeff
ext 📖	—	coeff	—	—	—
ext_iff 📖	mathematical	—	coeff	—	ext
iInf_ker_truncate 📖	mathematical	—	iInf Ideal WittVector CommSemiring.toSemiring CommRing.toCommSemiring WittVector.instCommRing Submodule.instInfSet NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring Semiring.toModule RingHom.ker TruncatedWittVector RingHom instCommRing RingHom.instFunLike RingHom.instRingHomClass WittVector.truncate Bot.bot Submodule.instBot	—	RingHom.instRingHomClass Submodule.eq_bot_iff WittVector.ext WittVector.zero_coeff
mk_coeff 📖	mathematical	—	coeff	—	ext
out_injective 📖	mathematical	—	TruncatedWittVector WittVector out	—	ext coeff_out WittVector.ext_iff
truncateFun_out 📖	mathematical	—	WittVector.truncateFun out	—	coeff_out mk_coeff
truncate_comp 📖	mathematical	—	RingHom.comp TruncatedWittVector Semiring.toNonAssocSemiring CommSemiring.toSemiring CommRing.toCommSemiring instCommRing truncate LE.le.trans Nat.instPreorder	—	RingHom.ext LE.le.trans truncate_truncate
truncate_comp_wittVector_truncate 📖	mathematical	—	RingHom.comp WittVector TruncatedWittVector Semiring.toNonAssocSemiring CommSemiring.toSemiring CommRing.toCommSemiring WittVector.instCommRing instCommRing truncate WittVector.truncate	—	RingHom.liftOfRightInverse_comp truncateFun_out
truncate_surjective 📖	mathematical	—	TruncatedWittVector DFunLike.coe RingHom Semiring.toNonAssocSemiring CommSemiring.toSemiring CommRing.toCommSemiring instCommRing RingHom.instFunLike truncate	—	WittVector.truncate_surjective truncate_wittVector_truncate
truncate_truncate 📖	mathematical	—	DFunLike.coe RingHom TruncatedWittVector Semiring.toNonAssocSemiring CommSemiring.toSemiring CommRing.toCommSemiring instCommRing RingHom.instFunLike truncate LE.le.trans Nat.instPreorder	—	LE.le.trans WittVector.truncate_surjective truncate_wittVector_truncate
truncate_wittVector_truncate 📖	mathematical	—	DFunLike.coe RingHom TruncatedWittVector Semiring.toNonAssocSemiring CommSemiring.toSemiring CommRing.toCommSemiring instCommRing RingHom.instFunLike truncate WittVector WittVector.instCommRing WittVector.truncate	—	RingHom.liftOfRightInverse_comp_apply truncateFun_out

WittVector

Definitions

Name	Category	Theorems
liftEquiv 📖	CompOp	2 math math: liftEquiv_apply, liftEquiv_symm_apply_coe
liftFun 📖	CompOp	1 math math: truncate_liftFun
truncate 📖	CompOp	11 math math: coeff_truncate, truncate_comp_lift, TruncatedWittVector.iInf_ker_truncate, TruncatedWittVector.truncate_wittVector_truncate, truncate_surjective, mem_ker_truncate, TruncatedWittVector.truncate_comp_wittVector_truncate, truncate_lift, liftEquiv_symm_apply_coe, truncate_mk', truncate_liftFun
truncateFun 📖	CompOp	19 math math: RecursionMain.succNthVal_spec', TruncatedWittVector.truncateFun_out, truncateFun_one, truncateFun_surjective, truncateFun_zero, truncateFun_add, truncateFun_pow, coeff_truncateFun, truncateFun_intCast, truncateFun_neg, truncateFun_natCast, nth_mul_coeff, truncateFun_nsmul, truncateFun_mul, out_truncateFun, nthRemainder_spec, truncateFun_sub, truncateFun_zsmul, nth_mul_coeff'

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
coeff_truncate 📖	mathematical	—	TruncatedWittVector.coeff DFunLike.coe RingHom WittVector TruncatedWittVector Semiring.toNonAssocSemiring CommSemiring.toSemiring CommRing.toCommSemiring instCommRing TruncatedWittVector.instCommRing RingHom.instFunLike truncate coeff	—	coeff_truncateFun
coeff_truncateFun 📖	mathematical	—	TruncatedWittVector.coeff truncateFun coeff	—	truncateFun.eq_1
hom_ext 📖	—	RingHom.comp WittVector TruncatedWittVector Semiring.toNonAssocSemiring CommSemiring.toSemiring CommRing.toCommSemiring instCommRing TruncatedWittVector.instCommRing truncate	—	—	Equiv.injective
liftEquiv_apply 📖	mathematical	—	DFunLike.coe Equiv RingHom WittVector Semiring.toNonAssocSemiring CommSemiring.toSemiring CommRing.toCommSemiring instCommRing EquivLike.toFunLike Equiv.instEquivLike liftEquiv lift	—	—
liftEquiv_symm_apply_coe 📖	mathematical	—	DFunLike.coe Equiv RingHom WittVector Semiring.toNonAssocSemiring CommSemiring.toSemiring CommRing.toCommSemiring instCommRing EquivLike.toFunLike Equiv.instEquivLike Equiv.symm liftEquiv RingHom.comp TruncatedWittVector TruncatedWittVector.instCommRing truncate	—	—
lift_unique 📖	mathematical	RingHom.comp TruncatedWittVector Semiring.toNonAssocSemiring CommSemiring.toSemiring CommRing.toCommSemiring TruncatedWittVector.instCommRing TruncatedWittVector.truncate WittVector instCommRing truncate	lift	—	RingHom.ext sub_eq_zero Ideal.mem_bot RingHom.instRingHomClass TruncatedWittVector.iInf_ker_truncate Ideal.mem_iInf map_sub RingHomClass.toAddMonoidHomClass truncate_comp_lift sub_self
mem_ker_truncate 📖	mathematical	—	WittVector Ideal CommSemiring.toSemiring CommRing.toCommSemiring instCommRing SetLike.instMembership Submodule.setLike NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring Semiring.toModule RingHom.ker TruncatedWittVector RingHom TruncatedWittVector.instCommRing RingHom.instFunLike RingHom.instRingHomClass truncate coeff MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing	—	RingHom.instRingHomClass truncateFun_one truncateFun_mul truncateFun_zero truncateFun_add TruncatedWittVector.coeff_zero
out_truncateFun 📖	mathematical	—	TruncatedWittVector.out truncateFun init	—	ext coeff_truncateFun
truncateFun_add 📖	mathematical	—	truncateFun WittVector instAdd TruncatedWittVector TruncatedWittVector.instAdd	—	TruncatedWittVector.out_injective out_truncateFun init_add
truncateFun_intCast 📖	mathematical	—	truncateFun WittVector instIntCast TruncatedWittVector TruncatedWittVector.instIntCast	—	—
truncateFun_mul 📖	mathematical	—	truncateFun WittVector instMul TruncatedWittVector TruncatedWittVector.instMul	—	TruncatedWittVector.out_injective out_truncateFun init_mul
truncateFun_natCast 📖	mathematical	—	truncateFun WittVector instNatCast TruncatedWittVector TruncatedWittVector.instNatCast	—	—
truncateFun_neg 📖	mathematical	—	truncateFun WittVector instNeg TruncatedWittVector TruncatedWittVector.instNeg	—	TruncatedWittVector.out_injective out_truncateFun init_neg
truncateFun_nsmul 📖	mathematical	—	truncateFun WittVector hasNatScalar TruncatedWittVector TruncatedWittVector.hasNatScalar	—	TruncatedWittVector.out_injective out_truncateFun init_nsmul
truncateFun_one 📖	mathematical	—	truncateFun WittVector instOne TruncatedWittVector TruncatedWittVector.instOne	—	—
truncateFun_pow 📖	mathematical	—	truncateFun WittVector hasNatPow TruncatedWittVector TruncatedWittVector.hasNatPow	—	TruncatedWittVector.out_injective out_truncateFun init_pow
truncateFun_sub 📖	mathematical	—	truncateFun WittVector instSub TruncatedWittVector TruncatedWittVector.instSub	—	TruncatedWittVector.out_injective out_truncateFun init_sub
truncateFun_surjective 📖	mathematical	—	WittVector TruncatedWittVector truncateFun	—	TruncatedWittVector.truncateFun_out
truncateFun_zero 📖	mathematical	—	truncateFun WittVector instZero TruncatedWittVector TruncatedWittVector.instZero	—	—
truncateFun_zsmul 📖	mathematical	—	truncateFun WittVector hasIntScalar TruncatedWittVector TruncatedWittVector.hasIntScalar	—	TruncatedWittVector.out_injective out_truncateFun init_zsmul
truncate_comp_lift 📖	mathematical	RingHom.comp TruncatedWittVector Semiring.toNonAssocSemiring CommSemiring.toSemiring CommRing.toCommSemiring TruncatedWittVector.instCommRing TruncatedWittVector.truncate	WittVector instCommRing truncate lift	—	RingHom.ext RingHom.comp_apply truncate_lift
truncate_lift 📖	mathematical	RingHom.comp TruncatedWittVector Semiring.toNonAssocSemiring CommSemiring.toSemiring CommRing.toCommSemiring TruncatedWittVector.instCommRing TruncatedWittVector.truncate	DFunLike.coe RingHom WittVector instCommRing RingHom.instFunLike truncate lift	—	truncate_liftFun
truncate_liftFun 📖	mathematical	RingHom.comp TruncatedWittVector Semiring.toNonAssocSemiring CommSemiring.toSemiring CommRing.toCommSemiring TruncatedWittVector.instCommRing TruncatedWittVector.truncate	DFunLike.coe RingHom WittVector instCommRing RingHom.instFunLike truncate liftFun	—	TruncatedWittVector.ext truncate_mk' RingHom.comp_apply TruncatedWittVector.coeff_truncate
truncate_mk' 📖	mathematical	—	DFunLike.coe RingHom WittVector TruncatedWittVector Semiring.toNonAssocSemiring CommSemiring.toSemiring CommRing.toCommSemiring instCommRing TruncatedWittVector.instCommRing RingHom.instFunLike truncate mk'	—	TruncatedWittVector.ext coeff_truncate
truncate_surjective 📖	mathematical	—	WittVector TruncatedWittVector DFunLike.coe RingHom Semiring.toNonAssocSemiring CommSemiring.toSemiring CommRing.toCommSemiring instCommRing TruncatedWittVector.instCommRing RingHom.instFunLike truncate	—	truncateFun_surjective

(root)

Definitions

Name	Category	Theorems
TruncatedWittVector 📖	CompOp	35 math math: TruncatedWittVector.card, WittVector.coeff_truncate, TruncatedWittVector.iInf_ker_truncate, TruncatedWittVector.truncate_wittVector_truncate, WittVector.truncateFun_one, WittVector.truncate_surjective, WittVector.truncateFun_surjective, WittVector.truncateFun_zero, WittVector.truncateFun_add, WittVector.truncateFun_pow, TruncatedWittVector.commutes_symm', TruncatedWittVector.truncate_truncate, TruncatedWittVector.coeff_zero, WittVector.mem_ker_truncate, TruncatedWittVector.truncate_comp_wittVector_truncate, TruncatedWittVector.charP_zmod, TruncatedWittVector.out_injective, WittVector.truncateFun_intCast, TruncatedWittVector.truncate_surjective, TruncatedWittVector.truncate_comp, WittVector.truncateFun_neg, TruncatedWittVector.card_zmod, WittVector.truncateFun_natCast, WittVector.liftEquiv_symm_apply_coe, WittVector.truncateFun_nsmul, TruncatedWittVector.zmodEquivTrunc_apply, WittVector.truncateFun_mul, TruncatedWittVector.coeff_truncate, TruncatedWittVector.commutes, WittVector.truncate_mk', TruncatedWittVector.commutes', WittVector.truncateFun_sub, WittVector.truncateFun_zsmul, WittVector.zmodEquivTrunc_compat, TruncatedWittVector.commutes_symm
instInhabitedTruncatedWittVector 📖	CompOp	—
witt_truncateFun_tac 📖	CompOp	—

---

← Back to Index