Injective

📁 Source: Mathlib/Algebra/Module/Injective.lean

Statistics

Metric	Count
Definitions Baer, ExtensionOf, inhabited, max, toLinearPMap, extendIdealTo, extensionToFun, fst, ideal, idealTo, snd, extensionOfMax, extensionOfMaxAdjoin, instMinExtensionOf, instPartialOrderExtensionOf, instSemilatticeInfExtensionOf, supExtensionOfMaxSingleton, Injective	18
Theorems dExt, dExt_iff, ext, is_extension, le, le_max, toLinearPMap_injective, eqn, extendIdealTo_eq, extendIdealTo_is_extension, extendIdealTo_wd, extendIdealTo_wd', extensionToFun_wd, chain_linearPMap_of_chain_extensionOf, extensionOfMax_is_max, extensionOfMax_le, extensionOfMax_to_submodule_eq_top, extension_property, extension_property_addMonoidHom, iff_injective, iff_surjective, injective, of_equiv, of_injective, extension_property, of_ringEquiv, out, pi, injective_iff, injective_iff_ulift_injective, injective_of_ulift_injective, ulift_injective_of_injective	32
Total	50

Module

Definitions

Name	Category	Theorems
Baer 📖	MathDef	7 math math: Baer.iff_surjective, Baer.of_equiv, Baer.iff_injective, Baer.of_injective, Baer.of_divisible, Baer.congr, Flat.iff_characterModule_baer
Injective 📖	CompData	16 math math: ulift_injective_of_injective, Baer.injective, Baer.iff_injective, injective_of_localization_maximal', Injective.of_ringEquiv, injective_of_ulift_injective, injective_iff_injective_object, injective_module_of_injective_object, injective_of_isLocalizedModule, injective_iff_ulift_injective, Injective.pi, injective_iff, Flat.injective_characterModule_iff_rTensor_preserves_injective_linearMap, injective_of_isSemisimpleRing, Flat.iff_characterModule_injective, injective_of_localization_maximal

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
injective_iff 📖	mathematical	—	Injective LinearMap Ring.toSemiring RingHom.id Semiring.toNonAssocSemiring AddCommGroup.toAddCommMonoid DFunLike.coe LinearMap.instFunLike	—	—
injective_iff_ulift_injective 📖	mathematical	—	Injective ULift.addCommGroup ULift.module' Ring.toSemiring AddCommGroup.toAddCommMonoid	—	ulift_injective_of_injective injective_of_ulift_injective
injective_of_ulift_injective 📖	mathematical	—	Injective	—	RingHomInvPair.ids RingHomCompTriple.ids Injective.out LinearEquiv.injective
ulift_injective_of_injective 📖	mathematical	—	Injective ULift.addCommGroup ULift.module' Ring.toSemiring AddCommGroup.toAddCommMonoid	—	Baer.injective RingHomCompTriple.ids RingHomInvPair.ids Baer.iff_injective ULift.ext

Module.Baer

Definitions

