Documentation Verification Report

EpiMono

📁 Source: Mathlib/Algebra/Category/ModuleCat/EpiMono.lean

Statistics

Metric	Count
Definitions `uniqueOfEpiZero`	1
Theorems `epi_as_hom''_mkQ`, `epi_iff_range_eq_top`, `epi_iff_surjective`, `forget_preservesEpimorphisms`, `forget_preservesMonomorphisms`, `ker_eq_bot_of_mono`, `mono_as_hom'_subtype`, `mono_iff_injective`, `mono_iff_ker_eq_bot`, `range_eq_top_of_epi`	10
Total	11

ModuleCat

Definitions

Name	Category	Theorems
`uniqueOfEpiZero` 📖	CompOp	—

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`epi_as_hom''_mkQ` 📖	mathematical	—	`CategoryTheory.Epi` `ModuleCat` `moduleCategory` `of` `carrier` `isAddCommGroup` `isModule` `HasQuotient.Quotient` `Submodule` `Ring.toSemiring` `AddCommGroup.toAddCommMonoid` `Submodule.hasQuotient` `Submodule.Quotient.addCommGroup` `Submodule.Quotient.module` `ofHom` `Submodule.mkQ`	—	`RingHomSurjective.ids` `epi_iff_range_eq_top` `Submodule.range_mkQ`
`epi_iff_range_eq_top` 📖	mathematical	—	`CategoryTheory.Epi` `ModuleCat` `moduleCategory` `LinearMap.range` `carrier` `Ring.toSemiring` `AddCommGroup.toAddCommMonoid` `isAddCommGroup` `isModule` `RingHom.id` `Semiring.toNonAssocSemiring` `RingHomSurjective.ids` `Hom.hom` `Top.top` `Submodule` `Submodule.instTop`	—	`RingHomSurjective.ids` `range_eq_top_of_epi` `CategoryTheory.ConcreteCategory.epi_of_surjective` `LinearMap.range_eq_top`
`epi_iff_surjective` 📖	mathematical	—	`CategoryTheory.Epi` `ModuleCat` `moduleCategory` `carrier` `DFunLike.coe` `CategoryTheory.ConcreteCategory.hom` `LinearMap` `Ring.toSemiring` `RingHom.id` `Semiring.toNonAssocSemiring` `AddCommGroup.toAddCommMonoid` `isAddCommGroup` `isModule` `LinearMap.instFunLike` `instConcreteCategoryLinearMapIdCarrier`	—	`RingHomSurjective.ids` `epi_iff_range_eq_top` `LinearMap.range_eq_top`
`forget_preservesEpimorphisms` 📖	mathematical	—	`CategoryTheory.Functor.PreservesEpimorphisms` `ModuleCat` `moduleCategory` `CategoryTheory.types` `CategoryTheory.forget` `LinearMap` `Ring.toSemiring` `RingHom.id` `Semiring.toNonAssocSemiring` `carrier` `AddCommGroup.toAddCommMonoid` `isAddCommGroup` `isModule` `LinearMap.instFunLike` `instConcreteCategoryLinearMapIdCarrier`	—	`CategoryTheory.epi_iff_surjective` `CategoryTheory.ConcreteCategory.forget_map_eq_coe` `epi_iff_surjective`
`forget_preservesMonomorphisms` 📖	mathematical	—	`CategoryTheory.Functor.PreservesMonomorphisms` `ModuleCat` `moduleCategory` `CategoryTheory.types` `CategoryTheory.forget` `LinearMap` `Ring.toSemiring` `RingHom.id` `Semiring.toNonAssocSemiring` `carrier` `AddCommGroup.toAddCommMonoid` `isAddCommGroup` `isModule` `LinearMap.instFunLike` `instConcreteCategoryLinearMapIdCarrier`	—	`CategoryTheory.mono_iff_injective` `CategoryTheory.ConcreteCategory.forget_map_eq_coe` `mono_iff_injective`
`ker_eq_bot_of_mono` 📖	mathematical	—	`LinearMap.ker` `carrier` `Ring.toSemiring` `AddCommGroup.toAddCommMonoid` `isAddCommGroup` `isModule` `RingHom.id` `Semiring.toNonAssocSemiring` `Hom.hom` `Bot.bot` `Submodule` `Submodule.instBot`	—	`LinearMap.ker_eq_bot_of_cancel` `RingHomCompTriple.ids` `hom_ext_iff` `CategoryTheory.cancel_mono`
`mono_as_hom'_subtype` 📖	mathematical	—	`CategoryTheory.Mono` `ModuleCat` `moduleCategory` `of` `carrier` `Submodule` `Ring.toSemiring` `AddCommGroup.toAddCommMonoid` `isAddCommGroup` `isModule` `SetLike.instMembership` `Submodule.setLike` `Submodule.addCommGroup` `Submodule.module` `ofHom` `Submodule.subtype`	—	`mono_iff_ker_eq_bot` `Submodule.ker_subtype`
`mono_iff_injective` 📖	mathematical	—	`CategoryTheory.Mono` `ModuleCat` `moduleCategory` `carrier` `DFunLike.coe` `CategoryTheory.ConcreteCategory.hom` `LinearMap` `Ring.toSemiring` `RingHom.id` `Semiring.toNonAssocSemiring` `AddCommGroup.toAddCommMonoid` `isAddCommGroup` `isModule` `LinearMap.instFunLike` `instConcreteCategoryLinearMapIdCarrier`	—	`mono_iff_ker_eq_bot` `LinearMap.ker_eq_bot`
`mono_iff_ker_eq_bot` 📖	mathematical	—	`CategoryTheory.Mono` `ModuleCat` `moduleCategory` `LinearMap.ker` `carrier` `Ring.toSemiring` `AddCommGroup.toAddCommMonoid` `isAddCommGroup` `isModule` `RingHom.id` `Semiring.toNonAssocSemiring` `Hom.hom` `Bot.bot` `Submodule` `Submodule.instBot`	—	`ker_eq_bot_of_mono` `CategoryTheory.ConcreteCategory.mono_of_injective` `LinearMap.ker_eq_bot`
`range_eq_top_of_epi` 📖	mathematical	—	`LinearMap.range` `carrier` `Ring.toSemiring` `AddCommGroup.toAddCommMonoid` `isAddCommGroup` `isModule` `RingHom.id` `Semiring.toNonAssocSemiring` `RingHomSurjective.ids` `Hom.hom` `Top.top` `Submodule` `Submodule.instTop`	—	`LinearMap.range_eq_top_of_cancel` `RingHomSurjective.ids` `RingHomCompTriple.right_ids` `hom_ext_iff` `CategoryTheory.cancel_epi`

---

← Back to Index