Equalizer

📁 Source: Mathlib/RingTheory/Flat/Equalizer.lean

Statistics

Metric	Count
Definitions tensorEqualizer, tensorEqualizerEquiv, kerTensorProductMapIdToAlgHomEquiv, kerLTensorEquivOfSurjective, tensorEqLocus, tensorEqLocusBil, tensorEqLocusEquiv, tensorKer, tensorKerBil, tensorKerEquiv	10
Theorems coe_tensorEqualizer, tensorEqualizerEquiv_apply, kerTensorProductMapIdToAlgHomEquiv_symm_apply, lTensor_eqLocus_subtype_tensoreqLocusEquiv_symm, lTensor_injective_of_exact_of_flat, lTensor_ker_subtype_tensorKerEquiv_symm, tensorEqLocusEquiv_apply, tensorEqLocus_coe, tensorEqLocus_tmul, tensorKerEquivOfSurjective_symm_tmul, tensorKerEquiv_apply, tensorKer_coe, tensorKer_tmul, eqLocus_lTensor_eq, ker_lTensor_eq	15
Total	25

AlgHom

Definitions

Name	Category	Theorems
tensorEqualizer 📖	CompOp	2 math math: coe_tensorEqualizer, tensorEqualizerEquiv_apply
tensorEqualizerEquiv 📖	CompOp	1 math math: tensorEqualizerEquiv_apply

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
coe_tensorEqualizer 📖	mathematical	—	TensorProduct CommRing.toCommSemiring NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring CommSemiring.toSemiring Algebra.toModule Subalgebra Algebra.TensorProduct.instSemiring Algebra.TensorProduct.leftAlgebra IsScalarTower.to_smulCommClass SetLike.instMembership Subalgebra.instSetLike equalizer AlgHom Algebra.TensorProduct.map id funLike algHomClass DFunLike.coe NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing Subalgebra.toCommRing Subalgebra.instModuleSubtypeMem Subalgebra.toSemiring Subalgebra.algebra tensorEqualizer Subalgebra.val	—	algHomClass
tensorEqualizerEquiv_apply 📖	mathematical	—	DFunLike.coe AlgEquiv TensorProduct CommRing.toCommSemiring Subalgebra CommSemiring.toSemiring SetLike.instMembership Subalgebra.instSetLike equalizer AlgHom funLike algHomClass NonUnitalNonAssocSemiring.toAddCommMonoid NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing Subalgebra.toCommRing Algebra.toModule Subalgebra.instModuleSubtypeMem NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring Algebra.TensorProduct.instSemiring Algebra.TensorProduct.leftAlgebra IsScalarTower.to_smulCommClass Algebra.TensorProduct.map id Subalgebra.toSemiring Subalgebra.algebra AlgEquiv.instFunLike tensorEqualizerEquiv tensorEqualizer	—	algHomClass IsScalarTower.to_smulCommClass

Algebra

Definitions

Name	Category	Theorems
kerTensorProductMapIdToAlgHomEquiv 📖	CompOp	1 math math: kerTensorProductMapIdToAlgHomEquiv_symm_apply

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
kerTensorProductMapIdToAlgHomEquiv_symm_apply 📖	mathematical	DFunLike.coe RingHom Semiring.toNonAssocSemiring CommSemiring.toSemiring CommRing.toCommSemiring RingHom.instFunLike algebraMap	TensorProduct NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring toModule Ideal TensorProduct.instSemiring SetLike.instMembership Submodule.setLike Semiring.toModule RingHom.ker AlgHom TensorProduct.leftAlgebra id IsScalarTower.to_smulCommClass IsScalarTower.right AlgHom.funLike AlgHomClass.toRingHomClass AlgHom.algHomClass TensorProduct.map AlgHom.id IsScalarTower.toAlgHom LinearEquiv NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing RingHom.id TensorProduct.instNonAssocSemiring to_smulCommClass RingHomInvPair.ids RingHom.instRingHomClass TensorProduct.addCommMonoid Submodule.addCommMonoid TensorProduct.rightAlgebra Submodule.module TensorProduct.leftModule EquivLike.toFunLike DFinsupp.instEquivLikeLinearEquiv LinearEquiv.symm kerTensorProductMapIdToAlgHomEquiv TensorProduct.tmul Distrib.toMul NonUnitalNonAssocSemiring.toDistrib	—	RingHom.instRingHomClass IsScalarTower.to_smulCommClass IsScalarTower.right AlgHomClass.toRingHomClass AlgHom.algHomClass to_smulCommClass RingHomInvPair.ids

