Basic

📁 Source: Mathlib/RingTheory/Extension/Cotangent/Basic.lean

Statistics

Metric	Count
Definitions CotangentSpace, map, H1Cotangent, equiv, map, sub, subToKer, cotangentComplex, h1Cotangentι, instAddCommGroupH1Cotangent, instModuleH1CotangentOfIsScalarTowerCotangent, toKaehler, equiv, cotangentRestrict, cotangentSpaceBasis, equivH1Cotangent, H1Cotangent, map, mapEquiv, cotangentComplexBaseChange	20
Theorems map_sub_map, map_comp, map_comp_apply, map_comp_cotangentComplex, map_cotangentComplex, map_id, map_sub_map, map_tmul, equiv_apply, map_apply_coe, map_comp, map_eq, map_id, val_add, val_smul, val_zero, subToKer_apply_coe, sub_aux, sub_one_tmul, sub_tmul, cotangentComplexBaseChange_eq_lTensor_cotangentComplex, cotangentComplex_mk, exact_cotangentComplex_toKaehler, h1Cotangentι_apply, h1Cotangentι_ext, h1Cotangentι_ext_iff, h1Cotangentι_injective, instIsScalarTowerH1CotangentOfCotangent, lTensor_cotangentComplex_eq_cotangentComplexBaseChange, subsingleton_h1Cotangent, toKaehler_surjective, equiv_apply, cotangentRestrict_mk, cotangentSpaceBasis_apply, cotangentSpaceBasis_repr_one_tmul, cotangentSpaceBasis_repr_tmul, instFreeCotangentSpaceToExtension, repr_CotangentSpaceMap, toKaehler_cotangentSpaceBasis, toKaehler_tmul_D, instFiniteH1CotangentOfFinitePresentationOfProjectiveKaehlerDifferential, instFinitePresentationKaehlerDifferentialOfFinitePresentation, cotangentComplexBaseChange_tmul	43
Total	63

Algebra

Definitions

Name	Category	Theorems
H1Cotangent 📖	CompOp	16 math math: formallyEtale_iff, FormallySmooth.iff_subsingleton_and_projective, instFiniteH1CotangentOfFinitePresentationOfProjectiveKaehlerDifferential, FormallySmooth.subsingleton_h1Cotangent, FormallySmooth.kerCotangentToTensor_injective_iff, Extension.cotangentComplex_injective_iff, H1Cotangent.isLocalizedModule, tensorH1CotangentOfIsLocalization_toLinearMap, formallySmooth_iff, H1Cotangent.exact_map_δ, IsStandardSmooth.iff_exists_basis_kaehlerDifferential, IsStandardSmooth.subsingleton_h1Cotangent, FormallyEtale.subsingleton_h1Cotangent, smoothLocus_eq_compl_support_inter, H1Cotangent.exact_δ_mapBaseChange, etaleLocus_eq_compl_support

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
instFiniteH1CotangentOfFinitePresentationOfProjectiveKaehlerDifferential 📖	mathematical	—	Module.Finite H1Cotangent CommSemiring.toSemiring CommRing.toCommSemiring AddCommGroup.toAddCommMonoid Extension.instAddCommGroupH1Cotangent Generators.toExtension Generators.self Extension.instModuleH1CotangentOfIsScalarTowerCotangent id Extension.instModuleCotangent Extension.instIsScalarTowerCotangent IsScalarTower.right	—	to_smulCommClass IsScalarTower.left FiniteType.instMvPolynomialOfFinite Finite.of_fintype FiniteType.of_finitePresentation FinitePresentation.self Extension.instIsScalarTowerCotangent IsScalarTower.right Module.finite_def Submodule.fg_top RingHomSurjective.ids LinearMap.ker_rangeRestrict Extension.Cotangent.finite Presentation.fg_ker LinearMap.exact_iff Extension.exact_cotangentComplex_toKaehler Module.finitePresentation_of_projective_of_exact Module.finitePresentation_of_projective Module.Projective.of_free Generators.instFreeCotangentSpaceToExtension Module.Finite.base_change KaehlerDifferential.finite EssFiniteType.of_finiteType Subtype.val_injective Extension.toKaehler_surjective LinearMap.exact_subtype_ker_map Module.FinitePresentation.fg_ker LinearMap.surjective_rangeRestrict Module.Finite.of_surjective RingHomInvPair.ids LinearEquiv.surjective
instFinitePresentationKaehlerDifferentialOfFinitePresentation 📖	mathematical	—	Module.FinitePresentation KaehlerDifferential CommSemiring.toSemiring CommRing.toCommSemiring AddCommGroup.toAddCommMonoid instAddCommGroupKaehlerDifferential KaehlerDifferential.module' id to_smulCommClass	—	IsScalarTower.left FiniteType.instMvPolynomialOfFinite Finite.of_fintype FiniteType.of_finitePresentation FinitePresentation.self Module.finitePresentation_of_surjective to_smulCommClass Module.finitePresentation_of_projective Module.Projective.of_free Generators.instFreeCotangentSpaceToExtension Module.Finite.base_change KaehlerDifferential.finite EssFiniteType.of_finiteType Extension.toKaehler_surjective RingHomSurjective.ids LinearMap.exact_iff Extension.exact_cotangentComplex_toKaehler Submodule.map_top Submodule.FG.map Module.Finite.fg_top Extension.Cotangent.finite Presentation.fg_ker

Algebra.Extension

Definitions

