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	51 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, Module.FaithfullyFlat.lTensor_exact_iff_exact, Exact.iff_of_ladder_linearEquiv, LinearMap.exact_subtype_mkQ, Module.FaithfullyFlat.rTensor_exact_iff_exact, Algebra.Generators.H1Cotangent.exact_map_δ, CategoryTheory.ShortComplex.ab_exact_iff_function_exact, LinearEquiv.conj_exact_iff_exact, KaehlerDifferential.exact_mapBaseChange_map, Module.Flat.iff_lTensor_exact, Surjective.comp_exact_iff_exact, Module.FaithfullyFlat.iff_exact_iff_rTensor_exact, Algebra.Generators.H1Cotangent.exact_δ_map, Ideal.exact_mulQuot_quotOfMul, 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, CategoryTheory.ShortComplex.ShortExact.moduleCat_exact_iff_function_exact, KaehlerDifferential.exact_kerCotangentToTensor_mapBaseChange, Exact.iff_of_ladder_addEquiv, Exact.iff_linearMap_rangeRestrict, Module.Flat.iff_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, LinearMap.exact_subtype_ker_map, Exact.iff_addMonoidHom_rangeRestrict, LinearMap.rTensor_exact_iff_lTensor_exact, Exact.iff_rangeFactorization, Algebra.H1Cotangent.exact_map_δ, AddMonoidHom.exact_of_comp_eq_zero_of_ker_le_range, LinearMap.exact_of_comp_of_mem_range, AddMonoidHom.exact_iff, LinearMap.exact_iff, Module.Relations.Solution.IsPresentation.exact, 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, Algebra.H1Cotangent.exact_δ_mapBaseChange, CategoryTheory.ShortComplex.ShortExact.ab_exact_iff_function_exact

LinearIndependent

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
linearIndependent_of_exact_of_retraction 📖	—	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	—	—	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 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	ofSplitExact	—	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 SetLike.instMembership setLike addCommMonoid module 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	SetLike.instMembership setLike addCommMonoid module 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 📖	—	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	—	—	RingHomCompTriple.ids Set.Sum.elim_range Set.range_comp Set.image_union Set.image_univ

---

← Back to Index