Documentation Verification Report

JacobiZariski

📁 Source: Mathlib/RingTheory/Kaehler/JacobiZariski.lean

Statistics

Metric	Count
Definitions `compEquiv`, `δ`, `δAux`, `δ`	4
Theorems `exact`, `surjective_map_ofComp`, `compEquiv_symm_inr`, `compEquiv_symm_zero`, `exact`, `fst_compEquiv`, `fst_compEquiv_apply`, `map_ofComp_surjective`, `map_toComp_injective`, `exact_map_δ`, `exact_map_δ'`, `exact_δ_map`, `map_comp_cotangentComplex_baseChange`, `δAux_C`, `δAux_X`, `δAux_monomial`, `δAux_mul`, `δAux_ofComp`, `δAux_toAlgHom`, `δ_comp_equiv`, `δ_eq`, `δ_eq_δ`, `δ_eq_δAux`, `δ_map`, `exact_map_δ`, `exact_δ_mapBaseChange`	26
Total	30

Algebra.Generators.Cotangent

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`exact` 📖	mathematical	—	`Function.Exact` `TensorProduct` `CommRing.toCommSemiring` `Algebra.Extension.Cotangent` `Algebra.Generators.toExtension` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `CommSemiring.toSemiring` `AddCommGroup.toAddCommMonoid` `Algebra.Extension.instAddCommGroupCotangent` `Algebra.toModule` `Algebra.Extension.instModuleCotangent` `Algebra.id` `Algebra.Generators.comp` `DFunLike.coe` `LinearMap` `RingHom.id` `TensorProduct.addCommMonoid` `TensorProduct.leftModule` `Semiring.toModule` `Algebra.to_smulCommClass` `LinearMap.instFunLike` `LinearMap.liftBaseChange` `Algebra.Extension.instIsScalarTowerCotangent` `IsScalarTower.right` `Algebra.Extension.Cotangent.map` `IsScalarTower.left` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `DistribMulAction.toMulAction` `AddCommMonoid.toAddMonoid` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing` `NonUnitalCommRing.toNonUnitalNonAssocCommRing` `CommRing.toNonUnitalCommRing` `Module.toDistribMulAction` `Algebra.Generators.Hom.toExtensionHom` `Algebra.Generators.toComp` `Algebra.Generators.ofComp` `NegZeroClass.toZero` `SubNegZeroMonoid.toNegZeroClass` `SubtractionMonoid.toSubNegZeroMonoid` `SubtractionCommMonoid.toSubtractionMonoid` `AddCommGroup.toDivisionAddCommMonoid`	—	`LinearMap.exact_of_comp_of_mem_range` `Algebra.to_smulCommClass` `Algebra.Extension.instIsScalarTowerCotangent` `IsScalarTower.right` `IsScalarTower.left` `RingHomCompTriple.ids` `LinearMap.IsScalarTower.compatibleSMul` `LinearMap.liftBaseChange_comp` `Algebra.Extension.Cotangent.map_comp` `EmbeddingLike.map_eq_zero_iff` `EquivLike.toEmbeddingLike` `AddMonoidHomClass.toZeroHomClass` `DistribMulActionSemiHomClass.toAddMonoidHomClass` `SemilinearMapClass.distribMulActionSemiHomClass` `SemilinearEquivClass.instSemilinearMapClass` `LinearEquiv.instSemilinearEquivClass` `LinearMap.ext` `Algebra.Extension.Cotangent.ext` `Algebra.Extension.Cotangent.mk_surjective` `Algebra.Extension.instIsScalarTowerRing_1` `Algebra.Generators.instIsScalarTowerRing` `MvPolynomial.algHom_ext` `Algebra.Generators.Hom.toAlgHom_X` `Algebra.Generators.algebraMap_apply` `MvPolynomial.aeval_X` `Algebra.Generators.aeval_val_eq_zero` `MvPolynomial.C_0` `LinearMap.map_zero` `RingHomSurjective.ids` `Ideal.mem_map_iff_of_surjective` `AlgHomClass.toRingHomClass` `AlgHom.algHomClass` `Algebra.Generators.toAlgHom_ofComp_surjective` `Ideal.map_mul` `Algebra.Generators.map_ofComp_ker` `pow_two` `LinearMap.range_liftBaseChange` `Ideal.sub_mem` `Ideal.mul_le_left` `Algebra.Generators.map_toComp_ker` `RingHom.mem_ker` `map_sub` `NonUnitalAlgSemiHomClass.toDistribMulActionSemiHomClass` `AlgHom.instNonUnitalAlgHomClassOfAlgHomClass` `sub_eq_zero` `sub_sub_cancel` `Submodule.restrictScalars_mem` `Submodule.mem_comap` `Submodule.span_singleton_le_iff_mem` `Submodule.map_le_map_iff_of_injective` `Subtype.val_injective` `Submodule.map_subtype_span_singleton` `RingHom.instRingHomClass` `Ideal.map_le_iff_le_comap` `Algebra.Generators.ker_eq_ker_aeval_val` `Algebra.Generators.Hom.algebraMap_toAlgHom` `map_zero` `MonoidWithZeroHomClass.toZeroHomClass` `RingHomClass.toMonoidWithZeroHomClass` `Submodule.subset_span`
`surjective_map_ofComp` 📖	mathematical	—	`Algebra.Extension.Cotangent` `Algebra.Generators.toExtension` `Algebra.Generators.comp` `DFunLike.coe` `LinearMap` `CommSemiring.toSemiring` `CommRing.toCommSemiring` `RingHom.id` `Semiring.toNonAssocSemiring` `AddCommGroup.toAddCommMonoid` `Algebra.Extension.instAddCommGroupCotangent` `Algebra.Extension.instModuleCotangent` `Algebra.id` `LinearMap.instFunLike` `Algebra.Extension.Cotangent.map` `Algebra.Generators.Hom.toExtensionHom` `IsScalarTower.right` `Algebra.Generators.ofComp`	—	`IsScalarTower.right` `Algebra.Extension.Cotangent.mk_surjective` `Ideal.mem_map_iff_of_surjective` `AlgHomClass.toRingHomClass` `AlgHom.algHomClass` `Algebra.Generators.toAlgHom_ofComp_surjective` `Algebra.Generators.map_ofComp_ker`

Algebra.Generators.CotangentSpace

Definitions

Name	Category	Theorems
`compEquiv` 📖	CompOp	5 math math: `compEquiv_symm_zero`, `Algebra.Generators.H1Cotangent.δAux_ofComp`, `compEquiv_symm_inr`, `fst_compEquiv_apply`, `fst_compEquiv`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`compEquiv_symm_inr` 📖	mathematical	—	`LinearMap.comp` `TensorProduct` `CommRing.toCommSemiring` `Algebra.Extension.CotangentSpace` `Algebra.Generators.toExtension` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing` `NonUnitalCommRing.toNonUnitalNonAssocCommRing` `CommRing.toNonUnitalCommRing` `TensorProduct.addCommMonoid` `Algebra.Extension.Ring` `Algebra.Extension.commRing` `KaehlerDifferential` `Algebra.Extension.instRingOfIsScalarTower` `Algebra.id` `AddCommGroup.toAddCommMonoid` `instAddCommGroupKaehlerDifferential` `Algebra.toModule` `CommSemiring.toSemiring` `Algebra.Extension.algebra₂` `KaehlerDifferential.module'` `TensorProduct.leftModule` `Semiring.toModule` `Algebra.to_smulCommClass` `Algebra.Generators.comp` `Prod.instAddCommMonoid` `Prod.instModule` `RingHom.id` `Semiring.toNonAssocSemiring` `RingHomCompTriple.ids` `LinearEquiv.toLinearMap` `RingHomInvPair.ids` `LinearEquiv.symm` `compEquiv` `LinearMap.inr` `LinearMap.liftBaseChange` `SMulCommClass.of_commMonoid` `CommRing.toCommMonoid` `SMulZeroClass.toSMul` `AddZero.toZero` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `AddCommMonoid.toAddMonoid` `DistribSMul.toSMulZeroClass` `DistribMulAction.toDistribSMul` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `Module.toDistribMulAction` `IsScalarTower.right` `TensorProduct.isScalarTower_left` `Algebra.toSMul` `Algebra.Extension.CotangentSpace.map` `IsScalarTower.left` `DistribMulAction.toMulAction` `Algebra.Generators.Hom.toExtensionHom` `Algebra.Generators.toComp`	—	`Module.Basis.ext` `Algebra.to_smulCommClass` `RingHomCompTriple.ids` `RingHomInvPair.ids` `SMulCommClass.of_commMonoid` `IsScalarTower.right` `TensorProduct.isScalarTower_left` `IsScalarTower.left` `LinearEquiv.injective` `Finsupp.ext` `Module.Basis.baseChange_apply` `Module.Basis.repr_symm_apply` `Module.Basis.repr_linearCombination` `one_smul` `Algebra.Generators.repr_CotangentSpaceMap` `MvPolynomial.pderiv_X` `map_zero` `AddMonoidHomClass.toZeroHomClass` `DistribMulActionSemiHomClass.toAddMonoidHomClass` `SemilinearMapClass.distribMulActionSemiHomClass` `SemilinearEquivClass.instSemilinearMapClass` `LinearEquiv.instSemilinearEquivClass` `Pi.single_eq_of_ne` `MonoidWithZeroHomClass.toZeroHomClass` `RingHomClass.toMonoidWithZeroHomClass` `AlgHomClass.toRingHomClass` `AlgHom.algHomClass` `Module.Basis.baseChange_repr_tmul` `Module.Basis.repr_self` `Finsupp.single_apply` `ite_smul` `zero_smul` `Pi.single_apply` `MonoidWithZeroHom.map_ite_one_zero`
`compEquiv_symm_zero` 📖	mathematical	—	`DFunLike.coe` `LinearEquiv` `CommSemiring.toSemiring` `CommRing.toCommSemiring` `RingHom.id` `Semiring.toNonAssocSemiring` `RingHomInvPair.ids` `Algebra.Extension.CotangentSpace` `Algebra.Generators.toExtension` `TensorProduct` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing` `NonUnitalCommRing.toNonUnitalNonAssocCommRing` `CommRing.toNonUnitalCommRing` `TensorProduct.addCommMonoid` `Algebra.Extension.Ring` `Algebra.Extension.commRing` `KaehlerDifferential` `Algebra.Extension.instRingOfIsScalarTower` `Algebra.id` `AddCommGroup.toAddCommMonoid` `instAddCommGroupKaehlerDifferential` `Algebra.toModule` `Algebra.Extension.algebra₂` `KaehlerDifferential.module'` `TensorProduct.leftModule` `Semiring.toModule` `Algebra.to_smulCommClass` `Algebra.Generators.comp` `Prod.instAddCommMonoid` `Prod.instModule` `EquivLike.toFunLike` `DFinsupp.instEquivLikeLinearEquiv` `LinearEquiv.symm` `compEquiv` `AddZero.toZero` `AddZeroClass.toAddZero` `TensorProduct.addZeroClass` `LinearMap` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `LinearMap.instFunLike` `LinearMap.liftBaseChange` `SMulCommClass.of_commMonoid` `CommRing.toCommMonoid` `SMulZeroClass.toSMul` `AddMonoid.toAddZeroClass` `AddCommMonoid.toAddMonoid` `DistribSMul.toSMulZeroClass` `DistribMulAction.toDistribSMul` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `Module.toDistribMulAction` `IsScalarTower.right` `TensorProduct.isScalarTower_left` `Algebra.toSMul` `Algebra.Extension.CotangentSpace.map` `IsScalarTower.left` `DistribMulAction.toMulAction` `Algebra.Generators.Hom.toExtensionHom` `Algebra.Generators.toComp`	—	`Algebra.to_smulCommClass` `DFunLike.congr_fun` `RingHomCompTriple.ids` `RingHomInvPair.ids` `SMulCommClass.of_commMonoid` `IsScalarTower.right` `TensorProduct.isScalarTower_left` `IsScalarTower.left` `compEquiv_symm_inr`
`exact` 📖	mathematical	—	`Function.Exact` `TensorProduct` `CommRing.toCommSemiring` `Algebra.Extension.CotangentSpace` `Algebra.Generators.toExtension` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `CommSemiring.toSemiring` `TensorProduct.addCommMonoid` `Algebra.Extension.Ring` `Algebra.Extension.commRing` `KaehlerDifferential` `Algebra.Extension.instRingOfIsScalarTower` `Algebra.id` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing` `NonUnitalCommRing.toNonUnitalNonAssocCommRing` `CommRing.toNonUnitalCommRing` `AddCommGroup.toAddCommMonoid` `instAddCommGroupKaehlerDifferential` `Algebra.toModule` `Algebra.Extension.algebra₂` `KaehlerDifferential.module'` `TensorProduct.leftModule` `Semiring.toModule` `Algebra.to_smulCommClass` `Algebra.Generators.comp` `DFunLike.coe` `LinearMap` `RingHom.id` `LinearMap.instFunLike` `LinearMap.liftBaseChange` `SMulCommClass.of_commMonoid` `CommRing.toCommMonoid` `SMulZeroClass.toSMul` `AddZero.toZero` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `AddCommMonoid.toAddMonoid` `DistribSMul.toSMulZeroClass` `DistribMulAction.toDistribSMul` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `Module.toDistribMulAction` `IsScalarTower.right` `TensorProduct.isScalarTower_left` `Algebra.toSMul` `Algebra.Extension.CotangentSpace.map` `IsScalarTower.left` `DistribMulAction.toMulAction` `Algebra.Generators.Hom.toExtensionHom` `Algebra.Generators.toComp` `Algebra.Generators.ofComp` `TensorProduct.addZeroClass`	—	`Algebra.to_smulCommClass` `SMulCommClass.of_commMonoid` `IsScalarTower.right` `TensorProduct.isScalarTower_left` `IsScalarTower.left` `RingHomCompTriple.ids` `RingHomInvPair.ids` `fst_compEquiv` `compEquiv_symm_inr` `LinearEquiv.symm_symm` `LinearEquiv.conj_exact_iff_exact` `Function.Exact.inr_fst`
`fst_compEquiv` 📖	mathematical	—	`LinearMap.comp` `Algebra.Extension.CotangentSpace` `Algebra.Generators.toExtension` `Algebra.Generators.comp` `TensorProduct` `CommRing.toCommSemiring` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing` `NonUnitalCommRing.toNonUnitalNonAssocCommRing` `CommRing.toNonUnitalCommRing` `TensorProduct.addCommMonoid` `Algebra.Extension.Ring` `Algebra.Extension.commRing` `KaehlerDifferential` `Algebra.Extension.instRingOfIsScalarTower` `Algebra.id` `AddCommGroup.toAddCommMonoid` `instAddCommGroupKaehlerDifferential` `Algebra.toModule` `CommSemiring.toSemiring` `Algebra.Extension.algebra₂` `KaehlerDifferential.module'` `TensorProduct.leftModule` `Semiring.toModule` `Algebra.to_smulCommClass` `Prod.instAddCommMonoid` `Prod.instModule` `RingHom.id` `Semiring.toNonAssocSemiring` `RingHomCompTriple.ids` `LinearMap.fst` `LinearEquiv.toLinearMap` `RingHomInvPair.ids` `compEquiv` `Algebra.Extension.CotangentSpace.map` `Algebra.Generators.Hom.toExtensionHom` `IsScalarTower.right` `Algebra.Generators.ofComp`	—	`Module.Basis.ext` `Algebra.to_smulCommClass` `RingHomCompTriple.ids` `RingHomInvPair.ids` `IsScalarTower.right` `LinearEquiv.injective` `Finsupp.ext` `Module.Basis.repr_self` `Algebra.Generators.repr_CotangentSpaceMap` `Module.Basis.repr_symm_apply` `Finsupp.linearCombination_single` `Module.Basis.prod_apply` `one_smul` `Finsupp.single_apply` `MvPolynomial.pderiv_X` `Pi.single_apply` `MonoidWithZeroHom.map_ite_one_zero` `RingHomClass.toMonoidWithZeroHomClass` `AlgHomClass.toRingHomClass` `AlgHom.algHomClass` `Module.Basis.baseChange_apply` `map_zero` `AddMonoidHomClass.toZeroHomClass` `DistribMulActionSemiHomClass.toAddMonoidHomClass` `SemilinearMapClass.distribMulActionSemiHomClass` `SemilinearEquivClass.instSemilinearMapClass` `LinearEquiv.instSemilinearEquivClass` `MvPolynomial.derivation_C` `MonoidWithZeroHomClass.toZeroHomClass`
`fst_compEquiv_apply` 📖	mathematical	—	`Algebra.Extension.CotangentSpace` `Algebra.Generators.toExtension` `TensorProduct` `CommRing.toCommSemiring` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing` `NonUnitalCommRing.toNonUnitalNonAssocCommRing` `CommRing.toNonUnitalCommRing` `TensorProduct.addCommMonoid` `Algebra.Extension.Ring` `Algebra.Extension.commRing` `KaehlerDifferential` `Algebra.Extension.instRingOfIsScalarTower` `Algebra.id` `AddCommGroup.toAddCommMonoid` `instAddCommGroupKaehlerDifferential` `Algebra.toModule` `CommSemiring.toSemiring` `Algebra.Extension.algebra₂` `KaehlerDifferential.module'` `TensorProduct.leftModule` `Semiring.toModule` `Algebra.to_smulCommClass` `DFunLike.coe` `LinearEquiv` `RingHom.id` `Semiring.toNonAssocSemiring` `RingHomInvPair.ids` `Algebra.Generators.comp` `Prod.instAddCommMonoid` `Prod.instModule` `EquivLike.toFunLike` `DFinsupp.instEquivLikeLinearEquiv` `compEquiv` `LinearMap` `SMulCommClass.of_commMonoid` `CommRing.toCommMonoid` `SMulZeroClass.toSMul` `AddZero.toZero` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `AddCommMonoid.toAddMonoid` `DistribSMul.toSMulZeroClass` `DistribMulAction.toDistribSMul` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `Module.toDistribMulAction` `IsScalarTower.right` `LinearMap.instFunLike` `Algebra.Extension.CotangentSpace.map` `Algebra.Generators.Hom.toExtensionHom` `Algebra.Generators.ofComp`	—	`DFunLike.congr_fun` `Algebra.to_smulCommClass` `RingHomCompTriple.ids` `RingHomInvPair.ids` `IsScalarTower.right` `fst_compEquiv`
`map_ofComp_surjective` 📖	mathematical	—	`Algebra.Extension.CotangentSpace` `Algebra.Generators.toExtension` `Algebra.Generators.comp` `DFunLike.coe` `LinearMap` `CommSemiring.toSemiring` `CommRing.toCommSemiring` `RingHom.id` `Semiring.toNonAssocSemiring` `TensorProduct.addCommMonoid` `Algebra.Extension.Ring` `Algebra.Extension.commRing` `KaehlerDifferential` `Algebra.Extension.instRingOfIsScalarTower` `Algebra.id` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing` `NonUnitalCommRing.toNonUnitalNonAssocCommRing` `CommRing.toNonUnitalCommRing` `AddCommGroup.toAddCommMonoid` `instAddCommGroupKaehlerDifferential` `Algebra.toModule` `Algebra.Extension.algebra₂` `KaehlerDifferential.module'` `TensorProduct.leftModule` `Semiring.toModule` `Algebra.to_smulCommClass` `SMulCommClass.of_commMonoid` `CommRing.toCommMonoid` `SMulZeroClass.toSMul` `AddZero.toZero` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `AddCommMonoid.toAddMonoid` `DistribSMul.toSMulZeroClass` `DistribMulAction.toDistribSMul` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `Module.toDistribMulAction` `IsScalarTower.right` `LinearMap.instFunLike` `Algebra.Extension.CotangentSpace.map` `Algebra.Generators.Hom.toExtensionHom` `Algebra.Generators.ofComp`	—	`Algebra.to_smulCommClass` `SMulCommClass.of_commMonoid` `IsScalarTower.right` `RingHomCompTriple.ids` `RingHomInvPair.ids` `fst_compEquiv` `Prod.fst_surjective` `LinearEquiv.surjective`
`map_toComp_injective` 📖	mathematical	—	`TensorProduct` `CommRing.toCommSemiring` `Algebra.Extension.CotangentSpace` `Algebra.Generators.toExtension` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `CommSemiring.toSemiring` `TensorProduct.addCommMonoid` `Algebra.Extension.Ring` `Algebra.Extension.commRing` `KaehlerDifferential` `Algebra.Extension.instRingOfIsScalarTower` `Algebra.id` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing` `NonUnitalCommRing.toNonUnitalNonAssocCommRing` `CommRing.toNonUnitalCommRing` `AddCommGroup.toAddCommMonoid` `instAddCommGroupKaehlerDifferential` `Algebra.toModule` `Algebra.Extension.algebra₂` `KaehlerDifferential.module'` `TensorProduct.leftModule` `Semiring.toModule` `Algebra.to_smulCommClass` `Algebra.Generators.comp` `DFunLike.coe` `LinearMap` `RingHom.id` `LinearMap.instFunLike` `LinearMap.liftBaseChange` `SMulCommClass.of_commMonoid` `CommRing.toCommMonoid` `SMulZeroClass.toSMul` `AddZero.toZero` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `AddCommMonoid.toAddMonoid` `DistribSMul.toSMulZeroClass` `DistribMulAction.toDistribSMul` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `Module.toDistribMulAction` `IsScalarTower.right` `TensorProduct.isScalarTower_left` `Algebra.toSMul` `Algebra.Extension.CotangentSpace.map` `IsScalarTower.left` `DistribMulAction.toMulAction` `Algebra.Generators.Hom.toExtensionHom` `Algebra.Generators.toComp`	—	`Algebra.to_smulCommClass` `SMulCommClass.of_commMonoid` `IsScalarTower.right` `TensorProduct.isScalarTower_left` `IsScalarTower.left` `RingHomCompTriple.ids` `RingHomInvPair.ids` `compEquiv_symm_inr` `LinearEquiv.injective` `Prod.mk_right_injective`