Name	Category	Theorems
CotangentSpace 📖	CompOp	54 math math: Algebra.Presentation.differentials.comm₁₂_single, H1Cotangent.equiv_apply, Algebra.Generators.cotangentSpaceBasis_apply, Algebra.Presentation.differentials.comm₂₃, formallySmooth_iff_split_injection, CotangentSpace.map_id, lTensor_cotangentComplex_eq_cotangentComplexBaseChange, Algebra.Generators.cotangentSpaceBasis_repr_one_tmul, subsingleton_h1Cotangent, CotangentSpace.map_tmul, H1Cotangent.val_zero, Algebra.FormallySmooth.iff_injective_lTensor_residueField, Algebra.Generators.CotangentSpace.compEquiv_symm_zero, Algebra.Generators.cotangentSpaceBasis_repr_tmul, Hom.sub_one_tmul, Algebra.Generators.H1Cotangent.δAux_toAlgHom, CotangentSpace.map_toInfinitesimal_bijective, Algebra.SubmersivePresentation.sectionCotangent_eq_iff, CotangentSpace.map_sub_map, CotangentSpace.map_cotangentComplex, cotangentComplexBaseChange_eq_lTensor_cotangentComplex, Algebra.Generators.H1Cotangent.δAux_ofComp, Algebra.Presentation.differentials.comm₂₃', h1Cotangentι_ext_iff, Algebra.Generators.toKaehler_tmul_D, H1Cotangent.val_add, H1Cotangent.val_smul, Algebra.Presentation.differentials.comm₁₂, toKaehler_surjective, Algebra.Generators.disjoint_ker_toKaehler_of_linearIndependent, Algebra.Generators.CotangentSpace.exact, Algebra.Generators.repr_CotangentSpaceMap, H1Cotangent.map_apply_coe, Algebra.Generators.toKaehler_cotangentSpaceBasis, Algebra.Generators.CotangentSpace.compEquiv_symm_inr, h1Cotangentι_apply, cotangentComplex_injective_iff, Algebra.Generators.CotangentSpace.map_toComp_injective, Hom.sub_tmul, Algebra.SubmersivePresentation.sectionCotangent_comp, Algebra.SubmersivePresentation.sectionCotangent_zero_of_notMem_range, Algebra.Generators.instFreeCotangentSpaceToExtension, Algebra.Generators.CotangentSpace.fst_compEquiv_apply, Algebra.SubmersivePresentation.cotangentComplex_injective, CotangentSpace.map_comp, exact_cotangentComplex_toKaehler, Algebra.Generators.CotangentSpace.map_ofComp_surjective, Algebra.Generators.H1Cotangent.map_comp_cotangentComplex_baseChange, Algebra.Generators.CotangentSpace.fst_compEquiv, CotangentSpace.map_comp_apply, Algebra.Generators.H1Cotangent.equiv_apply, CotangentSpace.map_comp_cotangentComplex, Cotangent.map_sub_map, cotangentComplex_mk
H1Cotangent 📖	CompOp	24 math math: H1Cotangent.equiv_apply, H1Cotangent.map_id, h1Cotangentι_injective, instIsScalarTowerH1CotangentOfCotangent, subsingleton_h1Cotangent, H1Cotangent.val_zero, Algebra.Generators.H1Cotangent.exact_map_δ, Algebra.Generators.H1Cotangent.exact_δ_map, H1Cotangent.equivOfFormallySmooth_apply, Algebra.SubmersivePresentation.subsingleton_h1Cotangent, H1Cotangent.equivOfFormallySmooth_symm, H1Cotangent.val_add, H1Cotangent.val_smul, Algebra.Generators.H1Cotangent.δ_eq, Algebra.Generators.H1Cotangent.exact_map_δ', H1Cotangent.map_apply_coe, h1Cotangentι_apply, Algebra.Generators.H1Cotangent.δ_eq_δAux, H1Cotangent.equivOfFormallySmooth_toLinearMap, Algebra.Generators.H1Cotangent.δ_comp_equiv, Algebra.Generators.H1Cotangent.equiv_apply, Algebra.Generators.H1Cotangent.δ_map, H1Cotangent.map_comp, H1Cotangent.map_toInfinitesimal_bijective
cotangentComplex 📖	CompOp	25 math math: Algebra.Presentation.differentials.comm₁₂_single, H1Cotangent.equiv_apply, formallySmooth_iff_split_injection, lTensor_cotangentComplex_eq_cotangentComplexBaseChange, subsingleton_h1Cotangent, H1Cotangent.val_zero, Algebra.FormallySmooth.iff_injective_lTensor_residueField, CotangentSpace.map_sub_map, CotangentSpace.map_cotangentComplex, cotangentComplexBaseChange_eq_lTensor_cotangentComplex, h1Cotangentι_ext_iff, H1Cotangent.val_add, H1Cotangent.val_smul, Algebra.Presentation.differentials.comm₁₂, H1Cotangent.map_apply_coe, h1Cotangentι_apply, cotangentComplex_injective_iff, Algebra.SubmersivePresentation.sectionCotangent_comp, Algebra.SubmersivePresentation.cotangentComplex_injective, exact_cotangentComplex_toKaehler, Algebra.Generators.H1Cotangent.map_comp_cotangentComplex_baseChange, Algebra.Generators.H1Cotangent.equiv_apply, CotangentSpace.map_comp_cotangentComplex, Cotangent.map_sub_map, cotangentComplex_mk
h1Cotangentι 📖	CompOp	2 math math: h1Cotangentι_injective, h1Cotangentι_apply
instAddCommGroupH1Cotangent 📖	CompOp	29 math math: H1Cotangent.equiv_apply, H1Cotangent.map_id, h1Cotangentι_injective, instIsScalarTowerH1CotangentOfCotangent, H1Cotangent.val_zero, Algebra.Generators.H1Cotangent.exact_map_δ, Algebra.Generators.H1Cotangent.exact_δ_map, Algebra.instFiniteH1CotangentOfFinitePresentationOfProjectiveKaehlerDifferential, H1Cotangent.equivOfFormallySmooth_apply, H1Cotangent.equivOfFormallySmooth_symm, H1Cotangent.val_add, H1Cotangent.val_smul, Algebra.Generators.H1Cotangent.δ_eq, Algebra.Generators.H1Cotangent.exact_map_δ', H1Cotangent.map_apply_coe, h1Cotangentι_apply, Algebra.H1Cotangent.isLocalizedModule, Algebra.Generators.H1Cotangent.δ_eq_δAux, Algebra.tensorH1CotangentOfIsLocalization_toLinearMap, H1Cotangent.equivOfFormallySmooth_toLinearMap, Algebra.H1Cotangent.exact_map_δ, Algebra.Generators.H1Cotangent.δ_comp_equiv, Algebra.smoothLocus_eq_compl_support_inter, Algebra.Generators.H1Cotangent.equiv_apply, Algebra.H1Cotangent.exact_δ_mapBaseChange, Algebra.Generators.H1Cotangent.δ_map, Algebra.etaleLocus_eq_compl_support, H1Cotangent.map_comp, H1Cotangent.map_toInfinitesimal_bijective
instModuleH1CotangentOfIsScalarTowerCotangent 📖	CompOp	27 math math: H1Cotangent.equiv_apply, H1Cotangent.map_id, h1Cotangentι_injective, instIsScalarTowerH1CotangentOfCotangent, Algebra.Generators.H1Cotangent.exact_map_δ, Algebra.Generators.H1Cotangent.exact_δ_map, Algebra.instFiniteH1CotangentOfFinitePresentationOfProjectiveKaehlerDifferential, H1Cotangent.equivOfFormallySmooth_apply, H1Cotangent.equivOfFormallySmooth_symm, H1Cotangent.val_smul, Algebra.Generators.H1Cotangent.δ_eq, Algebra.Generators.H1Cotangent.exact_map_δ', H1Cotangent.map_apply_coe, h1Cotangentι_apply, Algebra.H1Cotangent.isLocalizedModule, Algebra.Generators.H1Cotangent.δ_eq_δAux, Algebra.tensorH1CotangentOfIsLocalization_toLinearMap, H1Cotangent.equivOfFormallySmooth_toLinearMap, Algebra.H1Cotangent.exact_map_δ, Algebra.Generators.H1Cotangent.δ_comp_equiv, Algebra.smoothLocus_eq_compl_support_inter, Algebra.Generators.H1Cotangent.equiv_apply, Algebra.H1Cotangent.exact_δ_mapBaseChange, Algebra.Generators.H1Cotangent.δ_map, Algebra.etaleLocus_eq_compl_support, H1Cotangent.map_comp, H1Cotangent.map_toInfinitesimal_bijective
toKaehler 📖	CompOp	9 math math: Algebra.Presentation.differentials.comm₂₃, Algebra.Generators.H1Cotangent.δAux_ofComp, Algebra.Presentation.differentials.comm₂₃', Algebra.Generators.toKaehler_tmul_D, Algebra.Generators.H1Cotangent.δ_eq, toKaehler_surjective, Algebra.Generators.disjoint_ker_toKaehler_of_linearIndependent, Algebra.Generators.toKaehler_cotangentSpaceBasis, exact_cotangentComplex_toKaehler

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
cotangentComplexBaseChange_eq_lTensor_cotangentComplex 📖	mathematical	—	KaehlerDifferential.cotangentComplexBaseChange Ring commRing algebra₂ instRingOfIsScalarTower Algebra.id CommRing.toCommSemiring IsScalarTower.left MonoidWithZero.toMonoid Semiring.toMonoidWithZero CommSemiring.toSemiring DistribMulAction.toMulAction AddCommMonoid.toAddMonoid NonUnitalNonAssocSemiring.toAddCommMonoid NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing Module.toDistribMulAction Algebra.toModule LinearMap.comp TensorProduct Ideal SetLike.instMembership Submodule.setLike NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring Semiring.toModule RingHom.ker RingHom RingHom.instFunLike RingHom.instRingHomClass algebraMap Submodule.addCommMonoid Submodule.module CotangentSpace TensorProduct.addCommMonoid KaehlerDifferential AddCommGroup.toAddCommMonoid instAddCommGroupKaehlerDifferential KaehlerDifferential.module' TensorProduct.leftModule Algebra.to_smulCommClass RingHom.id RingHomCompTriple.ids LinearEquiv.toLinearMap RingHomInvPair.ids IsScalarTower.to_smulCommClass IsScalarTower.right TensorProduct.AlgebraTensorModule.cancelBaseChange Cotangent instAddCommGroupCotangent instModuleCotangent LinearMap.baseChange cotangentComplex ker LinearEquiv.trans LinearEquiv.symm LinearEquiv.baseChange cotangentEquiv	—	TensorProduct.AlgebraTensorModule.curry_injective RingHom.instRingHomClass IsScalarTower.left Algebra.to_smulCommClass IsScalarTower.right TensorProduct.isScalarTower_left RingHomCompTriple.ids RingHomInvPair.ids IsScalarTower.to_smulCommClass LinearMap.ext_ring LinearMap.ext smulCommClass_self one_smul
cotangentComplex_mk 📖	mathematical	—	DFunLike.coe LinearMap CommSemiring.toSemiring CommRing.toCommSemiring RingHom.id Semiring.toNonAssocSemiring Cotangent CotangentSpace AddCommGroup.toAddCommMonoid instAddCommGroupCotangent TensorProduct.addCommMonoid Ring commRing KaehlerDifferential instRingOfIsScalarTower Algebra.id NonUnitalNonAssocSemiring.toAddCommMonoid NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing instAddCommGroupKaehlerDifferential Algebra.toModule algebra₂ KaehlerDifferential.module' instModuleCotangent TensorProduct.leftModule Semiring.toModule Algebra.to_smulCommClass LinearMap.instFunLike cotangentComplex Ideal SetLike.instMembership Submodule.setLike NonAssocSemiring.toNonUnitalNonAssocSemiring ker Submodule.addCommMonoid Submodule.module TensorProduct.tmul AddMonoidWithOne.toOne AddGroupWithOne.toAddMonoidWithOne Ring.toAddGroupWithOne CommRing.toRing Derivation smulCommClass_self CommRing.toCommMonoid DistribMulAction.toMulAction CommMonoid.toMonoid AddCommMonoid.toAddMonoid Module.toDistribMulAction Ring.toSemiring Derivation.instFunLike KaehlerDifferential.D	—	Algebra.to_smulCommClass
exact_cotangentComplex_toKaehler 📖	mathematical	—	Function.Exact Cotangent CotangentSpace KaehlerDifferential DFunLike.coe LinearMap CommSemiring.toSemiring CommRing.toCommSemiring RingHom.id Semiring.toNonAssocSemiring AddCommGroup.toAddCommMonoid instAddCommGroupCotangent TensorProduct.addCommMonoid Ring commRing instRingOfIsScalarTower Algebra.id NonUnitalNonAssocSemiring.toAddCommMonoid NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing instAddCommGroupKaehlerDifferential Algebra.toModule algebra₂ KaehlerDifferential.module' instModuleCotangent TensorProduct.leftModule Semiring.toModule Algebra.to_smulCommClass LinearMap.instFunLike cotangentComplex toKaehler NegZeroClass.toZero SubNegZeroMonoid.toNegZeroClass SubtractionMonoid.toSubNegZeroMonoid SubtractionCommMonoid.toSubtractionMonoid AddCommGroup.toDivisionAddCommMonoid	—	KaehlerDifferential.exact_kerCotangentToTensor_mapBaseChange algebraMap_surjective
h1Cotangentι_apply 📖	mathematical	—	DFunLike.coe LinearMap CommSemiring.toSemiring CommRing.toCommSemiring RingHom.id Semiring.toNonAssocSemiring H1Cotangent Cotangent AddCommGroup.toAddCommMonoid instAddCommGroupH1Cotangent instAddCommGroupCotangent instModuleH1CotangentOfIsScalarTowerCotangent Algebra.id instModuleCotangent instIsScalarTowerCotangent IsScalarTower.right LinearMap.instFunLike h1Cotangentι Submodule SetLike.instMembership Submodule.setLike LinearMap.ker CotangentSpace TensorProduct.addCommMonoid Ring commRing KaehlerDifferential instRingOfIsScalarTower NonUnitalNonAssocSemiring.toAddCommMonoid NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing instAddCommGroupKaehlerDifferential Algebra.toModule algebra₂ KaehlerDifferential.module' TensorProduct.leftModule Semiring.toModule cotangentComplex	—	instIsScalarTowerCotangent IsScalarTower.right
h1Cotangentι_ext 📖	—	Cotangent Submodule CommSemiring.toSemiring CommRing.toCommSemiring AddCommGroup.toAddCommMonoid instAddCommGroupCotangent instModuleCotangent Algebra.id SetLike.instMembership Submodule.setLike LinearMap.ker CotangentSpace TensorProduct.addCommMonoid Ring commRing KaehlerDifferential instRingOfIsScalarTower NonUnitalNonAssocSemiring.toAddCommMonoid NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing instAddCommGroupKaehlerDifferential Algebra.toModule algebra₂ KaehlerDifferential.module' TensorProduct.leftModule Semiring.toModule RingHom.id Semiring.toNonAssocSemiring cotangentComplex	—	—	—
h1Cotangentι_ext_iff 📖	mathematical	—	Cotangent Submodule CommSemiring.toSemiring CommRing.toCommSemiring AddCommGroup.toAddCommMonoid instAddCommGroupCotangent instModuleCotangent Algebra.id SetLike.instMembership Submodule.setLike LinearMap.ker CotangentSpace TensorProduct.addCommMonoid Ring commRing KaehlerDifferential instRingOfIsScalarTower NonUnitalNonAssocSemiring.toAddCommMonoid NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing instAddCommGroupKaehlerDifferential Algebra.toModule algebra₂ KaehlerDifferential.module' TensorProduct.leftModule Semiring.toModule RingHom.id Semiring.toNonAssocSemiring cotangentComplex	—	h1Cotangentι_ext
h1Cotangentι_injective 📖	mathematical	—	H1Cotangent Cotangent DFunLike.coe LinearMap CommSemiring.toSemiring CommRing.toCommSemiring RingHom.id Semiring.toNonAssocSemiring AddCommGroup.toAddCommMonoid instAddCommGroupH1Cotangent instAddCommGroupCotangent instModuleH1CotangentOfIsScalarTowerCotangent Algebra.id instModuleCotangent instIsScalarTowerCotangent IsScalarTower.right LinearMap.instFunLike h1Cotangentι	—	Subtype.val_injective
instIsScalarTowerH1CotangentOfCotangent 📖	mathematical	—	IsScalarTower H1Cotangent Algebra.toSMul CommRing.toCommSemiring CommSemiring.toSemiring SMulZeroClass.toSMul AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass SubNegMonoid.toAddMonoid AddGroup.toSubNegMonoid AddCommGroup.toAddGroup instAddCommGroupH1Cotangent DistribSMul.toSMulZeroClass DistribMulAction.toDistribSMul MonoidWithZero.toMonoid Semiring.toMonoidWithZero Module.toDistribMulAction AddCommGroup.toAddCommMonoid instModuleH1CotangentOfIsScalarTowerCotangent	—	Submodule.isScalarTower'
lTensor_cotangentComplex_eq_cotangentComplexBaseChange 📖	mathematical	—	LinearMap.baseChange Cotangent CotangentSpace CommRing.toCommSemiring CommSemiring.toSemiring AddCommGroup.toAddCommMonoid instAddCommGroupCotangent TensorProduct.addCommMonoid Ring commRing KaehlerDifferential instRingOfIsScalarTower Algebra.id NonUnitalNonAssocSemiring.toAddCommMonoid NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing instAddCommGroupKaehlerDifferential Algebra.toModule algebra₂ KaehlerDifferential.module' instModuleCotangent TensorProduct.leftModule Semiring.toModule Algebra.to_smulCommClass cotangentComplex LinearMap.comp TensorProduct NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring IsScalarTower.left MonoidWithZero.toMonoid Semiring.toMonoidWithZero DistribMulAction.toMulAction AddCommMonoid.toAddMonoid Module.toDistribMulAction RingHom.id RingHomCompTriple.ids LinearEquiv.toLinearMap RingHomInvPair.ids IsScalarTower.to_smulCommClass IsScalarTower.right LinearEquiv.symm TensorProduct.AlgebraTensorModule.cancelBaseChange Ideal SetLike.instMembership Submodule.setLike RingHom.ker RingHom RingHom.instFunLike RingHom.instRingHomClass algebraMap Submodule.addCommMonoid Submodule.module KaehlerDifferential.cotangentComplexBaseChange ker LinearEquiv.trans LinearEquiv.baseChange cotangentEquiv	—	LinearMap.coe_injective Algebra.to_smulCommClass IsScalarTower.left RingHomCompTriple.ids RingHomInvPair.ids IsScalarTower.to_smulCommClass IsScalarTower.right RingHom.instRingHomClass LinearEquiv.eq_symm_comp LinearEquiv.comp_symm_eq cotangentComplexBaseChange_eq_lTensor_cotangentComplex
subsingleton_h1Cotangent 📖	mathematical	—	H1Cotangent Cotangent CotangentSpace DFunLike.coe LinearMap CommSemiring.toSemiring CommRing.toCommSemiring RingHom.id Semiring.toNonAssocSemiring AddCommGroup.toAddCommMonoid instAddCommGroupCotangent TensorProduct.addCommMonoid Ring commRing KaehlerDifferential instRingOfIsScalarTower Algebra.id NonUnitalNonAssocSemiring.toAddCommMonoid NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing instAddCommGroupKaehlerDifferential Algebra.toModule algebra₂ KaehlerDifferential.module' instModuleCotangent TensorProduct.leftModule Semiring.toModule Algebra.to_smulCommClass LinearMap.instFunLike cotangentComplex	—	Algebra.to_smulCommClass LinearMap.ker_eq_bot Submodule.eq_bot_iff Subtype.forall'
toKaehler_surjective 📖	mathematical	—	CotangentSpace KaehlerDifferential DFunLike.coe LinearMap CommSemiring.toSemiring CommRing.toCommSemiring RingHom.id Semiring.toNonAssocSemiring TensorProduct.addCommMonoid Ring commRing instRingOfIsScalarTower Algebra.id NonUnitalNonAssocSemiring.toAddCommMonoid NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing AddCommGroup.toAddCommMonoid instAddCommGroupKaehlerDifferential Algebra.toModule algebra₂ KaehlerDifferential.module' TensorProduct.leftModule Semiring.toModule Algebra.to_smulCommClass LinearMap.instFunLike toKaehler	—	KaehlerDifferential.mapBaseChange_surjective algebraMap_surjective

