StandardSmoothCotangent

📁 Source: Mathlib/RingTheory/Smooth/StandardSmoothCotangent.lean

Statistics

Metric	Count
Definitions basisCotangentAway, cMulXSubOneCotangent, cotangentComplexAux, basisCotangent, basisKaehler, basisKaehlerOfIsCompl, cotangentEquiv, sectionCotangent	8
Theorems basisCotangentAway_apply, cMulXSubOneCotangent_eq, free_kaehlerDifferential, subsingleton_h1Cotangent, subsingleton_kaehlerDifferential, iff_of_isStandardSmooth, rank_kaehlerDifferential, cotangentComplexAux_apply, cotangentComplexAux_zero_iff, basisCotangent_apply, basisCotangent_localizationAway_apply, basisKaehlerOfIsCompl_apply, basisKaehler_apply, cotangentComplexAux_injective, cotangentComplexAux_surjective, cotangentComplex_injective, cotangentEquiv_apply, free_cotangent, free_kaehlerDifferential, rank_kaehlerDifferential, sectionCotangent_comp, sectionCotangent_eq_iff, sectionCotangent_zero_of_notMem_range, subsingleton_h1Cotangent, instEtaleOfIsStandardSmoothOfRelativeDimensionOfNatNat, instFreeCotangentToExtensionUnitLocalizationAway, instSmoothOfIsStandardSmooth	27
Total	35

Algebra

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
instEtaleOfIsStandardSmoothOfRelativeDimensionOfNatNat 📖	mathematical	—	Etale	—	IsStandardSmoothOfRelativeDimension.isStandardSmooth IsStandardSmoothOfRelationDimension.subsingleton_kaehlerDifferential FormallyEtale.of_formallyUnramified_and_formallySmooth Smooth.formallySmooth instSmoothOfIsStandardSmooth IsStandardSmooth.finitePresentation
instFreeCotangentToExtensionUnitLocalizationAway 📖	mathematical	—	Module.Free Extension.Cotangent Generators.toExtension Generators.localizationAway CommSemiring.toSemiring CommRing.toCommSemiring AddCommGroup.toAddCommMonoid Extension.instAddCommGroupCotangent Extension.instModuleCotangent id	—	Finite.of_fintype SubmersivePresentation.free_cotangent
instSmoothOfIsStandardSmooth 📖	mathematical	—	Smooth	—	to_smulCommClass formallySmooth_iff Module.Projective.of_free IsStandardSmooth.free_kaehlerDifferential IsStandardSmooth.subsingleton_h1Cotangent IsStandardSmooth.finitePresentation

Algebra.Generators

Definitions

Name	Category	Theorems
basisCotangentAway 📖	CompOp	1 math math: basisCotangentAway_apply
cMulXSubOneCotangent 📖	CompOp	4 math math: cotangentCompAwaySec_apply, cMulXSubOneCotangent_eq, Algebra.SubmersivePresentation.basisCotangent_localizationAway_apply, basisCotangentAway_apply

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
basisCotangentAway_apply 📖	mathematical	—	DFunLike.coe Module.Basis Algebra.Extension.Cotangent toExtension localizationAway CommSemiring.toSemiring CommRing.toCommSemiring AddCommGroup.toAddCommMonoid Algebra.Extension.instAddCommGroupCotangent Algebra.Extension.instModuleCotangent Algebra.id Module.Basis.instFunLike basisCotangentAway cMulXSubOneCotangent	—	Algebra.SubmersivePresentation.basisCotangent_apply Finite.of_fintype
cMulXSubOneCotangent_eq 📖	mathematical	—	cMulXSubOneCotangent DFunLike.coe LinearMap Algebra.Extension.Ring toExtension localizationAway CommSemiring.toSemiring CommRing.toCommSemiring Algebra.Extension.commRing RingHom.id Semiring.toNonAssocSemiring Ideal SetLike.instMembership Submodule.setLike NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toModule Algebra.Extension.ker Algebra.Extension.Cotangent Submodule.addCommMonoid AddCommGroup.toAddCommMonoid Algebra.Extension.instAddCommGroupCotangent Submodule.module Algebra.Extension.instModuleCotangent Algebra.Extension.algebra₂ LinearMap.instFunLike MvPolynomial SubNegMonoid.toSub AddGroup.toSubNegMonoid AddGroupWithOne.toAddGroup Ring.toAddGroupWithOne CommRing.toRing MvPolynomial.instCommRingMvPolynomial Distrib.toMul NonUnitalNonAssocSemiring.toDistrib NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing RingHom MvPolynomial.commSemiring RingHom.instFunLike MvPolynomial.C MvPolynomial.X AddMonoidWithOne.toOne AddGroupWithOne.toAddMonoidWithOne C_mul_X_sub_one_mem_ker	—	—

