DirectLimit

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

Statistics

Metric	Count
Definitions `of`, `of`, `instAdd`, `instAddActionOfAddActionHomClass`, `instAddCommGroupOfAddMonoidHomClass`, `instAddCommGroupWithOneOfAddMonoidHomClass`, `instAddCommMagmaOfAddHomClass`, `instAddCommMonoidOfAddMonoidHomClass`, `instAddCommMonoidWithOneOfAddMonoidHomClass`, `instAddCommSemigroupOfAddHomClass`, `instAddGroup`, `instAddGroupWithOne`, `instAddMonoid`, `instAddMonoidWithOne`, `instAddSemigroupOfAddHomClass`, `instAddZeroClassOfAddMonoidHomClass`, `instCommGroupOfMonoidHomClass`, `instCommGroupWithZeroOfMonoidWithZeroHomClass`, `instCommMagmaOfMulHomClass`, `instCommMonoidOfMonoidHomClass`, `instCommMonoidWithZeroOfMonoidWithZeroHomClass`, `instCommRingOfRingHomClass`, `instCommSemigroupOfMulHomClass`, `instCommSemiringOfRingHomClass`, `instDistribMulAction`, `instDistribSMulOfMulActionHomClass`, `instDivisionRing`, `instDivisionSemiring`, `instFieldOfRingHomClass`, `instGroup`, `instGroupWithZero`, `instModule`, `instMonoid`, `instMonoidWithZeroOfMonoidWithZeroHomClass`, `instMul`, `instMulActionOfMulActionHomClass`, `instMulDistribMulActionOfMulActionHomClass`, `instMulOneClassOfMonoidHomClass`, `instMulZeroClassOfMulHomClassOfZeroHomClass`, `instMulZeroOneClass`, `instNonAssocCommRingOfRingHomClass`, `instNonAssocCommSemiringOfRingHomClass`, `instNonAssocRingOfRingHomClass`, `instNonAssocSemiringOfRingHomClass`, `instNonUnitalCommRingOfNonUnitalRingHomClass`, `instNonUnitalCommSemiringOfNonUnitalRingHomClass`, `instNonUnitalNonAssocCommRingOfNonUnitalRingHomClass`, `instNonUnitalNonAssocCommSemiringOfNonUnitalRingHomClass`, `instNonUnitalNonAssocRingOfNonUnitalRingHomClass`, `instNonUnitalNonAssocSemiringOfNonUnitalRingHomClass`, `instNonUnitalRingOfNonUnitalRingHomClass`, `instNonUnitalSemiringOfNonUnitalRingHomClass`, `instOne`, `instRingOfRingHomClass`, `instSMul`, `instSMulWithZeroOfMulActionHomClassOfZeroHomClass`, `instSMulZeroClassOfMulActionHomClass`, `instSemifieldOfRingHomClass`, `instSemigroupOfMulHomClass`, `instSemigroupWithZeroOfMulHomClassOfZeroHomClass`, `instSemiringOfRingHomClass`, `instVAdd`, `instZero`	63
Theorems `hom_ext`, `hom_ext_iff`, `lift_apply`, `lift_of`, `of_f`, `hom_ext`, `hom_ext_iff`, `lift_of`, `of_f`, `add_def`, `div_def`, `div₀_def`, `exists_eq_one`, `exists_eq_zero`, `instNontrivial`, `intCast_def`, `inv_def`, `inv₀_def`, `mul_def`, `natCast_def`, `neg_def`, `nnratCast_def`, `npow_def`, `nsmul_def`, `one_def`, `ratCast_def`, `smul_def`, `sub_def`, `vadd_def`, `zero_def`, `zpow_def`, `zpow₀_def`, `zsmul_def`	33
Total	96

DirectLimit

Definitions

