Differentials

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

Statistics

Metric	Count
Definitions differentials, hom₁, differentialsRelations, differentialsSolution	4
Theorems comm₁₂, comm₁₂_single, comm₂₃, comm₂₃', hom₁_single, surjective_hom₁, differentialsRelations_G, differentialsRelations_R, differentialsSolution_isPresentation	9
Total	13

Algebra.Presentation

Definitions

Name	Category	Theorems
differentials 📖	CompOp	—
differentialsRelations 📖	CompOp	6 math math: differentials.comm₁₂_single, differentialsSolution_isPresentation, differentials.comm₂₃, differentialsRelations_R, differentials.comm₁₂, differentialsRelations_G
differentialsSolution 📖	CompOp	2 math math: differentialsSolution_isPresentation, differentials.comm₂₃

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
differentialsRelations_G 📖	mathematical	—	Module.Relations.G CommRing.toRing differentialsRelations	—	—
differentialsRelations_R 📖	mathematical	—	Module.Relations.R CommRing.toRing differentialsRelations	—	—
differentialsSolution_isPresentation 📖	mathematical	—	Module.Relations.Solution.IsPresentation CommRing.toRing differentialsRelations KaehlerDifferential instAddCommGroupKaehlerDifferential KaehlerDifferential.module' Algebra.id CommRing.toCommSemiring Algebra.to_smulCommClass CommSemiring.toSemiring differentialsSolution	—	Algebra.to_smulCommClass Module.Relations.Solution.isPresentation_iff Module.Relations.Solution.surjective_π_iff_span_eq_top RingHomCompTriple.ids RingHomInvPair.ids differentials.comm₂₃ Algebra.Extension.toKaehler_surjective LinearEquiv.surjective RingHomSurjective.ids Module.Relations.range_map Function.Exact.linearMap_ker_eq LinearMap.exact_iff_of_surjective_of_bijective_of_injective differentials.comm₁₂ LinearMap.comp.congr_simp Module.Basis.coe_repr_symm differentials.surjective_hom₁ LinearEquiv.bijective Equiv.injective Algebra.Extension.exact_cotangentComplex_toKaehler

Algebra.Presentation.differentials

Definitions