Algebra.Generators.H1Cotangent

Definitions

Name	Category	Theorems
`δ` 📖	CompOp	8 math math: `exact_map_δ`, `exact_δ_map`, `δ_eq_δ`, `δ_eq`, `exact_map_δ'`, `δ_eq_δAux`, `δ_comp_equiv`, `δ_map`
`δAux` 📖	CompOp	7 math math: `δAux_mul`, `δAux_C`, `δAux_monomial`, `δAux_toAlgHom`, `δAux_ofComp`, `δAux_X`, `δ_eq_δAux`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`exact_map_δ` 📖	mathematical	—	`Function.Exact` `Algebra.Extension.H1Cotangent` `Algebra.Generators.toExtension` `Algebra.Generators.comp` `TensorProduct` `CommRing.toCommSemiring` `KaehlerDifferential` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing` `NonUnitalCommRing.toNonUnitalNonAssocCommRing` `CommRing.toNonUnitalCommRing` `AddCommGroup.toAddCommMonoid` `instAddCommGroupKaehlerDifferential` `Algebra.toModule` `CommSemiring.toSemiring` `KaehlerDifferential.module'` `Algebra.id` `Algebra.to_smulCommClass` `DFunLike.coe` `LinearMap` `RingHom.id` `Semiring.toNonAssocSemiring` `Algebra.Extension.instAddCommGroupH1Cotangent` `Algebra.Extension.instModuleH1CotangentOfIsScalarTowerCotangent` `Algebra.Extension.instModuleCotangent` `Algebra.Extension.instIsScalarTowerCotangent` `IsScalarTower.right` `LinearMap.instFunLike` `Algebra.Extension.H1Cotangent.map` `Algebra.Generators.Hom.toExtensionHom` `Algebra.Generators.ofComp` `TensorProduct.addCommMonoid` `TensorProduct.leftModule` `Semiring.toModule` `δ` `AddZero.toZero` `AddZeroClass.toAddZero` `TensorProduct.addZeroClass`	—	`Algebra.to_smulCommClass` `Algebra.Extension.instIsScalarTowerCotangent` `IsScalarTower.right` `RingHomCompTriple.ids` `SnakeLemma.exact_δ_right` `LinearMap.exact_subtype_ker_map` `Algebra.Generators.Cotangent.exact` `Algebra.Generators.CotangentSpace.exact` `map_comp_cotangentComplex_baseChange` `Algebra.Generators.Cotangent.surjective_map_ofComp` `Algebra.Generators.CotangentSpace.map_toComp_injective` `LinearMap.ext` `Algebra.Extension.Cotangent.ext` `Subtype.val_injective`
`exact_map_δ'` 📖	mathematical	—	`Function.Exact` `Algebra.Extension.H1Cotangent` `Algebra.Generators.toExtension` `TensorProduct` `CommRing.toCommSemiring` `KaehlerDifferential` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing` `NonUnitalCommRing.toNonUnitalNonAssocCommRing` `CommRing.toNonUnitalCommRing` `AddCommGroup.toAddCommMonoid` `instAddCommGroupKaehlerDifferential` `Algebra.toModule` `CommSemiring.toSemiring` `KaehlerDifferential.module'` `Algebra.id` `Algebra.to_smulCommClass` `DFunLike.coe` `LinearMap` `RingHom.id` `Semiring.toNonAssocSemiring` `Algebra.Extension.instAddCommGroupH1Cotangent` `Algebra.Extension.instModuleH1CotangentOfIsScalarTowerCotangent` `Algebra.Extension.instModuleCotangent` `Algebra.Extension.instIsScalarTowerCotangent` `IsScalarTower.right` `LinearMap.instFunLike` `Algebra.Extension.H1Cotangent.map` `Algebra.Generators.Hom.toExtensionHom` `TensorProduct.addCommMonoid` `TensorProduct.leftModule` `Semiring.toModule` `δ` `AddZero.toZero` `AddZeroClass.toAddZero` `TensorProduct.addZeroClass`	—	`Algebra.to_smulCommClass` `Algebra.Extension.instIsScalarTowerCotangent` `IsScalarTower.right` `RingHomCompTriple.ids` `RingHomInvPair.ids` `Function.Surjective.comp_exact_iff_exact` `LinearEquiv.surjective` `LinearMap.IsScalarTower.compatibleSMul` `Algebra.Extension.instIsScalarTowerH1CotangentOfCotangent` `IsScalarTower.left` `Algebra.Extension.H1Cotangent.map_comp` `Algebra.Extension.H1Cotangent.map_eq` `exact_map_δ`
`exact_δ_map` 📖	mathematical	—	`Function.Exact` `Algebra.Extension.H1Cotangent` `Algebra.Generators.toExtension` `TensorProduct` `CommRing.toCommSemiring` `KaehlerDifferential` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing` `NonUnitalCommRing.toNonUnitalNonAssocCommRing` `CommRing.toNonUnitalCommRing` `AddCommGroup.toAddCommMonoid` `instAddCommGroupKaehlerDifferential` `Algebra.toModule` `CommSemiring.toSemiring` `KaehlerDifferential.module'` `Algebra.id` `Algebra.to_smulCommClass` `DFunLike.coe` `LinearMap` `RingHom.id` `Semiring.toNonAssocSemiring` `Algebra.Extension.instAddCommGroupH1Cotangent` `TensorProduct.addCommMonoid` `Algebra.Extension.instModuleH1CotangentOfIsScalarTowerCotangent` `Algebra.Extension.instModuleCotangent` `Algebra.Extension.instIsScalarTowerCotangent` `IsScalarTower.right` `TensorProduct.leftModule` `Semiring.toModule` `LinearMap.instFunLike` `δ` `KaehlerDifferential.mapBaseChange` `AddZero.toZero` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `SubNegMonoid.toAddMonoid` `AddGroup.toSubNegMonoid` `AddCommGroup.toAddGroup`	—	`Algebra.to_smulCommClass` `Algebra.Extension.instIsScalarTowerCotangent` `IsScalarTower.right` `RingHomCompTriple.ids` `SnakeLemma.exact_δ_left` `Algebra.Extension.exact_cotangentComplex_toKaehler` `Algebra.Generators.Cotangent.exact` `Algebra.Generators.CotangentSpace.exact` `map_comp_cotangentComplex_baseChange` `Algebra.Generators.Cotangent.surjective_map_ofComp` `Algebra.Generators.CotangentSpace.map_toComp_injective` `Module.Basis.ext` `smulCommClass_self` `Module.Basis.baseChange_apply` `IsScalarTower.to_smulCommClass` `IsScalarTower.left` `Algebra.Generators.toKaehler_cotangentSpaceBasis` `KaehlerDifferential.mapBaseChange_tmul` `KaehlerDifferential.map_D` `one_smul` `Algebra.Generators.cotangentSpaceBasis_apply` `Algebra.Extension.CotangentSpace.map_tmul` `map_one` `MonoidHomClass.toOneHomClass` `MonoidWithZeroHomClass.toMonoidHomClass` `RingHomClass.toMonoidWithZeroHomClass` `RingHom.instRingHomClass` `Algebra.Generators.Hom.toAlgHom_X` `Algebra.Generators.algebraMap_apply` `MvPolynomial.aeval_X` `LinearMap.lTensor_surjective` `Algebra.Extension.toKaehler_surjective`
`map_comp_cotangentComplex_baseChange` 📖	mathematical	—	`LinearMap.comp` `TensorProduct` `CommRing.toCommSemiring` `Algebra.Extension.Cotangent` `Algebra.Generators.toExtension` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `CommSemiring.toSemiring` `AddCommGroup.toAddCommMonoid` `Algebra.Extension.instAddCommGroupCotangent` `Algebra.toModule` `Algebra.Extension.instModuleCotangent` `Algebra.id` `Algebra.Extension.CotangentSpace` `TensorProduct.addCommMonoid` `Algebra.Extension.Ring` `Algebra.Extension.commRing` `KaehlerDifferential` `Algebra.Extension.instRingOfIsScalarTower` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing` `NonUnitalCommRing.toNonUnitalNonAssocCommRing` `CommRing.toNonUnitalCommRing` `instAddCommGroupKaehlerDifferential` `Algebra.Extension.algebra₂` `KaehlerDifferential.module'` `TensorProduct.leftModule` `Semiring.toModule` `Algebra.to_smulCommClass` `Algebra.Generators.comp` `RingHom.id` `RingHomCompTriple.ids` `LinearMap.liftBaseChange` `SMulCommClass.of_commMonoid` `CommRing.toCommMonoid` `SMulZeroClass.toSMul` `AddZero.toZero` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `AddCommMonoid.toAddMonoid` `DistribSMul.toSMulZeroClass` `DistribMulAction.toDistribSMul` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `Module.toDistribMulAction` `IsScalarTower.right` `TensorProduct.isScalarTower_left` `Algebra.toSMul` `Algebra.Extension.CotangentSpace.map` `IsScalarTower.left` `DistribMulAction.toMulAction` `Algebra.Generators.Hom.toExtensionHom` `Algebra.Generators.toComp` `LinearMap.baseChange` `Algebra.Extension.cotangentComplex` `Algebra.Extension.instIsScalarTowerCotangent` `Algebra.Extension.Cotangent.map`	—	`TensorProduct.AlgebraTensorModule.curry_injective` `IsScalarTower.right` `SMulCommClass.of_commMonoid` `Algebra.to_smulCommClass` `TensorProduct.isScalarTower_left` `RingHomCompTriple.ids` `IsScalarTower.left` `Algebra.Extension.instIsScalarTowerCotangent` `LinearMap.ext_ring` `IsScalarTower.to_smulCommClass` `LinearMap.ext` `Algebra.Extension.CotangentSpace.map_cotangentComplex` `one_smul`
`δAux_C` 📖	mathematical	—	`DFunLike.coe` `LinearMap` `CommSemiring.toSemiring` `CommRing.toCommSemiring` `RingHom.id` `Semiring.toNonAssocSemiring` `Algebra.Generators.Ring` `TensorProduct` `KaehlerDifferential` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing` `NonUnitalCommRing.toNonUnitalNonAssocCommRing` `CommRing.toNonUnitalCommRing` `AddCommGroup.toAddCommMonoid` `instAddCommGroupKaehlerDifferential` `Algebra.toModule` `KaehlerDifferential.module'` `Algebra.id` `Algebra.to_smulCommClass` `MvPolynomial.instCommRingMvPolynomial` `TensorProduct.addCommMonoid` `MvPolynomial.module` `TensorProduct.leftModule` `SMulCommClass.of_commMonoid` `CommRing.toCommMonoid` `SMulZeroClass.toSMul` `AddZero.toZero` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `AddCommMonoid.toAddMonoid` `DistribSMul.toSMulZeroClass` `DistribMulAction.toDistribSMul` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `Module.toDistribMulAction` `IsScalarTower.right` `LinearMap.instFunLike` `δAux` `RingHom` `MvPolynomial` `MvPolynomial.commSemiring` `RingHom.instFunLike` `MvPolynomial.C` `TensorProduct.tmul` `AddMonoidWithOne.toOne` `AddGroupWithOne.toAddMonoidWithOne` `Ring.toAddGroupWithOne` `CommRing.toRing` `Derivation` `smulCommClass_self` `DistribMulAction.toMulAction` `CommMonoid.toMonoid` `Ring.toSemiring` `Derivation.instFunLike` `KaehlerDifferential.D`	—	`Algebra.to_smulCommClass` `SMulCommClass.of_commMonoid` `IsScalarTower.right` `smulCommClass_self` `MvPolynomial.monomial_zero'` `δAux_monomial` `Finsupp.prod_zero_index`
`δAux_X` 📖	mathematical	—	`DFunLike.coe` `LinearMap` `CommSemiring.toSemiring` `CommRing.toCommSemiring` `RingHom.id` `Semiring.toNonAssocSemiring` `Algebra.Generators.Ring` `TensorProduct` `KaehlerDifferential` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing` `NonUnitalCommRing.toNonUnitalNonAssocCommRing` `CommRing.toNonUnitalCommRing` `AddCommGroup.toAddCommMonoid` `instAddCommGroupKaehlerDifferential` `Algebra.toModule` `KaehlerDifferential.module'` `Algebra.id` `Algebra.to_smulCommClass` `MvPolynomial.instCommRingMvPolynomial` `TensorProduct.addCommMonoid` `MvPolynomial.module` `TensorProduct.leftModule` `SMulCommClass.of_commMonoid` `CommRing.toCommMonoid` `SMulZeroClass.toSMul` `AddZero.toZero` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `AddCommMonoid.toAddMonoid` `DistribSMul.toSMulZeroClass` `DistribMulAction.toDistribSMul` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `Module.toDistribMulAction` `IsScalarTower.right` `LinearMap.instFunLike` `δAux` `MvPolynomial.X` `TensorProduct.addZeroClass`	—	`Algebra.to_smulCommClass` `SMulCommClass.of_commMonoid` `IsScalarTower.right` `MvPolynomial.X.eq_1` `smulCommClass_self` `δAux_monomial` `Derivation.map_one_eq_zero` `TensorProduct.tmul_zero`
`δAux_monomial` 📖	mathematical	—	`DFunLike.coe` `LinearMap` `CommSemiring.toSemiring` `CommRing.toCommSemiring` `RingHom.id` `Semiring.toNonAssocSemiring` `Algebra.Generators.Ring` `TensorProduct` `KaehlerDifferential` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing` `NonUnitalCommRing.toNonUnitalNonAssocCommRing` `CommRing.toNonUnitalCommRing` `AddCommGroup.toAddCommMonoid` `instAddCommGroupKaehlerDifferential` `Algebra.toModule` `KaehlerDifferential.module'` `Algebra.id` `Algebra.to_smulCommClass` `MvPolynomial.instCommRingMvPolynomial` `TensorProduct.addCommMonoid` `MvPolynomial.module` `TensorProduct.leftModule` `SMulCommClass.of_commMonoid` `CommRing.toCommMonoid` `SMulZeroClass.toSMul` `AddZero.toZero` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `AddCommMonoid.toAddMonoid` `DistribSMul.toSMulZeroClass` `DistribMulAction.toDistribSMul` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `Module.toDistribMulAction` `IsScalarTower.right` `LinearMap.instFunLike` `δAux` `MvPolynomial` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `MvPolynomial.commSemiring` `Semiring.toModule` `MvPolynomial.monomial` `TensorProduct.tmul` `Finsupp.prod` `MulZeroClass.toZero` `Nat.instMulZeroClass` `Monoid.toNatPow` `Algebra.Generators.val` `Derivation` `smulCommClass_self` `DistribMulAction.toMulAction` `CommMonoid.toMonoid` `Ring.toSemiring` `CommRing.toRing` `Derivation.instFunLike` `KaehlerDifferential.D`	—	`Finsupp.lsum_single` `Algebra.to_smulCommClass`
`δAux_mul` 📖	mathematical	—	`DFunLike.coe` `LinearMap` `CommSemiring.toSemiring` `CommRing.toCommSemiring` `RingHom.id` `Semiring.toNonAssocSemiring` `Algebra.Generators.Ring` `TensorProduct` `KaehlerDifferential` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing` `NonUnitalCommRing.toNonUnitalNonAssocCommRing` `CommRing.toNonUnitalCommRing` `AddCommGroup.toAddCommMonoid` `instAddCommGroupKaehlerDifferential` `Algebra.toModule` `KaehlerDifferential.module'` `Algebra.id` `Algebra.to_smulCommClass` `MvPolynomial.instCommRingMvPolynomial` `TensorProduct.addCommMonoid` `MvPolynomial.module` `TensorProduct.leftModule` `SMulCommClass.of_commMonoid` `CommRing.toCommMonoid` `SMulZeroClass.toSMul` `AddZero.toZero` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `AddCommMonoid.toAddMonoid` `DistribSMul.toSMulZeroClass` `DistribMulAction.toDistribSMul` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `Module.toDistribMulAction` `IsScalarTower.right` `LinearMap.instFunLike` `δAux` `Distrib.toMul` `NonUnitalNonAssocSemiring.toDistrib` `TensorProduct.add` `TensorProduct.leftHasSMul` `MvPolynomial.commSemiring` `Algebra.Generators.instRing`	—	`MvPolynomial.induction_on'` `Algebra.to_smulCommClass` `SMulCommClass.of_commMonoid` `IsScalarTower.right` `smulCommClass_self` `MvPolynomial.monomial_mul` `δAux_monomial` `Derivation.leibniz` `TensorProduct.tmul_add` `TensorProduct.tmul_smul` `TensorProduct.CompatibleSMul.isScalarTower` `IsScalarTower.left` `KaehlerDifferential.isScalarTower_of_tower` `Algebra.smul_def` `Algebra.Generators.algebraMap_apply` `MvPolynomial.aeval_monomial` `mul_assoc` `mul_comm` `Finsupp.prod_add_index'` `pow_zero` `pow_add` `mul_add` `Distrib.leftDistribClass` `map_add` `SemilinearMapClass.toAddHomClass` `LinearMap.semilinearMapClass` `smul_add` `add_smul` `Mathlib.Tactic.Abel.subst_into_addg` `Mathlib.Tactic.Abel.term_atomg` `Mathlib.Tactic.Abel.term_add_constg` `zero_add` `Mathlib.Tactic.Abel.const_add_termg` `add_mul` `Distrib.rightDistribClass`
`δAux_ofComp` 📖	mathematical	—	`DFunLike.coe` `LinearMap` `CommSemiring.toSemiring` `CommRing.toCommSemiring` `RingHom.id` `Semiring.toNonAssocSemiring` `Algebra.Generators.Ring` `TensorProduct` `KaehlerDifferential` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing` `NonUnitalCommRing.toNonUnitalNonAssocCommRing` `CommRing.toNonUnitalCommRing` `AddCommGroup.toAddCommMonoid` `instAddCommGroupKaehlerDifferential` `Algebra.toModule` `KaehlerDifferential.module'` `Algebra.id` `Algebra.to_smulCommClass` `MvPolynomial.instCommRingMvPolynomial` `TensorProduct.addCommMonoid` `MvPolynomial.module` `TensorProduct.leftModule` `SMulCommClass.of_commMonoid` `CommRing.toCommMonoid` `SMulZeroClass.toSMul` `AddZero.toZero` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `AddCommMonoid.toAddMonoid` `DistribSMul.toSMulZeroClass` `DistribMulAction.toDistribSMul` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `Module.toDistribMulAction` `IsScalarTower.right` `LinearMap.instFunLike` `δAux` `AlgHom` `Algebra.Generators.comp` `MvPolynomial.commSemiring` `MvPolynomial.algebra` `AlgHom.funLike` `Algebra.Generators.Hom.toAlgHom` `Algebra.Generators.ofComp` `Algebra.Extension.CotangentSpace` `Algebra.Generators.toExtension` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Algebra.Extension.Ring` `Algebra.Extension.commRing` `Algebra.Extension.instRingOfIsScalarTower` `Algebra.Extension.algebra₂` `Semiring.toModule` `LinearMap.baseChange` `Algebra.Extension.toKaehler` `LinearEquiv` `RingHomInvPair.ids` `Prod.instAddCommMonoid` `Prod.instModule` `EquivLike.toFunLike` `DFinsupp.instEquivLikeLinearEquiv` `Algebra.Generators.CotangentSpace.compEquiv` `TensorProduct.tmul` `MvPolynomial` `AddMonoidWithOne.toOne` `AddGroupWithOne.toAddMonoidWithOne` `Ring.toAddGroupWithOne` `CommRing.toRing` `Derivation` `smulCommClass_self` `DistribMulAction.toMulAction` `CommMonoid.toMonoid` `Ring.toSemiring` `Derivation.instFunLike` `KaehlerDifferential.D`	—	`IsScalarTower.left` `MvPolynomial.induction_on` `Algebra.to_smulCommClass` `SMulCommClass.of_commMonoid` `IsScalarTower.right` `RingHomInvPair.ids` `smulCommClass_self` `MvPolynomial.algHom_C` `δAux_C` `Derivation.map_algebraMap` `TensorProduct.tmul_zero` `MvPolynomial.derivation_C` `map_zero` `AddMonoidHomClass.toZeroHomClass` `DistribMulActionSemiHomClass.toAddMonoidHomClass` `SemilinearMapClass.distribMulActionSemiHomClass` `SemilinearEquivClass.instSemilinearMapClass` `LinearEquiv.instSemilinearEquivClass` `LinearMap.semilinearMapClass` `map_add` `SemilinearMapClass.toAddHomClass` `NonUnitalAlgHomClass.instLinearMapClass` `AlgHom.instNonUnitalAlgHomClassOfAlgHomClass` `AlgHom.algHomClass` `AddMonoidHomClass.toAddHomClass` `Derivation.instAddMonoidHomClass` `TensorProduct.tmul_add` `map_mul` `NonUnitalAlgSemiHomClass.toMulHomClass` `Algebra.Generators.Hom.toAlgHom_X` `δAux_mul` `IsScalarTower.algebraMap_smul` `TensorProduct.isScalarTower_left` `Algebra.Generators.algebraMap_apply` `Algebra.Generators.Hom.algebraMap_toAlgHom` `MvPolynomial.map_aeval` `RingHomCompTriple.comp_eq` `RingHomCompTriple.right_ids` `Derivation.leibniz` `TensorProduct.tmul_smul` `TensorProduct.CompatibleSMul.isScalarTower` `KaehlerDifferential.isScalarTower_of_tower` `MvPolynomial.aeval_X` `map_smul` `SemilinearMapClass.toMulActionSemiHomClass` `δAux_X` `smul_zero` `Module.Basis.repr_symm_apply` `zero_add` `Module.Basis.repr_self` `Finsupp.linearCombination_single` `Module.Basis.prod_apply` `one_smul` `algebraMap_smul` `Module.Basis.baseChange_apply` `Algebra.Generators.toKaehler_cotangentSpaceBasis` `AddRightCancelSemigroup.toIsRightCancelAdd`
`δAux_toAlgHom` 📖	mathematical	—	`DFunLike.coe` `LinearMap` `CommSemiring.toSemiring` `CommRing.toCommSemiring` `RingHom.id` `Semiring.toNonAssocSemiring` `Algebra.Generators.Ring` `TensorProduct` `KaehlerDifferential` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing` `NonUnitalCommRing.toNonUnitalNonAssocCommRing` `CommRing.toNonUnitalCommRing` `AddCommGroup.toAddCommMonoid` `instAddCommGroupKaehlerDifferential` `Algebra.toModule` `KaehlerDifferential.module'` `Algebra.id` `Algebra.to_smulCommClass` `MvPolynomial.instCommRingMvPolynomial` `TensorProduct.addCommMonoid` `MvPolynomial.module` `TensorProduct.leftModule` `SMulCommClass.of_commMonoid` `CommRing.toCommMonoid` `SMulZeroClass.toSMul` `AddZero.toZero` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `AddCommMonoid.toAddMonoid` `DistribSMul.toSMulZeroClass` `DistribMulAction.toDistribSMul` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `Module.toDistribMulAction` `IsScalarTower.right` `LinearMap.instFunLike` `δAux` `AlgHom` `MvPolynomial.commSemiring` `MvPolynomial.algebra` `AlgHom.funLike` `Algebra.Generators.Hom.toAlgHom` `TensorProduct.add` `Finsupp` `MulZeroClass.toZero` `NonUnitalNonAssocSemiring.toMulZeroClass` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Finsupp.instAddCommMonoid` `Finsupp.module` `Semiring.toModule` `Finsupp.linearCombination` `Algebra.Generators.Hom.val` `LinearEquiv` `RingHomInvPair.ids` `Algebra.Extension.CotangentSpace` `Algebra.Generators.toExtension` `Algebra.Extension.Ring` `Algebra.Extension.commRing` `Algebra.Extension.instRingOfIsScalarTower` `Algebra.Extension.algebra₂` `EquivLike.toFunLike` `DFinsupp.instEquivLikeLinearEquiv` `Module.Basis.repr` `Algebra.Generators.cotangentSpaceBasis` `TensorProduct.tmul` `Algebra.Generators.instRing` `MvPolynomial` `AddMonoidWithOne.toOne` `AddGroupWithOne.toAddMonoidWithOne` `Ring.toAddGroupWithOne` `CommRing.toRing` `Derivation` `smulCommClass_self` `DistribMulAction.toMulAction` `CommMonoid.toMonoid` `Ring.toSemiring` `Derivation.instFunLike` `KaehlerDifferential.D`	—	`IsScalarTower.left` `MvPolynomial.induction_on` `Algebra.to_smulCommClass` `SMulCommClass.of_commMonoid` `IsScalarTower.right` `RingHomInvPair.ids` `smulCommClass_self` `MvPolynomial.algHom_C` `δAux_C` `MvPolynomial.derivation_C` `TensorProduct.tmul_zero` `map_zero` `AddMonoidHomClass.toZeroHomClass` `DistribMulActionSemiHomClass.toAddMonoidHomClass` `SemilinearMapClass.distribMulActionSemiHomClass` `SemilinearEquivClass.instSemilinearMapClass` `LinearEquiv.instSemilinearEquivClass` `LinearMap.semilinearMapClass` `add_zero` `map_add` `SemilinearMapClass.toAddHomClass` `NonUnitalAlgHomClass.instLinearMapClass` `AlgHom.instNonUnitalAlgHomClassOfAlgHomClass` `AlgHom.algHomClass` `AddMonoidHomClass.toAddHomClass` `Derivation.instAddMonoidHomClass` `TensorProduct.tmul_add` `add_add_add_comm` `map_mul` `NonUnitalAlgSemiHomClass.toMulHomClass` `Algebra.Generators.Hom.toAlgHom_X` `δAux_mul` `IsScalarTower.algebraMap_smul` `TensorProduct.isScalarTower_left` `Algebra.Generators.algebraMap_apply` `Algebra.Generators.Hom.algebraMap_toAlgHom` `MvPolynomial.map_aeval` `RingHomCompTriple.comp_eq` `RingHomCompTriple.right_ids` `Algebra.Generators.Hom.aeval_val` `smul_add` `δAux_X` `smul_zero` `MvPolynomial.aeval_X` `zero_add` `Derivation.leibniz` `TensorProduct.tmul_smul` `TensorProduct.CompatibleSMul.isScalarTower` `KaehlerDifferential.isScalarTower_of_tower` `map_smul` `SemilinearMapClass.toMulActionSemiHomClass` `Module.Basis.repr_self` `Finsupp.linearCombination_single` `one_smul` `add_left_comm`
`δ_comp_equiv` 📖	mathematical	—	`LinearMap.comp` `Algebra.Extension.H1Cotangent` `Algebra.Generators.toExtension` `TensorProduct` `CommRing.toCommSemiring` `KaehlerDifferential` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing` `NonUnitalCommRing.toNonUnitalNonAssocCommRing` `CommRing.toNonUnitalCommRing` `AddCommGroup.toAddCommMonoid` `instAddCommGroupKaehlerDifferential` `Algebra.toModule` `CommSemiring.toSemiring` `KaehlerDifferential.module'` `Algebra.id` `Algebra.to_smulCommClass` `Algebra.Extension.instAddCommGroupH1Cotangent` `TensorProduct.addCommMonoid` `Algebra.Extension.instModuleH1CotangentOfIsScalarTowerCotangent` `Algebra.Extension.instModuleCotangent` `Algebra.Extension.instIsScalarTowerCotangent` `IsScalarTower.right` `TensorProduct.leftModule` `Semiring.toModule` `RingHom.id` `Semiring.toNonAssocSemiring` `RingHomCompTriple.ids` `δ` `LinearEquiv.toLinearMap` `RingHomInvPair.ids` `equiv`	—	`LinearMap.ext` `Algebra.to_smulCommClass` `Algebra.Extension.instIsScalarTowerCotangent` `IsScalarTower.right` `RingHomCompTriple.ids` `RingHomInvPair.ids` `δ_map`
`δ_eq` 📖	mathematical	`DFunLike.coe` `LinearMap` `CommSemiring.toSemiring` `CommRing.toCommSemiring` `RingHom.id` `Semiring.toNonAssocSemiring` `Algebra.Extension.Cotangent` `Algebra.Generators.toExtension` `Algebra.Generators.comp` `AddCommGroup.toAddCommMonoid` `Algebra.Extension.instAddCommGroupCotangent` `Algebra.Extension.instModuleCotangent` `Algebra.id` `LinearMap.instFunLike` `Algebra.Extension.Cotangent.map` `Algebra.Generators.Hom.toExtensionHom` `IsScalarTower.right` `Algebra.Generators.ofComp` `Submodule` `SetLike.instMembership` `Submodule.setLike` `LinearMap.ker` `Algebra.Extension.CotangentSpace` `TensorProduct.addCommMonoid` `Algebra.Extension.Ring` `Algebra.Extension.commRing` `KaehlerDifferential` `Algebra.Extension.instRingOfIsScalarTower` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing` `NonUnitalCommRing.toNonUnitalNonAssocCommRing` `CommRing.toNonUnitalCommRing` `instAddCommGroupKaehlerDifferential` `Algebra.toModule` `Algebra.Extension.algebra₂` `KaehlerDifferential.module'` `TensorProduct.leftModule` `Semiring.toModule` `Algebra.Extension.cotangentComplex` `TensorProduct` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Algebra.to_smulCommClass` `LinearMap.liftBaseChange` `SMulCommClass.of_commMonoid` `CommRing.toCommMonoid` `SMulZeroClass.toSMul` `AddZero.toZero` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `AddCommMonoid.toAddMonoid` `DistribSMul.toSMulZeroClass` `DistribMulAction.toDistribSMul` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `Module.toDistribMulAction` `TensorProduct.isScalarTower_left` `Algebra.toSMul` `Algebra.Extension.CotangentSpace.map` `IsScalarTower.left` `DistribMulAction.toMulAction` `Algebra.Generators.toComp`	`Algebra.Extension.H1Cotangent` `Algebra.Extension.instAddCommGroupH1Cotangent` `Algebra.Extension.instModuleH1CotangentOfIsScalarTowerCotangent` `Algebra.Extension.instIsScalarTowerCotangent` `δ` `LinearMap.baseChange` `Algebra.Extension.toKaehler`	—	`IsScalarTower.right` `Algebra.to_smulCommClass` `SMulCommClass.of_commMonoid` `TensorProduct.isScalarTower_left` `IsScalarTower.left` `Algebra.Extension.instIsScalarTowerCotangent` `SnakeLemma.δ_eq` `Algebra.Generators.Cotangent.exact` `Algebra.Generators.CotangentSpace.exact` `map_comp_cotangentComplex_baseChange` `Algebra.Generators.Cotangent.surjective_map_ofComp` `Algebra.Generators.CotangentSpace.map_toComp_injective`
`δ_eq_δ` 📖	mathematical	—	`δ`	—	`LinearMap.ext` `Algebra.to_smulCommClass` `Algebra.Extension.instIsScalarTowerCotangent` `IsScalarTower.right` `Algebra.Extension.Cotangent.mk_surjective` `SMulCommClass.of_commMonoid` `δ_eq_δAux`
`δ_eq_δAux` 📖	mathematical	`Algebra.Extension.Cotangent` `Algebra.Generators.toExtension` `Submodule` `CommSemiring.toSemiring` `CommRing.toCommSemiring` `AddCommGroup.toAddCommMonoid` `Algebra.Extension.instAddCommGroupCotangent` `Algebra.Extension.instModuleCotangent` `Algebra.id` `SetLike.instMembership` `Submodule.setLike` `LinearMap.ker` `Algebra.Extension.CotangentSpace` `TensorProduct.addCommMonoid` `Algebra.Extension.Ring` `Algebra.Extension.commRing` `KaehlerDifferential` `Algebra.Extension.instRingOfIsScalarTower` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing` `NonUnitalCommRing.toNonUnitalNonAssocCommRing` `CommRing.toNonUnitalCommRing` `instAddCommGroupKaehlerDifferential` `Algebra.toModule` `Algebra.Extension.algebra₂` `KaehlerDifferential.module'` `TensorProduct.leftModule` `Semiring.toModule` `RingHom.id` `Semiring.toNonAssocSemiring` `Algebra.Extension.cotangentComplex` `DFunLike.coe` `LinearMap` `Ideal` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Algebra.Extension.ker` `Submodule.addCommMonoid` `Submodule.module` `LinearMap.instFunLike`	`Algebra.Extension.H1Cotangent` `TensorProduct` `Algebra.to_smulCommClass` `Algebra.Extension.instAddCommGroupH1Cotangent` `Algebra.Extension.instModuleH1CotangentOfIsScalarTowerCotangent` `Algebra.Extension.instIsScalarTowerCotangent` `IsScalarTower.right` `δ` `Algebra.Generators.Ring` `MvPolynomial.instCommRingMvPolynomial` `MvPolynomial.module` `SMulCommClass.of_commMonoid` `CommRing.toCommMonoid` `SMulZeroClass.toSMul` `AddZero.toZero` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `AddCommMonoid.toAddMonoid` `DistribSMul.toSMulZeroClass` `DistribMulAction.toDistribSMul` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `Module.toDistribMulAction` `δAux` `MvPolynomial.commSemiring` `Algebra.Generators.ker`	—	`IsScalarTower.right` `IsScalarTower.left` `Algebra.Generators.ofComp_kerCompPreimage` `Algebra.to_smulCommClass` `RingHomInvPair.ids` `Algebra.Extension.instIsScalarTowerCotangent` `SMulCommClass.of_commMonoid` `δ_eq` `TensorProduct.isScalarTower_left` `RingHomCompTriple.ids` `Algebra.Generators.CotangentSpace.compEquiv_symm_inr` `LinearEquiv.injective` `LinearEquiv.apply_symm_apply` `Algebra.Generators.CotangentSpace.fst_compEquiv` `Algebra.Extension.CotangentSpace.map_cotangentComplex` `smulCommClass_self` `δAux_ofComp`
`δ_map` 📖	mathematical	—	`DFunLike.coe` `LinearMap` `CommSemiring.toSemiring` `CommRing.toCommSemiring` `RingHom.id` `Semiring.toNonAssocSemiring` `Algebra.Extension.H1Cotangent` `Algebra.Generators.toExtension` `TensorProduct` `KaehlerDifferential` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing` `NonUnitalCommRing.toNonUnitalNonAssocCommRing` `CommRing.toNonUnitalCommRing` `AddCommGroup.toAddCommMonoid` `instAddCommGroupKaehlerDifferential` `Algebra.toModule` `KaehlerDifferential.module'` `Algebra.id` `Algebra.to_smulCommClass` `Algebra.Extension.instAddCommGroupH1Cotangent` `TensorProduct.addCommMonoid` `Algebra.Extension.instModuleH1CotangentOfIsScalarTowerCotangent` `Algebra.Extension.instModuleCotangent` `Algebra.Extension.instIsScalarTowerCotangent` `IsScalarTower.right` `TensorProduct.leftModule` `Semiring.toModule` `LinearMap.instFunLike` `δ` `Algebra.Extension.H1Cotangent.map` `IsScalarTower.left` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `DistribMulAction.toMulAction` `AddCommMonoid.toAddMonoid` `Module.toDistribMulAction` `Algebra.Generators.Hom.toExtensionHom`	—	`Algebra.to_smulCommClass` `Algebra.Extension.instIsScalarTowerCotangent` `IsScalarTower.right` `IsScalarTower.left` `Algebra.Extension.Cotangent.mk_surjective` `smulCommClass_self` `SMulCommClass.of_commMonoid` `δ_eq_δAux` `RingHomInvPair.ids` `δAux_toAlgHom` `map_zero` `AddMonoidHomClass.toZeroHomClass` `DistribMulActionSemiHomClass.toAddMonoidHomClass` `SemilinearMapClass.distribMulActionSemiHomClass` `SemilinearEquivClass.instSemilinearMapClass` `LinearEquiv.instSemilinearEquivClass` `LinearMap.semilinearMapClass` `add_zero`