Name	Category	Theorems
ExtensionOf 📖	CompData	4 math math: chain_linearPMap_of_chain_extensionOf, extensionOfMax_le, ExtensionOf.toLinearPMap_injective, ExtensionOf.le_max
extensionOfMax 📖	CompOp	6 math math: ExtensionOfMaxAdjoin.extensionToFun_wd, extensionOfMax_le, ExtensionOfMaxAdjoin.extendIdealTo_eq, extensionOfMax_is_max, extensionOfMax_to_submodule_eq_top, ExtensionOfMaxAdjoin.eqn
extensionOfMaxAdjoin 📖	CompOp	1 math math: extensionOfMax_le
instMinExtensionOf 📖	CompOp	—
instPartialOrderExtensionOf 📖	CompOp	2 math math: extensionOfMax_le, ExtensionOf.le_max
instSemilatticeInfExtensionOf 📖	CompOp	—
supExtensionOfMaxSingleton 📖	CompOp	1 math math: ExtensionOfMaxAdjoin.eqn

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
chain_linearPMap_of_chain_extensionOf 📖	mathematical	IsChain ExtensionOf Preorder.toLE PartialOrder.toPreorder instPartialOrderExtensionOf	IsChain LinearPMap LinearPMap.le Set.image ExtensionOf ExtensionOf.toLinearPMap	—	—
extensionOfMax_is_max 📖	mathematical	ExtensionOf Preorder.toLE PartialOrder.toPreorder instPartialOrderExtensionOf extensionOfMax	extensionOfMax	—	IsMax.eq_of_ge zorn_le_nonempty ExtensionOf.le_max
extensionOfMax_le 📖	mathematical	Module.Baer	ExtensionOf Preorder.toLE PartialOrder.toPreorder instPartialOrderExtensionOf extensionOfMax extensionOfMaxAdjoin	—	le_sup_left ExtensionOfMaxAdjoin.extensionToFun_wd zero_smul add_zero map_zero AddMonoidHomClass.toZeroHomClass DistribMulActionSemiHomClass.toAddMonoidHomClass SemilinearMapClass.distribMulActionSemiHomClass LinearMap.semilinearMapClass
extensionOfMax_to_submodule_eq_top 📖	mathematical	Module.Baer	LinearPMap.domain ExtensionOf.toLinearPMap extensionOfMax Top.top Submodule Ring.toSemiring AddCommGroup.toAddCommMonoid Submodule.instTop	—	Submodule.eq_top_iff' extensionOfMax_is_max extensionOfMax_le extensionOfMaxAdjoin.eq_1 Submodule.mem_sup Submodule.zero_mem Submodule.mem_span_singleton_self zero_add
extension_property 📖	mathematical	Module.Baer DFunLike.coe LinearMap Ring.toSemiring RingHom.id Semiring.toNonAssocSemiring AddCommGroup.toAddCommMonoid LinearMap.instFunLike	LinearMap Ring.toSemiring RingHom.id Semiring.toNonAssocSemiring AddCommGroup.toAddCommMonoid LinearMap.comp RingHomCompTriple.ids	—	RingHomCompTriple.ids extensionOfMax_to_submodule_eq_top LinearPMap.map_add IsScalarTower.left LinearPMap.map_smul LinearMap.ext ExtensionOf.le ExtensionOf.is_extension
extension_property_addMonoidHom 📖	mathematical	Module.Baer Int.instRing AddCommGroup.toIntModule DFunLike.coe AddMonoidHom AddZeroClass.toAddZero AddMonoid.toAddZeroClass SubNegMonoid.toAddMonoid AddGroup.toSubNegMonoid AddCommGroup.toAddGroup AddMonoidHom.instFunLike	AddMonoidHom AddZeroClass.toAddZero AddMonoid.toAddZeroClass SubNegMonoid.toAddMonoid AddGroup.toSubNegMonoid AddCommGroup.toAddGroup AddMonoidHom.comp	—	RingHomCompTriple.ids extension_property DistribMulActionSemiHomClass.toAddMonoidHomClass SemilinearMapClass.distribMulActionSemiHomClass LinearMap.semilinearMapClass
iff_injective 📖	mathematical	—	Module.Baer Module.Injective	—	injective of_injective
iff_surjective 📖	mathematical	—	Module.Baer CommRing.toRing LinearMap CommSemiring.toSemiring CommRing.toCommSemiring RingHom.id Semiring.toNonAssocSemiring NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring AddCommGroup.toAddCommMonoid Semiring.toModule Submodule SetLike.instMembership Submodule.setLike Submodule.addCommMonoid Submodule.module DFunLike.coe LinearMap.addCommMonoid LinearMap.module smulCommClass_self CommRing.toCommMonoid DistribMulAction.toMulAction CommMonoid.toMonoid AddCommMonoid.toAddMonoid Module.toDistribMulAction Ring.toSemiring LinearMap.instFunLike LinearMap.lcomp Submodule.subtype	—	smulCommClass_self LinearMap.ext Subtype.coe_eta
injective 📖	mathematical	Module.Baer	Module.Injective	—	RingHomCompTriple.ids extension_property DFunLike.congr_fun
of_equiv 📖	mathematical	Module.Baer	Module.Baer	—	RingHomInvPair.ids RingHomCompTriple.ids
of_injective 📖	mathematical	—	Module.Baer	—	RingHomInvPair.ids small_subtype RingHomCompTriple.ids Module.Injective.out LinearEquiv.injective Subtype.val_injective Equiv.symm_apply_apply

