Documentation Verification Report

Exact

📁 Source: Mathlib/LinearAlgebra/Basis/Exact.lean

Statistics

Metric	Count
Definitions `Exact`, `ofSplitExact`	2
Theorems `linearIndependent_of_exact_of_retraction`, `linearProjOfIsCompl_comp_bijective_of_exact`, `ofSplitExact_apply`, `linearProjOfIsCompl_comp_bijective_of_exact`, `linearProjOfIsCompl_comp_surjective_of_exact`, `top_le_span_of_exact_of_retraction`	6
Total	8

Function

Definitions

Name	Category	Theorems
`Exact` 📖	MathDef	82 math math: `Module.Flat.iff_lTensor_exact'`, `AddMonoidHom.exact_of_comp_of_mem_range`, `Module.FaithfullyFlat.iff_exact_iff_lTensor_exact`, `LinearMap.exact_zero_iff_surjective`, `Exact.of_comp_of_mem_range`, `Exact.of_ladder_linearEquiv_of_exact`, `exact_of_isLocalized_maximal`, `Module.Flat.lTensor_exact`, `Module.FaithfullyFlat.lTensor_exact_iff_exact`, `Module.FaithfullyFlat.rTensor_reflects_exact`, `Exact.of_ladder_addEquiv_of_exact`, `Exact.iff_of_ladder_linearEquiv`, `Algebra.Extension.exact_hCotangentι_cotangentComplex`, `LinearMap.exact_subtype_mkQ`, `Exact.rangeFactorization`, `Module.FaithfullyFlat.rTensor_exact_iff_exact`, `Algebra.Generators.H1Cotangent.exact_map_δ`, `CategoryTheory.ShortComplex.ab_exact_iff_function_exact`, `Exact.exact_mapQ_iff`, `LinearEquiv.conj_exact_iff_exact`, `KaehlerDifferential.exact_mapBaseChange_map`, `lTensor_exact`, `Module.Flat.iff_lTensor_exact`, `Surjective.comp_exact_iff_exact`, `Module.Flat.rTensor_exact`, `Module.FaithfullyFlat.iff_exact_iff_rTensor_exact`, `Algebra.Generators.H1Cotangent.exact_δ_map`, `Ideal.exact_mulQuot_quotOfMul`, `SnakeLemma.exact_δ_right`, `LinearMap.exact_smul_id_smul_top_mkQ`, `Exact.inr_fst`, `Module.Flat.iff_rTensor_exact'`, `Exact.of_comp_eq_zero_of_ker_in_range`, `Algebra.Generators.Cotangent.exact`, `QuotSMulTop.map_exact`, `CategoryTheory.ShortComplex.ShortExact.moduleCat_exact_iff_function_exact`, `Module.FaithfullyFlat.lTensor_reflects_exact`, `Exact.linearMap_rangeRestrict`, `KaehlerDifferential.exact_kerCotangentToTensor_mapBaseChange`, `exact_of_localized_span`, `Exact.iff_of_ladder_addEquiv`, `Exact.iff_linearMap_rangeRestrict`, `Module.Flat.iff_rTensor_exact`, `exact_of_isLocalized_span`, `rTensor_exact`, `Algebra.Generators.H1Cotangent.exact_map_δ'`, `LinearMap.exact_of_comp_eq_zero_of_ker_le_range`, `LinearMap.exact_zero_iff_injective`, `LinearMap.exact_map_mkQ_range`, `Algebra.Generators.CotangentSpace.exact`, `LocalizedModule.map_exact`, `AdicCompletion.map_exact`, `LinearMap.exact_subtype_ker_map`, `SnakeLemma.exact_δ_left`, `Exact.addMonoidHom_rangeRestrict`, `QuotSMulTop.map_first_exact_on_four_term_exact_of_isSMulRegular_last`, `exact_of_localized_maximal`, `SnakeLemma.exact_δ'_right`, `Exact.iff_addMonoidHom_rangeRestrict`, `LinearMap.rTensor_exact_iff_lTensor_exact`, `IsLocalizedModule.map_exact`, `Exact.iff_rangeFactorization`, `SnakeLemma.exact_δ'_left`, `Algebra.H1Cotangent.exact_map_δ`, `AddMonoidHom.exact_of_comp_eq_zero_of_ker_le_range`, `LinearMap.exact_of_comp_of_mem_range`, `AddMonoidHom.exact_iff`, `RingTheory.Sequence.map_first_exact_on_four_term_right_exact_of_isSMulRegular_last`, `LinearMap.exact_iff`, `Module.Relations.Solution.IsPresentation.exact`, `LinearMap.exact_lcomp_of_exact_of_surjective`, `Exact.comp_injective`, `Exact.inl_snd`, `Algebra.Extension.exact_cotangentComplex_toKaehler`, `LinearMap.exact_iff_of_surjective_of_bijective_of_injective`, `Injective.comp_exact_iff_exact`, `AddMonoidHom.exact_iff_of_surjective_of_bijective_of_injective`, `LieHom.range_eq_ker_iff`, `Exact.of_ladder_addEquiv_of_exact'`, `Algebra.H1Cotangent.exact_δ_mapBaseChange`, `CategoryTheory.ShortComplex.ShortExact.ab_exact_iff_function_exact`, `TopologicalAddGroup.IsSES.exact`