Name	Category	Theorems
`instAdd` 📖	CompOp	3 math math: `add_def`, `Ring.DirectLimit.ringEquiv_of`, `Ring.DirectLimit.ringEquiv_symm_mk`
`instAddActionOfAddActionHomClass` 📖	CompOp	—
`instAddCommGroupOfAddMonoidHomClass` 📖	CompOp	—
`instAddCommGroupWithOneOfAddMonoidHomClass` 📖	CompOp	—
`instAddCommMagmaOfAddHomClass` 📖	CompOp	—
`instAddCommMonoidOfAddMonoidHomClass` 📖	CompOp	6 math math: `Module.of_f`, `Module.lift_of`, `Module.DirectLimit.linearEquiv_of`, `Module.DirectLimit.linearEquiv_symm_mk`, `Module.hom_ext_iff`, `Module.lift_apply`
`instAddCommMonoidWithOneOfAddMonoidHomClass` 📖	CompOp	—
`instAddCommSemigroupOfAddHomClass` 📖	CompOp	—
`instAddGroup` 📖	CompOp	3 math math: `zsmul_def`, `neg_def`, `sub_def`
`instAddGroupWithOne` 📖	CompOp	1 math math: `intCast_def`
`instAddMonoid` 📖	CompOp	1 math math: `nsmul_def`
`instAddMonoidWithOne` 📖	CompOp	1 math math: `natCast_def`
`instAddSemigroupOfAddHomClass` 📖	CompOp	—
`instAddZeroClassOfAddMonoidHomClass` 📖	CompOp	—
`instCommGroupOfMonoidHomClass` 📖	CompOp	—
`instCommGroupWithZeroOfMonoidWithZeroHomClass` 📖	CompOp	—
`instCommMagmaOfMulHomClass` 📖	CompOp	—
`instCommMonoidOfMonoidHomClass` 📖	CompOp	—
`instCommMonoidWithZeroOfMonoidWithZeroHomClass` 📖	CompOp	—
`instCommRingOfRingHomClass` 📖	CompOp	—
`instCommSemigroupOfMulHomClass` 📖	CompOp	—
`instCommSemiringOfRingHomClass` 📖	CompOp	—
`instDistribMulAction` 📖	CompOp	—
`instDistribSMulOfMulActionHomClass` 📖	CompOp	—
`instDivisionRing` 📖	CompOp	1 math math: `ratCast_def`
`instDivisionSemiring` 📖	CompOp	1 math math: `nnratCast_def`
`instFieldOfRingHomClass` 📖	CompOp	—
`instGroup` 📖	CompOp	3 math math: `zpow_def`, `inv_def`, `div_def`
`instGroupWithZero` 📖	CompOp	3 math math: `zpow₀_def`, `inv₀_def`, `div₀_def`
`instModule` 📖	CompOp	6 math math: `Module.of_f`, `Module.lift_of`, `Module.DirectLimit.linearEquiv_of`, `Module.DirectLimit.linearEquiv_symm_mk`, `Module.hom_ext_iff`, `Module.lift_apply`
`instMonoid` 📖	CompOp	1 math math: `npow_def`
`instMonoidWithZeroOfMonoidWithZeroHomClass` 📖	CompOp	—
`instMul` 📖	CompOp	3 math math: `mul_def`, `Ring.DirectLimit.ringEquiv_of`, `Ring.DirectLimit.ringEquiv_symm_mk`
`instMulActionOfMulActionHomClass` 📖	CompOp	—
`instMulDistribMulActionOfMulActionHomClass` 📖	CompOp	—
`instMulOneClassOfMonoidHomClass` 📖	CompOp	—
`instMulZeroClassOfMulHomClassOfZeroHomClass` 📖	CompOp	—
`instMulZeroOneClass` 📖	CompOp	—
`instNonAssocCommRingOfRingHomClass` 📖	CompOp	—
`instNonAssocCommSemiringOfRingHomClass` 📖	CompOp	—
`instNonAssocRingOfRingHomClass` 📖	CompOp	—
`instNonAssocSemiringOfRingHomClass` 📖	CompOp	3 math math: `Ring.of_f`, `Ring.hom_ext_iff`, `Ring.lift_of`
`instNonUnitalCommRingOfNonUnitalRingHomClass` 📖	CompOp	—
`instNonUnitalCommSemiringOfNonUnitalRingHomClass` 📖	CompOp	—
`instNonUnitalNonAssocCommRingOfNonUnitalRingHomClass` 📖	CompOp	—
`instNonUnitalNonAssocCommSemiringOfNonUnitalRingHomClass` 📖	CompOp	—
`instNonUnitalNonAssocRingOfNonUnitalRingHomClass` 📖	CompOp	—
`instNonUnitalNonAssocSemiringOfNonUnitalRingHomClass` 📖	CompOp	—
`instNonUnitalRingOfNonUnitalRingHomClass` 📖	CompOp	—
`instNonUnitalSemiringOfNonUnitalRingHomClass` 📖	CompOp	—
`instOne` 📖	CompOp	2 math math: `exists_eq_one`, `one_def`
`instRingOfRingHomClass` 📖	CompOp	—
`instSMul` 📖	CompOp	1 math math: `smul_def`
`instSMulWithZeroOfMulActionHomClassOfZeroHomClass` 📖	CompOp	—
`instSMulZeroClassOfMulActionHomClass` 📖	CompOp	—
`instSemifieldOfRingHomClass` 📖	CompOp	—
`instSemigroupOfMulHomClass` 📖	CompOp	—
`instSemigroupWithZeroOfMulHomClassOfZeroHomClass` 📖	CompOp	—
`instSemiringOfRingHomClass` 📖	CompOp	—
`instVAdd` 📖	CompOp	1 math math: `vadd_def`
`instZero` 📖	CompOp	2 math math: `exists_eq_zero`, `zero_def`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`add_def` 📖	mathematical	`AddHomClass`	`setoid` `instAdd`	—	`map₂_def`
`div_def` 📖	mathematical	`MonoidHomClass` `MulOneClass.toMulOne` `Monoid.toMulOneClass` `DivInvMonoid.toMonoid` `Group.toDivInvMonoid`	`setoid` `DivInvMonoid.toDiv` `instGroup`	—	`map₂_def`
`div₀_def` 📖	mathematical	`MonoidWithZeroHomClass` `MonoidWithZero.toMulZeroOneClass` `GroupWithZero.toMonoidWithZero`	`setoid` `DivInvMonoid.toDiv` `GroupWithZero.toDivInvMonoid` `instGroupWithZero`	—	`map₂_def`
`exists_eq_one` 📖	mathematical	`OneHomClass`	`setoid` `DirectLimit` `instOne` `DFunLike.coe`	—	`one_def` `Quotient.eq` `map_one`
`exists_eq_zero` 📖	mathematical	`ZeroHomClass`	`setoid` `DirectLimit` `instZero` `DFunLike.coe`	—	`zero_def` `Quotient.eq` `map_zero`
`instNontrivial` 📖	mathematical	`MonoidWithZeroHomClass` `Nontrivial`	`DirectLimit`	—	`Quotient.eq` `map_zero` `MonoidWithZeroHomClass.toZeroHomClass` `map_one` `MonoidHomClass.toOneHomClass` `MonoidWithZeroHomClass.toMonoidHomClass` `NeZero.one`
`intCast_def` 📖	mathematical	`AddMonoidHomClass` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `AddMonoidWithOne.toAddMonoid` `AddGroupWithOne.toAddMonoidWithOne` `OneHomClass` `AddMonoidWithOne.toOne`	`DirectLimit` `AddGroupWithOne.toIntCast` `instAddGroupWithOne` `setoid`	—	`map₀_def` `map_intCast'` `map_one`
`inv_def` 📖	mathematical	`MonoidHomClass` `MulOneClass.toMulOne` `Monoid.toMulOneClass` `DivInvMonoid.toMonoid` `Group.toDivInvMonoid`	`setoid` `InvOneClass.toInv` `DivInvOneMonoid.toInvOneClass` `DivisionMonoid.toDivInvOneMonoid` `Group.toDivisionMonoid` `instGroup`	—	—
`inv₀_def` 📖	mathematical	`MonoidWithZeroHomClass` `MonoidWithZero.toMulZeroOneClass` `GroupWithZero.toMonoidWithZero`	`setoid` `InvOneClass.toInv` `DivInvOneMonoid.toInvOneClass` `DivisionMonoid.toDivInvOneMonoid` `GroupWithZero.toDivisionMonoid` `instGroupWithZero`	—	—
`mul_def` 📖	mathematical	`MulHomClass`	`setoid` `instMul`	—	`map₂_def`
`natCast_def` 📖	mathematical	`AddMonoidHomClass` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `AddMonoidWithOne.toAddMonoid` `OneHomClass` `AddMonoidWithOne.toOne`	`DirectLimit` `AddMonoidWithOne.toNatCast` `instAddMonoidWithOne` `setoid`	—	`map₀_def` `map_natCast'` `map_one`
`neg_def` 📖	mathematical	`AddMonoidHomClass` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `SubNegMonoid.toAddMonoid` `AddGroup.toSubNegMonoid`	`setoid` `NegZeroClass.toNeg` `SubNegZeroMonoid.toNegZeroClass` `SubtractionMonoid.toSubNegZeroMonoid` `AddGroup.toSubtractionMonoid` `instAddGroup`	—	—
`nnratCast_def` 📖	mathematical	`RingHomClass` `Semiring.toNonAssocSemiring` `DivisionSemiring.toSemiring`	`NNRat.cast` `DirectLimit` `DivisionSemiring.toNNRatCast` `instDivisionSemiring` `setoid`	—	`map₀_def` `map_nnratCast`
`npow_def` 📖	mathematical	`MonoidHomClass` `MulOneClass.toMulOne` `Monoid.toMulOneClass`	`setoid` `Monoid.toNatPow` `instMonoid`	—	—
`nsmul_def` 📖	mathematical	`AddMonoidHomClass` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass`	`setoid` `AddMonoid.toNatSMul` `instAddMonoid`	—	—
`one_def` 📖	mathematical	`OneHomClass`	`DirectLimit` `instOne` `setoid`	—	`map₀_def` `map_one`
`ratCast_def` 📖	mathematical	`RingHomClass` `Semiring.toNonAssocSemiring` `DivisionSemiring.toSemiring` `DivisionRing.toDivisionSemiring`	`DirectLimit` `DivisionRing.toRatCast` `instDivisionRing` `setoid`	—	`map₀_def` `map_ratCast`
`smul_def` 📖	mathematical	`MulActionHomClass`	`setoid` `instSMul`	—	—
`sub_def` 📖	mathematical	`AddMonoidHomClass` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `SubNegMonoid.toAddMonoid` `AddGroup.toSubNegMonoid`	`setoid` `SubNegMonoid.toSub` `instAddGroup`	—	`map₂_def`
`vadd_def` 📖	mathematical	`AddActionHomClass`	`HVAdd.hVAdd` `setoid` `instHVAdd` `instVAdd`	—	—
`zero_def` 📖	mathematical	`ZeroHomClass`	`DirectLimit` `instZero` `setoid`	—	`map₀_def` `map_zero`
`zpow_def` 📖	mathematical	`MonoidHomClass` `MulOneClass.toMulOne` `Monoid.toMulOneClass` `DivInvMonoid.toMonoid` `Group.toDivInvMonoid`	`setoid` `DivInvMonoid.toZPow` `instGroup`	—	—
`zpow₀_def` 📖	mathematical	`MonoidWithZeroHomClass` `MonoidWithZero.toMulZeroOneClass` `GroupWithZero.toMonoidWithZero`	`setoid` `DivInvMonoid.toZPow` `GroupWithZero.toDivInvMonoid` `instGroupWithZero`	—	—
`zsmul_def` 📖	mathematical	`AddMonoidHomClass` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `SubNegMonoid.toAddMonoid` `AddGroup.toSubNegMonoid`	`setoid` `SubNegMonoid.toZSMul` `instAddGroup`	—	—

DirectLimit.Module

Definitions

Name	Category	Theorems
`of` 📖	CompOp	3 math math: `of_f`, `lift_of`, `hom_ext_iff`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`hom_ext` 📖	—	`LinearMapClass` `LinearMap.comp` `DirectLimit` `DirectLimit.instAddCommMonoidOfAddMonoidHomClass` `DistribMulActionSemiHomClass.toAddMonoidHomClass` `DFunLike.coe` `RingHom` `Semiring.toNonAssocSemiring` `RingHom.instFunLike` `RingHom.id` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `AddCommMonoid.toAddMonoid` `Module.toDistribMulAction` `SemilinearMapClass.distribMulActionSemiHomClass` `DirectLimit.instModule` `RingHomCompTriple.ids` `of`	—	—	`DistribMulActionSemiHomClass.toAddMonoidHomClass` `SemilinearMapClass.distribMulActionSemiHomClass` `RingHomCompTriple.ids` `LinearMap.ext` `DirectLimit.induction`
`hom_ext_iff` 📖	mathematical	`LinearMapClass`	`LinearMap.comp` `DirectLimit` `DirectLimit.instAddCommMonoidOfAddMonoidHomClass` `DistribMulActionSemiHomClass.toAddMonoidHomClass` `DFunLike.coe` `RingHom` `Semiring.toNonAssocSemiring` `RingHom.instFunLike` `RingHom.id` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `AddCommMonoid.toAddMonoid` `Module.toDistribMulAction` `SemilinearMapClass.distribMulActionSemiHomClass` `DirectLimit.instModule` `RingHomCompTriple.ids` `of`	—	`DistribMulActionSemiHomClass.toAddMonoidHomClass` `SemilinearMapClass.distribMulActionSemiHomClass` `RingHomCompTriple.ids` `hom_ext`
`lift_apply` 📖	mathematical	`LinearMapClass` `DFunLike.coe` `LinearMap` `RingHom.id` `Semiring.toNonAssocSemiring` `LinearMap.instFunLike`	`DirectLimit` `DirectLimit.instAddCommMonoidOfAddMonoidHomClass` `DistribMulActionSemiHomClass.toAddMonoidHomClass` `RingHom` `RingHom.instFunLike` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `AddCommMonoid.toAddMonoid` `Module.toDistribMulAction` `SemilinearMapClass.distribMulActionSemiHomClass` `DirectLimit.instModule` `lift` `DirectLimit.lift`	—	`DistribMulActionSemiHomClass.toAddMonoidHomClass` `SemilinearMapClass.distribMulActionSemiHomClass`
`lift_of` 📖	mathematical	`LinearMapClass` `DFunLike.coe` `LinearMap` `RingHom.id` `Semiring.toNonAssocSemiring` `LinearMap.instFunLike`	`DirectLimit` `DirectLimit.instAddCommMonoidOfAddMonoidHomClass` `DistribMulActionSemiHomClass.toAddMonoidHomClass` `RingHom` `RingHom.instFunLike` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `AddCommMonoid.toAddMonoid` `Module.toDistribMulAction` `SemilinearMapClass.distribMulActionSemiHomClass` `DirectLimit.instModule` `lift` `of`	—	`DistribMulActionSemiHomClass.toAddMonoidHomClass` `SemilinearMapClass.distribMulActionSemiHomClass`
`of_f` 📖	mathematical	`LinearMapClass` `Preorder.toLE`	`DFunLike.coe` `LinearMap` `RingHom.id` `Semiring.toNonAssocSemiring` `DirectLimit` `DirectLimit.instAddCommMonoidOfAddMonoidHomClass` `DistribMulActionSemiHomClass.toAddMonoidHomClass` `RingHom` `RingHom.instFunLike` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `AddCommMonoid.toAddMonoid` `Module.toDistribMulAction` `SemilinearMapClass.distribMulActionSemiHomClass` `DirectLimit.instModule` `LinearMap.instFunLike` `of`	—	`DistribMulActionSemiHomClass.toAddMonoidHomClass` `SemilinearMapClass.distribMulActionSemiHomClass` `DirectLimit.eq_of_le`

DirectLimit.Ring

Definitions

Name	Category	Theorems
`of` 📖	CompOp	3 math math: `of_f`, `hom_ext_iff`, `lift_of`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`hom_ext` 📖	—	`RingHomClass` `RingHom.comp` `DirectLimit` `DirectLimit.instNonAssocSemiringOfRingHomClass` `of`	—	—	`RingHom.ext` `DirectLimit.induction`
`hom_ext_iff` 📖	mathematical	`RingHomClass`	`RingHom.comp` `DirectLimit` `DirectLimit.instNonAssocSemiringOfRingHomClass` `of`	—	`hom_ext`
`lift_of` 📖	mathematical	`RingHomClass` `DFunLike.coe` `RingHom` `RingHom.instFunLike`	`DirectLimit` `DirectLimit.instNonAssocSemiringOfRingHomClass` `lift` `of`	—	—
`of_f` 📖	mathematical	`RingHomClass` `Preorder.toLE`	`DFunLike.coe` `RingHom` `DirectLimit` `DirectLimit.instNonAssocSemiringOfRingHomClass` `RingHom.instFunLike` `of`	—	`DirectLimit.eq_of_le`

---

← Back to Index