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 CommRing.toCommSemiring NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring CommSemiring.toSemiring 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 DFunLike.coe LinearEquiv NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing RingHom.id TensorProduct.instNonAssocSemiring to_smulCommClass RingHomInvPair.ids RingHom RingHom.instFunLike RingHom.instRingHomClass algebraMap 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 CommRing.toCommSemiring AddCommGroup.toAddCommMonoid DFunLike.coe LinearMap CommSemiring.toSemiring RingHom.id Semiring.toNonAssocSemiring TensorProduct.addCommMonoid TensorProduct.instModule instFunLike 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 CommRing.toCommSemiring AddCommGroup.toAddCommMonoid Submodule CommSemiring.toSemiring TensorProduct.addCommMonoid TensorProduct.instModule SetLike.instMembership Submodule.setLike ker RingHom.id Semiring.toNonAssocSemiring lTensor DFunLike.coe 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