Name	Category	Theorems
hom₁ 📖	CompOp	4 math math: comm₁₂_single, hom₁_single, surjective_hom₁, comm₁₂

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
comm₁₂ 📖	mathematical	—	LinearMap.comp Finsupp MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing Algebra.Extension.Cotangent Algebra.Generators.toExtension Algebra.Presentation.toGenerators Algebra.Extension.CotangentSpace CommSemiring.toSemiring CommRing.toCommSemiring Finsupp.instAddCommMonoid NonUnitalNonAssocSemiring.toAddCommMonoid AddCommGroup.toAddCommMonoid Algebra.Extension.instAddCommGroupCotangent TensorProduct.addCommMonoid Algebra.Extension.Ring Algebra.Extension.commRing KaehlerDifferential Algebra.Extension.instRingOfIsScalarTower Algebra.id instAddCommGroupKaehlerDifferential Algebra.toModule Algebra.Extension.algebra₂ KaehlerDifferential.module' Finsupp.module Semiring.toModule Algebra.Extension.instModuleCotangent TensorProduct.leftModule Algebra.to_smulCommClass RingHom.id Semiring.toNonAssocSemiring RingHomCompTriple.ids Algebra.Extension.cotangentComplex hom₁ Module.Relations.R CommRing.toRing Algebra.Presentation.differentialsRelations NonAssocRing.toNonUnitalNonAssocRing Ring.toNonAssocRing NonAssocSemiring.toNonUnitalNonAssocSemiring Ring.toSemiring LinearEquiv.toLinearMap RingHomInvPair.ids LinearEquiv.symm Module.Basis.repr Algebra.Generators.cotangentSpaceBasis Module.Relations.map	—	Finsupp.lhom_ext' Algebra.to_smulCommClass RingHomCompTriple.ids RingHomInvPair.ids LinearMap.ext_ring Module.Relations.map_single comm₁₂_single
comm₁₂_single 📖	mathematical	—	DFunLike.coe LinearMap CommSemiring.toSemiring CommRing.toCommSemiring RingHom.id Semiring.toNonAssocSemiring Algebra.Extension.Cotangent Algebra.Generators.toExtension Algebra.Presentation.toGenerators Algebra.Extension.CotangentSpace AddCommGroup.toAddCommMonoid Algebra.Extension.instAddCommGroupCotangent TensorProduct.addCommMonoid Algebra.Extension.Ring Algebra.Extension.commRing KaehlerDifferential Algebra.Extension.instRingOfIsScalarTower Algebra.id NonUnitalNonAssocSemiring.toAddCommMonoid NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing instAddCommGroupKaehlerDifferential Algebra.toModule Algebra.Extension.algebra₂ KaehlerDifferential.module' Algebra.Extension.instModuleCotangent TensorProduct.leftModule Semiring.toModule Algebra.to_smulCommClass LinearMap.instFunLike Algebra.Extension.cotangentComplex Finsupp MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass Finsupp.instAddCommMonoid Finsupp.module hom₁ Finsupp.single AddMonoidWithOne.toOne AddGroupWithOne.toAddMonoidWithOne Ring.toAddGroupWithOne CommRing.toRing LinearEquiv RingHomInvPair.ids NonAssocSemiring.toNonUnitalNonAssocSemiring EquivLike.toFunLike DFinsupp.instEquivLikeLinearEquiv LinearEquiv.symm Module.Basis.repr Algebra.Generators.cotangentSpaceBasis Module.Relations.relation Algebra.Presentation.differentialsRelations	—	Algebra.to_smulCommClass RingHomInvPair.ids smulCommClass_self Finsupp.linearCombination_single one_smul Module.Basis.repr_symm_apply LinearEquiv.injective Finsupp.ext Algebra.Generators.cotangentSpaceBasis_repr_tmul one_mul Module.Basis.repr_linearCombination KaehlerDifferential.mvPolynomialBasis_repr_apply Algebra.Generators.algebraMap_apply
comm₂₃ 📖	mathematical	—	LinearMap.comp Finsupp MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring CommSemiring.toSemiring CommRing.toCommSemiring Algebra.Extension.CotangentSpace Algebra.Generators.toExtension Algebra.Presentation.toGenerators KaehlerDifferential Finsupp.instAddCommMonoid NonUnitalNonAssocSemiring.toAddCommMonoid TensorProduct.addCommMonoid Algebra.Extension.Ring Algebra.Extension.commRing Algebra.Extension.instRingOfIsScalarTower Algebra.id NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing AddCommGroup.toAddCommMonoid instAddCommGroupKaehlerDifferential Algebra.toModule Algebra.Extension.algebra₂ KaehlerDifferential.module' Finsupp.module Semiring.toModule TensorProduct.leftModule Algebra.to_smulCommClass RingHom.id RingHomCompTriple.ids Algebra.Extension.toKaehler LinearEquiv.toLinearMap RingHomInvPair.ids LinearEquiv.symm Module.Basis.repr Algebra.Generators.cotangentSpaceBasis Module.Relations.Solution.π CommRing.toRing Algebra.Presentation.differentialsRelations Algebra.Presentation.differentialsSolution	—	comm₂₃'
comm₂₃' 📖	mathematical	—	LinearMap.comp Finsupp MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring CommSemiring.toSemiring CommRing.toCommSemiring Algebra.Extension.CotangentSpace Algebra.Generators.toExtension Algebra.Presentation.toGenerators KaehlerDifferential Finsupp.instAddCommMonoid NonUnitalNonAssocSemiring.toAddCommMonoid TensorProduct.addCommMonoid Algebra.Extension.Ring Algebra.Extension.commRing Algebra.Extension.instRingOfIsScalarTower Algebra.id NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing AddCommGroup.toAddCommMonoid instAddCommGroupKaehlerDifferential Algebra.toModule Algebra.Extension.algebra₂ KaehlerDifferential.module' Finsupp.module Semiring.toModule TensorProduct.leftModule Algebra.to_smulCommClass RingHom.id RingHomCompTriple.ids Algebra.Extension.toKaehler LinearEquiv.toLinearMap RingHomInvPair.ids LinearEquiv.symm Module.Basis.repr Algebra.Generators.cotangentSpaceBasis Finsupp.linearCombination DFunLike.coe Derivation smulCommClass_self CommRing.toCommMonoid DistribMulAction.toMulAction CommMonoid.toMonoid AddCommMonoid.toAddMonoid Module.toDistribMulAction Ring.toSemiring CommRing.toRing Derivation.instFunLike KaehlerDifferential.D Algebra.Generators.val	—	Finsupp.lhom_ext' Algebra.to_smulCommClass RingHomCompTriple.ids RingHomInvPair.ids smulCommClass_self LinearMap.ext_ring LinearMap.comp.congr_simp Module.Basis.coe_repr_symm Finsupp.linearCombination_single one_smul Algebra.Generators.toKaehler_cotangentSpaceBasis
hom₁_single 📖	mathematical	—	DFunLike.coe LinearMap CommSemiring.toSemiring CommRing.toCommSemiring RingHom.id Semiring.toNonAssocSemiring Finsupp MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing Algebra.Extension.Cotangent Algebra.Generators.toExtension Algebra.Presentation.toGenerators Finsupp.instAddCommMonoid NonUnitalNonAssocSemiring.toAddCommMonoid AddCommGroup.toAddCommMonoid Algebra.Extension.instAddCommGroupCotangent Finsupp.module Semiring.toModule Algebra.Extension.instModuleCotangent Algebra.id LinearMap.instFunLike hom₁ Finsupp.single AddMonoidWithOne.toOne AddGroupWithOne.toAddMonoidWithOne Ring.toAddGroupWithOne CommRing.toRing Algebra.Extension.Ring Algebra.Extension.commRing Ideal SetLike.instMembership Submodule.setLike NonAssocSemiring.toNonUnitalNonAssocSemiring Algebra.Extension.ker Submodule.addCommMonoid Submodule.module Algebra.Extension.algebra₂ Algebra.Presentation.relation	—	Finsupp.linearCombination_single one_smul
surjective_hom₁ 📖	mathematical	—	Finsupp MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing Algebra.Extension.Cotangent Algebra.Generators.toExtension Algebra.Presentation.toGenerators DFunLike.coe LinearMap CommSemiring.toSemiring CommRing.toCommSemiring RingHom.id Semiring.toNonAssocSemiring Finsupp.instAddCommMonoid NonUnitalNonAssocSemiring.toAddCommMonoid AddCommGroup.toAddCommMonoid Algebra.Extension.instAddCommGroupCotangent Finsupp.module Semiring.toModule Algebra.Extension.instModuleCotangent Algebra.id LinearMap.instFunLike hom₁	—	map_add SemilinearMapClass.toAddHomClass LinearMap.semilinearMapClass LinearMap.map_smul_of_tower LinearMap.CompatibleSMul.finsupp_dom LinearMap.IsScalarTower.compatibleSMul' Algebra.Extension.instIsScalarTowerCotangent IsScalarTower.right Algebra.Extension.Cotangent.mk_surjective Algebra.Generators.algebraMap_apply Algebra.Presentation.aeval_val_relation Submodule.map_injective_of_injective RingHomSurjective.ids Subtype.coe_injective Submodule.map_top Submodule.range_subtype Submodule.map_span Submodule.coe_subtype Ideal.submodule_span_eq Algebra.Presentation.span_range_relation_eq_ker Set.ext LinearMap.range_eq_top top_le_iff LinearMap.range_eq_map Submodule.map_span_le hom₁_single

---

← Back to Index