Cotangent

📁 Source: Mathlib/RingTheory/Ideal/Cotangent.lean

Statistics

Metric	Count
Definitions kerSquareLift, Cotangent, kerSquareLift, Cotangent, cotangentEquivIdeal, cotangentIdeal, cotangentToQuotientSquare, instAddCommGroupCotangent, instInhabitedCotangent, instIsNoetherianCotangentOfSubtypeMem, instIsScalarTowerCotangent, instModuleCotangentOfAlgebra, instModuleQuotientCotangent, mapCotangent, quotCotangent, toCotangent, CotangentSpace, instModuleResidueFieldCotangentSpace	18
Theorems kerSquareLift_mk, ker_kerSquareLift, smul_eq_zero_of_mem, comap_cotangentIdeal, cotangentEquivIdeal_apply, cotangentEquivIdeal_symm_apply, cotangentIdeal_square, cotangent_subsingleton_iff, instIsScalarTowerQuotientHPowKerRingHomAlgebraMapOfNat, isTorsionBySet_cotangent, mapCotangent_toCotangent, map_toCotangent_ker, mem_toCotangent_ker, mk_mem_cotangentIdeal, range_cotangentToQuotientSquare, toCotangent_apply, toCotangent_eq, toCotangent_eq_zero, toCotangent_range, toCotangent_surjective, toCotangent_to_quotient_square, to_quotient_square_comp_toCotangent, map_eq_top_iff, span_image_eq_top_iff, finrank_cotangentSpace_eq_zero, finrank_cotangentSpace_eq_zero_iff, finrank_cotangentSpace_le_one_iff, instFiniteDimensionalResidueFieldCotangentSpaceOfIsNoetherianRing, instIsScalarTowerResidueFieldCotangentSpace, subsingleton_cotangentSpace_iff	30
Total	48

AlgHom

Definitions

Name	Category	Theorems
kerSquareLift 📖	CompOp	4 math math: KaehlerDifferential.End_equiv_aux, Algebra.FormallySmooth.iff_split_surjection, ker_kerSquareLift, kerSquareLift_mk

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
kerSquareLift_mk 📖	mathematical	—	DFunLike.coe AlgHom HasQuotient.Quotient Ideal CommSemiring.toSemiring CommRing.toCommSemiring Ideal.instHasQuotient_1 Monoid.toNatPow MonoidWithZero.toMonoid Semiring.toMonoidWithZero IdemSemiring.toSemiring Submodule.idemSemiring Algebra.id RingHom.ker RingHom Semiring.toNonAssocSemiring RingHom.instFunLike RingHom.instRingHomClass toRingHom Ideal.Quotient.semiring Ideal.instAlgebraQuotient funLike kerSquareLift Ring.toSemiring CommRing.toRing Ideal.instHasQuotient Ideal.Quotient.ring Ideal.instIsTwoSided_1	—	RingHom.instRingHomClass Ideal.instIsTwoSided_1
ker_kerSquareLift 📖	mathematical	—	RingHom.ker HasQuotient.Quotient Ideal CommSemiring.toSemiring CommRing.toCommSemiring Ideal.instHasQuotient_1 Monoid.toNatPow MonoidWithZero.toMonoid Semiring.toMonoidWithZero IdemSemiring.toSemiring Submodule.idemSemiring Algebra.id RingHom Semiring.toNonAssocSemiring RingHom.instFunLike RingHom.instRingHomClass toRingHom Ideal.Quotient.semiring Ideal.instAlgebraQuotient kerSquareLift Ideal.cotangentIdeal	—	le_antisymm RingHom.instRingHomClass Ideal.instIsTwoSided_1 Ideal.Quotient.mk_surjective

Algebra.Extension

Definitions