Module.Baer.ExtensionOf

Definitions

Name	Category	Theorems
inhabited 📖	CompOp	—
max 📖	CompOp	1 math math: le_max
toLinearPMap 📖	CompOp	9 math math: Module.Baer.ExtensionOfMaxAdjoin.extensionToFun_wd, Module.Baer.chain_linearPMap_of_chain_extensionOf, Module.Baer.ExtensionOfMaxAdjoin.extendIdealTo_eq, is_extension, dExt_iff, Module.Baer.extensionOfMax_to_submodule_eq_top, le, Module.Baer.ExtensionOfMaxAdjoin.eqn, toLinearPMap_injective

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
dExt 📖	—	LinearPMap.domain toLinearPMap LinearPMap.toFun'	—	—	ext
dExt_iff 📖	mathematical	—	Submodule Ring.toSemiring AddCommGroup.toAddCommMonoid LinearPMap.domain toLinearPMap LinearPMap.toFun'	—	dExt
ext 📖	—	LinearPMap.domain toLinearPMap LinearPMap.toFun' Submodule Ring.toSemiring AddCommGroup.toAddCommMonoid SetLike.instMembership Submodule.setLike	—	—	RingHomSurjective.ids LinearPMap.ext
is_extension 📖	mathematical	—	DFunLike.coe LinearMap Ring.toSemiring RingHom.id Semiring.toNonAssocSemiring AddCommGroup.toAddCommMonoid LinearMap.instFunLike LinearPMap.toFun' toLinearPMap Submodule SetLike.instMembership Submodule.setLike LinearPMap.domain le	—	—
le 📖	mathematical	—	Submodule Ring.toSemiring AddCommGroup.toAddCommMonoid Preorder.toLE PartialOrder.toPreorder Submodule.instPartialOrder LinearMap.range RingHom.id Semiring.toNonAssocSemiring RingHomSurjective.ids LinearPMap.domain toLinearPMap	—	—
le_max 📖	mathematical	IsChain Module.Baer.ExtensionOf Preorder.toLE PartialOrder.toPreorder Module.Baer.instPartialOrderExtensionOf Set.Nonempty Set Set.instMembership	Module.Baer.ExtensionOf Preorder.toLE PartialOrder.toPreorder Module.Baer.instPartialOrderExtensionOf max	—	LinearPMap.le_sSup IsChain.directedOn instReflLe Module.Baer.chain_linearPMap_of_chain_extensionOf Set.mem_image
toLinearPMap_injective 📖	mathematical	—	Module.Baer.ExtensionOf LinearPMap toLinearPMap	—	ext Submodule.ext

Module.Baer.ExtensionOfMaxAdjoin

Definitions

