QuotSMulTop

📁 Source: Mathlib/RingTheory/QuotSMulTop.lean

Statistics

Metric	Count
Definitions QuotSMulTop, algebraMapTensorEquivTensorQuotSMulTop, equivQuotTensor, equivTensorQuot, map, quotSMulTopTensorEquivQuotSMulTop, tensorQuotSMulTopEquivQuotSMulTop	7
Theorems equivQuotTensor_naturality, equivQuotTensor_naturality_mk, equivTensorQuot_naturality, equivTensorQuot_naturality_mk, map_apply_mk, map_comp, map_comp_mkQ, map_exact, map_id, map_surjective	10
Total	17

QuotSMulTop

Definitions

Name	Category	Theorems
algebraMapTensorEquivTensorQuotSMulTop 📖	CompOp	—
equivQuotTensor 📖	CompOp	2 math math: equivQuotTensor_naturality, equivQuotTensor_naturality_mk
equivTensorQuot 📖	CompOp	2 math math: equivTensorQuot_naturality, equivTensorQuot_naturality_mk
map 📖	CompOp	12 math math: equivTensorQuot_naturality, equivTensorQuot_naturality_mk, map_comp_mkQ, map_surjective, equivQuotTensor_naturality, Submodule.quotOfListConsSMulTopEquivQuotSMulTopInner_naturality, map_exact, equivQuotTensor_naturality_mk, map_first_exact_on_four_term_exact_of_isSMulRegular_last, map_comp, map_apply_mk, map_id
quotSMulTopTensorEquivQuotSMulTop 📖	CompOp	—
tensorQuotSMulTopEquivQuotSMulTop 📖	CompOp	—

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
equivQuotTensor_naturality 📖	mathematical	—	LinearMap.comp QuotSMulTop TensorProduct CommRing.toCommSemiring HasQuotient.Quotient Ideal CommSemiring.toSemiring Ideal.instHasQuotient_1 Ideal.span Set Set.instSingletonSet NonUnitalNonAssocSemiring.toAddCommMonoid NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing Ideal.Quotient.commRing AddCommGroup.toAddCommMonoid Submodule.Quotient.module CommRing.toRing Ring.toAddCommGroup Semiring.toModule Submodule.Quotient.addCommGroup Submodule SMulZeroClass.toSMul AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass AddCommMonoid.toAddMonoid Submodule.pointwiseAddCommMonoid DistribSMul.toSMulZeroClass DistribMulAction.toDistribSMul MonoidWithZero.toMonoid Semiring.toMonoidWithZero Submodule.pointwiseDistribMulAction Module.toDistribMulAction Top.top Submodule.instTop TensorProduct.addCommMonoid TensorProduct.instModule RingHom.id Semiring.toNonAssocSemiring RingHomCompTriple.ids LinearEquiv.toLinearMap RingHomInvPair.ids equivQuotTensor DFunLike.coe LinearMap LinearMap.addCommMonoid LinearMap.module smulCommClass_self CommRing.toCommMonoid DistribMulAction.toMulAction CommMonoid.toMonoid Ring.toSemiring Submodule.Quotient.smulCommClass AddMonoidWithOne.toAddMonoid AddGroupWithOne.toAddMonoidWithOne Ring.toAddGroupWithOne instDistribSMul NonAssocRing.toNonUnitalNonAssocRing Ring.toNonAssocRing SemigroupAction.toSMul Monoid.toSemigroup MulAction.toSemigroupAction SubNegMonoid.toAddMonoid AddGroup.toSubNegMonoid AddCommGroup.toAddGroup LinearMap.instFunLike map LinearMap.lTensor	—	Submodule.quot_hom_ext RingHomCompTriple.ids RingHomInvPair.ids smulCommClass_self Submodule.Quotient.smulCommClass
equivQuotTensor_naturality_mk 📖	mathematical	—	DFunLike.coe LinearEquiv CommSemiring.toSemiring CommRing.toCommSemiring RingHom.id Semiring.toNonAssocSemiring RingHomInvPair.ids QuotSMulTop TensorProduct HasQuotient.Quotient Ideal Ideal.instHasQuotient_1 Ideal.span Set Set.instSingletonSet NonUnitalNonAssocSemiring.toAddCommMonoid NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing Ideal.Quotient.commRing AddCommGroup.toAddCommMonoid Submodule.Quotient.module CommRing.toRing Ring.toAddCommGroup Semiring.toModule Submodule.Quotient.addCommGroup Submodule SMulZeroClass.toSMul AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass AddCommMonoid.toAddMonoid Submodule.pointwiseAddCommMonoid DistribSMul.toSMulZeroClass DistribMulAction.toDistribSMul MonoidWithZero.toMonoid Semiring.toMonoidWithZero Submodule.pointwiseDistribMulAction Module.toDistribMulAction Top.top Submodule.instTop TensorProduct.addCommMonoid TensorProduct.instModule EquivLike.toFunLike DFinsupp.instEquivLikeLinearEquiv equivQuotTensor LinearMap LinearMap.instFunLike LinearMap.addCommMonoid LinearMap.module smulCommClass_self CommRing.toCommMonoid DistribMulAction.toMulAction CommMonoid.toMonoid Ring.toSemiring Submodule.Quotient.smulCommClass AddMonoidWithOne.toAddMonoid AddGroupWithOne.toAddMonoidWithOne Ring.toAddGroupWithOne instDistribSMul NonAssocRing.toNonUnitalNonAssocRing Ring.toNonAssocRing SemigroupAction.toSMul Monoid.toSemigroup MulAction.toSemigroupAction SubNegMonoid.toAddMonoid AddGroup.toSubNegMonoid AddCommGroup.toAddGroup map LinearMap.lTensor	—	LinearMap.lTensor_tmul
equivTensorQuot_naturality 📖	mathematical	—	LinearMap.comp QuotSMulTop TensorProduct CommRing.toCommSemiring HasQuotient.Quotient Ideal CommSemiring.toSemiring Ideal.instHasQuotient_1 Ideal.span Set Set.instSingletonSet AddCommGroup.toAddCommMonoid NonUnitalNonAssocSemiring.toAddCommMonoid NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing Ideal.Quotient.commRing Submodule.Quotient.module CommRing.toRing Ring.toAddCommGroup Semiring.toModule Submodule.Quotient.addCommGroup Submodule SMulZeroClass.toSMul AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass AddCommMonoid.toAddMonoid Submodule.pointwiseAddCommMonoid DistribSMul.toSMulZeroClass DistribMulAction.toDistribSMul MonoidWithZero.toMonoid Semiring.toMonoidWithZero Submodule.pointwiseDistribMulAction Module.toDistribMulAction Top.top Submodule.instTop TensorProduct.addCommMonoid TensorProduct.instModule RingHom.id Semiring.toNonAssocSemiring RingHomCompTriple.ids LinearEquiv.toLinearMap RingHomInvPair.ids equivTensorQuot DFunLike.coe LinearMap LinearMap.addCommMonoid LinearMap.module smulCommClass_self CommRing.toCommMonoid DistribMulAction.toMulAction CommMonoid.toMonoid Ring.toSemiring Submodule.Quotient.smulCommClass AddMonoidWithOne.toAddMonoid AddGroupWithOne.toAddMonoidWithOne Ring.toAddGroupWithOne instDistribSMul NonAssocRing.toNonUnitalNonAssocRing Ring.toNonAssocRing SemigroupAction.toSMul Monoid.toSemigroup MulAction.toSemigroupAction SubNegMonoid.toAddMonoid AddGroup.toSubNegMonoid AddCommGroup.toAddGroup LinearMap.instFunLike map LinearMap.rTensor	—	Submodule.quot_hom_ext RingHomCompTriple.ids RingHomInvPair.ids smulCommClass_self Submodule.Quotient.smulCommClass
equivTensorQuot_naturality_mk 📖	mathematical	—	DFunLike.coe LinearEquiv CommSemiring.toSemiring CommRing.toCommSemiring RingHom.id Semiring.toNonAssocSemiring RingHomInvPair.ids QuotSMulTop TensorProduct HasQuotient.Quotient Ideal Ideal.instHasQuotient_1 Ideal.span Set Set.instSingletonSet AddCommGroup.toAddCommMonoid NonUnitalNonAssocSemiring.toAddCommMonoid NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing Ideal.Quotient.commRing Submodule.Quotient.module CommRing.toRing Ring.toAddCommGroup Semiring.toModule Submodule.Quotient.addCommGroup Submodule SMulZeroClass.toSMul AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass AddCommMonoid.toAddMonoid Submodule.pointwiseAddCommMonoid DistribSMul.toSMulZeroClass DistribMulAction.toDistribSMul MonoidWithZero.toMonoid Semiring.toMonoidWithZero Submodule.pointwiseDistribMulAction Module.toDistribMulAction Top.top Submodule.instTop TensorProduct.addCommMonoid TensorProduct.instModule EquivLike.toFunLike DFinsupp.instEquivLikeLinearEquiv equivTensorQuot LinearMap LinearMap.instFunLike LinearMap.addCommMonoid LinearMap.module smulCommClass_self CommRing.toCommMonoid DistribMulAction.toMulAction CommMonoid.toMonoid Ring.toSemiring Submodule.Quotient.smulCommClass AddMonoidWithOne.toAddMonoid AddGroupWithOne.toAddMonoidWithOne Ring.toAddGroupWithOne instDistribSMul NonAssocRing.toNonUnitalNonAssocRing Ring.toNonAssocRing SemigroupAction.toSMul Monoid.toSemigroup MulAction.toSemigroupAction SubNegMonoid.toAddMonoid AddGroup.toSubNegMonoid AddCommGroup.toAddGroup map LinearMap.rTensor	—	LinearMap.rTensor_tmul
map_apply_mk 📖	mathematical	—	DFunLike.coe LinearMap CommSemiring.toSemiring CommRing.toCommSemiring RingHom.id Semiring.toNonAssocSemiring QuotSMulTop AddCommGroup.toAddCommMonoid Submodule.Quotient.addCommGroup CommRing.toRing Submodule SMulZeroClass.toSMul AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass AddCommMonoid.toAddMonoid Submodule.pointwiseAddCommMonoid DistribSMul.toSMulZeroClass DistribMulAction.toDistribSMul MonoidWithZero.toMonoid Semiring.toMonoidWithZero Submodule.pointwiseDistribMulAction Module.toDistribMulAction Top.top Submodule.instTop Submodule.Quotient.module LinearMap.instFunLike LinearMap.addCommMonoid LinearMap.module smulCommClass_self CommRing.toCommMonoid DistribMulAction.toMulAction CommMonoid.toMonoid Ring.toSemiring Submodule.Quotient.smulCommClass AddMonoidWithOne.toAddMonoid AddGroupWithOne.toAddMonoidWithOne Ring.toAddGroupWithOne instDistribSMul NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonAssocRing.toNonUnitalNonAssocRing Ring.toNonAssocRing SemigroupAction.toSMul Monoid.toSemigroup MulAction.toSemigroupAction SubNegMonoid.toAddMonoid AddGroup.toSubNegMonoid AddCommGroup.toAddGroup map	—	smulCommClass_self Submodule.Quotient.smulCommClass
map_comp 📖	mathematical	—	DFunLike.coe LinearMap CommSemiring.toSemiring CommRing.toCommSemiring RingHom.id Semiring.toNonAssocSemiring AddCommGroup.toAddCommMonoid QuotSMulTop Submodule.Quotient.addCommGroup CommRing.toRing Submodule SMulZeroClass.toSMul AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass AddCommMonoid.toAddMonoid Submodule.pointwiseAddCommMonoid DistribSMul.toSMulZeroClass DistribMulAction.toDistribSMul MonoidWithZero.toMonoid Semiring.toMonoidWithZero Submodule.pointwiseDistribMulAction Module.toDistribMulAction Top.top Submodule.instTop Submodule.Quotient.module LinearMap.addCommMonoid LinearMap.module smulCommClass_self CommRing.toCommMonoid DistribMulAction.toMulAction CommMonoid.toMonoid Ring.toSemiring Submodule.Quotient.smulCommClass AddMonoidWithOne.toAddMonoid AddGroupWithOne.toAddMonoidWithOne Ring.toAddGroupWithOne instDistribSMul NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonAssocRing.toNonUnitalNonAssocRing Ring.toNonAssocRing SemigroupAction.toSMul Monoid.toSemigroup MulAction.toSemigroupAction SubNegMonoid.toAddMonoid AddGroup.toSubNegMonoid AddCommGroup.toAddGroup LinearMap.instFunLike map LinearMap.comp RingHomCompTriple.ids	—	DFunLike.ext smulCommClass_self Submodule.Quotient.smulCommClass RingHomCompTriple.ids Function.Surjective.forall Submodule.mkQ_surjective
map_comp_mkQ 📖	mathematical	—	LinearMap.comp QuotSMulTop CommSemiring.toSemiring CommRing.toCommSemiring AddCommGroup.toAddCommMonoid Submodule.Quotient.addCommGroup CommRing.toRing Submodule SMulZeroClass.toSMul AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass AddCommMonoid.toAddMonoid Submodule.pointwiseAddCommMonoid DistribSMul.toSMulZeroClass DistribMulAction.toDistribSMul MonoidWithZero.toMonoid Semiring.toMonoidWithZero Submodule.pointwiseDistribMulAction Module.toDistribMulAction Top.top Submodule.instTop Submodule.Quotient.module RingHom.id Semiring.toNonAssocSemiring RingHomCompTriple.ids DFunLike.coe LinearMap LinearMap.addCommMonoid LinearMap.module smulCommClass_self CommRing.toCommMonoid DistribMulAction.toMulAction CommMonoid.toMonoid Ring.toSemiring Submodule.Quotient.smulCommClass AddMonoidWithOne.toAddMonoid AddGroupWithOne.toAddMonoidWithOne Ring.toAddGroupWithOne instDistribSMul NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonAssocRing.toNonUnitalNonAssocRing Ring.toNonAssocRing SemigroupAction.toSMul Monoid.toSemigroup MulAction.toSemigroupAction SubNegMonoid.toAddMonoid AddGroup.toSubNegMonoid AddCommGroup.toAddGroup LinearMap.instFunLike map Submodule.mkQ HasQuotient.Quotient Submodule.hasQuotient	—	LinearMap.ext RingHomCompTriple.ids smulCommClass_self Submodule.Quotient.smulCommClass
map_exact 📖	mathematical	Function.Exact DFunLike.coe LinearMap CommSemiring.toSemiring CommRing.toCommSemiring RingHom.id Semiring.toNonAssocSemiring AddCommGroup.toAddCommMonoid LinearMap.instFunLike NegZeroClass.toZero SubNegZeroMonoid.toNegZeroClass SubtractionMonoid.toSubNegZeroMonoid SubtractionCommMonoid.toSubtractionMonoid AddCommGroup.toDivisionAddCommMonoid	QuotSMulTop Submodule.Quotient.addCommGroup CommRing.toRing Submodule SMulZeroClass.toSMul AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass AddCommMonoid.toAddMonoid Submodule.pointwiseAddCommMonoid DistribSMul.toSMulZeroClass DistribMulAction.toDistribSMul MonoidWithZero.toMonoid Semiring.toMonoidWithZero Submodule.pointwiseDistribMulAction Module.toDistribMulAction Top.top Submodule.instTop Submodule.Quotient.module LinearMap.addCommMonoid LinearMap.module smulCommClass_self CommRing.toCommMonoid DistribMulAction.toMulAction CommMonoid.toMonoid Ring.toSemiring Submodule.Quotient.smulCommClass AddMonoidWithOne.toAddMonoid AddGroupWithOne.toAddMonoidWithOne Ring.toAddGroupWithOne instDistribSMul NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonAssocRing.toNonUnitalNonAssocRing Ring.toNonAssocRing SemigroupAction.toSMul Monoid.toSemigroup MulAction.toSemigroupAction SubNegMonoid.toAddMonoid AddGroup.toSubNegMonoid AddCommGroup.toAddGroup map Submodule.Quotient.instZeroQuotient	—	smulCommClass_self Submodule.Quotient.smulCommClass Function.Exact.iff_of_ladder_linearEquiv RingHomCompTriple.ids RingHomInvPair.ids equivQuotTensor_naturality lTensor_exact
map_id 📖	mathematical	—	DFunLike.coe LinearMap CommSemiring.toSemiring CommRing.toCommSemiring RingHom.id Semiring.toNonAssocSemiring AddCommGroup.toAddCommMonoid QuotSMulTop Submodule.Quotient.addCommGroup CommRing.toRing Submodule SMulZeroClass.toSMul AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass AddCommMonoid.toAddMonoid Submodule.pointwiseAddCommMonoid DistribSMul.toSMulZeroClass DistribMulAction.toDistribSMul MonoidWithZero.toMonoid Semiring.toMonoidWithZero Submodule.pointwiseDistribMulAction Module.toDistribMulAction Top.top Submodule.instTop Submodule.Quotient.module LinearMap.addCommMonoid LinearMap.module smulCommClass_self CommRing.toCommMonoid DistribMulAction.toMulAction CommMonoid.toMonoid Ring.toSemiring Submodule.Quotient.smulCommClass AddMonoidWithOne.toAddMonoid AddGroupWithOne.toAddMonoidWithOne Ring.toAddGroupWithOne instDistribSMul NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonAssocRing.toNonUnitalNonAssocRing Ring.toNonAssocRing SemigroupAction.toSMul Monoid.toSemigroup MulAction.toSemigroupAction SubNegMonoid.toAddMonoid AddGroup.toSubNegMonoid AddCommGroup.toAddGroup LinearMap.instFunLike map LinearMap.id	—	DFunLike.ext smulCommClass_self Submodule.Quotient.smulCommClass Function.Surjective.forall Submodule.mkQ_surjective
map_surjective 📖	mathematical	DFunLike.coe LinearMap CommSemiring.toSemiring CommRing.toCommSemiring RingHom.id Semiring.toNonAssocSemiring AddCommGroup.toAddCommMonoid LinearMap.instFunLike	QuotSMulTop Submodule.Quotient.addCommGroup CommRing.toRing Submodule SMulZeroClass.toSMul AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass AddCommMonoid.toAddMonoid Submodule.pointwiseAddCommMonoid DistribSMul.toSMulZeroClass DistribMulAction.toDistribSMul MonoidWithZero.toMonoid Semiring.toMonoidWithZero Submodule.pointwiseDistribMulAction Module.toDistribMulAction Top.top Submodule.instTop Submodule.Quotient.module LinearMap.addCommMonoid LinearMap.module smulCommClass_self CommRing.toCommMonoid DistribMulAction.toMulAction CommMonoid.toMonoid Ring.toSemiring Submodule.Quotient.smulCommClass AddMonoidWithOne.toAddMonoid AddGroupWithOne.toAddMonoidWithOne Ring.toAddGroupWithOne instDistribSMul NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonAssocRing.toNonUnitalNonAssocRing Ring.toNonAssocRing SemigroupAction.toSMul Monoid.toSemigroup MulAction.toSemigroupAction SubNegMonoid.toAddMonoid AddGroup.toSubNegMonoid AddCommGroup.toAddGroup map	—	smulCommClass_self Submodule.mkQ_surjective Function.Surjective.of_comp Submodule.Quotient.smulCommClass RingHomCompTriple.ids LinearMap.coe_comp map_comp_mkQ