Algebra.IsStandardSmooth

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
free_kaehlerDifferential 📖	mathematical	—	Module.Free KaehlerDifferential CommSemiring.toSemiring CommRing.toCommSemiring AddCommGroup.toAddCommMonoid instAddCommGroupKaehlerDifferential KaehlerDifferential.module' Algebra.id Algebra.to_smulCommClass	—	Algebra.to_smulCommClass Algebra.SubmersivePresentation.free_kaehlerDifferential
subsingleton_h1Cotangent 📖	mathematical	—	Algebra.H1Cotangent	—	Equiv.subsingleton Algebra.Extension.instIsScalarTowerCotangent IsScalarTower.right RingHomInvPair.ids Algebra.SubmersivePresentation.subsingleton_h1Cotangent

Algebra.IsStandardSmoothOfRelationDimension

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
subsingleton_kaehlerDifferential 📖	mathematical	—	KaehlerDifferential	—	subsingleton_or_nontrivial Module.subsingleton Algebra.to_smulCommClass Module.subsingleton_of_rank_zero commRing_strongRankCondition Algebra.IsStandardSmooth.free_kaehlerDifferential Algebra.IsStandardSmoothOfRelativeDimension.isStandardSmooth Algebra.IsStandardSmoothOfRelativeDimension.rank_kaehlerDifferential

Algebra.IsStandardSmoothOfRelativeDimension

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
iff_of_isStandardSmooth 📖	mathematical	—	Algebra.IsStandardSmoothOfRelativeDimension Module.rank KaehlerDifferential CommSemiring.toSemiring CommRing.toCommSemiring AddCommGroup.toAddCommMonoid instAddCommGroupKaehlerDifferential KaehlerDifferential.module' Algebra.id Algebra.to_smulCommClass Cardinal Cardinal.instNatCast	—	Algebra.to_smulCommClass rank_kaehlerDifferential Nat.cast_injective Cardinal.instCharZero Algebra.SubmersivePresentation.rank_kaehlerDifferential
rank_kaehlerDifferential 📖	mathematical	—	Module.rank KaehlerDifferential CommSemiring.toSemiring CommRing.toCommSemiring AddCommGroup.toAddCommMonoid instAddCommGroupKaehlerDifferential KaehlerDifferential.module' Algebra.id Algebra.to_smulCommClass Cardinal Cardinal.instNatCast	—	Algebra.to_smulCommClass Algebra.SubmersivePresentation.rank_kaehlerDifferential

Algebra.PreSubmersivePresentation

Definitions