Algebra.H1Cotangent

Definitions

Name	Category	Theorems
`δ` 📖	CompOp	2 math math: `exact_map_δ`, `exact_δ_mapBaseChange`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`exact_map_δ` 📖	mathematical	—	`Function.Exact` `Algebra.H1Cotangent` `TensorProduct` `CommRing.toCommSemiring` `KaehlerDifferential` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing` `NonUnitalCommRing.toNonUnitalNonAssocCommRing` `CommRing.toNonUnitalCommRing` `AddCommGroup.toAddCommMonoid` `instAddCommGroupKaehlerDifferential` `Algebra.toModule` `CommSemiring.toSemiring` `KaehlerDifferential.module'` `Algebra.id` `Algebra.to_smulCommClass` `DFunLike.coe` `LinearMap` `RingHom.id` `Semiring.toNonAssocSemiring` `Algebra.Extension.instAddCommGroupH1Cotangent` `Algebra.Generators.toExtension` `Algebra.Generators.self` `Algebra.Extension.instModuleH1CotangentOfIsScalarTowerCotangent` `Algebra.Extension.instModuleCotangent` `Algebra.Extension.instIsScalarTowerCotangent` `IsScalarTower.right` `LinearMap.instFunLike` `map` `TensorProduct.addCommMonoid` `TensorProduct.leftModule` `Semiring.toModule` `δ` `TensorProduct.zero`	—	`Algebra.Generators.H1Cotangent.exact_map_δ'`
`exact_δ_mapBaseChange` 📖	mathematical	—	`Function.Exact` `Algebra.H1Cotangent` `TensorProduct` `CommRing.toCommSemiring` `KaehlerDifferential` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing` `NonUnitalCommRing.toNonUnitalNonAssocCommRing` `CommRing.toNonUnitalCommRing` `AddCommGroup.toAddCommMonoid` `instAddCommGroupKaehlerDifferential` `Algebra.toModule` `CommSemiring.toSemiring` `KaehlerDifferential.module'` `Algebra.id` `Algebra.to_smulCommClass` `DFunLike.coe` `LinearMap` `RingHom.id` `Semiring.toNonAssocSemiring` `Algebra.Extension.instAddCommGroupH1Cotangent` `Algebra.Generators.toExtension` `Algebra.Generators.self` `TensorProduct.addCommMonoid` `Algebra.Extension.instModuleH1CotangentOfIsScalarTowerCotangent` `Algebra.Extension.instModuleCotangent` `Algebra.Extension.instIsScalarTowerCotangent` `IsScalarTower.right` `TensorProduct.leftModule` `Semiring.toModule` `LinearMap.instFunLike` `δ` `KaehlerDifferential.mapBaseChange` `NegZeroClass.toZero` `SubNegZeroMonoid.toNegZeroClass` `SubtractionMonoid.toSubNegZeroMonoid` `SubtractionCommMonoid.toSubtractionMonoid` `AddCommGroup.toDivisionAddCommMonoid`	—	`Algebra.Generators.H1Cotangent.exact_δ_map`

---

← Back to Index