Name	Category	Theorems
Cotangent 📖	CompOp	75 math math: Algebra.SubmersivePresentation.cotangentComplexAux_injective, Algebra.Presentation.differentials.comm₁₂_single, Cotangent.span_eq_top_of_span_eq_ker, Algebra.PreSubmersivePresentation.cotangentComplexAux_apply, H1Cotangent.equiv_apply, Cotangent.val_sub, formallySmooth_iff_split_injection, h1Cotangentι_injective, Algebra.PreSubmersivePresentation.cotangentComplexAux_zero_iff, Algebra.Presentation.differentials.hom₁_single, Algebra.Generators.exists_presentation_of_basis_cotangent, lTensor_cotangentComplex_eq_cotangentComplexBaseChange, Algebra.Generators.liftBaseChange_injective_of_isLocalizationAway, Cotangent.val_mk, subsingleton_h1Cotangent, Algebra.Generators.exists_presentation_of_free_cotangent, H1Cotangent.val_zero, Algebra.FormallySmooth.iff_injective_lTensor_residueField, Cotangent.val_smul''', Cotangent.val_add, Cotangent.finite, instIsScalarTowerCotangent, Hom.sub_one_tmul, Algebra.SubmersivePresentation.sectionCotangent_eq_iff, Cotangent.mk_eq_zero_iff, Algebra.Presentation.differentials.surjective_hom₁, Algebra.Generators.Cotangent.surjective_map_ofComp, CotangentSpace.map_sub_map, Algebra.Generators.cotangentRestrict_bijective_of_isCompl, CotangentSpace.map_cotangentComplex, cotangentComplexBaseChange_eq_lTensor_cotangentComplex, Cotangent.val_smul', Cotangent.map_comp, Algebra.Generators.cotangentCompAwaySec_apply, Cotangent.map_id, Algebra.Generators.Cotangent.exact, contangentEquiv_tmul, Algebra.Generators.cMulXSubOneCotangent_eq, h1Cotangentι_ext_iff, Cotangent.map_toInfinitesimal_bijective, H1Cotangent.val_add, H1Cotangent.val_smul, Algebra.Presentation.differentials.comm₁₂, Cotangent.mk_eq_mk_iff_sub_mem, Cotangent.mk_surjective, Algebra.SubmersivePresentation.basisCotangent_localizationAway_apply, Algebra.SubmersivePresentation.cotangentComplexAux_surjective, H1Cotangent.map_apply_coe, Cotangent.val_smul, tensorCotangentInvFun_smul_mk, h1Cotangentι_apply, cotangentComplex_injective_iff, Algebra.Generators.cotangentRestrict_mk, Algebra.Generators.cotangentRestrict_bijective_of_basis_kaehlerDifferential, Cotangent.val_zero, Hom.sub_tmul, Cotangent.of_add, Algebra.SubmersivePresentation.sectionCotangent_comp, Algebra.SubmersivePresentation.sectionCotangent_zero_of_notMem_range, Algebra.SubmersivePresentation.free_cotangent, Algebra.SubmersivePresentation.cotangentComplex_injective, Algebra.instFreeCotangentToExtensionUnitLocalizationAway, Algebra.SubmersivePresentation.basisCotangent_apply, Cotangent.map_mk, exact_cotangentComplex_toKaehler, Algebra.Generators.basisCotangentAway_apply, Algebra.Generators.H1Cotangent.map_comp_cotangentComplex_baseChange, Algebra.Generators.H1Cotangent.equiv_apply, CotangentSpace.map_comp_cotangentComplex, Cotangent.ker_mk, Algebra.SubmersivePresentation.cotangentEquiv_apply, Cotangent.map_sub_map, Cotangent.of_zero, cotangentComplex_mk, Cotangent.val_smul''

Ideal

Definitions

Name	Category	Theorems
Cotangent 📖	CompOp	38 math math: toCotangent_to_quotient_square, KaehlerDifferential.kerCotangentToTensor_toCotangent, toCotangent_eq, Algebra.Extension.Cotangent.val_sub, range_cotangentToQuotientSquare, mem_toCotangent_ker, Algebra.Extension.Cotangent.smul_eq_zero_of_mem, Algebra.Extension.Cotangent.val_mk, toCotangent_range, isTorsionBySet_cotangent, Algebra.Extension.Cotangent.val_smul''', Algebra.Extension.Cotangent.val_add, KaehlerDifferential.D_apply, mapCotangent_toCotangent, Cotangent.smul_eq_zero_of_mem, Algebra.Extension.Cotangent.val_smul', toCotangent_apply, toCotangent_eq_zero, cotangentEquivIdeal_apply, KaehlerDifferential.exact_kerCotangentToTensor_mapBaseChange, KaehlerDifferential.D_tensorProductTo, Algebra.Extension.Cotangent.val_smul, Algebra.FormallySmooth.kerCotangentToTensor_injective_iff, IsLocalRing.CotangentSpace.map_eq_top_iff, IsLocalRing.CotangentSpace.span_image_eq_top_iff, Algebra.Extension.Cotangent.val_zero, Algebra.Extension.Cotangent.of_add, cotangentEquivIdeal_symm_apply, KaehlerDifferential.range_kerCotangentToTensor, Derivation.liftKaehlerDifferential_apply, KaehlerDifferential.DLinearMap_apply, map_toCotangent_ker, toCotangent_surjective, Algebra.FormallySmooth.iff_split_injection, Algebra.Extension.Cotangent.of_zero, to_quotient_square_comp_toCotangent, Algebra.Extension.Cotangent.val_smul'', cotangent_subsingleton_iff
cotangentEquivIdeal 📖	CompOp	2 math math: cotangentEquivIdeal_apply, cotangentEquivIdeal_symm_apply
cotangentIdeal 📖	CompOp	9 math math: comap_cotangentIdeal, range_cotangentToQuotientSquare, KaehlerDifferential.End_equiv_aux, mk_mem_cotangentIdeal, Algebra.Extension.ker_infinitesimal, cotangentEquivIdeal_apply, AlgHom.ker_kerSquareLift, cotangentEquivIdeal_symm_apply, cotangentIdeal_square
cotangentToQuotientSquare 📖	CompOp	4 math math: toCotangent_to_quotient_square, range_cotangentToQuotientSquare, cotangentEquivIdeal_apply, to_quotient_square_comp_toCotangent
instAddCommGroupCotangent 📖	CompOp	46 math math: toCotangent_to_quotient_square, KaehlerDifferential.kerCotangentToTensor_toCotangent, IsLocalRing.finrank_CotangentSpace_eq_one_iff, toCotangent_eq, Algebra.Extension.Cotangent.val_sub, IsLocalRing.finrank_cotangentSpace_eq_zero, range_cotangentToQuotientSquare, mem_toCotangent_ker, Algebra.Extension.Cotangent.smul_eq_zero_of_mem, Algebra.Extension.Cotangent.val_mk, toCotangent_range, isTorsionBySet_cotangent, Algebra.Extension.Cotangent.val_smul''', IsLocalRing.finrank_CotangentSpace_eq_one, IsLocalRing.finrank_cotangentSpace_eq_zero_iff, Algebra.Extension.Cotangent.val_add, KaehlerDifferential.D_apply, mapCotangent_toCotangent, IsLocalRing.instFiniteDimensionalResidueFieldCotangentSpaceOfIsNoetherianRing, Cotangent.smul_eq_zero_of_mem, Algebra.Extension.Cotangent.val_smul', tfae_of_isNoetherianRing_of_isLocalRing_of_isDomain, toCotangent_apply, toCotangent_eq_zero, IsLocalRing.finrank_cotangentSpace_le_one_iff, cotangentEquivIdeal_apply, KaehlerDifferential.exact_kerCotangentToTensor_mapBaseChange, IsLocalRing.instIsScalarTowerResidueFieldCotangentSpace, KaehlerDifferential.D_tensorProductTo, Algebra.Extension.Cotangent.val_smul, IsDiscreteValuationRing.TFAE, Algebra.FormallySmooth.kerCotangentToTensor_injective_iff, IsLocalRing.CotangentSpace.map_eq_top_iff, IsLocalRing.CotangentSpace.span_image_eq_top_iff, Algebra.Extension.Cotangent.val_zero, Algebra.Extension.Cotangent.of_add, cotangentEquivIdeal_symm_apply, KaehlerDifferential.range_kerCotangentToTensor, Derivation.liftKaehlerDifferential_apply, KaehlerDifferential.DLinearMap_apply, map_toCotangent_ker, toCotangent_surjective, Algebra.FormallySmooth.iff_split_injection, Algebra.Extension.Cotangent.of_zero, to_quotient_square_comp_toCotangent, Algebra.Extension.Cotangent.val_smul''
instInhabitedCotangent 📖	CompOp	—
instIsNoetherianCotangentOfSubtypeMem 📖	CompOp	—
instIsScalarTowerCotangent 📖	CompOp	—
instModuleCotangentOfAlgebra 📖	CompOp	33 math math: toCotangent_to_quotient_square, KaehlerDifferential.kerCotangentToTensor_toCotangent, toCotangent_eq, range_cotangentToQuotientSquare, mem_toCotangent_ker, Algebra.Extension.Cotangent.smul_eq_zero_of_mem, Algebra.Extension.Cotangent.val_mk, toCotangent_range, isTorsionBySet_cotangent, Algebra.Extension.Cotangent.val_smul''', KaehlerDifferential.D_apply, mapCotangent_toCotangent, Cotangent.smul_eq_zero_of_mem, Algebra.Extension.Cotangent.val_smul', toCotangent_apply, toCotangent_eq_zero, cotangentEquivIdeal_apply, KaehlerDifferential.exact_kerCotangentToTensor_mapBaseChange, IsLocalRing.instIsScalarTowerResidueFieldCotangentSpace, KaehlerDifferential.D_tensorProductTo, Algebra.Extension.Cotangent.val_smul, Algebra.FormallySmooth.kerCotangentToTensor_injective_iff, IsLocalRing.CotangentSpace.map_eq_top_iff, IsLocalRing.CotangentSpace.span_image_eq_top_iff, cotangentEquivIdeal_symm_apply, KaehlerDifferential.range_kerCotangentToTensor, Derivation.liftKaehlerDifferential_apply, KaehlerDifferential.DLinearMap_apply, map_toCotangent_ker, toCotangent_surjective, Algebra.FormallySmooth.iff_split_injection, to_quotient_square_comp_toCotangent, Algebra.Extension.Cotangent.val_smul''
instModuleQuotientCotangent 📖	CompOp	—
mapCotangent 📖	CompOp	1 math math: mapCotangent_toCotangent
quotCotangent 📖	CompOp	—
toCotangent 📖	CompOp	19 math math: toCotangent_to_quotient_square, KaehlerDifferential.kerCotangentToTensor_toCotangent, toCotangent_eq, mem_toCotangent_ker, Algebra.Extension.Cotangent.val_mk, toCotangent_range, KaehlerDifferential.D_apply, mapCotangent_toCotangent, toCotangent_apply, toCotangent_eq_zero, KaehlerDifferential.D_tensorProductTo, IsLocalRing.CotangentSpace.map_eq_top_iff, IsLocalRing.CotangentSpace.span_image_eq_top_iff, cotangentEquivIdeal_symm_apply, Derivation.liftKaehlerDifferential_apply, KaehlerDifferential.DLinearMap_apply, map_toCotangent_ker, toCotangent_surjective, to_quotient_square_comp_toCotangent

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
comap_cotangentIdeal 📖	mathematical	—	comap HasQuotient.Quotient Ideal CommSemiring.toSemiring CommRing.toCommSemiring instHasQuotient_1 Monoid.toNatPow MonoidWithZero.toMonoid Semiring.toMonoidWithZero IdemSemiring.toSemiring Submodule.idemSemiring Algebra.id RingHom Ring.toSemiring CommRing.toRing instHasQuotient Semiring.toNonAssocSemiring Quotient.ring instIsTwoSided_1 Quotient.semiring RingHom.instFunLike RingHom.instRingHomClass cotangentIdeal	—	ext instIsTwoSided_1 RingHom.instRingHomClass mk_mem_cotangentIdeal
cotangentEquivIdeal_apply 📖	mathematical	—	HasQuotient.Quotient Ideal CommSemiring.toSemiring CommRing.toCommSemiring instHasQuotient_1 Monoid.toNatPow MonoidWithZero.toMonoid Semiring.toMonoidWithZero IdemSemiring.toSemiring Submodule.idemSemiring Algebra.id Quotient.semiring SetLike.instMembership Submodule.setLike NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring Semiring.toModule cotangentIdeal DFunLike.coe LinearEquiv RingHom.id RingHomInvPair.ids Cotangent AddCommGroup.toAddCommMonoid instAddCommGroupCotangent Submodule.addCommMonoid instModuleCotangentOfAlgebra Submodule.module' Submodule.Quotient.instSMul CommRing.toRing Ring.toAddCommGroup Submodule.Quotient.module IsScalarTower.right instAlgebraQuotient EquivLike.toFunLike DFinsupp.instEquivLikeLinearEquiv cotangentEquivIdeal LinearMap NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing Quotient.commRing LinearMap.instFunLike cotangentToQuotientSquare	—	RingHomInvPair.ids IsScalarTower.right
cotangentEquivIdeal_symm_apply 📖	mathematical	Ideal CommSemiring.toSemiring CommRing.toCommSemiring SetLike.instMembership Submodule.setLike NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring Semiring.toModule	DFunLike.coe LinearEquiv RingHom.id RingHomInvPair.ids HasQuotient.Quotient instHasQuotient_1 Monoid.toNatPow MonoidWithZero.toMonoid Semiring.toMonoidWithZero IdemSemiring.toSemiring Submodule.idemSemiring Algebra.id Quotient.semiring cotangentIdeal Cotangent Submodule.addCommMonoid AddCommGroup.toAddCommMonoid instAddCommGroupCotangent Submodule.module' Submodule.Quotient.instSMul CommRing.toRing Ring.toAddCommGroup Submodule.Quotient.module IsScalarTower.right instAlgebraQuotient instModuleCotangentOfAlgebra EquivLike.toFunLike DFinsupp.instEquivLikeLinearEquiv LinearEquiv.symm cotangentEquivIdeal LinearMap Ring.toSemiring Submodule Submodule.hasQuotient Submodule.Quotient.addCommGroup LinearMap.instFunLike Submodule.mkQ Submodule.mem_map_of_mem RingHom.toSemilinearMap instHasQuotient Quotient.ring Submodule.module toCotangent	—	RingHomInvPair.ids IsScalarTower.right instIsTwoSided_1 Submodule.mem_map_of_mem LinearEquiv.symm_apply_eq
cotangentIdeal_square 📖	mathematical	—	Ideal HasQuotient.Quotient CommSemiring.toSemiring CommRing.toCommSemiring instHasQuotient_1 Monoid.toNatPow MonoidWithZero.toMonoid Semiring.toMonoidWithZero IdemSemiring.toSemiring Submodule.idemSemiring Algebra.id Quotient.semiring Quotient.commSemiring cotangentIdeal Bot.bot Submodule.instBot NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring Semiring.toModule	—	eq_bot_iff pow_two smul_eq_mul Submodule.smul_induction_on IsScalarTower.right Submodule.Quotient.eq sub_zero mul_mem_mul AddMemClass.add_mem AddSubmonoidClass.toAddMemClass Submodule.addSubmonoidClass
cotangent_subsingleton_iff 📖	mathematical	—	Cotangent IsIdempotentElem Ideal CommSemiring.toSemiring CommRing.toCommSemiring Submodule.mul Semiring.toModule IsScalarTower.right Algebra.id	—	IsScalarTower.right pow_two le_antisymm pow_le_self two_ne_zero toCotangent_eq_zero Quotient.inductionOn₂' toCotangent_eq sub_mem Subtype.prop
instIsScalarTowerQuotientHPowKerRingHomAlgebraMapOfNat 📖	mathematical	—	IsScalarTower HasQuotient.Quotient Ideal CommSemiring.toSemiring CommRing.toCommSemiring instHasQuotient_1 Monoid.toNatPow MonoidWithZero.toMonoid Semiring.toMonoidWithZero IdemSemiring.toSemiring Submodule.idemSemiring Algebra.id RingHom.ker RingHom Semiring.toNonAssocSemiring RingHom.instFunLike RingHom.instRingHomClass algebraMap Submodule.Quotient.instSMul' CommRing.toRing Ring.toAddCommGroup Semiring.toModule Algebra.toSMul IsScalarTower.right Quotient.commSemiring Algebra.kerSquareLift	—	IsScalarTower.of_algebraMap_eq' RingHom.instRingHomClass AlgHomClass.toRingHomClass AlgHom.algHomClass AlgHom.comp_algebraMap
isTorsionBySet_cotangent 📖	mathematical	—	Module.IsTorsionBySet Cotangent CommSemiring.toSemiring CommRing.toCommSemiring AddCommGroup.toAddCommMonoid instAddCommGroupCotangent instModuleCotangentOfAlgebra Algebra.id SetLike.coe Ideal Submodule.setLike NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring Semiring.toModule	—	Cotangent.smul_eq_zero_of_mem
mapCotangent_toCotangent 📖	mathematical	Ideal CommSemiring.toSemiring CommRing.toCommSemiring Preorder.toLE PartialOrder.toPreorder Submodule.instPartialOrder NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring Semiring.toModule comap AlgHom AlgHom.funLike AlgHomClass.toRingHomClass AlgHom.algHomClass	DFunLike.coe LinearMap RingHom.id Cotangent AddCommGroup.toAddCommMonoid instAddCommGroupCotangent instModuleCotangentOfAlgebra LinearMap.instFunLike mapCotangent SetLike.instMembership Submodule.setLike Submodule.addCommMonoid Submodule.module Algebra.id toCotangent	—	AlgHomClass.toRingHomClass AlgHom.algHomClass
map_toCotangent_ker 📖	mathematical	—	Submodule.map Submodule CommSemiring.toSemiring CommRing.toCommSemiring NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring Semiring.toModule SetLike.instMembership Submodule.setLike Submodule.addCommMonoid Submodule.module RingHom.id RingHomSurjective.ids Submodule.subtype LinearMap.ker Ideal Cotangent AddCommGroup.toAddCommMonoid instAddCommGroupCotangent instModuleCotangentOfAlgebra Algebra.id toCotangent Monoid.toNatPow MonoidWithZero.toMonoid Semiring.toMonoidWithZero IdemSemiring.toSemiring Submodule.idemSemiring	—	RingHomSurjective.ids toCotangent.eq_1 Submodule.ker_mkQ pow_two IsScalarTower.left Submodule.map_smul'' IsScalarTower.right smul_eq_mul Submodule.map_subtype_top
mem_toCotangent_ker 📖	mathematical	—	Ideal CommSemiring.toSemiring CommRing.toCommSemiring SetLike.instMembership Submodule.setLike NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring Semiring.toModule Submodule Submodule.addCommMonoid Submodule.module LinearMap.ker Cotangent AddCommGroup.toAddCommMonoid instAddCommGroupCotangent instModuleCotangentOfAlgebra Algebra.id RingHom.id toCotangent Monoid.toNatPow MonoidWithZero.toMonoid Semiring.toMonoidWithZero IdemSemiring.toSemiring Submodule.idemSemiring	—	RingHomSurjective.ids map_toCotangent_ker
mk_mem_cotangentIdeal 📖	mathematical	—	HasQuotient.Quotient Ideal Ring.toSemiring CommRing.toRing instHasQuotient CommSemiring.toSemiring CommRing.toCommSemiring Monoid.toNatPow MonoidWithZero.toMonoid Semiring.toMonoidWithZero IdemSemiring.toSemiring Submodule.idemSemiring Algebra.id instHasQuotient_1 Quotient.semiring SetLike.instMembership Submodule.setLike NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring Semiring.toModule cotangentIdeal DFunLike.coe RingHom Quotient.ring instIsTwoSided_1 RingHom.instFunLike	—	instIsTwoSided_1 sub_sub_cancel sub_mem Submodule.addSubgroupClass pow_le_self two_ne_zero IsScalarTower.left Quotient.mk_eq_mk_iff_sub_mem
range_cotangentToQuotientSquare 📖	mathematical	—	LinearMap.range Cotangent HasQuotient.Quotient Ideal CommSemiring.toSemiring CommRing.toCommSemiring instHasQuotient_1 Monoid.toNatPow MonoidWithZero.toMonoid Semiring.toMonoidWithZero IdemSemiring.toSemiring Submodule.idemSemiring Algebra.id AddCommGroup.toAddCommMonoid instAddCommGroupCotangent NonUnitalNonAssocSemiring.toAddCommMonoid NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing Quotient.commRing instModuleCotangentOfAlgebra Submodule.Quotient.module CommRing.toRing Ring.toAddCommGroup Semiring.toModule RingHom.id Semiring.toNonAssocSemiring RingHomSurjective.ids cotangentToQuotientSquare Submodule.restrictScalars Quotient.semiring NonAssocSemiring.toNonUnitalNonAssocSemiring Submodule.Quotient.instSMul IsScalarTower.right instAlgebraQuotient cotangentIdeal	—	RingHomSurjective.ids RingHomCompTriple.ids IsScalarTower.right LinearMap.range_comp toCotangent_range Submodule.map_top to_quotient_square_comp_toCotangent Submodule.range_subtype Submodule.ext
toCotangent_apply 📖	mathematical	—	DFunLike.coe LinearMap CommSemiring.toSemiring CommRing.toCommSemiring RingHom.id Semiring.toNonAssocSemiring Ideal SetLike.instMembership Submodule.setLike NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toModule Cotangent Submodule.addCommMonoid AddCommGroup.toAddCommMonoid instAddCommGroupCotangent Submodule.module instModuleCotangentOfAlgebra Algebra.id LinearMap.instFunLike toCotangent CommRing.toRing Submodule.addCommGroup Ring.toAddCommGroup Submodule Submodule.instSMul Top.top Submodule.instTop	—	—
toCotangent_eq 📖	mathematical	—	DFunLike.coe LinearMap CommSemiring.toSemiring CommRing.toCommSemiring RingHom.id Semiring.toNonAssocSemiring Ideal SetLike.instMembership Submodule.setLike NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toModule Cotangent Submodule.addCommMonoid AddCommGroup.toAddCommMonoid instAddCommGroupCotangent Submodule.module instModuleCotangentOfAlgebra Algebra.id LinearMap.instFunLike toCotangent Monoid.toNatPow MonoidWithZero.toMonoid Semiring.toMonoidWithZero IdemSemiring.toSemiring Submodule.idemSemiring SubNegMonoid.toSub AddGroup.toSubNegMonoid AddGroupWithOne.toAddGroup Ring.toAddGroupWithOne CommRing.toRing	—	sub_eq_zero mem_toCotangent_ker
toCotangent_eq_zero 📖	mathematical	—	DFunLike.coe LinearMap CommSemiring.toSemiring CommRing.toCommSemiring RingHom.id Semiring.toNonAssocSemiring Ideal SetLike.instMembership Submodule.setLike NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toModule Cotangent Submodule.addCommMonoid AddCommGroup.toAddCommMonoid instAddCommGroupCotangent Submodule.module instModuleCotangentOfAlgebra Algebra.id LinearMap.instFunLike toCotangent NegZeroClass.toZero SubNegZeroMonoid.toNegZeroClass SubtractionMonoid.toSubNegZeroMonoid SubtractionCommMonoid.toSubtractionMonoid AddCommGroup.toDivisionAddCommMonoid Monoid.toNatPow MonoidWithZero.toMonoid Semiring.toMonoidWithZero IdemSemiring.toSemiring Submodule.idemSemiring	—	mem_toCotangent_ker
toCotangent_range 📖	mathematical	—	LinearMap.range Ideal CommSemiring.toSemiring CommRing.toCommSemiring SetLike.instMembership Submodule.setLike NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring Semiring.toModule Cotangent Submodule.addCommMonoid AddCommGroup.toAddCommMonoid instAddCommGroupCotangent Submodule.module instModuleCotangentOfAlgebra Algebra.id RingHom.id RingHomSurjective.ids toCotangent Top.top Submodule Submodule.instTop	—	Submodule.range_mkQ
toCotangent_surjective 📖	mathematical	—	Ideal CommSemiring.toSemiring CommRing.toCommSemiring SetLike.instMembership Submodule.setLike NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring Semiring.toModule Cotangent DFunLike.coe LinearMap RingHom.id Submodule.addCommMonoid AddCommGroup.toAddCommMonoid instAddCommGroupCotangent Submodule.module instModuleCotangentOfAlgebra Algebra.id LinearMap.instFunLike toCotangent	—	Submodule.mkQ_surjective
toCotangent_to_quotient_square 📖	mathematical	—	DFunLike.coe LinearMap CommSemiring.toSemiring CommRing.toCommSemiring RingHom.id Semiring.toNonAssocSemiring Cotangent HasQuotient.Quotient Ideal instHasQuotient_1 Monoid.toNatPow MonoidWithZero.toMonoid Semiring.toMonoidWithZero IdemSemiring.toSemiring Submodule.idemSemiring Algebra.id AddCommGroup.toAddCommMonoid instAddCommGroupCotangent NonUnitalNonAssocSemiring.toAddCommMonoid NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing Quotient.commRing instModuleCotangentOfAlgebra Submodule.Quotient.module CommRing.toRing Ring.toAddCommGroup Semiring.toModule LinearMap.instFunLike cotangentToQuotientSquare SetLike.instMembership Submodule.setLike NonAssocSemiring.toNonUnitalNonAssocSemiring Submodule.addCommMonoid Submodule.module toCotangent Ring.toSemiring Submodule Submodule.hasQuotient Submodule.Quotient.addCommGroup Submodule.mkQ	—	—
to_quotient_square_comp_toCotangent 📖	mathematical	—	LinearMap.comp Ideal CommSemiring.toSemiring CommRing.toCommSemiring SetLike.instMembership Submodule.setLike NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring Semiring.toModule Cotangent HasQuotient.Quotient instHasQuotient_1 Monoid.toNatPow MonoidWithZero.toMonoid Semiring.toMonoidWithZero IdemSemiring.toSemiring Submodule.idemSemiring Algebra.id Submodule.addCommMonoid AddCommGroup.toAddCommMonoid instAddCommGroupCotangent NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing Quotient.commRing Submodule.module instModuleCotangentOfAlgebra Submodule.Quotient.module CommRing.toRing Ring.toAddCommGroup RingHom.id RingHomCompTriple.ids cotangentToQuotientSquare toCotangent Submodule Ring.toSemiring Submodule.hasQuotient Submodule.Quotient.addCommGroup Submodule.mkQ Submodule.subtype	—	LinearMap.ext RingHomCompTriple.ids