(root)

Definitions

Name	Category	Theorems
QuotSMulTop 📖	CompOp	29 math math: RingTheory.Sequence.isWeaklyRegular_cons_iff', RingTheory.Sequence.isWeaklyRegular_cons_iff, QuotSMulTop.equivTensorQuot_naturality, Submodule.top_eq_ofList_cons_smul_iff, RingTheory.Sequence.isRegular_cons_iff, QuotSMulTop.equivTensorQuot_naturality_mk, QuotSMulTop.map_comp_mkQ, ringKrullDim_quotSMulTop_succ_eq_ringKrullDim_of_mem_jacobson, ringKrullDim_quotSMulTop_succ_eq_ringKrullDim, QuotSMulTop.map_surjective, Module.supportDim_quotSMulTop_succ_eq_of_notMem_minimalPrimes_of_mem_maximalIdeal, ModuleCat.smulShortComplex_g, QuotSMulTop.equivQuotTensor_naturality, Submodule.quotOfListConsSMulTopEquivQuotSMulTopInner_naturality, ModuleCat.smulShortComplex_X₃_carrier, QuotSMulTop.map_exact, Module.supportDim_quotSMulTop_succ_eq_supportDim, Module.supportDim_le_supportDim_quotSMulTop_succ, QuotSMulTop.equivQuotTensor_naturality_mk, Module.supportDim_quotSMulTop_succ_eq_supportDim_mem_jacobson, Module.support_quotSMulTop, QuotSMulTop.map_first_exact_on_four_term_exact_of_isSMulRegular_last, Module.supportDim_le_supportDim_quotSMulTop_succ_of_mem_jacobson, QuotSMulTop.map_comp, QuotSMulTop.map_apply_mk, Module.supportDim_quotSMulTop_succ_eq_of_notMem_minimalPrimes_of_mem_jacobson, QuotSMulTop.map_id, Module.supportDim_quotSMulTop_succ_le_of_notMem_minimalPrimes, RingTheory.Sequence.isRegular_cons_iff'

---

← Back to Index