Algebra.Extension.Cotangent

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
map_sub_map 📖	mathematical	—	LinearMap CommSemiring.toSemiring CommRing.toCommSemiring RingHom.id Semiring.toNonAssocSemiring Algebra.Extension.Cotangent AddCommGroup.toAddCommMonoid Algebra.Extension.instAddCommGroupCotangent Algebra.Extension.instModuleCotangent Algebra.id LinearMap.instSub map LinearMap.comp 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.to_smulCommClass RingHomCompTriple.ids Algebra.Extension.Hom.sub Algebra.Extension.cotangentComplex	—	LinearMap.ext Algebra.to_smulCommClass RingHomCompTriple.ids ext mk_surjective IsScalarTower.left IsScalarTower.right smulCommClass_self Algebra.Extension.Hom.sub_tmul one_smul LinearEquiv.injective RingHomInvPair.ids Ideal.instIsTwoSided_1 map_sub DistribMulActionSemiHomClass.toAddMonoidHomClass SemilinearMapClass.distribMulActionSemiHomClass SemilinearEquivClass.instSemilinearMapClass LinearEquiv.instSemilinearEquivClass LinearMap.semilinearMapClass

Algebra.Extension.CotangentSpace

Definitions

Name	Category	Theorems
map 📖	CompOp	17 math math: map_id, map_tmul, Algebra.Generators.CotangentSpace.compEquiv_symm_zero, map_toInfinitesimal_bijective, map_sub_map, map_cotangentComplex, Algebra.Generators.CotangentSpace.exact, Algebra.Generators.repr_CotangentSpaceMap, Algebra.Generators.CotangentSpace.compEquiv_symm_inr, Algebra.Generators.CotangentSpace.map_toComp_injective, Algebra.Generators.CotangentSpace.fst_compEquiv_apply, map_comp, Algebra.Generators.CotangentSpace.map_ofComp_surjective, Algebra.Generators.H1Cotangent.map_comp_cotangentComplex_baseChange, Algebra.Generators.CotangentSpace.fst_compEquiv, map_comp_apply, map_comp_cotangentComplex

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
map_comp 📖	mathematical	—	map Algebra.Extension.Hom.comp LinearMap.comp Algebra.Extension.CotangentSpace CommSemiring.toSemiring CommRing.toCommSemiring 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 RingHom.id Semiring.toNonAssocSemiring RingHomCompTriple.ids LinearMap.restrictScalars LinearMap.IsScalarTower.compatibleSMul Algebra.toSMul TensorProduct.isScalarTower_left	—	LinearMap.ext Algebra.to_smulCommClass SMulCommClass.of_commMonoid IsScalarTower.right RingHomCompTriple.ids LinearMap.IsScalarTower.compatibleSMul TensorProduct.isScalarTower_left TensorProduct.induction_on map_zero AddMonoidHomClass.toZeroHomClass DistribMulActionSemiHomClass.toAddMonoidHomClass SemilinearMapClass.distribMulActionSemiHomClass LinearMap.semilinearMapClass smulCommClass_self KaehlerDifferential.isScalarTower_of_tower KaehlerDifferential.tensorProductTo_surjective TensorProduct.tmul_zero IsScalarTower.left TensorProduct.tmul_smul TensorProduct.CompatibleSMul.isScalarTower map_tmul IsScalarTower.algebraMap_apply map_add SemilinearMapClass.toAddHomClass TensorProduct.tmul_add
map_comp_apply 📖	mathematical	—	DFunLike.coe LinearMap CommSemiring.toSemiring CommRing.toCommSemiring RingHom.id Semiring.toNonAssocSemiring Algebra.Extension.CotangentSpace 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 map Algebra.Extension.Hom.comp	—	DFunLike.congr_fun Algebra.to_smulCommClass SMulCommClass.of_commMonoid IsScalarTower.right RingHomCompTriple.ids LinearMap.IsScalarTower.compatibleSMul TensorProduct.isScalarTower_left map_comp
map_comp_cotangentComplex 📖	mathematical	—	LinearMap.comp Algebra.Extension.Cotangent Algebra.Extension.CotangentSpace CommSemiring.toSemiring CommRing.toCommSemiring 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 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 RingHom.id Semiring.toNonAssocSemiring RingHomCompTriple.ids map Algebra.Extension.cotangentComplex LinearMap.restrictScalars LinearMap.IsScalarTower.compatibleSMul Algebra.toSMul Algebra.Extension.instIsScalarTowerCotangent TensorProduct.isScalarTower_left Algebra.Extension.Cotangent.map	—	LinearMap.ext SMulCommClass.of_commMonoid IsScalarTower.right Algebra.to_smulCommClass RingHomCompTriple.ids LinearMap.IsScalarTower.compatibleSMul Algebra.Extension.instIsScalarTowerCotangent TensorProduct.isScalarTower_left map_cotangentComplex
map_cotangentComplex 📖	mathematical	—	DFunLike.coe LinearMap CommSemiring.toSemiring CommRing.toCommSemiring RingHom.id Semiring.toNonAssocSemiring Algebra.Extension.CotangentSpace 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 map Algebra.Extension.Cotangent Algebra.Extension.instAddCommGroupCotangent Algebra.Extension.instModuleCotangent Algebra.Extension.cotangentComplex Algebra.Extension.Cotangent.map	—	Algebra.to_smulCommClass SMulCommClass.of_commMonoid IsScalarTower.right Algebra.Extension.Cotangent.mk_surjective smulCommClass_self IsScalarTower.left map_tmul map_one MonoidHomClass.toOneHomClass MonoidWithZeroHomClass.toMonoidHomClass RingHomClass.toMonoidWithZeroHomClass RingHom.instRingHomClass
map_id 📖	mathematical	—	map Algebra.id CommRing.toCommSemiring IsScalarTower.left MonoidWithZero.toMonoid Semiring.toMonoidWithZero CommSemiring.toSemiring DistribMulAction.toMulAction AddCommMonoid.toAddMonoid NonUnitalNonAssocSemiring.toAddCommMonoid NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing Module.toDistribMulAction Algebra.toModule Algebra.Extension.Hom.id LinearMap.id Algebra.Extension.CotangentSpace TensorProduct.addCommMonoid Algebra.Extension.Ring Algebra.Extension.commRing KaehlerDifferential Algebra.Extension.instRingOfIsScalarTower AddCommGroup.toAddCommMonoid instAddCommGroupKaehlerDifferential Algebra.Extension.algebra₂ KaehlerDifferential.module' TensorProduct.leftModule Semiring.toModule Algebra.to_smulCommClass	—	TensorProduct.AlgebraTensorModule.curry_injective IsScalarTower.right SMulCommClass.of_commMonoid TensorProduct.isScalarTower_left IsScalarTower.left Algebra.to_smulCommClass LinearMap.ext_ring IsScalarTower.to_smulCommClass Derivation.liftKaehlerDifferential_unique TensorProduct.isScalarTower Algebra.Extension.instIsScalarTowerRing_2 Derivation.ext smulCommClass_self KaehlerDifferential.isScalarTower_of_tower map_tmul Algebra.Extension.Hom.toAlgHom_id
map_sub_map 📖	mathematical	—	LinearMap CommSemiring.toSemiring CommRing.toCommSemiring RingHom.id Semiring.toNonAssocSemiring Algebra.Extension.CotangentSpace 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.instSub TensorProduct.addCommGroup Ring.toAddCommGroup CommRing.toRing map LinearMap.comp Algebra.Extension.Cotangent Algebra.Extension.instAddCommGroupCotangent Algebra.Extension.instModuleCotangent RingHomCompTriple.ids LinearMap.restrictScalars LinearMap.IsScalarTower.compatibleSMul Algebra.toSMul Algebra.Extension.instIsScalarTowerCotangent TensorProduct.isScalarTower_left Algebra.Extension.cotangentComplex Algebra.Extension.Hom.sub	—	LinearMap.ext Algebra.to_smulCommClass SMulCommClass.of_commMonoid IsScalarTower.right RingHomCompTriple.ids LinearMap.IsScalarTower.compatibleSMul Algebra.Extension.instIsScalarTowerCotangent TensorProduct.isScalarTower_left TensorProduct.induction_on map_zero AddMonoidHomClass.toZeroHomClass DistribMulActionSemiHomClass.toAddMonoidHomClass SemilinearMapClass.distribMulActionSemiHomClass LinearMap.semilinearMapClass smulCommClass_self KaehlerDifferential.isScalarTower_of_tower KaehlerDifferential.tensorProductTo_surjective TensorProduct.tmul_zero TensorProduct.tmul_smul TensorProduct.CompatibleSMul.isScalarTower IsScalarTower.left map_tmul Algebra.Extension.Hom.sub_tmul LinearMap.map_smul_of_tower map_sub Derivation.instAddMonoidHomClass TensorProduct.tmul_sub smul_sub map_add SemilinearMapClass.toAddHomClass TensorProduct.tmul_add
map_tmul 📖	mathematical	—	DFunLike.coe LinearMap CommSemiring.toSemiring CommRing.toCommSemiring RingHom.id Semiring.toNonAssocSemiring Algebra.Extension.CotangentSpace 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 map TensorProduct.tmul Derivation smulCommClass_self DistribMulAction.toMulAction CommMonoid.toMonoid Ring.toSemiring CommRing.toRing Derivation.instFunLike KaehlerDifferential.D RingHom RingHom.instFunLike algebraMap AlgHom IsScalarTower.left AlgHom.funLike Algebra.Extension.Hom.toAlgHom	—	Algebra.to_smulCommClass SMulCommClass.of_commMonoid IsScalarTower.right smulCommClass_self IsScalarTower.left AlgHomClass.toRingHomClass AlgHom.algHomClass KaehlerDifferential.map_D TensorProduct.smul_tmul' Algebra.algebraMap_eq_smul_one

