DirectLimitFG

📁 Source: Mathlib/RingTheory/TensorProduct/DirectLimitFG.lean

Statistics

Metric	Count
Definitions directLimit, directLimit, directLimit	3
Theorems lTensor, rTensor, directedSystem, directLimit_apply, directLimit_apply', directedSystem, directLimit_apply, directLimit_apply', directedSystem, exists_fg_of_baseChange_eq_zero, eq_of_fg_of_subtype_eq, eq_of_fg_of_subtype_eq', exists_of_fg, eq_of_fg_of_subtype_eq, eq_of_fg_of_subtype_eq', eq_zero_of_fg_of_subtype_eq_zero, exists_of_fg	17
Total	20

DirectedSystem

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
lTensor 📖	mathematical	—	DirectedSystem TensorProduct DFunLike.coe LinearMap CommSemiring.toSemiring RingHom.id Semiring.toNonAssocSemiring TensorProduct.addCommMonoid TensorProduct.instModule LinearMap.instFunLike LinearMap.lTensor	—	le_rfl LinearMap.id_apply DFunLike.congr_fun TensorProduct.AlgebraTensorModule.curry_injective IsScalarTower.left TensorProduct.isScalarTower LinearMap.ext IsScalarTower.to_smulCommClass map_self LE.le.trans RingHomCompTriple.ids LinearMap.comp_apply LinearMap.lTensor_comp map_map
rTensor 📖	mathematical	—	DirectedSystem TensorProduct DFunLike.coe LinearMap CommSemiring.toSemiring RingHom.id Semiring.toNonAssocSemiring TensorProduct.addCommMonoid TensorProduct.instModule LinearMap.instFunLike LinearMap.rTensor	—	le_rfl LinearMap.id_apply DFunLike.congr_fun TensorProduct.AlgebraTensorModule.curry_injective IsScalarTower.left TensorProduct.isScalarTower LinearMap.ext IsScalarTower.to_smulCommClass map_self LE.le.trans RingHomCompTriple.ids LinearMap.comp_apply LinearMap.rTensor_comp map_map

Submodule

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
exists_fg_of_baseChange_eq_zero 📖	mathematical	DFunLike.coe LinearMap RingHom.id Semiring.toNonAssocSemiring TensorProduct NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring Algebra.toModule TensorProduct.addCommMonoid TensorProduct.leftModule Semiring.toModule Algebra.to_smulCommClass LinearMap.instFunLike LinearMap.baseChange TensorProduct.zero	Subalgebra SetLike.instMembership Subalgebra.instSetLike Subalgebra.toSemiring Subalgebra.algebra CommSemiring.toSemiring TensorProduct.instModule LinearMap.rTensor AlgHom.toLinearMap Subalgebra.val	—	Algebra.to_smulCommClass RingHomSurjective.ids TensorProduct.Algebra.exists_of_fg TensorProduct.Algebra.eq_of_fg_of_subtype_eq LinearMap.rTensor_baseChange map_zero AddMonoidHomClass.toZeroHomClass DistribMulActionSemiHomClass.toAddMonoidHomClass SemilinearMapClass.distribMulActionSemiHomClass LinearMap.semilinearMapClass RingHomCompTriple.ids LinearMap.comp_apply LinearMap.rTensor_comp

Submodule.FG

Definitions

Name	Category	Theorems
directLimit 📖	CompOp	—

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
directedSystem 📖	mathematical	—	DirectedSystem Submodule Submodule.FG Subtype.preorder PartialOrder.toPreorder Submodule.instPartialOrder SetLike.instMembership Submodule.setLike DFunLike.coe LinearMap RingHom.id Semiring.toNonAssocSemiring Submodule.addCommMonoid Submodule.module LinearMap.instFunLike Submodule.inclusion	—	le_rfl

Submodule.FG.lTensor

Definitions