LinearMap

Definitions

Name	Category	Theorems
kerLTensorEquivOfSurjective 📖	CompOp	1 math math: tensorKerEquivOfSurjective_symm_tmul
tensorEqLocus 📖	CompOp	3 math math: tensorEqLocusEquiv_apply, tensorEqLocus_coe, tensorEqLocus_tmul
tensorEqLocusBil 📖	CompOp	—
tensorEqLocusEquiv 📖	CompOp	2 math math: tensorEqLocusEquiv_apply, lTensor_eqLocus_subtype_tensoreqLocusEquiv_symm
tensorKer 📖	CompOp	3 math math: tensorKer_tmul, tensorKer_coe, tensorKerEquiv_apply
tensorKerBil 📖	CompOp	—
tensorKerEquiv 📖	CompOp	2 math math: lTensor_ker_subtype_tensorKerEquiv_symm, tensorKerEquiv_apply

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
lTensor_eqLocus_subtype_tensoreqLocusEquiv_symm 📖	mathematical	—	DFunLike.coe LinearMap CommSemiring.toSemiring CommRing.toCommSemiring RingHom.id Semiring.toNonAssocSemiring TensorProduct Submodule AddCommGroup.toAddCommMonoid SetLike.instMembership Submodule.setLike eqLocus instFunLike semilinearMapClass Submodule.addCommMonoid Submodule.module TensorProduct.addCommMonoid TensorProduct.instModule lTensor Submodule.subtype LinearEquiv RingHomInvPair.ids TensorProduct.leftModule IsScalarTower.to_smulCommClass addCommMonoid module smulCommClass_self CommSemiring.toCommMonoid DistribMulAction.toMulAction CommMonoid.toMonoid AddCommMonoid.toAddMonoid Module.toDistribMulAction TensorProduct.smulCommClass_left MonoidWithZero.toMonoid Semiring.toMonoidWithZero IsScalarTower.to_smulCommClass' TensorProduct.AlgebraTensorModule.lTensor EquivLike.toFunLike DFinsupp.instEquivLikeLinearEquiv LinearEquiv.symm tensorEqLocusEquiv	—	IsScalarTower.to_smulCommClass semilinearMapClass smulCommClass_self TensorProduct.smulCommClass_left IsScalarTower.to_smulCommClass'
lTensor_injective_of_exact_of_flat 📖	mathematical	DFunLike.coe LinearMap CommSemiring.toSemiring CommRing.toCommSemiring RingHom.id Semiring.toNonAssocSemiring AddCommGroup.toAddCommMonoid instFunLike Function.Exact NegZeroClass.toZero SubNegZeroMonoid.toNegZeroClass SubtractionMonoid.toSubNegZeroMonoid SubtractionCommMonoid.toSubtractionMonoid AddCommGroup.toDivisionAddCommMonoid	TensorProduct TensorProduct.addCommMonoid TensorProduct.instModule lTensor	—	Finsupp.linearCombination_surjective lTensor_exact RingHomCompTriple.ids lTensor_comp_rTensor rTensor_comp_lTensor Module.Flat.rTensor_preserves_injective_linearMap Submodule.subtype_injective rTensor_exact exact_subtype_ker_map lTensor_surjective Module.Flat.lTensor_preserves_injective_linearMap Module.Flat.finsupp SnakeLemma.exact_δ'_left rTensor_surjective Unique.instSubsingleton
lTensor_ker_subtype_tensorKerEquiv_symm 📖	mathematical	—	DFunLike.coe LinearMap CommSemiring.toSemiring CommRing.toCommSemiring RingHom.id Semiring.toNonAssocSemiring TensorProduct Submodule AddCommGroup.toAddCommMonoid SetLike.instMembership Submodule.setLike ker Submodule.addCommMonoid Submodule.module TensorProduct.addCommMonoid TensorProduct.instModule instFunLike lTensor Submodule.subtype LinearEquiv RingHomInvPair.ids TensorProduct.leftModule IsScalarTower.to_smulCommClass addCommMonoid module smulCommClass_self CommSemiring.toCommMonoid DistribMulAction.toMulAction CommMonoid.toMonoid AddCommMonoid.toAddMonoid Module.toDistribMulAction TensorProduct.smulCommClass_left MonoidWithZero.toMonoid Semiring.toMonoidWithZero IsScalarTower.to_smulCommClass' TensorProduct.AlgebraTensorModule.lTensor EquivLike.toFunLike DFinsupp.instEquivLikeLinearEquiv LinearEquiv.symm tensorKerEquiv	—	IsScalarTower.to_smulCommClass smulCommClass_self TensorProduct.smulCommClass_left IsScalarTower.to_smulCommClass'
tensorEqLocusEquiv_apply 📖	mathematical	—	DFunLike.coe LinearEquiv CommSemiring.toSemiring CommRing.toCommSemiring RingHom.id Semiring.toNonAssocSemiring RingHomInvPair.ids TensorProduct Submodule AddCommGroup.toAddCommMonoid SetLike.instMembership Submodule.setLike eqLocus LinearMap instFunLike semilinearMapClass Submodule.addCommMonoid Submodule.module TensorProduct.addCommMonoid TensorProduct.leftModule IsScalarTower.to_smulCommClass addCommMonoid module smulCommClass_self CommSemiring.toCommMonoid DistribMulAction.toMulAction CommMonoid.toMonoid AddCommMonoid.toAddMonoid Module.toDistribMulAction TensorProduct.instModule TensorProduct.smulCommClass_left MonoidWithZero.toMonoid Semiring.toMonoidWithZero IsScalarTower.to_smulCommClass' TensorProduct.AlgebraTensorModule.lTensor EquivLike.toFunLike DFinsupp.instEquivLikeLinearEquiv tensorEqLocusEquiv tensorEqLocus	—	semilinearMapClass IsScalarTower.to_smulCommClass smulCommClass_self TensorProduct.smulCommClass_left IsScalarTower.to_smulCommClass' RingHomInvPair.ids
tensorEqLocus_coe 📖	mathematical	—	TensorProduct CommRing.toCommSemiring AddCommGroup.toAddCommMonoid Submodule CommSemiring.toSemiring TensorProduct.addCommMonoid TensorProduct.leftModule IsScalarTower.to_smulCommClass SetLike.instMembership Submodule.setLike eqLocus RingHom.id Semiring.toNonAssocSemiring LinearMap instFunLike semilinearMapClass DFunLike.coe addCommMonoid module smulCommClass_self CommSemiring.toCommMonoid DistribMulAction.toMulAction CommMonoid.toMonoid AddCommMonoid.toAddMonoid Module.toDistribMulAction TensorProduct.instModule TensorProduct.smulCommClass_left MonoidWithZero.toMonoid Semiring.toMonoidWithZero IsScalarTower.to_smulCommClass' TensorProduct.AlgebraTensorModule.lTensor Submodule.addCommMonoid Submodule.module tensorEqLocus lTensor Submodule.subtype	—	semilinearMapClass TensorProduct.induction_on IsScalarTower.to_smulCommClass smulCommClass_self TensorProduct.smulCommClass_left IsScalarTower.to_smulCommClass' map_zero AddMonoidHomClass.toZeroHomClass DistribMulActionSemiHomClass.toAddMonoidHomClass SemilinearMapClass.distribMulActionSemiHomClass map_add SemilinearMapClass.toAddHomClass
tensorEqLocus_tmul 📖	mathematical	—	TensorProduct CommRing.toCommSemiring AddCommGroup.toAddCommMonoid Submodule CommSemiring.toSemiring TensorProduct.addCommMonoid TensorProduct.leftModule IsScalarTower.to_smulCommClass SetLike.instMembership Submodule.setLike eqLocus RingHom.id Semiring.toNonAssocSemiring LinearMap instFunLike semilinearMapClass DFunLike.coe addCommMonoid module smulCommClass_self CommSemiring.toCommMonoid DistribMulAction.toMulAction CommMonoid.toMonoid AddCommMonoid.toAddMonoid Module.toDistribMulAction TensorProduct.instModule TensorProduct.smulCommClass_left MonoidWithZero.toMonoid Semiring.toMonoidWithZero IsScalarTower.to_smulCommClass' TensorProduct.AlgebraTensorModule.lTensor Submodule.addCommMonoid Submodule.module tensorEqLocus TensorProduct.tmul	—	semilinearMapClass IsScalarTower.to_smulCommClass smulCommClass_self TensorProduct.smulCommClass_left IsScalarTower.to_smulCommClass'
tensorKerEquivOfSurjective_symm_tmul 📖	mathematical	DFunLike.coe LinearMap CommSemiring.toSemiring CommRing.toCommSemiring RingHom.id Semiring.toNonAssocSemiring AddCommGroup.toAddCommMonoid instFunLike	TensorProduct Submodule TensorProduct.addCommMonoid TensorProduct.instModule SetLike.instMembership Submodule.setLike ker lTensor LinearEquiv RingHomInvPair.ids Submodule.addCommMonoid Submodule.module EquivLike.toFunLike DFinsupp.instEquivLikeLinearEquiv LinearEquiv.symm kerLTensorEquivOfSurjective TensorProduct.tmul	—	RingHomInvPair.ids
tensorKerEquiv_apply 📖	mathematical	—	DFunLike.coe LinearEquiv CommSemiring.toSemiring CommRing.toCommSemiring RingHom.id Semiring.toNonAssocSemiring RingHomInvPair.ids TensorProduct Submodule AddCommGroup.toAddCommMonoid SetLike.instMembership Submodule.setLike ker Submodule.addCommMonoid Submodule.module TensorProduct.addCommMonoid TensorProduct.leftModule IsScalarTower.to_smulCommClass LinearMap addCommMonoid module smulCommClass_self CommSemiring.toCommMonoid DistribMulAction.toMulAction CommMonoid.toMonoid AddCommMonoid.toAddMonoid Module.toDistribMulAction TensorProduct.instModule TensorProduct.smulCommClass_left MonoidWithZero.toMonoid Semiring.toMonoidWithZero IsScalarTower.to_smulCommClass' instFunLike TensorProduct.AlgebraTensorModule.lTensor EquivLike.toFunLike DFinsupp.instEquivLikeLinearEquiv tensorKerEquiv tensorKer	—	IsScalarTower.to_smulCommClass smulCommClass_self TensorProduct.smulCommClass_left IsScalarTower.to_smulCommClass' RingHomInvPair.ids
tensorKer_coe 📖	mathematical	—	TensorProduct CommRing.toCommSemiring AddCommGroup.toAddCommMonoid Submodule CommSemiring.toSemiring TensorProduct.addCommMonoid TensorProduct.leftModule IsScalarTower.to_smulCommClass SetLike.instMembership Submodule.setLike ker RingHom.id Semiring.toNonAssocSemiring DFunLike.coe LinearMap addCommMonoid module smulCommClass_self CommSemiring.toCommMonoid DistribMulAction.toMulAction CommMonoid.toMonoid AddCommMonoid.toAddMonoid Module.toDistribMulAction TensorProduct.instModule TensorProduct.smulCommClass_left MonoidWithZero.toMonoid Semiring.toMonoidWithZero IsScalarTower.to_smulCommClass' instFunLike TensorProduct.AlgebraTensorModule.lTensor Submodule.addCommMonoid Submodule.module tensorKer lTensor Submodule.subtype	—	TensorProduct.induction_on IsScalarTower.to_smulCommClass smulCommClass_self TensorProduct.smulCommClass_left IsScalarTower.to_smulCommClass' map_zero AddMonoidHomClass.toZeroHomClass DistribMulActionSemiHomClass.toAddMonoidHomClass SemilinearMapClass.distribMulActionSemiHomClass semilinearMapClass map_add SemilinearMapClass.toAddHomClass
tensorKer_tmul 📖	mathematical	—	TensorProduct CommRing.toCommSemiring AddCommGroup.toAddCommMonoid Submodule CommSemiring.toSemiring TensorProduct.addCommMonoid TensorProduct.leftModule IsScalarTower.to_smulCommClass SetLike.instMembership Submodule.setLike ker RingHom.id Semiring.toNonAssocSemiring DFunLike.coe LinearMap addCommMonoid module smulCommClass_self CommSemiring.toCommMonoid DistribMulAction.toMulAction CommMonoid.toMonoid AddCommMonoid.toAddMonoid Module.toDistribMulAction TensorProduct.instModule TensorProduct.smulCommClass_left MonoidWithZero.toMonoid Semiring.toMonoidWithZero IsScalarTower.to_smulCommClass' instFunLike TensorProduct.AlgebraTensorModule.lTensor Submodule.addCommMonoid Submodule.module tensorKer TensorProduct.tmul	—	IsScalarTower.to_smulCommClass smulCommClass_self TensorProduct.smulCommClass_left IsScalarTower.to_smulCommClass'