LinearIndependent

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`linearIndependent_of_exact_of_retraction` 📖	mathematical	`LinearMap.comp` `Ring.toSemiring` `AddCommGroup.toAddCommMonoid` `RingHom.id` `Semiring.toNonAssocSemiring` `RingHomCompTriple.ids` `LinearMap.id` `Function.Exact` `DFunLike.coe` `LinearMap` `LinearMap.instFunLike` `NegZeroClass.toZero` `SubNegZeroMonoid.toNegZeroClass` `SubtractionMonoid.toSubNegZeroMonoid` `SubtractionCommMonoid.toSubtractionMonoid` `AddCommGroup.toDivisionAddCommMonoid` `LinearIndependent`	`LinearIndependent` `DFunLike.coe` `LinearMap` `Ring.toSemiring` `RingHom.id` `Semiring.toNonAssocSemiring` `AddCommGroup.toAddCommMonoid` `LinearMap.instFunLike`	—	`RingHomCompTriple.ids` `map` `comp` `Submodule.disjoint_def` `RingHomSurjective.ids` `Function.Exact.linearMap_ker_eq` `Submodule.span_induction` `map_zero` `AddMonoidHomClass.toZeroHomClass` `DistribMulActionSemiHomClass.toAddMonoidHomClass` `SemilinearMapClass.distribMulActionSemiHomClass` `LinearMap.semilinearMapClass` `map_add` `SemilinearMapClass.toAddHomClass` `add_zero` `map_smul` `SemilinearMapClass.toMulActionSemiHomClass` `smul_zero` `DFunLike.congr_fun`

LinearMap

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`linearProjOfIsCompl_comp_bijective_of_exact` 📖	mathematical	`Function.Exact` `DFunLike.coe` `LinearMap` `Ring.toSemiring` `RingHom.id` `Semiring.toNonAssocSemiring` `AddCommGroup.toAddCommMonoid` `instFunLike` `NegZeroClass.toZero` `SubNegZeroMonoid.toNegZeroClass` `SubtractionMonoid.toSubNegZeroMonoid` `SubtractionCommMonoid.toSubtractionMonoid` `AddCommGroup.toDivisionAddCommMonoid` `IsCompl` `Submodule` `Submodule.instPartialOrder` `CompleteLattice.toBoundedOrder` `Submodule.completeLattice` `range` `RingHomSurjective.ids` `Disjoint` `Submodule.instOrderBot` `ker` `Submodule.map` `Top.top` `Submodule.instTop`	`Function.Bijective` `DFunLike.coe` `LinearMap` `Ring.toSemiring` `RingHom.id` `Semiring.toNonAssocSemiring` `AddCommGroup.toAddCommMonoid` `instFunLike` `comp` `RingHomCompTriple.ids` `linearProjOfIsCompl`	—	`RingHomSurjective.ids` `RingHomCompTriple.ids` `linearProjOfIsCompl.eq_1` `comp_assoc` `coe_comp` `Function.Bijective.of_comp_iff` `Submodule.linearProjOfIsCompl_comp_bijective_of_exact` `LinearEquiv.bijective` `RingHomSurjective.invPair` `RingHomInvPair.ids`

Module.Basis

Definitions

Name	Category	Theorems
`ofSplitExact` 📖	CompOp	1 math math: `ofSplitExact_apply`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`ofSplitExact_apply` 📖	mathematical	`LinearMap.comp` `Ring.toSemiring` `AddCommGroup.toAddCommMonoid` `RingHom.id` `Semiring.toNonAssocSemiring` `RingHomCompTriple.ids` `LinearMap.id` `Function.Exact` `DFunLike.coe` `LinearMap` `LinearMap.instFunLike` `NegZeroClass.toZero` `SubNegZeroMonoid.toNegZeroClass` `SubtractionMonoid.toSubNegZeroMonoid` `SubtractionCommMonoid.toSubtractionMonoid` `AddCommGroup.toDivisionAddCommMonoid` `Module.Basis` `instFunLike` `LinearIndependent` `Codisjoint` `Set` `OmegaCompletePartialOrder.toPartialOrder` `CompleteLattice.instOmegaCompletePartialOrder` `CompleteBooleanAlgebra.toCompleteLattice` `CompleteAtomicBooleanAlgebra.toCompleteBooleanAlgebra` `Set.instCompleteAtomicBooleanAlgebra` `Set.instOrderTop` `Set.range`	`DFunLike.coe` `Module.Basis` `Ring.toSemiring` `AddCommGroup.toAddCommMonoid` `instFunLike` `ofSplitExact` `LinearMap` `RingHom.id` `Semiring.toNonAssocSemiring` `LinearMap.instFunLike`	—	`RingHomCompTriple.ids`