Ideal.Algebra

Definitions

Name	Category	Theorems
kerSquareLift 📖	CompOp	4 math math: Ideal.instIsScalarTowerQuotientHPowKerRingHomAlgebraMapOfNat, tensorKaehlerQuotKerSqEquiv_symm_tmul_D, tensorKaehlerQuotKerSqEquiv_tmul_D, derivationQuotKerSq_mk

Ideal.Cotangent

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
smul_eq_zero_of_mem 📖	mathematical	Ideal CommSemiring.toSemiring CommRing.toCommSemiring SetLike.instMembership Submodule.setLike NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring Semiring.toModule	Ideal.Cotangent SMulZeroClass.toSMul AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass SubNegMonoid.toAddMonoid AddGroup.toSubNegMonoid AddCommGroup.toAddGroup Ideal.instAddCommGroupCotangent DistribSMul.toSMulZeroClass DistribMulAction.toDistribSMul MonoidWithZero.toMonoid Semiring.toMonoidWithZero Module.toDistribMulAction AddCommGroup.toAddCommMonoid Ideal.instModuleCotangentOfAlgebra Algebra.id NegZeroClass.toZero SubNegZeroMonoid.toNegZeroClass SubtractionMonoid.toSubNegZeroMonoid SubtractionCommMonoid.toSubtractionMonoid AddCommGroup.toDivisionAddCommMonoid	—	Ideal.toCotangent_surjective IsScalarTower.right map_smul SemilinearMapClass.toMulActionSemiHomClass LinearMap.semilinearMapClass Ideal.toCotangent_eq_zero pow_two Ideal.mul_mem_mul