Name	Category	Theorems
cotangentComplexAux 📖	CompOp	6 math math: Algebra.SubmersivePresentation.cotangentComplexAux_injective, cotangentComplexAux_apply, cotangentComplexAux_zero_iff, Algebra.SubmersivePresentation.sectionCotangent_eq_iff, Algebra.SubmersivePresentation.cotangentComplexAux_surjective, Algebra.SubmersivePresentation.cotangentEquiv_apply

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
cotangentComplexAux_apply 📖	mathematical	—	DFunLike.coe LinearMap CommSemiring.toSemiring CommRing.toCommSemiring RingHom.id Semiring.toNonAssocSemiring Algebra.Extension.Cotangent Algebra.Generators.toExtension Algebra.Presentation.toGenerators toPresentation AddCommGroup.toAddCommMonoid Algebra.Extension.instAddCommGroupCotangent Pi.addCommMonoid NonUnitalNonAssocSemiring.toAddCommMonoid NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing Algebra.Extension.instModuleCotangent Algebra.id Pi.Function.module Semiring.toModule LinearMap.instFunLike cotangentComplexAux 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 Algebra.Generators.val Derivation MvPolynomial.module Derivation.instFunLike MvPolynomial.pderiv map Algebra.Generators.Ring Algebra.Generators.ker	—	Algebra.to_smulCommClass smulCommClass_self RingHomInvPair.ids Algebra.Generators.cotangentSpaceBasis_repr_tmul one_mul
cotangentComplexAux_zero_iff 📖	mathematical	—	DFunLike.coe LinearMap CommSemiring.toSemiring CommRing.toCommSemiring RingHom.id Semiring.toNonAssocSemiring Algebra.Extension.Cotangent Algebra.Generators.toExtension Algebra.Presentation.toGenerators toPresentation AddCommGroup.toAddCommMonoid Algebra.Extension.instAddCommGroupCotangent Pi.addCommMonoid NonUnitalNonAssocSemiring.toAddCommMonoid NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing Algebra.Extension.instModuleCotangent Algebra.id Pi.Function.module Semiring.toModule LinearMap.instFunLike cotangentComplexAux Algebra.Extension.Ring Algebra.Extension.commRing Ideal SetLike.instMembership Submodule.setLike NonAssocSemiring.toNonUnitalNonAssocSemiring Algebra.Extension.ker Submodule.addCommMonoid Submodule.module Algebra.Extension.algebra₂ Pi.instZero MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass AlgHom MvPolynomial MvPolynomial.commSemiring MvPolynomial.algebra AlgHom.funLike MvPolynomial.aeval Algebra.Generators.val Derivation MvPolynomial.module Derivation.instFunLike MvPolynomial.pderiv map Algebra.Generators.Ring Algebra.Generators.ker	—	cotangentComplexAux_apply

Algebra.SubmersivePresentation

Definitions

