Documentation Verification Report

Cokernel

📁 Source: Mathlib/Algebra/Module/Presentation/Cokernel.lean

Statistics

Metric	Count
Definitions `CokernelData`, `ofSection`, `cokernel`, `cokernelRelations`, `cokernelSolution`, `isPresentationCore`, `ofExact`	7
Theorems `ofSection_lift`, `π_lift`, `cokernelRelations_G`, `cokernelRelations_R`, `cokernelRelations_relation`, `isPresentation`, `cokernelSolution_var`, `cokernel_G`, `cokernel_R`, `cokernel_relation`, `cokernel_var`, `nonempty_cokernelData`, `ofExact_G`, `ofExact_R`, `ofExact_relation`, `ofExact_var`	16
Total	23

Module.Presentation

Definitions

Name	Category	Theorems
`CokernelData` 📖	CompData	1 math math: `nonempty_cokernelData`
`cokernel` 📖	CompOp	4 math math: `cokernel_relation`, `cokernel_R`, `cokernel_var`, `cokernel_G`
`cokernelRelations` 📖	CompOp	5 math math: `cokernelRelations_relation`, `cokernelSolution_var`, `cokernelSolution.isPresentation`, `cokernelRelations_R`, `cokernelRelations_G`
`cokernelSolution` 📖	CompOp	2 math math: `cokernelSolution_var`, `cokernelSolution.isPresentation`
`ofExact` 📖	CompOp	4 math math: `ofExact_G`, `ofExact_R`, `ofExact_relation`, `ofExact_var`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`cokernelRelations_G` 📖	mathematical	—	`Module.Relations.G` `cokernelRelations` `toRelations`	—	—
`cokernelRelations_R` 📖	mathematical	—	`Module.Relations.R` `cokernelRelations` `toRelations`	—	—
`cokernelRelations_relation` 📖	mathematical	—	`Module.Relations.relation` `cokernelRelations` `Finsupp` `Module.Relations.G` `toRelations` `MulZeroClass.toZero` `NonUnitalNonAssocSemiring.toMulZeroClass` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonAssocRing.toNonUnitalNonAssocRing` `Ring.toNonAssocRing` `CokernelData.lift`	—	—
`cokernelSolution_var` 📖	mathematical	—	`Module.Relations.Solution.var` `cokernelRelations` `HasQuotient.Quotient` `Submodule` `Ring.toSemiring` `AddCommGroup.toAddCommMonoid` `Submodule.hasQuotient` `LinearMap.range` `RingHom.id` `Semiring.toNonAssocSemiring` `RingHomSurjective.ids` `Submodule.Quotient.addCommGroup` `Submodule.Quotient.module` `cokernelSolution` `DFunLike.coe` `LinearMap` `LinearMap.instFunLike` `Submodule.mkQ` `toRelations` `toSolution`	—	`RingHomSurjective.ids`
`cokernel_G` 📖	mathematical	`Submodule.span` `Ring.toSemiring` `AddCommGroup.toAddCommMonoid` `Set.range` `Top.top` `Submodule` `Submodule.instTop`	`Module.Relations.G` `toRelations` `HasQuotient.Quotient` `Submodule` `Ring.toSemiring` `AddCommGroup.toAddCommMonoid` `Submodule.hasQuotient` `LinearMap.range` `RingHom.id` `Semiring.toNonAssocSemiring` `RingHomSurjective.ids` `Submodule.Quotient.addCommGroup` `Submodule.Quotient.module` `cokernel`	—	`RingHomSurjective.ids`
`cokernel_R` 📖	mathematical	`Submodule.span` `Ring.toSemiring` `AddCommGroup.toAddCommMonoid` `Set.range` `Top.top` `Submodule` `Submodule.instTop`	`Module.Relations.R` `toRelations` `HasQuotient.Quotient` `Submodule` `Ring.toSemiring` `AddCommGroup.toAddCommMonoid` `Submodule.hasQuotient` `LinearMap.range` `RingHom.id` `Semiring.toNonAssocSemiring` `RingHomSurjective.ids` `Submodule.Quotient.addCommGroup` `Submodule.Quotient.module` `cokernel`	—	`RingHomSurjective.ids`
`cokernel_relation` 📖	mathematical	`Submodule.span` `Ring.toSemiring` `AddCommGroup.toAddCommMonoid` `Set.range` `Top.top` `Submodule` `Submodule.instTop`	`Module.Relations.relation` `toRelations` `HasQuotient.Quotient` `Submodule` `Ring.toSemiring` `AddCommGroup.toAddCommMonoid` `Submodule.hasQuotient` `LinearMap.range` `RingHom.id` `Semiring.toNonAssocSemiring` `RingHomSurjective.ids` `Submodule.Quotient.addCommGroup` `Submodule.Quotient.module` `cokernel` `Finsupp` `Module.Relations.G` `MulZeroClass.toZero` `NonUnitalNonAssocSemiring.toMulZeroClass` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonAssocRing.toNonUnitalNonAssocRing` `Ring.toNonAssocRing` `CokernelData.lift`	—	`RingHomSurjective.ids`
`cokernel_var` 📖	mathematical	`Submodule.span` `Ring.toSemiring` `AddCommGroup.toAddCommMonoid` `Set.range` `Top.top` `Submodule` `Submodule.instTop`	`Module.Relations.Solution.var` `toRelations` `HasQuotient.Quotient` `Submodule` `Ring.toSemiring` `AddCommGroup.toAddCommMonoid` `Submodule.hasQuotient` `LinearMap.range` `RingHom.id` `Semiring.toNonAssocSemiring` `RingHomSurjective.ids` `Submodule.Quotient.addCommGroup` `Submodule.Quotient.module` `cokernel` `toSolution`	—	`RingHomSurjective.ids`
`nonempty_cokernelData` 📖	mathematical	—	`CokernelData`	—	`Function.Surjective.hasRightInverse` `Module.Relations.Solution.IsPresentation.surjective_π` `toIsPresentation`
`ofExact_G` 📖	mathematical	`Function.Exact` `DFunLike.coe` `LinearMap` `Ring.toSemiring` `RingHom.id` `Semiring.toNonAssocSemiring` `AddCommGroup.toAddCommMonoid` `LinearMap.instFunLike` `NegZeroClass.toZero` `SubNegZeroMonoid.toNegZeroClass` `SubtractionMonoid.toSubNegZeroMonoid` `SubtractionCommMonoid.toSubtractionMonoid` `AddCommGroup.toDivisionAddCommMonoid` `Submodule.span` `Set.range` `Top.top` `Submodule` `Submodule.instTop`	`Module.Relations.G` `toRelations` `ofExact`	—	—
`ofExact_R` 📖	mathematical	`Function.Exact` `DFunLike.coe` `LinearMap` `Ring.toSemiring` `RingHom.id` `Semiring.toNonAssocSemiring` `AddCommGroup.toAddCommMonoid` `LinearMap.instFunLike` `NegZeroClass.toZero` `SubNegZeroMonoid.toNegZeroClass` `SubtractionMonoid.toSubNegZeroMonoid` `SubtractionCommMonoid.toSubtractionMonoid` `AddCommGroup.toDivisionAddCommMonoid` `Submodule.span` `Set.range` `Top.top` `Submodule` `Submodule.instTop`	`Module.Relations.R` `toRelations` `ofExact`	—	—
`ofExact_relation` 📖	mathematical	`Function.Exact` `DFunLike.coe` `LinearMap` `Ring.toSemiring` `RingHom.id` `Semiring.toNonAssocSemiring` `AddCommGroup.toAddCommMonoid` `LinearMap.instFunLike` `NegZeroClass.toZero` `SubNegZeroMonoid.toNegZeroClass` `SubtractionMonoid.toSubNegZeroMonoid` `SubtractionCommMonoid.toSubtractionMonoid` `AddCommGroup.toDivisionAddCommMonoid` `Submodule.span` `Set.range` `Top.top` `Submodule` `Submodule.instTop`	`Module.Relations.relation` `toRelations` `ofExact` `Finsupp` `Module.Relations.G` `MulZeroClass.toZero` `NonUnitalNonAssocSemiring.toMulZeroClass` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonAssocRing.toNonUnitalNonAssocRing` `Ring.toNonAssocRing` `CokernelData.lift`	—	—
`ofExact_var` 📖	mathematical	`Function.Exact` `DFunLike.coe` `LinearMap` `Ring.toSemiring` `RingHom.id` `Semiring.toNonAssocSemiring` `AddCommGroup.toAddCommMonoid` `LinearMap.instFunLike` `NegZeroClass.toZero` `SubNegZeroMonoid.toNegZeroClass` `SubtractionMonoid.toSubNegZeroMonoid` `SubtractionCommMonoid.toSubtractionMonoid` `AddCommGroup.toDivisionAddCommMonoid` `Submodule.span` `Set.range` `Top.top` `Submodule` `Submodule.instTop`	`Module.Relations.Solution.var` `toRelations` `ofExact` `toSolution` `DFunLike.coe` `LinearMap` `Ring.toSemiring` `RingHom.id` `Semiring.toNonAssocSemiring` `AddCommGroup.toAddCommMonoid` `LinearMap.instFunLike`	—	—

Module.Presentation.CokernelData

Definitions

Name	Category	Theorems
`ofSection` 📖	CompOp	1 math math: `ofSection_lift`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`ofSection_lift` 📖	mathematical	`DFunLike.coe` `LinearMap` `Ring.toSemiring` `RingHom.id` `Semiring.toNonAssocSemiring` `Finsupp` `Module.Relations.G` `Module.Presentation.toRelations` `MulZeroClass.toZero` `NonUnitalNonAssocSemiring.toMulZeroClass` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonAssocRing.toNonUnitalNonAssocRing` `Ring.toNonAssocRing` `Finsupp.instAddCommMonoid` `NonUnitalNonAssocSemiring.toAddCommMonoid` `AddCommGroup.toAddCommMonoid` `Finsupp.module` `Semiring.toModule` `LinearMap.instFunLike` `Module.Relations.Solution.π` `Module.Presentation.toSolution`	`lift` `ofSection` `DFunLike.coe` `LinearMap` `Ring.toSemiring` `RingHom.id` `Semiring.toNonAssocSemiring` `AddCommGroup.toAddCommMonoid` `LinearMap.instFunLike`	—	—
`π_lift` 📖	mathematical	—	`DFunLike.coe` `LinearMap` `Ring.toSemiring` `RingHom.id` `Semiring.toNonAssocSemiring` `Finsupp` `Module.Relations.G` `Module.Presentation.toRelations` `MulZeroClass.toZero` `NonUnitalNonAssocSemiring.toMulZeroClass` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonAssocRing.toNonUnitalNonAssocRing` `Ring.toNonAssocRing` `Finsupp.instAddCommMonoid` `NonUnitalNonAssocSemiring.toAddCommMonoid` `AddCommGroup.toAddCommMonoid` `Finsupp.module` `Semiring.toModule` `LinearMap.instFunLike` `Module.Relations.Solution.π` `Module.Presentation.toSolution` `lift`	—	—

Module.Presentation.cokernelSolution

Definitions

Name	Category	Theorems
`isPresentationCore` 📖	CompOp	—

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`isPresentation` 📖	mathematical	`Submodule.span` `Ring.toSemiring` `AddCommGroup.toAddCommMonoid` `Set.range` `Top.top` `Submodule` `Submodule.instTop`	`Module.Relations.Solution.IsPresentation` `Module.Presentation.cokernelRelations` `HasQuotient.Quotient` `Submodule` `Ring.toSemiring` `AddCommGroup.toAddCommMonoid` `Submodule.hasQuotient` `LinearMap.range` `RingHom.id` `Semiring.toNonAssocSemiring` `RingHomSurjective.ids` `Submodule.Quotient.addCommGroup` `Submodule.Quotient.module` `Module.Presentation.cokernelSolution`	—	`Module.Relations.Solution.IsPresentationCore.isPresentation` `RingHomSurjective.ids`

---

← Back to Index