Documentation Verification Report

Module

📁 Source: Mathlib/Algebra/Colimit/Module.lean

Statistics

Metric	Count
Definitions `addCommGroup`, `instAddCommMonoid`, `instInhabited`, `instUniqueOfIsEmpty`, `map`, `of`, `Eqv`, `addCommGroup`, `addCommMonoid`, `inhabited`, `linearEquiv`, `map`, `moduleCon`, `of`, `unique`	15
Theorems `congr_apply_of`, `congr_symm_apply_of`, `directedSystem`, `hom_ext`, `hom_ext_iff`, `induction_on`, `lift_comp_of`, `lift_injective`, `lift_of`, `lift_of'`, `map_apply_of`, `map_comp`, `map_id`, `zero_exact`, `of_f`, `congr_apply_of`, `congr_symm_apply_of`, `exists_eq_of_of_eq`, `exists_of`, `exists_of₂`, `hom_ext`, `hom_ext_iff`, `induction_on`, `lift_comp_of`, `lift_injective`, `lift_of`, `lift_of'`, `linearEquiv_of`, `linearEquiv_symm_mk`, `map_apply_of`, `map_comp`, `map_id`, `zero_exact`, `of_f`, `quotMk_of`, `map_map`, `map_self`	37
Total	52

AddCommGroup.DirectLimit

Definitions