Algebra.Extension.H1Cotangent

Definitions

Name	Category	Theorems
equiv 📖	CompOp	1 math math: equiv_apply
map 📖	CompOp	10 math math: map_id, map_eq, Algebra.Generators.H1Cotangent.exact_map_δ, equivOfFormallySmooth_apply, Algebra.Generators.H1Cotangent.exact_map_δ', map_apply_coe, equivOfFormallySmooth_toLinearMap, Algebra.Generators.H1Cotangent.δ_map, map_comp, map_toInfinitesimal_bijective

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
equiv_apply 📖	mathematical	—	DFunLike.coe LinearEquiv CommSemiring.toSemiring CommRing.toCommSemiring RingHom.id Semiring.toNonAssocSemiring RingHomInvPair.ids Algebra.Extension.H1Cotangent AddCommGroup.toAddCommMonoid Algebra.Extension.instAddCommGroupH1Cotangent Algebra.Extension.instModuleH1CotangentOfIsScalarTowerCotangent Algebra.id Algebra.Extension.instModuleCotangent Algebra.Extension.instIsScalarTowerCotangent IsScalarTower.right EquivLike.toFunLike LinearEquiv.instEquivLike equiv Algebra.Extension.Cotangent Submodule Algebra.Extension.instAddCommGroupCotangent SetLike.instMembership Submodule.setLike Submodule.restrictScalars Algebra.toSMul 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 LinearMap LinearMap.instFunLike Algebra.Extension.Cotangent.map	—	RingHomInvPair.ids Algebra.Extension.instIsScalarTowerCotangent IsScalarTower.right
map_apply_coe 📖	mathematical	—	Algebra.Extension.Cotangent Submodule CommSemiring.toSemiring CommRing.toCommSemiring AddCommGroup.toAddCommMonoid Algebra.Extension.instAddCommGroupCotangent Algebra.Extension.instModuleCotangent SetLike.instMembership Submodule.setLike Submodule.restrictScalars Algebra.id Algebra.toSMul 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 Algebra.Extension.H1Cotangent Algebra.Extension.instAddCommGroupH1Cotangent Algebra.Extension.instModuleH1CotangentOfIsScalarTowerCotangent Algebra.Extension.instIsScalarTowerCotangent IsScalarTower.right LinearMap.instFunLike map Algebra.Extension.Cotangent.map	—	Algebra.Extension.instIsScalarTowerCotangent IsScalarTower.right
map_comp 📖	mathematical	—	map Algebra.Extension.Hom.comp LinearMap.comp Algebra.Extension.H1Cotangent CommSemiring.toSemiring CommRing.toCommSemiring AddCommGroup.toAddCommMonoid Algebra.Extension.instAddCommGroupH1Cotangent Algebra.Extension.instModuleH1CotangentOfIsScalarTowerCotangent Algebra.id Algebra.Extension.instModuleCotangent Algebra.Extension.instIsScalarTowerCotangent IsScalarTower.right RingHom.id Semiring.toNonAssocSemiring RingHomCompTriple.ids LinearMap.restrictScalars LinearMap.IsScalarTower.compatibleSMul SMulZeroClass.toSMul AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass AddCommMonoid.toAddMonoid DistribSMul.toSMulZeroClass DistribMulAction.toDistribSMul MonoidWithZero.toMonoid Semiring.toMonoidWithZero Module.toDistribMulAction Algebra.toSMul Algebra.Extension.instIsScalarTowerH1CotangentOfCotangent	—	LinearMap.ext Algebra.Extension.instIsScalarTowerCotangent IsScalarTower.right RingHomCompTriple.ids LinearMap.IsScalarTower.compatibleSMul Algebra.Extension.instIsScalarTowerH1CotangentOfCotangent Algebra.Extension.h1Cotangentι_ext Algebra.Extension.Cotangent.ext Algebra.Extension.Cotangent.map_comp
map_eq 📖	mathematical	—	map	—	LinearMap.ext Algebra.Extension.instIsScalarTowerCotangent IsScalarTower.right Algebra.Extension.h1Cotangentι_ext Algebra.Extension.Cotangent.ext sub_eq_zero Algebra.Extension.Cotangent.val_sub LinearMap.sub_apply Algebra.to_smulCommClass RingHomCompTriple.ids Algebra.Extension.Cotangent.map_sub_map LinearMap.map_coe_ker map_zero AddMonoidHomClass.toZeroHomClass DistribMulActionSemiHomClass.toAddMonoidHomClass SemilinearMapClass.distribMulActionSemiHomClass LinearMap.semilinearMapClass
map_id 📖	mathematical	—	map Algebra.id CommRing.toCommSemiring IsScalarTower.left MonoidWithZero.toMonoid Semiring.toMonoidWithZero CommSemiring.toSemiring DistribMulAction.toMulAction AddCommMonoid.toAddMonoid NonUnitalNonAssocSemiring.toAddCommMonoid NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing Module.toDistribMulAction Algebra.toModule Algebra.Extension.Hom.id LinearMap.id Algebra.Extension.H1Cotangent AddCommGroup.toAddCommMonoid Algebra.Extension.instAddCommGroupH1Cotangent Algebra.Extension.instModuleH1CotangentOfIsScalarTowerCotangent Algebra.Extension.instModuleCotangent Algebra.Extension.instIsScalarTowerCotangent IsScalarTower.right	—	LinearMap.ext Algebra.Extension.instIsScalarTowerCotangent IsScalarTower.right IsScalarTower.left Algebra.Extension.h1Cotangentι_ext Algebra.Extension.Cotangent.ext Algebra.Extension.Cotangent.map_id
val_add 📖	mathematical	—	Algebra.Extension.Cotangent 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 Algebra.Extension.H1Cotangent AddCommMagma.toAdd AddCommSemigroup.toAddCommMagma AddCommMonoid.toAddCommSemigroup Algebra.Extension.instAddCommGroupH1Cotangent	—	—
val_smul 📖	mathematical	—	Algebra.Extension.Cotangent 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 Algebra.Extension.H1Cotangent SMulZeroClass.toSMul AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass SubNegMonoid.toAddMonoid AddGroup.toSubNegMonoid AddCommGroup.toAddGroup Algebra.Extension.instAddCommGroupH1Cotangent DistribSMul.toSMulZeroClass DistribMulAction.toDistribSMul MonoidWithZero.toMonoid Semiring.toMonoidWithZero Module.toDistribMulAction Algebra.Extension.instModuleH1CotangentOfIsScalarTowerCotangent	—	—
val_zero 📖	mathematical	—	Algebra.Extension.Cotangent 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 Algebra.Extension.H1Cotangent NegZeroClass.toZero SubNegZeroMonoid.toNegZeroClass SubtractionMonoid.toSubNegZeroMonoid SubtractionCommMonoid.toSubtractionMonoid AddCommGroup.toDivisionAddCommMonoid Algebra.Extension.instAddCommGroupH1Cotangent	—	—