Name	Category	Theorems
extendIdealTo 📖	CompOp	5 math math: extensionToFun_wd, extendIdealTo_wd, extendIdealTo_eq, extendIdealTo_is_extension, extendIdealTo_wd'
extensionToFun 📖	CompOp	1 math math: extensionToFun_wd
fst 📖	CompOp	1 math math: eqn
ideal 📖	CompOp	1 math math: extendIdealTo_is_extension
idealTo 📖	CompOp	1 math math: extendIdealTo_is_extension
snd 📖	CompOp	1 math math: eqn

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
eqn 📖	mathematical	—	Submodule Ring.toSemiring AddCommGroup.toAddCommMonoid SetLike.instMembership Submodule.setLike Module.Baer.supExtensionOfMaxSingleton AddCommMagma.toAdd AddCommSemigroup.toAddCommMagma AddCommMonoid.toAddCommSemigroup LinearPMap.domain Module.Baer.ExtensionOf.toLinearPMap Module.Baer.extensionOfMax fst SMulZeroClass.toSMul AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass SubNegMonoid.toAddMonoid AddGroup.toSubNegMonoid AddCommGroup.toAddGroup DistribSMul.toSMulZeroClass DistribMulAction.toDistribSMul MonoidWithZero.toMonoid Semiring.toMonoidWithZero Module.toDistribMulAction snd	—	—
extendIdealTo_eq 📖	mathematical	Module.Baer Submodule Ring.toSemiring AddCommGroup.toAddCommMonoid SetLike.instMembership Submodule.setLike LinearPMap.domain Module.Baer.ExtensionOf.toLinearPMap Module.Baer.extensionOfMax SMulZeroClass.toSMul AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass SubNegMonoid.toAddMonoid AddGroup.toSubNegMonoid AddCommGroup.toAddGroup DistribSMul.toSMulZeroClass DistribMulAction.toDistribSMul MonoidWithZero.toMonoid Semiring.toMonoidWithZero Module.toDistribMulAction	DFunLike.coe LinearMap Ring.toSemiring RingHom.id Semiring.toNonAssocSemiring NonUnitalNonAssocSemiring.toAddCommMonoid NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonAssocRing.toNonUnitalNonAssocRing Ring.toNonAssocRing AddCommGroup.toAddCommMonoid Semiring.toModule LinearMap.instFunLike extendIdealTo LinearPMap.toFun' Module.Baer.ExtensionOf.toLinearPMap Module.Baer.extensionOfMax Submodule SetLike.instMembership Submodule.setLike LinearPMap.domain SMulZeroClass.toSMul AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass SubNegMonoid.toAddMonoid AddGroup.toSubNegMonoid AddCommGroup.toAddGroup DistribSMul.toSMulZeroClass DistribMulAction.toDistribSMul MonoidWithZero.toMonoid Semiring.toMonoidWithZero Module.toDistribMulAction	—	extendIdealTo_is_extension
extendIdealTo_is_extension 📖	mathematical	Module.Baer Ideal Ring.toSemiring SetLike.instMembership Submodule.setLike NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring Semiring.toModule ideal	DFunLike.coe LinearMap Ring.toSemiring RingHom.id Semiring.toNonAssocSemiring NonUnitalNonAssocSemiring.toAddCommMonoid NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonAssocRing.toNonUnitalNonAssocRing Ring.toNonAssocRing AddCommGroup.toAddCommMonoid Semiring.toModule LinearMap.instFunLike extendIdealTo Ideal SetLike.instMembership Submodule.setLike NonAssocSemiring.toNonUnitalNonAssocSemiring ideal Submodule.addCommMonoid Submodule.module idealTo	—	—
extendIdealTo_wd 📖	mathematical	Module.Baer SMulZeroClass.toSMul AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass SubNegMonoid.toAddMonoid AddGroup.toSubNegMonoid AddCommGroup.toAddGroup DistribSMul.toSMulZeroClass DistribMulAction.toDistribSMul MonoidWithZero.toMonoid Semiring.toMonoidWithZero Ring.toSemiring Module.toDistribMulAction AddCommGroup.toAddCommMonoid	DFunLike.coe LinearMap Ring.toSemiring RingHom.id Semiring.toNonAssocSemiring NonUnitalNonAssocSemiring.toAddCommMonoid NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonAssocRing.toNonUnitalNonAssocRing Ring.toNonAssocRing AddCommGroup.toAddCommMonoid Semiring.toModule LinearMap.instFunLike extendIdealTo	—	sub_eq_zero map_sub DistribMulActionSemiHomClass.toAddMonoidHomClass SemilinearMapClass.distribMulActionSemiHomClass LinearMap.semilinearMapClass extendIdealTo_wd' sub_smul
extendIdealTo_wd' 📖	mathematical	Module.Baer SMulZeroClass.toSMul AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass SubNegMonoid.toAddMonoid AddGroup.toSubNegMonoid AddCommGroup.toAddGroup DistribSMul.toSMulZeroClass DistribMulAction.toDistribSMul MonoidWithZero.toMonoid Semiring.toMonoidWithZero Ring.toSemiring Module.toDistribMulAction AddCommGroup.toAddCommMonoid NegZeroClass.toZero SubNegZeroMonoid.toNegZeroClass SubtractionMonoid.toSubNegZeroMonoid SubtractionCommMonoid.toSubtractionMonoid AddCommGroup.toDivisionAddCommMonoid	DFunLike.coe LinearMap Ring.toSemiring RingHom.id Semiring.toNonAssocSemiring NonUnitalNonAssocSemiring.toAddCommMonoid NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonAssocRing.toNonUnitalNonAssocRing Ring.toNonAssocRing AddCommGroup.toAddCommMonoid Semiring.toModule LinearMap.instFunLike extendIdealTo NegZeroClass.toZero SubNegZeroMonoid.toNegZeroClass SubtractionMonoid.toSubNegZeroMonoid SubtractionCommMonoid.toSubtractionMonoid AddCommGroup.toDivisionAddCommMonoid	—	Submodule.zero_mem extendIdealTo_is_extension AddSubmonoidClass.toZeroMemClass Submodule.addSubmonoidClass LinearPMap.map_zero
extensionToFun_wd 📖	mathematical	Module.Baer Submodule Ring.toSemiring AddCommGroup.toAddCommMonoid SetLike.instMembership Submodule.setLike Module.Baer.supExtensionOfMaxSingleton AddCommMagma.toAdd AddCommSemigroup.toAddCommMagma AddCommMonoid.toAddCommSemigroup LinearPMap.domain Module.Baer.ExtensionOf.toLinearPMap Module.Baer.extensionOfMax SMulZeroClass.toSMul AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass SubNegMonoid.toAddMonoid AddGroup.toSubNegMonoid AddCommGroup.toAddGroup DistribSMul.toSMulZeroClass DistribMulAction.toDistribSMul MonoidWithZero.toMonoid Semiring.toMonoidWithZero Module.toDistribMulAction	extensionToFun AddCommMagma.toAdd AddCommSemigroup.toAddCommMagma AddCommMonoid.toAddCommSemigroup AddCommGroup.toAddCommMonoid LinearPMap.toFun' Module.Baer.ExtensionOf.toLinearPMap Module.Baer.extensionOfMax DFunLike.coe LinearMap Ring.toSemiring RingHom.id Semiring.toNonAssocSemiring NonUnitalNonAssocSemiring.toAddCommMonoid NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonAssocRing.toNonUnitalNonAssocRing Ring.toNonAssocRing Semiring.toModule LinearMap.instFunLike extendIdealTo	—	sub_smul sub_eq_zero sub_sub_sub_eq eqn Submodule.sub_mem extendIdealTo_eq map_sub DistribMulActionSemiHomClass.toAddMonoidHomClass SemilinearMapClass.distribMulActionSemiHomClass LinearMap.semilinearMapClass add_assoc LinearPMap.map_add AddMemClass.add_mem AddSubmonoidClass.toAddMemClass Submodule.addSubmonoidClass add_sub eq_sub_of_add_eq