Name	Category	Theorems
directLimit 📖	CompOp	2 math math: directLimit_apply', directLimit_apply

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
directLimit_apply 📖	mathematical	—	DFunLike.coe LinearEquiv CommSemiring.toSemiring RingHom.id Semiring.toNonAssocSemiring RingHomInvPair.ids Module.DirectLimit Submodule Submodule.FG Subtype.preorder PartialOrder.toPreorder Submodule.instPartialOrder TensorProduct SetLike.instMembership Submodule.setLike Submodule.addCommMonoid Submodule.module TensorProduct.addCommMonoid TensorProduct.instModule LinearMap.lTensor Submodule.inclusion Module.DirectLimit.addCommMonoid Module.DirectLimit.module EquivLike.toFunLike DFinsupp.instEquivLikeLinearEquiv directLimit LinearMap LinearMap.instFunLike Module.DirectLimit.of Submodule.subtype	—	RingHomCompTriple.ids RingHomInvPair.ids TensorProduct.AlgebraTensorModule.curry_injective IsScalarTower.left TensorProduct.isScalarTower LinearMap.ext IsScalarTower.to_smulCommClass TensorProduct.directLimitRight_symm_of_tmul Module.DirectLimit.lift_of DFunLike.congr_fun
directLimit_apply' 📖	mathematical	Submodule.FG CommSemiring.toSemiring	DFunLike.coe LinearEquiv RingHom.id Semiring.toNonAssocSemiring RingHomInvPair.ids Module.DirectLimit Submodule Subtype.preorder PartialOrder.toPreorder Submodule.instPartialOrder TensorProduct SetLike.instMembership Submodule.setLike Submodule.addCommMonoid Submodule.module TensorProduct.addCommMonoid TensorProduct.instModule LinearMap.lTensor Submodule.inclusion Module.DirectLimit.addCommMonoid Module.DirectLimit.module EquivLike.toFunLike DFinsupp.instEquivLikeLinearEquiv directLimit LinearMap LinearMap.instFunLike Module.DirectLimit.of Submodule.subtype	—	directLimit_apply
directedSystem 📖	mathematical	—	DirectedSystem Submodule CommSemiring.toSemiring Submodule.FG Subtype.preorder PartialOrder.toPreorder Submodule.instPartialOrder TensorProduct SetLike.instMembership Submodule.setLike Submodule.addCommMonoid Submodule.module DFunLike.coe LinearMap RingHom.id Semiring.toNonAssocSemiring TensorProduct.addCommMonoid TensorProduct.instModule LinearMap.instFunLike LinearMap.lTensor Submodule.inclusion	—	DirectedSystem.lTensor Submodule.FG.directedSystem

Submodule.FG.rTensor

Definitions

Name	Category	Theorems
directLimit 📖	CompOp	2 math math: directLimit_apply, directLimit_apply'

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
directLimit_apply 📖	mathematical	—	DFunLike.coe LinearEquiv CommSemiring.toSemiring RingHom.id Semiring.toNonAssocSemiring RingHomInvPair.ids Module.DirectLimit Submodule Submodule.FG Subtype.preorder PartialOrder.toPreorder Submodule.instPartialOrder TensorProduct SetLike.instMembership Submodule.setLike Submodule.addCommMonoid Submodule.module TensorProduct.addCommMonoid TensorProduct.instModule LinearMap.rTensor Submodule.inclusion Module.DirectLimit.addCommMonoid Module.DirectLimit.module EquivLike.toFunLike DFinsupp.instEquivLikeLinearEquiv directLimit LinearMap LinearMap.instFunLike Module.DirectLimit.of Submodule.subtype	—	RingHomCompTriple.ids RingHomInvPair.ids TensorProduct.AlgebraTensorModule.curry_injective Submodule.isScalarTower' IsScalarTower.left TensorProduct.isScalarTower LinearMap.ext IsScalarTower.to_smulCommClass TensorProduct.directLimitLeft_symm_of_tmul Module.DirectLimit.lift_of DFunLike.congr_fun
directLimit_apply' 📖	mathematical	Submodule.FG CommSemiring.toSemiring	DFunLike.coe LinearEquiv RingHom.id Semiring.toNonAssocSemiring RingHomInvPair.ids Module.DirectLimit Submodule Subtype.preorder PartialOrder.toPreorder Submodule.instPartialOrder TensorProduct SetLike.instMembership Submodule.setLike Submodule.addCommMonoid Submodule.module TensorProduct.addCommMonoid TensorProduct.instModule LinearMap.rTensor Submodule.inclusion Module.DirectLimit.addCommMonoid Module.DirectLimit.module EquivLike.toFunLike DFinsupp.instEquivLikeLinearEquiv directLimit LinearMap LinearMap.instFunLike Module.DirectLimit.of Submodule.subtype	—	directLimit_apply
directedSystem 📖	mathematical	—	DirectedSystem Submodule CommSemiring.toSemiring Submodule.FG Subtype.preorder PartialOrder.toPreorder Submodule.instPartialOrder TensorProduct SetLike.instMembership Submodule.setLike Submodule.addCommMonoid Submodule.module DFunLike.coe LinearMap RingHom.id Semiring.toNonAssocSemiring TensorProduct.addCommMonoid TensorProduct.instModule LinearMap.instFunLike LinearMap.rTensor Submodule.inclusion	—	DirectedSystem.rTensor Submodule.FG.directedSystem