Algebra.Extension.Hom

Definitions

Name	Category	Theorems
sub 📖	CompOp	4 math math: sub_one_tmul, Algebra.Extension.CotangentSpace.map_sub_map, sub_tmul, Algebra.Extension.Cotangent.map_sub_map
subToKer 📖	CompOp	3 math math: sub_one_tmul, subToKer_apply_coe, sub_tmul

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
subToKer_apply_coe 📖	mathematical	—	Algebra.Extension.Ring Submodule CommSemiring.toSemiring CommRing.toCommSemiring NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring Algebra.Extension.commRing Algebra.toModule Algebra.Extension.instRingOfIsScalarTower SetLike.instMembership Submodule.setLike Submodule.restrictScalars Semiring.toModule Algebra.toSMul Algebra.Extension.ker DFunLike.coe LinearMap RingHom.id Ideal NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing Submodule.addCommMonoid Algebra.id IsScalarTower.left MonoidWithZero.toMonoid Semiring.toMonoidWithZero DistribMulAction.toMulAction AddCommMonoid.toAddMonoid Module.toDistribMulAction Submodule.module' IsScalarTower.right LinearMap.instFunLike subToKer SubNegMonoid.toSub AddGroup.toSubNegMonoid AddCommGroup.toAddGroup Ring.toAddCommGroup CommRing.toRing RingHom RingHom.instFunLike toRingHom	—	IsScalarTower.left IsScalarTower.right
sub_aux 📖	mathematical	—	Algebra.Extension.Ring Ideal CommSemiring.toSemiring CommRing.toCommSemiring Algebra.Extension.commRing SetLike.instMembership Submodule.setLike NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring Semiring.toModule Monoid.toNatPow MonoidWithZero.toMonoid Semiring.toMonoidWithZero IdemSemiring.toSemiring Submodule.idemSemiring Algebra.id Algebra.Extension.ker SubNegMonoid.toSub AddGroup.toSubNegMonoid AddGroupWithOne.toAddGroup Ring.toAddGroupWithOne CommRing.toRing DFunLike.coe AlgHom Algebra.Extension.instRingOfIsScalarTower IsScalarTower.left DistribMulAction.toMulAction AddCommMonoid.toAddMonoid NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing Module.toDistribMulAction Algebra.toModule AlgHom.funLike toAlgHom Distrib.toMul NonUnitalNonAssocSemiring.toDistrib Distrib.toAdd Algebra.Extension.σ RingHom RingHom.instFunLike algebraMap RingHom.toAlgebra RingHom.comp Algebra.Extension.algebra₂	—	IsScalarTower.left pow_two Ideal.add_mem Ideal.mul_mem_mul map_sub RingHomClass.toAddMonoidHomClass RingHom.instRingHomClass algebraMap_toRingHom Algebra.Extension.algebraMap_σ sub_self map_mul NonUnitalAlgSemiHomClass.toMulHomClass AlgHom.instNonUnitalAlgHomClassOfAlgHomClass AlgHom.algHomClass Mathlib.Tactic.Ring.of_eq Mathlib.Tactic.Ring.sub_congr Mathlib.Tactic.Ring.mul_congr Mathlib.Tactic.Ring.atom_pf Mathlib.Tactic.Ring.add_mul Mathlib.Tactic.Ring.mul_add Mathlib.Tactic.Ring.mul_pf_left Mathlib.Tactic.Ring.mul_pf_right Mathlib.Tactic.Ring.one_mul Mathlib.Tactic.Ring.mul_zero Mathlib.Tactic.Ring.add_pf_add_zero Mathlib.Tactic.Ring.zero_mul Mathlib.Tactic.Ring.sub_pf Mathlib.Tactic.Ring.neg_add Mathlib.Tactic.Ring.neg_mul Mathlib.Tactic.Ring.neg_one_mul Mathlib.Meta.NormNum.IsInt.to_raw_eq Mathlib.Meta.NormNum.isInt_mul Mathlib.Meta.NormNum.IsInt.of_raw Mathlib.Meta.NormNum.IsNat.to_isInt Mathlib.Meta.NormNum.IsNat.of_raw Mathlib.Tactic.Ring.neg_zero Mathlib.Tactic.Ring.add_pf_add_lt Mathlib.Tactic.Ring.add_pf_zero_add Mathlib.Tactic.Ring.add_congr Mathlib.Tactic.Ring.add_pf_add_gt Mathlib.Meta.NormNum.IsNat.to_raw_eq Mathlib.Meta.NormNum.IsInt.to_isNat Mathlib.Tactic.Ring.mul_one Mathlib.Tactic.Ring.add_pf_add_overlap_zero Mathlib.Tactic.Ring.add_overlap_pf_zero Mathlib.Meta.NormNum.isInt_add
sub_one_tmul 📖	mathematical	—	DFunLike.coe LinearMap CommSemiring.toSemiring CommRing.toCommSemiring RingHom.id Semiring.toNonAssocSemiring Algebra.Extension.CotangentSpace Algebra.Extension.Cotangent 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' Algebra.Extension.instAddCommGroupCotangent TensorProduct.leftModule Semiring.toModule Algebra.to_smulCommClass Algebra.Extension.instModuleCotangent LinearMap.instFunLike sub TensorProduct.tmul AddMonoidWithOne.toOne AddGroupWithOne.toAddMonoidWithOne Ring.toAddGroupWithOne CommRing.toRing Derivation smulCommClass_self CommRing.toCommMonoid DistribMulAction.toMulAction CommMonoid.toMonoid AddCommMonoid.toAddMonoid Module.toDistribMulAction Ring.toSemiring Derivation.instFunLike KaehlerDifferential.D Ideal SetLike.instMembership Submodule.setLike NonAssocSemiring.toNonUnitalNonAssocSemiring Algebra.Extension.ker Submodule.addCommMonoid Submodule.module IsScalarTower.left MonoidWithZero.toMonoid Semiring.toMonoidWithZero Submodule.module' Algebra.toSMul IsScalarTower.right subToKer	—	Algebra.to_smulCommClass smulCommClass_self IsScalarTower.left IsScalarTower.right Derivation.liftKaehlerDifferential_comp_D one_smul
sub_tmul 📖	mathematical	—	DFunLike.coe LinearMap CommSemiring.toSemiring CommRing.toCommSemiring RingHom.id Semiring.toNonAssocSemiring Algebra.Extension.CotangentSpace Algebra.Extension.Cotangent 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' Algebra.Extension.instAddCommGroupCotangent TensorProduct.leftModule Semiring.toModule Algebra.to_smulCommClass Algebra.Extension.instModuleCotangent LinearMap.instFunLike sub TensorProduct.tmul Derivation smulCommClass_self CommRing.toCommMonoid DistribMulAction.toMulAction CommMonoid.toMonoid AddCommMonoid.toAddMonoid Module.toDistribMulAction Ring.toSemiring CommRing.toRing Derivation.instFunLike KaehlerDifferential.D SMulZeroClass.toSMul AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass SubNegMonoid.toAddMonoid AddGroup.toSubNegMonoid AddCommGroup.toAddGroup DistribSMul.toSMulZeroClass DistribMulAction.toDistribSMul MonoidWithZero.toMonoid Semiring.toMonoidWithZero Ideal SetLike.instMembership Submodule.setLike NonAssocSemiring.toNonUnitalNonAssocSemiring Algebra.Extension.ker Submodule.addCommMonoid Submodule.module IsScalarTower.left Submodule.module' Algebra.toSMul IsScalarTower.right subToKer	—	Algebra.to_smulCommClass smulCommClass_self IsScalarTower.left IsScalarTower.right Derivation.liftKaehlerDifferential_comp_D