Name	Category	Theorems
`addCommGroup` 📖	CompOp	—
`instAddCommMonoid` 📖	CompOp	11 math math: `lift_of'`, `of_f`, `congr_apply_of`, `congr_symm_apply_of`, `lift_comp_of`, `lift_of`, `lift_injective`, `map_id`, `map_comp`, `hom_ext_iff`, `map_apply_of`
`instInhabited` 📖	CompOp	—
`instUniqueOfIsEmpty` 📖	CompOp	—
`map` 📖	CompOp	3 math math: `map_id`, `map_comp`, `map_apply_of`
`of` 📖	CompOp	8 math math: `lift_of'`, `of_f`, `congr_apply_of`, `congr_symm_apply_of`, `lift_comp_of`, `lift_of`, `hom_ext_iff`, `map_apply_of`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`congr_apply_of` 📖	mathematical	`AddMonoidHom.comp` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `AddCommMonoid.toAddMonoid` `AddEquiv.toAddMonoidHom` `AddMonoidHomClass.toAddMonoidHom` `AddEquiv` `AddCommMagma.toAdd` `AddCommSemigroup.toAddCommMagma` `AddCommMonoid.toAddCommSemigroup` `EquivLike.toFunLike` `AddEquiv.instEquivLike` `AddEquivClass.instAddMonoidHomClass` `AddEquiv.instAddEquivClass`	`DFunLike.coe` `AddCommGroup.DirectLimit` `instAddCommMonoid` `congr` `AddMonoidHom` `AddMonoidHom.instFunLike` `of`	—	`AddEquivClass.instAddMonoidHomClass` `AddEquiv.instAddEquivClass` `map_apply_of`
`congr_symm_apply_of` 📖	mathematical	`AddMonoidHom.comp` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `AddCommMonoid.toAddMonoid` `AddEquiv.toAddMonoidHom` `AddMonoidHomClass.toAddMonoidHom` `AddEquiv` `AddCommMagma.toAdd` `AddCommSemigroup.toAddCommMagma` `AddCommMonoid.toAddCommSemigroup` `EquivLike.toFunLike` `AddEquiv.instEquivLike` `AddEquivClass.instAddMonoidHomClass` `AddEquiv.instAddEquivClass`	`DFunLike.coe` `AddCommGroup.DirectLimit` `instAddCommMonoid` `AddEquiv.symm` `congr` `AddMonoidHom` `AddMonoidHom.instFunLike` `of`	—	`AddEquivClass.instAddMonoidHomClass` `AddEquiv.instAddEquivClass` `map_apply_of`
`directedSystem` 📖	mathematical	—	`DirectedSystem` `DFunLike.coe` `LinearMap` `Nat.instSemiring` `RingHom.id` `Nat.instNonAssocSemiring` `AddCommMonoid.toNatModule` `LinearMap.instFunLike` `AddMonoidHom.toNatLinearMap`	—	—
`hom_ext` 📖	—	`AddMonoidHom.comp` `AddCommGroup.DirectLimit` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `AddCommMonoid.toAddMonoid` `instAddCommMonoid` `of`	—	—	`AddCon.hom_ext` `DirectSum.addHom_ext'`
`hom_ext_iff` 📖	mathematical	—	`AddMonoidHom.comp` `AddCommGroup.DirectLimit` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `AddCommMonoid.toAddMonoid` `instAddCommMonoid` `of`	—	`hom_ext`
`induction_on` 📖	—	`DFunLike.coe` `AddMonoidHom` `AddCommGroup.DirectLimit` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `AddCommMonoid.toAddMonoid` `instAddCommMonoid` `AddMonoidHom.instFunLike` `of`	—	—	`Module.DirectLimit.induction_on`
`lift_comp_of` 📖	mathematical	—	`lift` `AddMonoidHom.comp` `AddCommGroup.DirectLimit` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `AddCommMonoid.toAddMonoid` `instAddCommMonoid` `of`	—	`hom_ext` `AddMonoidHom.ext` `lift_of`
`lift_injective` 📖	mathematical	`DFunLike.coe` `AddMonoidHom` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `AddCommMonoid.toAddMonoid` `AddMonoidHom.instFunLike`	`AddCommGroup.DirectLimit` `instAddCommMonoid` `lift`	—	`Module.DirectLimit.lift_injective`
`lift_of` 📖	mathematical	`DFunLike.coe` `AddMonoidHom` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `AddCommMonoid.toAddMonoid` `AddMonoidHom.instFunLike`	`AddCommGroup.DirectLimit` `instAddCommMonoid` `lift` `of`	—	`Module.DirectLimit.lift_of`
`lift_of'` 📖	mathematical	—	`lift` `AddCommGroup.DirectLimit` `instAddCommMonoid` `of` `AddMonoidHom.id` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `AddCommMonoid.toAddMonoid`	—	`hom_ext` `AddMonoidHom.ext` `lift_of` `AddMonoidHom.id_comp`
`map_apply_of` 📖	mathematical	`AddMonoidHom.comp` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `AddCommMonoid.toAddMonoid`	`DFunLike.coe` `AddMonoidHom` `AddCommGroup.DirectLimit` `instAddCommMonoid` `AddMonoidHom.instFunLike` `map` `of`	—	`lift_of`
`map_comp` 📖	mathematical	`AddMonoidHom.comp` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `AddCommMonoid.toAddMonoid`	`AddCommGroup.DirectLimit` `instAddCommMonoid` `map`	—	`hom_ext` `AddMonoidHom.ext` `map_apply_of`
`map_id` 📖	mathematical	—	`map` `AddMonoidHom.id` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `AddCommMonoid.toAddMonoid` `AddMonoidHom` `AddMonoidHom.comp` `AddCommGroup.DirectLimit` `instAddCommMonoid`	—	`hom_ext` `AddMonoidHom.ext` `map_apply_of` `AddMonoidHom.id_comp`
`of_f` 📖	mathematical	`Preorder.toLE`	`DFunLike.coe` `AddMonoidHom` `AddCommGroup.DirectLimit` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `AddCommMonoid.toAddMonoid` `instAddCommMonoid` `AddMonoidHom.instFunLike` `of`	—	`Module.DirectLimit.of_f`

AddCommGroup.DirectLimit.of

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`zero_exact` 📖	—	`DFunLike.coe` `AddMonoidHom` `AddCommGroup.DirectLimit` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `AddCommMonoid.toAddMonoid` `AddCommGroup.DirectLimit.instAddCommMonoid` `AddMonoidHom.instFunLike` `AddCommGroup.DirectLimit.of` `AddZero.toZero`	—	—	`Module.DirectLimit.of.zero_exact` `AddCommGroup.DirectLimit.directedSystem`

Module.DirectLimit

Definitions