IsLocalRing

Definitions

Name	Category	Theorems
CotangentSpace 📖	CompOp	10 math math: finrank_CotangentSpace_eq_one_iff, finrank_cotangentSpace_eq_zero, finrank_CotangentSpace_eq_one, subsingleton_cotangentSpace_iff, finrank_cotangentSpace_eq_zero_iff, instFiniteDimensionalResidueFieldCotangentSpaceOfIsNoetherianRing, tfae_of_isNoetherianRing_of_isLocalRing_of_isDomain, finrank_cotangentSpace_le_one_iff, instIsScalarTowerResidueFieldCotangentSpace, IsDiscreteValuationRing.TFAE
instModuleResidueFieldCotangentSpace 📖	CompOp	10 math math: finrank_CotangentSpace_eq_one_iff, finrank_cotangentSpace_eq_zero, finrank_CotangentSpace_eq_one, finrank_cotangentSpace_eq_zero_iff, instFiniteDimensionalResidueFieldCotangentSpaceOfIsNoetherianRing, tfae_of_isNoetherianRing_of_isLocalRing_of_isDomain, finrank_cotangentSpace_le_one_iff, instIsScalarTowerResidueFieldCotangentSpace, IsDiscreteValuationRing.TFAE, CotangentSpace.span_image_eq_top_iff

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
finrank_cotangentSpace_eq_zero 📖	mathematical	—	Module.finrank ResidueField EuclideanDomain.toCommRing Field.toEuclideanDomain Field.instIsLocalRing CotangentSpace DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield ResidueField.field AddCommGroup.toAddCommMonoid Ideal.instAddCommGroupCotangent maximalIdeal CommRing.toCommSemiring instModuleResidueFieldCotangentSpace	—	Field.instIsLocalRing finrank_cotangentSpace_eq_zero_iff isNoetherian_of_isNoetherianRing_of_finite IsSimpleModule.instIsNoetherian instIsSimpleModule FiniteDimensional.finiteDimensional_self Field.toIsField
finrank_cotangentSpace_eq_zero_iff 📖	mathematical	—	Module.finrank ResidueField CotangentSpace DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield ResidueField.field AddCommGroup.toAddCommMonoid Ideal.instAddCommGroupCotangent maximalIdeal CommRing.toCommSemiring instModuleResidueFieldCotangentSpace IsField CommSemiring.toSemiring	—	Module.finrank_zero_iff IsNoetherianRing.strongRankCondition toNontrivial Field.instIsLocalRing IsSimpleModule.instIsNoetherian instIsSimpleModule instFiniteDimensionalResidueFieldCotangentSpaceOfIsNoetherianRing instIsDomain instIsTorsionFreeOfIsDomainOfNoZeroSMulDivisors GroupWithZero.toNoZeroSMulDivisors subsingleton_cotangentSpace_iff
finrank_cotangentSpace_le_one_iff 📖	mathematical	—	Module.finrank ResidueField CotangentSpace DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield ResidueField.field AddCommGroup.toAddCommMonoid Ideal.instAddCommGroupCotangent maximalIdeal CommRing.toCommSemiring instModuleResidueFieldCotangentSpace Submodule.IsPrincipal CommSemiring.toSemiring NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring Semiring.toModule	—	Module.finrank_le_one_iff_top_isPrincipal IsNoetherianRing.strongRankCondition toNontrivial Field.instIsLocalRing IsSimpleModule.instIsNoetherian instIsSimpleModule Module.Free.of_divisionRing Ideal.instIsTwoSided_1 instFiniteDimensionalResidueFieldCotangentSpaceOfIsNoetherianRing Submodule.isPrincipal_iff Function.Surjective.exists Ideal.toCotangent_surjective RingHomSurjective.ids Submodule.map_injective_of_injective Submodule.injective_subtype Submodule.map_span Set.image_singleton Submodule.map_top Submodule.range_subtype Submodule.subset_span Set.mem_singleton
instFiniteDimensionalResidueFieldCotangentSpaceOfIsNoetherianRing 📖	mathematical	—	FiniteDimensional ResidueField CotangentSpace Field.toDivisionRing ResidueField.field Ideal.instAddCommGroupCotangent maximalIdeal CommRing.toCommSemiring instModuleResidueFieldCotangentSpace	—	Module.Finite.of_restrictScalars_finite instIsScalarTowerResidueFieldCotangentSpace Module.IsNoetherian.finite isNoetherian_submodule'
instIsScalarTowerResidueFieldCotangentSpace 📖	mathematical	—	IsScalarTower ResidueField CotangentSpace Algebra.toSMul CommRing.toCommSemiring DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield ResidueField.field ResidueField.algebra Algebra.id SMulZeroClass.toSMul AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass SubNegMonoid.toAddMonoid AddGroup.toSubNegMonoid AddCommGroup.toAddGroup Ideal.instAddCommGroupCotangent maximalIdeal DistribSMul.toSMulZeroClass DistribMulAction.toDistribSMul MonoidWithZero.toMonoid Semiring.toMonoidWithZero Module.toDistribMulAction AddCommGroup.toAddCommMonoid instModuleResidueFieldCotangentSpace CommSemiring.toSemiring Ideal.instModuleCotangentOfAlgebra	—	Module.IsTorsionBySet.isScalarTower Ideal.instIsTwoSided_1 Module.isTorsionBySet_quotient_ideal_smul IsScalarTower.right
subsingleton_cotangentSpace_iff 📖	mathematical	—	CotangentSpace IsField CommSemiring.toSemiring CommRing.toCommSemiring	—	IsScalarTower.right Ideal.cotangent_subsingleton_iff isField_iff_maximalIdeal_eq Ideal.isIdempotentElem_iff_eq_bot_or_top_of_isLocalRing Ideal.IsMaximal.ne_top maximalIdeal.isMaximal