Algebra.Generators

Definitions

Name	Category	Theorems
cotangentRestrict 📖	CompOp	3 math math: cotangentRestrict_bijective_of_isCompl, cotangentRestrict_mk, cotangentRestrict_bijective_of_basis_kaehlerDifferential
cotangentSpaceBasis 📖	CompOp	13 math math: Algebra.Presentation.differentials.comm₁₂_single, cotangentSpaceBasis_apply, Algebra.Presentation.differentials.comm₂₃, cotangentSpaceBasis_repr_one_tmul, cotangentSpaceBasis_repr_tmul, H1Cotangent.δAux_toAlgHom, Algebra.SubmersivePresentation.sectionCotangent_eq_iff, Algebra.Presentation.differentials.comm₂₃', Algebra.Presentation.differentials.comm₁₂, disjoint_ker_toKaehler_of_linearIndependent, repr_CotangentSpaceMap, toKaehler_cotangentSpaceBasis, Algebra.SubmersivePresentation.sectionCotangent_zero_of_notMem_range
equivH1Cotangent 📖	CompOp	—

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
cotangentRestrict_mk 📖	mathematical	—	DFunLike.coe Finsupp MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing Finsupp.instFunLike LinearMap CommSemiring.toSemiring CommRing.toCommSemiring RingHom.id Semiring.toNonAssocSemiring Algebra.Extension.Cotangent toExtension AddCommGroup.toAddCommMonoid Algebra.Extension.instAddCommGroupCotangent Finsupp.instAddCommMonoid NonUnitalNonAssocSemiring.toAddCommMonoid Algebra.Extension.instModuleCotangent Algebra.id Finsupp.module Semiring.toModule LinearMap.instFunLike cotangentRestrict Algebra.Extension.Ring Algebra.Extension.commRing Ideal SetLike.instMembership Submodule.setLike NonAssocSemiring.toNonUnitalNonAssocSemiring Algebra.Extension.ker Submodule.addCommMonoid Submodule.module Algebra.Extension.algebra₂ AlgHom MvPolynomial MvPolynomial.commSemiring MvPolynomial.algebra AlgHom.funLike MvPolynomial.aeval val Derivation MvPolynomial.module Derivation.instFunLike MvPolynomial.pderiv Ring ker	—	Algebra.to_smulCommClass smulCommClass_self RingHomInvPair.ids cotangentSpaceBasis_repr_tmul one_mul
cotangentSpaceBasis_apply 📖	mathematical	—	DFunLike.coe Module.Basis Algebra.Extension.CotangentSpace toExtension CommSemiring.toSemiring CommRing.toCommSemiring 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 Module.Basis.instFunLike cotangentSpaceBasis TensorProduct.tmul Ring MvPolynomial.commSemiring MvPolynomial.instCommRingMvPolynomial MvPolynomial.algebra instRing MvPolynomial AddMonoidWithOne.toOne AddGroupWithOne.toAddMonoidWithOne Ring.toAddGroupWithOne CommRing.toRing Derivation smulCommClass_self CommRing.toCommMonoid DistribMulAction.toMulAction CommMonoid.toMonoid AddCommMonoid.toAddMonoid Module.toDistribMulAction Ring.toSemiring Derivation.instFunLike KaehlerDifferential.D MvPolynomial.X	—	Algebra.to_smulCommClass smulCommClass_self Module.Basis.baseChange_apply KaehlerDifferential.mvPolynomialBasis_apply
cotangentSpaceBasis_repr_one_tmul 📖	mathematical	—	DFunLike.coe Finsupp MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring CommSemiring.toSemiring CommRing.toCommSemiring Finsupp.instFunLike LinearEquiv RingHom.id RingHomInvPair.ids Algebra.Extension.CotangentSpace toExtension 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' Finsupp.instAddCommMonoid TensorProduct.leftModule Semiring.toModule Algebra.to_smulCommClass Finsupp.module EquivLike.toFunLike DFinsupp.instEquivLikeLinearEquiv Module.Basis.repr cotangentSpaceBasis TensorProduct.tmul AddMonoidWithOne.toOne AddGroupWithOne.toAddMonoidWithOne Ring.toAddGroupWithOne CommRing.toRing Derivation smulCommClass_self CommRing.toCommMonoid DistribMulAction.toMulAction CommMonoid.toMonoid AddCommMonoid.toAddMonoid Module.toDistribMulAction Ring.toSemiring Derivation.instFunLike KaehlerDifferential.D AlgHom MvPolynomial MvPolynomial.commSemiring MvPolynomial.algebra AlgHom.funLike MvPolynomial.aeval val MvPolynomial.module MvPolynomial.pderiv	—	RingHomInvPair.ids Algebra.to_smulCommClass smulCommClass_self cotangentSpaceBasis_repr_tmul one_mul
cotangentSpaceBasis_repr_tmul 📖	mathematical	—	DFunLike.coe Finsupp MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring CommSemiring.toSemiring CommRing.toCommSemiring Finsupp.instFunLike LinearEquiv RingHom.id RingHomInvPair.ids Algebra.Extension.CotangentSpace toExtension 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' Finsupp.instAddCommMonoid TensorProduct.leftModule Semiring.toModule Algebra.to_smulCommClass Finsupp.module EquivLike.toFunLike DFinsupp.instEquivLikeLinearEquiv Module.Basis.repr cotangentSpaceBasis TensorProduct.tmul Ring MvPolynomial.commSemiring MvPolynomial.instCommRingMvPolynomial MvPolynomial.algebra MvPolynomial Derivation smulCommClass_self CommRing.toCommMonoid DistribMulAction.toMulAction CommMonoid.toMonoid AddCommMonoid.toAddMonoid Module.toDistribMulAction Ring.toSemiring CommRing.toRing Derivation.instFunLike KaehlerDifferential.D Distrib.toMul NonUnitalNonAssocSemiring.toDistrib AlgHom AlgHom.funLike MvPolynomial.aeval val MvPolynomial.module MvPolynomial.pderiv	—	RingHomInvPair.ids Algebra.to_smulCommClass smulCommClass_self Module.Basis.baseChange_repr_tmul KaehlerDifferential.mvPolynomialBasis_repr_apply Algebra.smul_def algebraMap_apply mul_comm
instFreeCotangentSpaceToExtension 📖	mathematical	—	Module.Free Algebra.Extension.CotangentSpace toExtension CommSemiring.toSemiring CommRing.toCommSemiring 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	—	Module.Free.of_basis Algebra.to_smulCommClass
repr_CotangentSpaceMap 📖	mathematical	—	DFunLike.coe Finsupp MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring CommSemiring.toSemiring CommRing.toCommSemiring Finsupp.instFunLike LinearEquiv RingHom.id RingHomInvPair.ids Algebra.Extension.CotangentSpace toExtension 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' Finsupp.instAddCommMonoid TensorProduct.leftModule Semiring.toModule Algebra.to_smulCommClass Finsupp.module EquivLike.toFunLike DFinsupp.instEquivLikeLinearEquiv Module.Basis.repr cotangentSpaceBasis 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 Hom.toExtensionHom Module.Basis Module.Basis.instFunLike AlgHom MvPolynomial MvPolynomial.commSemiring MvPolynomial.algebra AlgHom.funLike MvPolynomial.aeval val Derivation MvPolynomial.module Derivation.instFunLike MvPolynomial.pderiv Hom.val	—	RingHomInvPair.ids Algebra.to_smulCommClass SMulCommClass.of_commMonoid IsScalarTower.right smulCommClass_self cotangentSpaceBasis_apply IsScalarTower.left Algebra.Extension.CotangentSpace.map_tmul map_one MonoidHomClass.toOneHomClass MonoidWithZeroHomClass.toMonoidHomClass RingHomClass.toMonoidWithZeroHomClass RingHom.instRingHomClass cotangentSpaceBasis_repr_one_tmul Hom.toAlgHom_X
toKaehler_cotangentSpaceBasis 📖	mathematical	—	DFunLike.coe LinearMap CommSemiring.toSemiring CommRing.toCommSemiring RingHom.id Semiring.toNonAssocSemiring Algebra.Extension.CotangentSpace toExtension KaehlerDifferential TensorProduct.addCommMonoid Algebra.Extension.Ring Algebra.Extension.commRing 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 LinearMap.instFunLike Algebra.Extension.toKaehler Module.Basis Module.Basis.instFunLike cotangentSpaceBasis Derivation smulCommClass_self CommRing.toCommMonoid DistribMulAction.toMulAction CommMonoid.toMonoid AddCommMonoid.toAddMonoid Module.toDistribMulAction Ring.toSemiring CommRing.toRing Derivation.instFunLike KaehlerDifferential.D val	—	Algebra.to_smulCommClass smulCommClass_self cotangentSpaceBasis_apply toKaehler_tmul_D
toKaehler_tmul_D 📖	mathematical	—	DFunLike.coe LinearMap CommSemiring.toSemiring CommRing.toCommSemiring RingHom.id Semiring.toNonAssocSemiring Algebra.Extension.CotangentSpace toExtension KaehlerDifferential TensorProduct.addCommMonoid Algebra.Extension.Ring Algebra.Extension.commRing 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 LinearMap.instFunLike Algebra.Extension.toKaehler TensorProduct.tmul AddMonoidWithOne.toOne AddGroupWithOne.toAddMonoidWithOne Ring.toAddGroupWithOne CommRing.toRing Derivation Ring MvPolynomial.instCommRingMvPolynomial MvPolynomial.algebra smulCommClass_self CommRing.toCommMonoid DistribMulAction.toMulAction CommMonoid.toMonoid AddCommMonoid.toAddMonoid Module.toDistribMulAction Ring.toSemiring Derivation.instFunLike KaehlerDifferential.D MvPolynomial.X val	—	Algebra.to_smulCommClass smulCommClass_self IsScalarTower.to_smulCommClass IsScalarTower.left KaehlerDifferential.mapBaseChange_tmul KaehlerDifferential.map_D algebraMap_apply MvPolynomial.aeval_X one_smul