Name	Category	Theorems
basisCotangent 📖	CompOp	2 math math: basisCotangent_localizationAway_apply, basisCotangent_apply
basisKaehler 📖	CompOp	1 math math: basisKaehler_apply
basisKaehlerOfIsCompl 📖	CompOp	1 math math: basisKaehlerOfIsCompl_apply
cotangentEquiv 📖	CompOp	1 math math: cotangentEquiv_apply
sectionCotangent 📖	CompOp	3 math math: sectionCotangent_eq_iff, sectionCotangent_comp, sectionCotangent_zero_of_notMem_range

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
basisCotangent_apply 📖	mathematical	—	DFunLike.coe Module.Basis Algebra.Extension.Cotangent Algebra.Generators.toExtension Algebra.Presentation.toGenerators Algebra.PreSubmersivePresentation.toPresentation toPreSubmersivePresentation CommSemiring.toSemiring CommRing.toCommSemiring AddCommGroup.toAddCommMonoid Algebra.Extension.instAddCommGroupCotangent Algebra.Extension.instModuleCotangent Algebra.id Module.Basis.instFunLike basisCotangent LinearMap Algebra.Extension.Ring Algebra.Extension.commRing RingHom.id Semiring.toNonAssocSemiring Ideal SetLike.instMembership Submodule.setLike NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toModule Algebra.Extension.ker Submodule.addCommMonoid Submodule.module Algebra.Extension.algebra₂ LinearMap.instFunLike Algebra.Presentation.relation Algebra.Presentation.relation_mem_ker	—	Algebra.Presentation.relation_mem_ker LinearEquiv.injective RingHomInvPair.ids LinearEquiv.apply_symm_apply basisDeriv_apply Algebra.PreSubmersivePresentation.cotangentComplexAux_apply
basisCotangent_localizationAway_apply 📖	mathematical	—	DFunLike.coe Module.Basis Algebra.Extension.Cotangent Algebra.Generators.toExtension Algebra.Presentation.toGenerators Algebra.PreSubmersivePresentation.toPresentation toPreSubmersivePresentation Finite.of_fintype PUnit.fintype localizationAway CommSemiring.toSemiring CommRing.toCommSemiring AddCommGroup.toAddCommMonoid Algebra.Extension.instAddCommGroupCotangent Algebra.Extension.instModuleCotangent Algebra.id Module.Basis.instFunLike basisCotangent Algebra.Generators.cMulXSubOneCotangent	—	basisCotangent_apply Finite.of_fintype
basisKaehlerOfIsCompl_apply 📖	mathematical	IsCompl Set OmegaCompletePartialOrder.toPartialOrder CompleteLattice.instOmegaCompletePartialOrder CompleteBooleanAlgebra.toCompleteLattice CompleteAtomicBooleanAlgebra.toCompleteBooleanAlgebra Set.instCompleteAtomicBooleanAlgebra Set.instBoundedOrder Set.range Algebra.PreSubmersivePresentation.map toPreSubmersivePresentation	DFunLike.coe Module.Basis KaehlerDifferential CommSemiring.toSemiring CommRing.toCommSemiring AddCommGroup.toAddCommMonoid instAddCommGroupKaehlerDifferential KaehlerDifferential.module' Algebra.id Algebra.to_smulCommClass Module.Basis.instFunLike basisKaehlerOfIsCompl Derivation smulCommClass_self CommRing.toCommMonoid DistribMulAction.toMulAction CommMonoid.toMonoid AddCommMonoid.toAddMonoid NonUnitalNonAssocSemiring.toAddCommMonoid NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing Module.toDistribMulAction Ring.toSemiring CommRing.toRing Algebra.toModule Derivation.instFunLike KaehlerDifferential.D Algebra.Generators.val Algebra.Presentation.toGenerators Algebra.PreSubmersivePresentation.toPresentation	—	Algebra.to_smulCommClass smulCommClass_self sectionCotangent_comp Module.Basis.ofSplitExact_apply Algebra.Generators.toKaehler_cotangentSpaceBasis
basisKaehler_apply 📖	mathematical	—	DFunLike.coe Module.Basis Set.Elem Compl.compl Set Set.instCompl Set.range Algebra.PreSubmersivePresentation.map toPreSubmersivePresentation KaehlerDifferential CommSemiring.toSemiring CommRing.toCommSemiring AddCommGroup.toAddCommMonoid instAddCommGroupKaehlerDifferential KaehlerDifferential.module' Algebra.id Algebra.to_smulCommClass Module.Basis.instFunLike basisKaehler Derivation smulCommClass_self CommRing.toCommMonoid DistribMulAction.toMulAction CommMonoid.toMonoid AddCommMonoid.toAddMonoid NonUnitalNonAssocSemiring.toAddCommMonoid NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing Module.toDistribMulAction Ring.toSemiring CommRing.toRing Algebra.toModule Derivation.instFunLike KaehlerDifferential.D Algebra.Generators.val Algebra.Presentation.toGenerators Algebra.PreSubmersivePresentation.toPresentation Set.instMembership	—	Algebra.to_smulCommClass smulCommClass_self basisKaehlerOfIsCompl_apply
cotangentComplexAux_injective 📖	mathematical	—	Algebra.Extension.Cotangent Algebra.Generators.toExtension Algebra.Presentation.toGenerators Algebra.PreSubmersivePresentation.toPresentation toPreSubmersivePresentation DFunLike.coe LinearMap CommSemiring.toSemiring CommRing.toCommSemiring RingHom.id Semiring.toNonAssocSemiring AddCommGroup.toAddCommMonoid Algebra.Extension.instAddCommGroupCotangent Pi.addCommMonoid NonUnitalNonAssocSemiring.toAddCommMonoid NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing Algebra.Extension.instModuleCotangent Algebra.id Pi.Function.module Semiring.toModule LinearMap.instFunLike Algebra.PreSubmersivePresentation.cotangentComplexAux	—	LinearMap.ker_eq_bot eq_bot_iff Algebra.Extension.Cotangent.mk_surjective Submodule.mem_bot Algebra.Extension.Cotangent.mk_eq_zero_iff Algebra.Presentation.span_range_relation_eq_ker Finsupp.mem_ideal_span_range_iff_exists_finsupp Algebra.PreSubmersivePresentation.cotangentComplexAux_zero_iff LinearMap.mem_ker Finset.sum_apply Finset.sum_congr map_sum Derivation.instAddMonoidHomClass Derivation.leibniz DistribMulActionSemiHomClass.toAddMonoidHomClass NonUnitalAlgSemiHomClass.toDistribMulActionSemiHomClass AlgHom.instNonUnitalAlgHomClassOfAlgHomClass AlgHom.algHomClass map_add SemilinearMapClass.toAddHomClass NonUnitalAlgHomClass.instLinearMapClass map_mul NonUnitalAlgSemiHomClass.toMulHomClass Algebra.Presentation.aeval_val_relation MulZeroClass.zero_mul add_zero linearIndependent_aeval_val_pderiv_relation linearIndependent_iff'' map_zero MonoidWithZeroHomClass.toZeroHomClass RingHomClass.toMonoidWithZeroHomClass AlgHomClass.toRingHomClass Ideal.sum_mem pow_two Ideal.mul_mem_mul Algebra.Generators.ker_eq_ker_aeval_val Algebra.Presentation.relation_mem_ker
cotangentComplexAux_surjective 📖	mathematical	—	Algebra.Extension.Cotangent Algebra.Generators.toExtension Algebra.Presentation.toGenerators Algebra.PreSubmersivePresentation.toPresentation toPreSubmersivePresentation DFunLike.coe LinearMap CommSemiring.toSemiring CommRing.toCommSemiring RingHom.id Semiring.toNonAssocSemiring AddCommGroup.toAddCommMonoid Algebra.Extension.instAddCommGroupCotangent Pi.addCommMonoid NonUnitalNonAssocSemiring.toAddCommMonoid NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing Algebra.Extension.instModuleCotangent Algebra.id Pi.Function.module Semiring.toModule LinearMap.instFunLike Algebra.PreSubmersivePresentation.cotangentComplexAux	—	RingHomSurjective.ids LinearMap.range_eq_top eq_top_iff Module.Basis.span_eq Submodule.span_le Algebra.Presentation.relation_mem_ker Algebra.PreSubmersivePresentation.cotangentComplexAux_apply basisDeriv_apply
cotangentComplex_injective 📖	mathematical	—	Algebra.Extension.Cotangent Algebra.Generators.toExtension Algebra.Presentation.toGenerators Algebra.PreSubmersivePresentation.toPresentation toPreSubmersivePresentation Algebra.Extension.CotangentSpace DFunLike.coe LinearMap CommSemiring.toSemiring CommRing.toCommSemiring RingHom.id Semiring.toNonAssocSemiring AddCommGroup.toAddCommMonoid Algebra.Extension.instAddCommGroupCotangent TensorProduct.addCommMonoid Algebra.Extension.Ring Algebra.Extension.commRing KaehlerDifferential Algebra.Extension.instRingOfIsScalarTower Algebra.id NonUnitalNonAssocSemiring.toAddCommMonoid NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing instAddCommGroupKaehlerDifferential Algebra.toModule Algebra.Extension.algebra₂ KaehlerDifferential.module' Algebra.Extension.instModuleCotangent TensorProduct.leftModule Semiring.toModule Algebra.to_smulCommClass LinearMap.instFunLike Algebra.Extension.cotangentComplex	—	cotangentComplexAux_injective Function.Injective.of_comp Algebra.to_smulCommClass
cotangentEquiv_apply 📖	mathematical	—	DFunLike.coe LinearEquiv CommSemiring.toSemiring CommRing.toCommSemiring RingHom.id Semiring.toNonAssocSemiring RingHomInvPair.ids Algebra.Extension.Cotangent Algebra.Generators.toExtension Algebra.Presentation.toGenerators Algebra.PreSubmersivePresentation.toPresentation toPreSubmersivePresentation AddCommGroup.toAddCommMonoid Algebra.Extension.instAddCommGroupCotangent Pi.addCommMonoid NonUnitalNonAssocSemiring.toAddCommMonoid NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing Algebra.Extension.instModuleCotangent Algebra.id Pi.Function.module Semiring.toModule EquivLike.toFunLike LinearEquiv.instEquivLike cotangentEquiv LinearMap LinearMap.instFunLike Algebra.PreSubmersivePresentation.cotangentComplexAux	—	RingHomInvPair.ids
free_cotangent 📖	mathematical	—	Module.Free Algebra.Extension.Cotangent Algebra.Generators.toExtension Algebra.Presentation.toGenerators Algebra.PreSubmersivePresentation.toPresentation toPreSubmersivePresentation CommSemiring.toSemiring CommRing.toCommSemiring AddCommGroup.toAddCommMonoid Algebra.Extension.instAddCommGroupCotangent Algebra.Extension.instModuleCotangent Algebra.id	—	Module.Free.of_basis
free_kaehlerDifferential 📖	mathematical	—	Module.Free KaehlerDifferential CommSemiring.toSemiring CommRing.toCommSemiring AddCommGroup.toAddCommMonoid instAddCommGroupKaehlerDifferential KaehlerDifferential.module' Algebra.id Algebra.to_smulCommClass	—	Module.Free.of_basis Algebra.to_smulCommClass
rank_kaehlerDifferential 📖	mathematical	—	Module.rank KaehlerDifferential CommSemiring.toSemiring CommRing.toCommSemiring AddCommGroup.toAddCommMonoid instAddCommGroupKaehlerDifferential KaehlerDifferential.module' Algebra.id Algebra.to_smulCommClass Cardinal Cardinal.instNatCast Algebra.Presentation.dimension Algebra.PreSubmersivePresentation.toPresentation toPreSubmersivePresentation	—	Algebra.to_smulCommClass Subtype.finite rank_eq_card_basis commRing_strongRankCondition Finite.Set.finite_range Fintype.card_compl_set Set.card_range_of_injective Nat.card_eq_fintype_card
sectionCotangent_comp 📖	mathematical	—	LinearMap.comp Algebra.Extension.Cotangent Algebra.Generators.toExtension Algebra.Presentation.toGenerators Algebra.PreSubmersivePresentation.toPresentation toPreSubmersivePresentation 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 RingHom.id Semiring.toNonAssocSemiring RingHomCompTriple.ids sectionCotangent Algebra.Extension.cotangentComplex LinearMap.id	—	LinearMap.ext Algebra.to_smulCommClass RingHomCompTriple.ids RingHomInvPair.ids sectionCotangent_eq_iff
sectionCotangent_eq_iff 📖	mathematical	—	DFunLike.coe LinearMap CommSemiring.toSemiring CommRing.toCommSemiring RingHom.id Semiring.toNonAssocSemiring Algebra.Extension.CotangentSpace Algebra.Generators.toExtension Algebra.Presentation.toGenerators Algebra.PreSubmersivePresentation.toPresentation toPreSubmersivePresentation 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 sectionCotangent Finsupp MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass NonAssocSemiring.toNonUnitalNonAssocSemiring Finsupp.instFunLike LinearEquiv RingHomInvPair.ids Finsupp.instAddCommMonoid Finsupp.module EquivLike.toFunLike DFinsupp.instEquivLikeLinearEquiv Module.Basis.repr Algebra.Generators.cotangentSpaceBasis Algebra.PreSubmersivePresentation.map Pi.addCommMonoid Pi.Function.module Algebra.PreSubmersivePresentation.cotangentComplexAux	—	Algebra.to_smulCommClass RingHomInvPair.ids LinearEquiv.injective LinearEquiv.apply_symm_apply
sectionCotangent_zero_of_notMem_range 📖	mathematical	Set Set.instMembership Set.range Algebra.PreSubmersivePresentation.map toPreSubmersivePresentation	DFunLike.coe LinearMap CommSemiring.toSemiring CommRing.toCommSemiring RingHom.id Semiring.toNonAssocSemiring Algebra.Extension.CotangentSpace Algebra.Generators.toExtension Algebra.Presentation.toGenerators Algebra.PreSubmersivePresentation.toPresentation 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 sectionCotangent Module.Basis Module.Basis.instFunLike Algebra.Generators.cotangentSpaceBasis NegZeroClass.toZero SubNegZeroMonoid.toNegZeroClass SubtractionMonoid.toSubNegZeroMonoid SubtractionCommMonoid.toSubtractionMonoid AddCommGroup.toDivisionAddCommMonoid	—	Mathlib.Tactic.Contrapose.contrapose₂ Algebra.to_smulCommClass RingHomInvPair.ids Module.Basis.repr_self Finsupp.single_apply map_zero AddMonoidHomClass.toZeroHomClass DistribMulActionSemiHomClass.toAddMonoidHomClass SemilinearMapClass.distribMulActionSemiHomClass LinearMap.semilinearMapClass sectionCotangent_eq_iff
subsingleton_h1Cotangent 📖	mathematical	—	Algebra.Extension.H1Cotangent Algebra.Generators.toExtension Algebra.Presentation.toGenerators Algebra.PreSubmersivePresentation.toPresentation toPreSubmersivePresentation	—	Algebra.to_smulCommClass Algebra.Extension.subsingleton_h1Cotangent cotangentComplex_injective

---

← Back to Index