Submodule

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`linearProjOfIsCompl_comp_bijective_of_exact` 📖	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` `IsCompl` `Submodule` `instPartialOrder` `CompleteLattice.toBoundedOrder` `completeLattice` `Disjoint` `instOrderBot` `LinearMap.ker` `map` `RingHomSurjective.ids` `Top.top` `instTop`	`Function.Bijective` `Submodule` `Ring.toSemiring` `AddCommGroup.toAddCommMonoid` `SetLike.instMembership` `setLike` `DFunLike.coe` `LinearMap` `RingHom.id` `Semiring.toNonAssocSemiring` `addCommMonoid` `module` `LinearMap.instFunLike` `LinearMap.comp` `RingHomCompTriple.ids` `linearProjOfIsCompl`	—	`RingHomSurjective.ids` `RingHomCompTriple.ids` `LinearMap.coe_comp` `Set.InjOn.injective_iff` `Function.Exact.linearMap_ker_eq` `linearProjOfIsCompl_ker` `subset_rfl` `Set.instReflSubset` `linearProjOfIsCompl_comp_surjective_of_exact`
`linearProjOfIsCompl_comp_surjective_of_exact` 📖	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` `IsCompl` `Submodule` `instPartialOrder` `CompleteLattice.toBoundedOrder` `completeLattice` `map` `RingHomSurjective.ids` `Top.top` `instTop`	`Submodule` `Ring.toSemiring` `AddCommGroup.toAddCommMonoid` `SetLike.instMembership` `setLike` `DFunLike.coe` `LinearMap` `RingHom.id` `Semiring.toNonAssocSemiring` `addCommMonoid` `module` `LinearMap.instFunLike` `LinearMap.comp` `RingHomCompTriple.ids` `linearProjOfIsCompl`	—	`RingHomSurjective.ids` `RingHomCompTriple.ids` `Set.surjOn_univ` `LinearMap.coe_comp` `Set.surjOn_comp_iff` `Set.image_univ` `LinearMap.coe_range` `top_coe` `surjOn_iff_le_map` `Function.Exact.linearMap_ker_eq` `map_sub` `DistribMulActionSemiHomClass.toAddMonoidHomClass` `SemilinearMapClass.distribMulActionSemiHomClass` `LinearMap.semilinearMapClass` `sub_self` `linearProjOfIsCompl_apply_left`
`top_le_span_of_exact_of_retraction` 📖	mathematical	`LinearMap.comp` `Ring.toSemiring` `AddCommGroup.toAddCommMonoid` `RingHom.id` `Semiring.toNonAssocSemiring` `RingHomCompTriple.ids` `LinearMap.id` `Function.Exact` `DFunLike.coe` `LinearMap` `LinearMap.instFunLike` `NegZeroClass.toZero` `SubNegZeroMonoid.toNegZeroClass` `SubtractionMonoid.toSubNegZeroMonoid` `SubtractionCommMonoid.toSubtractionMonoid` `AddCommGroup.toDivisionAddCommMonoid` `LinearIndependent` `Codisjoint` `Set` `OmegaCompletePartialOrder.toPartialOrder` `CompleteLattice.instOmegaCompletePartialOrder` `CompleteBooleanAlgebra.toCompleteLattice` `CompleteAtomicBooleanAlgebra.toCompleteBooleanAlgebra` `Set.instCompleteAtomicBooleanAlgebra` `Set.instOrderTop` `Set.range` `Submodule` `Preorder.toLE` `PartialOrder.toPreorder` `instPartialOrder` `Top.top` `instTop` `span`	`Submodule` `Ring.toSemiring` `AddCommGroup.toAddCommMonoid` `Preorder.toLE` `PartialOrder.toPreorder` `instPartialOrder` `Top.top` `instTop` `span` `Set.range` `DFunLike.coe` `LinearMap` `RingHom.id` `Semiring.toNonAssocSemiring` `LinearMap.instFunLike`	—	`RingHomCompTriple.ids` `Set.Sum.elim_range` `Set.range_comp` `Set.image_union` `Set.image_univ`

---

← Back to Index