Algebra.Generators.H1Cotangent

Definitions

Name	Category	Theorems
equiv 📖	CompOp	2 math math: δ_comp_equiv, equiv_apply

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
equiv_apply 📖	mathematical	—	DFunLike.coe LinearEquiv CommSemiring.toSemiring CommRing.toCommSemiring RingHom.id Semiring.toNonAssocSemiring RingHomInvPair.ids Algebra.Extension.H1Cotangent Algebra.Generators.toExtension AddCommGroup.toAddCommMonoid Algebra.Extension.instAddCommGroupH1Cotangent Algebra.Extension.instModuleH1CotangentOfIsScalarTowerCotangent Algebra.id Algebra.Extension.instModuleCotangent Algebra.Extension.instIsScalarTowerCotangent IsScalarTower.right EquivLike.toFunLike LinearEquiv.instEquivLike equiv Algebra.Extension.Cotangent Submodule Algebra.Extension.instAddCommGroupCotangent SetLike.instMembership Submodule.setLike Submodule.restrictScalars Algebra.toSMul LinearMap.ker Algebra.Extension.CotangentSpace TensorProduct.addCommMonoid Algebra.Generators.Ring MvPolynomial.instCommRingMvPolynomial KaehlerDifferential Algebra.Extension.instRingOfIsScalarTower NonUnitalNonAssocSemiring.toAddCommMonoid NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing instAddCommGroupKaehlerDifferential Algebra.toModule Algebra.Generators.instRing KaehlerDifferential.module' TensorProduct.leftModule Semiring.toModule Algebra.Extension.cotangentComplex LinearMap LinearMap.instFunLike Algebra.Extension.Cotangent.map Algebra.Generators.Hom.toExtensionHom Algebra.Generators.defaultHom Algebra.Extension.Ring Algebra.Extension.commRing Algebra.Extension.algebra₂	—	RingHomInvPair.ids Algebra.Extension.instIsScalarTowerCotangent IsScalarTower.right

