Documentation Verification Report

Free

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

Statistics

Metric	Count
Definitions `ofShortExact`	1
Theorems `disjoint_span_sum`, `free_shortExact`, `free_shortExact_finrank_add`, `free_shortExact_rank_add`, `linearIndependent_leftExact`, `linearIndependent_shortExact`, `span_exact`, `span_rightExact`	8
Total	9

ModuleCat

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`disjoint_span_sum` 📖	mathematical	`CategoryTheory.ShortComplex.Exact` `ModuleCat` `moduleCategory` `CategoryTheory.Preadditive.preadditiveHasZeroMorphisms` `instPreadditive` `LinearIndependent` `carrier` `CategoryTheory.ShortComplex.X₃` `CategoryTheory.ShortComplex.X₂` `DFunLike.coe` `CategoryTheory.ConcreteCategory.hom` `LinearMap` `Ring.toSemiring` `RingHom.id` `Semiring.toNonAssocSemiring` `AddCommGroup.toAddCommMonoid` `isAddCommGroup` `isModule` `LinearMap.instFunLike` `instConcreteCategoryLinearMapIdCarrier` `CategoryTheory.ShortComplex.g` `CategoryTheory.ShortComplex.X₁` `CategoryTheory.ShortComplex.f`	`Disjoint` `Submodule` `Submodule.instPartialOrder` `Submodule.instOrderBot` `Submodule.span` `Set.range`	—	`disjoint_comm` `Disjoint.mono_right` `Submodule.span_mono` `Set.range_comp_subset_range` `RingHomSurjective.ids` `LinearMap.coe_range` `Submodule.span_eq` `CategoryTheory.ShortComplex.Exact.moduleCat_range_eq_ker` `Submodule.range_ker_disjoint`
`free_shortExact` 📖	mathematical	`CategoryTheory.ShortComplex.ShortExact` `ModuleCat` `moduleCategory` `CategoryTheory.Preadditive.preadditiveHasZeroMorphisms` `instPreadditive`	`Module.Free` `carrier` `CategoryTheory.ShortComplex.X₂` `Ring.toSemiring` `AddCommGroup.toAddCommMonoid` `isAddCommGroup` `isModule`	—	`Module.Free.of_basis`
`free_shortExact_finrank_add` 📖	mathematical	`CategoryTheory.ShortComplex.ShortExact` `ModuleCat` `moduleCategory` `CategoryTheory.Preadditive.preadditiveHasZeroMorphisms` `instPreadditive` `Module.finrank` `carrier` `CategoryTheory.ShortComplex.X₁` `Ring.toSemiring` `AddCommGroup.toAddCommMonoid` `isAddCommGroup` `isModule` `CategoryTheory.ShortComplex.X₃`	`CategoryTheory.ShortComplex.X₂`	—	`Module.finrank_eq_of_rank_eq` `free_shortExact_rank_add` `Nat.cast_add` `Module.finrank_eq_rank`
`free_shortExact_rank_add` 📖	mathematical	`CategoryTheory.ShortComplex.ShortExact` `ModuleCat` `moduleCategory` `CategoryTheory.Preadditive.preadditiveHasZeroMorphisms` `instPreadditive`	`Module.rank` `carrier` `CategoryTheory.ShortComplex.X₂` `Ring.toSemiring` `AddCommGroup.toAddCommMonoid` `isAddCommGroup` `isModule` `Cardinal` `Cardinal.instAdd` `CategoryTheory.ShortComplex.X₁` `CategoryTheory.ShortComplex.X₃`	—	`free_shortExact` `Module.Free.rank_eq_card_chooseBasisIndex` `Cardinal.add_def` `Cardinal.eq` `invariantBasisNumber_of_rankCondition` `rankCondition_of_strongRankCondition`
`linearIndependent_leftExact` 📖	—	`CategoryTheory.ShortComplex.Exact` `ModuleCat` `moduleCategory` `CategoryTheory.Preadditive.preadditiveHasZeroMorphisms` `instPreadditive` `LinearIndependent` `carrier` `CategoryTheory.ShortComplex.X₁` `Ring.toSemiring` `AddCommGroup.toAddCommMonoid` `isAddCommGroup` `isModule` `CategoryTheory.ShortComplex.X₃` `CategoryTheory.ShortComplex.X₂` `DFunLike.coe` `CategoryTheory.ConcreteCategory.hom` `LinearMap` `RingHom.id` `Semiring.toNonAssocSemiring` `LinearMap.instFunLike` `instConcreteCategoryLinearMapIdCarrier` `CategoryTheory.ShortComplex.g` `CategoryTheory.ShortComplex.f`	—	—	`linearIndependent_sum` `LinearMap.linearIndependent_iff` `LinearMap.ker_eq_bot` `mono_iff_injective` `LinearIndependent.of_comp` `disjoint_span_sum`
`linearIndependent_shortExact` 📖	mathematical	`CategoryTheory.ShortComplex.ShortExact` `ModuleCat` `moduleCategory` `CategoryTheory.Preadditive.preadditiveHasZeroMorphisms` `instPreadditive` `LinearIndependent` `carrier` `CategoryTheory.ShortComplex.X₁` `Ring.toSemiring` `AddCommGroup.toAddCommMonoid` `isAddCommGroup` `isModule` `CategoryTheory.ShortComplex.X₃`	`CategoryTheory.ShortComplex.X₂` `DFunLike.coe` `CategoryTheory.ConcreteCategory.hom` `LinearMap` `RingHom.id` `Semiring.toNonAssocSemiring` `LinearMap.instFunLike` `instConcreteCategoryLinearMapIdCarrier` `CategoryTheory.ShortComplex.f` `Function.invFun` `Zero.instNonempty` `NegZeroClass.toZero` `SubNegZeroMonoid.toNegZeroClass` `SubtractionMonoid.toSubNegZeroMonoid` `SubtractionCommMonoid.toSubtractionMonoid` `AddCommGroup.toDivisionAddCommMonoid` `AddHom.toFun` `AddCommMagma.toAdd` `AddCommSemigroup.toAddCommMagma` `AddCommMonoid.toAddCommSemigroup` `LinearMap.toAddHom` `Hom.hom` `CategoryTheory.ShortComplex.g`	—	`linearIndependent_leftExact` `CategoryTheory.ShortComplex.ShortExact.exact` `Zero.instNonempty` `Function.rightInverse_invFun` `epi_iff_surjective` `CategoryTheory.ShortComplex.ShortExact.epi_g` `CategoryTheory.ShortComplex.ShortExact.mono_f`
`span_exact` 📖	—	`CategoryTheory.ShortComplex.Exact` `ModuleCat` `moduleCategory` `CategoryTheory.Preadditive.preadditiveHasZeroMorphisms` `instPreadditive` `carrier` `CategoryTheory.ShortComplex.X₂` `CategoryTheory.ShortComplex.X₁` `DFunLike.coe` `CategoryTheory.ConcreteCategory.hom` `LinearMap` `Ring.toSemiring` `RingHom.id` `Semiring.toNonAssocSemiring` `AddCommGroup.toAddCommMonoid` `isAddCommGroup` `isModule` `LinearMap.instFunLike` `instConcreteCategoryLinearMapIdCarrier` `CategoryTheory.ShortComplex.f` `Submodule` `Preorder.toLE` `PartialOrder.toPreorder` `Submodule.instPartialOrder` `Top.top` `Submodule.instTop` `Submodule.span` `Set.range` `CategoryTheory.ShortComplex.X₃` `CategoryTheory.ShortComplex.g`	—	—	`Submodule.mem_top` `Finsupp.mem_span_range_iff_exists_finsupp` `RingHomSurjective.ids` `CategoryTheory.ShortComplex.Exact.moduleCat_range_eq_ker` `map_sub` `DistribMulActionSemiHomClass.toAddMonoidHomClass` `SemilinearMapClass.distribMulActionSemiHomClass` `LinearMap.semilinearMapClass` `map_finsuppSum` `map_smul` `SemilinearMapClass.toMulActionSemiHomClass` `sub_add_cancel` `AddMemClass.add_mem` `AddSubmonoidClass.toAddMemClass` `Submodule.addSubmonoidClass` `Sum.inl_injective` `Sum.inr_injective`
`span_rightExact` 📖	mathematical	`CategoryTheory.ShortComplex.Exact` `ModuleCat` `moduleCategory` `CategoryTheory.Preadditive.preadditiveHasZeroMorphisms` `instPreadditive` `Submodule` `carrier` `CategoryTheory.ShortComplex.X₁` `Ring.toSemiring` `AddCommGroup.toAddCommMonoid` `isAddCommGroup` `isModule` `Preorder.toLE` `PartialOrder.toPreorder` `Submodule.instPartialOrder` `Top.top` `Submodule.instTop` `Submodule.span` `Set.range` `CategoryTheory.ShortComplex.X₃`	`CategoryTheory.ShortComplex.X₂` `DFunLike.coe` `CategoryTheory.ConcreteCategory.hom` `LinearMap` `RingHom.id` `Semiring.toNonAssocSemiring` `LinearMap.instFunLike` `instConcreteCategoryLinearMapIdCarrier` `CategoryTheory.ShortComplex.f` `Function.invFun` `Zero.instNonempty` `NegZeroClass.toZero` `SubNegZeroMonoid.toNegZeroClass` `SubtractionMonoid.toSubNegZeroMonoid` `SubtractionCommMonoid.toSubtractionMonoid` `AddCommGroup.toDivisionAddCommMonoid` `AddHom.toFun` `AddCommMagma.toAdd` `AddCommSemigroup.toAddCommMagma` `AddCommMonoid.toAddCommSemigroup` `LinearMap.toAddHom` `Hom.hom` `CategoryTheory.ShortComplex.g`	—	`span_exact` `Zero.instNonempty` `Function.comp_assoc` `Function.RightInverse.comp_eq_id` `Function.rightInverse_invFun` `epi_iff_surjective`

ModuleCat.Basis

Definitions

Name	Category	Theorems
`ofShortExact` 📖	CompOp	—

---

← Back to Index