TensorProduct

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
eq_of_fg_of_subtype_eq 📖	mathematical	Submodule.FG CommSemiring.toSemiring DFunLike.coe LinearMap RingHom.id Semiring.toNonAssocSemiring TensorProduct Submodule SetLike.instMembership Submodule.setLike Submodule.addCommMonoid Submodule.module addCommMonoid instModule LinearMap.instFunLike LinearMap.rTensor Submodule.subtype	Submodule.inclusion	—	Module.DirectLimit.exists_eq_of_of_eq instDirectedSystemCoeLinearMapIdRTensor Submodule.FG.directedSystem SemilatticeSup.instIsDirectedOrder RingHomInvPair.ids Submodule.FG.rTensor.directLimit_apply' EquivLike.toEmbeddingLike Subtype.coe_le_coe
eq_of_fg_of_subtype_eq' 📖	mathematical	Submodule.FG CommSemiring.toSemiring DFunLike.coe LinearMap RingHom.id Semiring.toNonAssocSemiring TensorProduct Submodule SetLike.instMembership Submodule.setLike Submodule.addCommMonoid Submodule.module addCommMonoid instModule LinearMap.instFunLike LinearMap.rTensor Submodule.subtype	Submodule.inclusion	—	le_sup_left le_sup_right eq_of_fg_of_subtype_eq Submodule.FG.sup RingHomCompTriple.ids LinearMap.rTensor_comp le_trans
eq_zero_of_fg_of_subtype_eq_zero 📖	mathematical	Submodule.FG CommSemiring.toSemiring DFunLike.coe LinearMap RingHom.id Semiring.toNonAssocSemiring TensorProduct Submodule SetLike.instMembership Submodule.setLike Submodule.addCommMonoid Submodule.module addCommMonoid instModule LinearMap.instFunLike LinearMap.rTensor Submodule.subtype zero	Submodule.inclusion	—	map_zero AddMonoidHomClass.toZeroHomClass DistribMulActionSemiHomClass.toAddMonoidHomClass SemilinearMapClass.distribMulActionSemiHomClass LinearMap.semilinearMapClass eq_of_fg_of_subtype_eq LinearMap.map_zero
exists_of_fg 📖	mathematical	—	Submodule.FG CommSemiring.toSemiring TensorProduct Submodule addCommMonoid instModule SetLike.instMembership Submodule.setLike LinearMap.range Submodule.addCommMonoid Submodule.module RingHom.id Semiring.toNonAssocSemiring RingHomSurjective.ids LinearMap.rTensor Submodule.subtype	—	RingHomInvPair.ids RingHomSurjective.ids Module.DirectLimit.exists_of SemilatticeSup.instIsDirectedOrder Submodule.FG.rTensor.directLimit_apply LinearEquiv.apply_symm_apply

TensorProduct.Algebra

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
eq_of_fg_of_subtype_eq 📖	mathematical	Subalgebra.FG DFunLike.coe LinearMap CommSemiring.toSemiring RingHom.id Semiring.toNonAssocSemiring TensorProduct Subalgebra SetLike.instMembership Subalgebra.instSetLike NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring Subalgebra.toSemiring Algebra.toModule Subalgebra.algebra TensorProduct.addCommMonoid TensorProduct.instModule LinearMap.instFunLike LinearMap.rTensor AlgHom.toLinearMap Subalgebra.val	Subalgebra.inclusion	—	RingHomSurjective.ids TensorProduct.exists_of_fg Submodule.FG.map Submodule.FG.sup Submodule.map_sup Submodule.mem_sup_left Submodule.mem_sup_right RingHomCompTriple.ids LinearMap.rTensor_comp TensorProduct.eq_of_fg_of_subtype_eq Algebra.adjoin_mono Finset.coe_union Subalgebra.fg_adjoin_finset subset_trans Set.instIsTransSubset Set.subset_union_left Algebra.subset_adjoin LinearMap.ext LinearMap.comp.congr_simp
eq_of_fg_of_subtype_eq' 📖	mathematical	Subalgebra.FG DFunLike.coe LinearMap CommSemiring.toSemiring RingHom.id Semiring.toNonAssocSemiring TensorProduct Subalgebra SetLike.instMembership Subalgebra.instSetLike NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring Subalgebra.toSemiring Algebra.toModule Subalgebra.algebra TensorProduct.addCommMonoid TensorProduct.instModule LinearMap.instFunLike LinearMap.rTensor AlgHom.toLinearMap Subalgebra.val	Subalgebra.inclusion	—	le_sup_left AlgHom.ext le_sup_right eq_of_fg_of_subtype_eq Subalgebra.FG.sup RingHomCompTriple.ids LinearMap.rTensor_comp le_trans
exists_of_fg 📖	mathematical	—	Subalgebra.FG TensorProduct NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring Algebra.toModule Submodule CommSemiring.toSemiring TensorProduct.addCommMonoid TensorProduct.instModule SetLike.instMembership Submodule.setLike LinearMap.range Subalgebra Subalgebra.instSetLike Subalgebra.toSemiring Subalgebra.algebra RingHom.id RingHomSurjective.ids LinearMap.rTensor AlgHom.toLinearMap Subalgebra.val	—	RingHomSurjective.ids TensorProduct.exists_of_fg Subalgebra.fg_adjoin_finset Algebra.subset_adjoin LinearMap.range_comp_le_range RingHomCompTriple.ids LinearMap.rTensor_comp Submodule.subtype_comp_inclusion

---

← Back to Index