Algebra.H1Cotangent

Definitions

Name	Category	Theorems
map 📖	CompOp	3 math math: isLocalizedModule, Algebra.tensorH1CotangentOfIsLocalization_toLinearMap, exact_map_δ
mapEquiv 📖	CompOp	—

KaehlerDifferential

Definitions

Name	Category	Theorems
cotangentComplexBaseChange 📖	CompOp	5 math math: cotangentComplexBaseChange_tmul, Algebra.Extension.lTensor_cotangentComplex_eq_cotangentComplexBaseChange, Algebra.FormallySmooth.iff_injective_cotangentComplexBaseChange_residueField, Algebra.Extension.cotangentComplexBaseChange_eq_lTensor_cotangentComplex, Algebra.FormallySmooth.iff_injective_cotangentComplexBaseChange

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
cotangentComplexBaseChange_tmul 📖	mathematical	—	DFunLike.coe LinearMap CommSemiring.toSemiring CommRing.toCommSemiring RingHom.id Semiring.toNonAssocSemiring TensorProduct Ideal SetLike.instMembership Submodule.setLike NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toModule RingHom.ker RingHom RingHom.instFunLike RingHom.instRingHomClass algebraMap NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing Submodule.addCommMonoid Algebra.toModule Submodule.module KaehlerDifferential AddCommGroup.toAddCommMonoid instAddCommGroupKaehlerDifferential module' Algebra.id Algebra.to_smulCommClass TensorProduct.addCommMonoid TensorProduct.leftModule LinearMap.instFunLike cotangentComplexBaseChange TensorProduct.tmul TensorProduct.leftHasSMul MonoidWithZero.toMonoid Semiring.toMonoidWithZero Module.toDistribMulAction TensorProduct.instModule kerToTensor	—	RingHom.instRingHomClass Algebra.to_smulCommClass

---

← Back to Index