IsLocalRing.CotangentSpace

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
map_eq_top_iff 📖	mathematical	—	Submodule.map Ideal CommSemiring.toSemiring CommRing.toCommSemiring SetLike.instMembership Submodule.setLike NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring Semiring.toModule IsLocalRing.maximalIdeal Ideal.Cotangent Submodule.addCommMonoid AddCommGroup.toAddCommMonoid Ideal.instAddCommGroupCotangent Submodule.module Ideal.instModuleCotangentOfAlgebra Algebra.id RingHom.id RingHomSurjective.ids Ideal.toCotangent Top.top Submodule Submodule.instTop	—	RingHomSurjective.ids eq_top_iff Submodule.map_le_map_iff_of_injective Submodule.injective_subtype Submodule.map_top Submodule.range_subtype Submodule.le_of_le_smul_of_le_jacobson_bot IsNoetherian.noetherian Eq.ge IsLocalRing.jacobson_eq_maximalIdeal bot_ne_top Ideal.instNontrivial IsLocalRing.toNontrivial IsScalarTower.left IsScalarTower.right smul_eq_mul pow_two Ideal.map_toCotangent_ker Submodule.map_sup Submodule.comap_map_eq Submodule.comap_top le_refl Ideal.toCotangent_range
span_image_eq_top_iff 📖	mathematical	—	Submodule.span IsLocalRing.ResidueField Ideal.Cotangent IsLocalRing.maximalIdeal CommRing.toCommSemiring DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield IsLocalRing.ResidueField.field AddCommGroup.toAddCommMonoid Ideal.instAddCommGroupCotangent IsLocalRing.instModuleResidueFieldCotangentSpace Set.image Ideal CommSemiring.toSemiring SetLike.instMembership Submodule.setLike NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring Semiring.toModule DFunLike.coe LinearMap RingHom.id Submodule.addCommMonoid Submodule.module Ideal.instModuleCotangentOfAlgebra Algebra.id LinearMap.instFunLike Ideal.toCotangent Top.top Submodule Submodule.instTop	—	RingHomSurjective.ids map_eq_top_iff IsLocalRing.instIsScalarTowerResidueFieldCotangentSpace Submodule.restrictScalars_injective Submodule.restrictScalars_span Ideal.Quotient.mk_surjective Set.image_congr Submodule.map_span

---

← Back to Index