Module.Injective

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
extension_property 📖	mathematical	DFunLike.coe LinearMap Ring.toSemiring RingHom.id Semiring.toNonAssocSemiring AddCommGroup.toAddCommMonoid LinearMap.instFunLike	LinearMap Ring.toSemiring RingHom.id Semiring.toNonAssocSemiring AddCommGroup.toAddCommMonoid LinearMap.comp RingHomCompTriple.ids	—	Module.Baer.extension_property Module.Baer.of_injective
of_ringEquiv 📖	mathematical	—	Module.Injective	—	RingEquivClass.toRingHomClass RingEquiv.instRingEquivClass RingHomInvPair.of_ringEquiv Module.Baer.injective RingHomSurjective.instToRingHomRingEquiv RingHomInvPair.symm RingHomSurjective.invPair RingHomInvPair.triples RingHomCompTriple.right_ids Module.Baer.of_injective RingHomInvPair.triples₂ EquivLike.apply_coe_symm_apply LinearEquiv.apply_symm_apply
out 📖	mathematical	DFunLike.coe LinearMap Ring.toSemiring RingHom.id Semiring.toNonAssocSemiring AddCommGroup.toAddCommMonoid LinearMap.instFunLike	LinearMap Ring.toSemiring RingHom.id Semiring.toNonAssocSemiring AddCommGroup.toAddCommMonoid DFunLike.coe LinearMap.instFunLike	—	—
pi 📖	mathematical	Module.Injective	Module.Injective Pi.addCommGroup Pi.module Ring.toSemiring AddCommGroup.toAddCommMonoid	—	RingHomCompTriple.ids DFunLike.congr_fun extension_property

---

← Back to Index