Name	Category	Theorems
`Eqv` 📖	CompData	—
`addCommGroup` 📖	CompOp	3 math math: `ModuleCat.directLimitIsColimit_desc`, `ModuleCat.directLimitCocone_pt_isAddCommGroup`, `ModuleCat.directLimitCocone_ι_app`
`addCommMonoid` 📖	CompOp	28 math math: `lift_injective`, `map_apply_of`, `lift_of`, `TensorProduct.directLimitRight_tmul_of`, `quotMk_of`, `congr_symm_apply_of`, `map_comp`, `of_f`, `Submodule.FG.lTensor.directLimit_apply'`, `linearEquiv_of`, `Submodule.FG.rTensor.directLimit_apply`, `TensorProduct.directLimitLeft_rTensor_of`, `lift_comp_of`, `congr_apply_of`, `exists_of`, `map_id`, `linearEquiv_symm_mk`, `lift_of'`, `Submodule.FG.lTensor.directLimit_apply`, `Module.fgSystem.equiv_comp_of`, `TensorProduct.directLimitLeft_tmul_of`, `TensorProduct.directLimitLeft_symm_of_tmul`, `TensorProduct.fromDirectLimit_of_tmul`, `TensorProduct.directLimitRight_symm_of_tmul`, `Submodule.FG.rTensor.directLimit_apply'`, `hom_ext_iff`, `exists_of₂`, `TensorProduct.toDirectLimit_tmul_of`
`inhabited` 📖	CompOp	—
`linearEquiv` 📖	CompOp	2 math math: `linearEquiv_of`, `linearEquiv_symm_mk`
`map` 📖	CompOp	3 math math: `map_apply_of`, `map_comp`, `map_id`
`moduleCon` 📖	CompOp	1 math math: `quotMk_of`
`of` 📖	CompOp	26 math math: `map_apply_of`, `lift_of`, `TensorProduct.directLimitRight_tmul_of`, `quotMk_of`, `congr_symm_apply_of`, `of_f`, `Submodule.FG.lTensor.directLimit_apply'`, `linearEquiv_of`, `Submodule.FG.rTensor.directLimit_apply`, `TensorProduct.directLimitLeft_rTensor_of`, `lift_comp_of`, `congr_apply_of`, `exists_of`, `linearEquiv_symm_mk`, `lift_of'`, `Submodule.FG.lTensor.directLimit_apply`, `Module.fgSystem.equiv_comp_of`, `ModuleCat.directLimitCocone_ι_app`, `TensorProduct.directLimitLeft_tmul_of`, `TensorProduct.directLimitLeft_symm_of_tmul`, `TensorProduct.fromDirectLimit_of_tmul`, `TensorProduct.directLimitRight_symm_of_tmul`, `Submodule.FG.rTensor.directLimit_apply'`, `hom_ext_iff`, `exists_of₂`, `TensorProduct.toDirectLimit_tmul_of`
`unique` 📖	CompOp	—

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`congr_apply_of` 📖	mathematical	`LinearMap.comp` `RingHom.id` `Semiring.toNonAssocSemiring` `RingHomCompTriple.ids` `LinearEquiv.toLinearMap` `RingHomInvPair.ids`	`DFunLike.coe` `LinearEquiv` `Module.DirectLimit` `addCommMonoid` `module` `EquivLike.toFunLike` `DFinsupp.instEquivLikeLinearEquiv` `congr` `LinearMap` `LinearMap.instFunLike` `of`	—	`RingHomInvPair.ids` `RingHomCompTriple.ids` `map_apply_of`
`congr_symm_apply_of` 📖	mathematical	`LinearMap.comp` `RingHom.id` `Semiring.toNonAssocSemiring` `RingHomCompTriple.ids` `LinearEquiv.toLinearMap` `RingHomInvPair.ids`	`DFunLike.coe` `LinearEquiv` `Module.DirectLimit` `addCommMonoid` `module` `EquivLike.toFunLike` `DFinsupp.instEquivLikeLinearEquiv` `LinearEquiv.symm` `congr` `LinearMap` `LinearMap.instFunLike` `of`	—	`RingHomInvPair.ids` `RingHomCompTriple.ids` `map_apply_of` `LinearEquiv.toLinearMap_symm_comp_eq` `LinearMap.comp_assoc` `LinearEquiv.comp_coe` `RingHomInvPair.triples₂` `LinearEquiv.symm_trans_self` `LinearEquiv.refl_toLinearMap` `LinearMap.comp_id`
`exists_eq_of_of_eq` 📖	—	`DFunLike.coe` `LinearMap` `RingHom.id` `Semiring.toNonAssocSemiring` `Module.DirectLimit` `addCommMonoid` `module` `LinearMap.instFunLike` `of`	—	—	`RingHomInvPair.ids` `DistribMulActionSemiHomClass.toAddMonoidHomClass` `SemilinearMapClass.distribMulActionSemiHomClass` `LinearMap.semilinearMapClass` `linearEquiv_of`
`exists_of` 📖	mathematical	—	`DFunLike.coe` `LinearMap` `RingHom.id` `Semiring.toNonAssocSemiring` `Module.DirectLimit` `addCommMonoid` `module` `LinearMap.instFunLike` `of`	—	`Quotient.inductionOn'` `DirectSum.induction_on` `map_zero` `AddMonoidHomClass.toZeroHomClass` `DistribMulActionSemiHomClass.toAddMonoidHomClass` `SemilinearMapClass.distribMulActionSemiHomClass` `LinearMap.semilinearMapClass` `exists_ge_ge` `map_add` `SemilinearMapClass.toAddHomClass` `of_f`
`exists_of₂` 📖	mathematical	—	`DFunLike.coe` `LinearMap` `RingHom.id` `Semiring.toNonAssocSemiring` `Module.DirectLimit` `addCommMonoid` `module` `LinearMap.instFunLike` `of`	—	`exists_of` `exists_ge_ge` `of_f`
`hom_ext` 📖	—	`LinearMap.comp` `Module.DirectLimit` `addCommMonoid` `module` `RingHom.id` `Semiring.toNonAssocSemiring` `RingHomCompTriple.ids` `of`	—	—	`RingHomCompTriple.ids` `LinearMap.toAddMonoidHom_injective` `AddCon.hom_ext` `DirectSum.addHom_ext'`
`hom_ext_iff` 📖	mathematical	—	`LinearMap.comp` `Module.DirectLimit` `addCommMonoid` `module` `RingHom.id` `Semiring.toNonAssocSemiring` `RingHomCompTriple.ids` `of`	—	`RingHomCompTriple.ids` `hom_ext`
`induction_on` 📖	—	`DFunLike.coe` `LinearMap` `RingHom.id` `Semiring.toNonAssocSemiring` `Module.DirectLimit` `addCommMonoid` `module` `LinearMap.instFunLike` `of`	—	—	`exists_of`
`lift_comp_of` 📖	mathematical	—	`lift` `LinearMap.comp` `Module.DirectLimit` `addCommMonoid` `module` `RingHom.id` `Semiring.toNonAssocSemiring` `RingHomCompTriple.ids` `of`	—	`hom_ext` `RingHomCompTriple.ids` `LinearMap.ext` `lift_of`
`lift_injective` 📖	mathematical	`DFunLike.coe` `LinearMap` `RingHom.id` `Semiring.toNonAssocSemiring` `LinearMap.instFunLike`	`Module.DirectLimit` `addCommMonoid` `module` `lift`	—	`isEmpty_or_nonempty` `Function.injective_of_subsingleton` `Unique.instSubsingleton` `exists_of₂` `lift_of`
`lift_of` 📖	mathematical	`DFunLike.coe` `LinearMap` `RingHom.id` `Semiring.toNonAssocSemiring` `LinearMap.instFunLike`	`Module.DirectLimit` `addCommMonoid` `module` `lift` `of`	—	`DirectSum.toModule_lof`
`lift_of'` 📖	mathematical	—	`lift` `Module.DirectLimit` `addCommMonoid` `module` `of` `LinearMap.id`	—	`hom_ext` `LinearMap.ext` `RingHomCompTriple.ids` `lift_of`
`linearEquiv_of` 📖	mathematical	—	`DFunLike.coe` `LinearEquiv` `RingHom.id` `Semiring.toNonAssocSemiring` `RingHomInvPair.ids` `Module.DirectLimit` `DirectLimit` `LinearMap` `LinearMap.instFunLike` `addCommMonoid` `DirectLimit.instAddCommMonoidOfAddMonoidHomClass` `module` `DirectLimit.instModule` `EquivLike.toFunLike` `DFinsupp.instEquivLikeLinearEquiv` `linearEquiv` `of` `DirectLimit.setoid`	—	`RingHomInvPair.ids` `DistribMulActionSemiHomClass.toAddMonoidHomClass` `SemilinearMapClass.distribMulActionSemiHomClass` `LinearMap.semilinearMapClass` `lift_of`
`linearEquiv_symm_mk` 📖	mathematical	—	`DFunLike.coe` `LinearEquiv` `RingHom.id` `Semiring.toNonAssocSemiring` `RingHomInvPair.ids` `DirectLimit` `LinearMap` `LinearMap.instFunLike` `Module.DirectLimit` `DirectLimit.instAddCommMonoidOfAddMonoidHomClass` `addCommMonoid` `DirectLimit.instModule` `module` `EquivLike.toFunLike` `DFinsupp.instEquivLikeLinearEquiv` `LinearEquiv.symm` `linearEquiv` `DirectLimit.setoid` `of`	—	`RingHomInvPair.ids` `DistribMulActionSemiHomClass.toAddMonoidHomClass` `SemilinearMapClass.distribMulActionSemiHomClass` `LinearMap.semilinearMapClass`
`map_apply_of` 📖	mathematical	`LinearMap.comp` `RingHom.id` `Semiring.toNonAssocSemiring` `RingHomCompTriple.ids`	`DFunLike.coe` `LinearMap` `Module.DirectLimit` `addCommMonoid` `module` `LinearMap.instFunLike` `map` `of`	—	`RingHomCompTriple.ids` `lift_of`
`map_comp` 📖	mathematical	`LinearMap.comp` `RingHom.id` `Semiring.toNonAssocSemiring` `RingHomCompTriple.ids`	`Module.DirectLimit` `addCommMonoid` `module` `map`	—	`RingHomCompTriple.ids` `hom_ext` `LinearMap.ext` `map_apply_of`
`map_id` 📖	mathematical	—	`map` `LinearMap.id` `LinearMap` `RingHom.id` `Semiring.toNonAssocSemiring` `LinearMap.comp` `RingHomCompTriple.ids` `Module.DirectLimit` `addCommMonoid` `module`	—	`hom_ext` `RingHomCompTriple.ids` `LinearMap.ext` `map_apply_of`
`of_f` 📖	mathematical	`Preorder.toLE`	`DFunLike.coe` `LinearMap` `RingHom.id` `Semiring.toNonAssocSemiring` `Module.DirectLimit` `addCommMonoid` `module` `LinearMap.instFunLike` `of`	—	`AddCon.eq`
`quotMk_of` 📖	mathematical	—	`DirectSum` `AddCon.toSetoid` `AddCommMagma.toAdd` `AddCommSemigroup.toAddCommMagma` `AddCommMonoid.toAddCommSemigroup` `instAddCommMonoidDirectSum` `ModuleCon.toAddCon` `SMulZeroClass.toSMul` `AddZero.toZero` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `AddCommMonoid.toAddMonoid` `DistribSMul.toSMulZeroClass` `DistribMulAction.toDistribSMul` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `Module.toDistribMulAction` `DirectSum.instModule` `moduleCon` `DFunLike.coe` `AddMonoidHom` `AddMonoidHom.instFunLike` `DirectSum.of` `LinearMap` `RingHom.id` `Semiring.toNonAssocSemiring` `Module.DirectLimit` `addCommMonoid` `module` `LinearMap.instFunLike` `of`	—	—

Module.DirectLimit.of

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`zero_exact` 📖	—	`DFunLike.coe` `LinearMap` `RingHom.id` `Semiring.toNonAssocSemiring` `Module.DirectLimit` `Module.DirectLimit.addCommMonoid` `Module.DirectLimit.module` `LinearMap.instFunLike` `Module.DirectLimit.of` `AddZero.toZero` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `AddCommMonoid.toAddMonoid`	—	—	`map_zero` `AddMonoidHomClass.toZeroHomClass` `DistribMulActionSemiHomClass.toAddMonoidHomClass` `SemilinearMapClass.distribMulActionSemiHomClass` `LinearMap.semilinearMapClass` `Module.DirectLimit.exists_eq_of_of_eq`

Module.DirectedSystem

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`map_map` 📖	mathematical	`Preorder.toLE`	`DFunLike.coe` `LE.le.trans`	—	`DirectedSystem.map_map'`
`map_self` 📖	mathematical	—	`DFunLike.coe` `le_rfl`	—	`DirectedSystem.map_self'`

---

← Back to Index