Module.Flat

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
eqLocus_lTensor_eq 📖	mathematical	—	LinearMap.eqLocus TensorProduct CommRing.toCommSemiring AddCommGroup.toAddCommMonoid CommSemiring.toSemiring TensorProduct.addCommMonoid TensorProduct.leftModule IsScalarTower.to_smulCommClass RingHom.id Semiring.toNonAssocSemiring LinearMap LinearMap.instFunLike LinearMap.semilinearMapClass DFunLike.coe LinearMap.addCommMonoid LinearMap.module smulCommClass_self CommSemiring.toCommMonoid DistribMulAction.toMulAction CommMonoid.toMonoid AddCommMonoid.toAddMonoid Module.toDistribMulAction TensorProduct.instModule TensorProduct.smulCommClass_left MonoidWithZero.toMonoid Semiring.toMonoidWithZero IsScalarTower.to_smulCommClass' TensorProduct.AlgebraTensorModule.lTensor LinearMap.range Submodule SetLike.instMembership Submodule.setLike Submodule.addCommMonoid Submodule.module RingHomSurjective.ids Submodule.subtype	—	IsScalarTower.to_smulCommClass LinearMap.semilinearMapClass smulCommClass_self TensorProduct.smulCommClass_left IsScalarTower.to_smulCommClass' RingHomSurjective.ids LinearMap.eqLocus_eq_ker_sub map_sub DistribMulActionSemiHomClass.toAddMonoidHomClass SemilinearMapClass.distribMulActionSemiHomClass ker_lTensor_eq
ker_lTensor_eq 📖	mathematical	—	LinearMap.ker TensorProduct CommRing.toCommSemiring AddCommGroup.toAddCommMonoid CommSemiring.toSemiring TensorProduct.addCommMonoid TensorProduct.leftModule IsScalarTower.to_smulCommClass RingHom.id Semiring.toNonAssocSemiring DFunLike.coe LinearMap LinearMap.addCommMonoid LinearMap.module smulCommClass_self CommSemiring.toCommMonoid DistribMulAction.toMulAction CommMonoid.toMonoid AddCommMonoid.toAddMonoid Module.toDistribMulAction TensorProduct.instModule TensorProduct.smulCommClass_left MonoidWithZero.toMonoid Semiring.toMonoidWithZero IsScalarTower.to_smulCommClass' LinearMap.instFunLike TensorProduct.AlgebraTensorModule.lTensor LinearMap.range Submodule SetLike.instMembership Submodule.setLike Submodule.addCommMonoid Submodule.module RingHomSurjective.ids Submodule.subtype	—	IsScalarTower.to_smulCommClass smulCommClass_self TensorProduct.smulCommClass_left IsScalarTower.to_smulCommClass' RingHomSurjective.ids LinearMap.exact_iff lTensor_exact LinearMap.exact_subtype_ker_map

---

← Back to Index