Documentation Verification Report

IncludeLeftSubRight

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

Statistics

Metric	Count
Definitions `IsEffective`, `includeLeftSubRight`, `codRestrictEqLocusPushoutCocone`	3
Theorems `eqLocus_includeLeft_includeRight`, `of_faithfullyFlat`, `of_isEffective_tensorProduct_of_faithfullyFlat`, `of_section`, `distribBaseChange_comp_includeLeftSubRight`, `distribBaseChange_includeLeftSubRight_apply`, `includeLeftSubRight_algebraMap_zero`, `includeLeftSubRight_apply`, `includeLeftSubRight_zero_of_mem_range`, `bijective_of_faithfullyFlat`, `injective_of_faithfulSMul`, `surjective_of_isEffective`	12
Total	15

Algebra

Definitions

Name	Category	Theorems
`IsEffective` 📖	MathDef	3 math math: `IsEffective.of_section`, `IsEffective.of_faithfullyFlat`, `IsEffective.of_isEffective_tensorProduct_of_faithfullyFlat`
`codRestrictEqLocusPushoutCocone` 📖	CompOp	3 math math: `codRestrictEqLocusPushoutCocone.surjective_of_isEffective`, `codRestrictEqLocusPushoutCocone.injective_of_faithfulSMul`, `codRestrictEqLocusPushoutCocone.bijective_of_faithfullyFlat`

Algebra.IsEffective

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`eqLocus_includeLeft_includeRight` 📖	mathematical	`Algebra.IsEffective`	`SetLike.coe` `Subring` `Ring.toNonAssocRing` `Subring.instSetLike` `RingHom.eqLocus` `TensorProduct` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonAssocRing.toNonUnitalNonAssocRing` `Algebra.toModule` `Ring.toSemiring` `Algebra.TensorProduct.instSemiring` `Algebra.TensorProduct.includeLeftRingHom` `AlgHom.toRingHom` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `Algebra.TensorProduct.instAlgebra` `Algebra.TensorProduct.includeRight` `Set.range` `DFunLike.coe` `RingHom` `CommSemiring.toSemiring` `RingHom.instFunLike` `algebraMap`	—	`Set.ext` `sub_eq_zero` `Algebra.TensorProduct.includeLeftSubRight_apply` `AlgHomClass.toRingHomClass` `AlgHom.algHomClass` `AlgHom.commutes`
`of_faithfullyFlat` 📖	mathematical	—	`Algebra.IsEffective` `CommRing.toCommSemiring` `CommRing.toRing`	—	`of_isEffective_tensorProduct_of_faithfullyFlat` `of_section` `Algebra.to_smulCommClass`
`of_isEffective_tensorProduct_of_faithfullyFlat` 📖	mathematical	`Algebra.IsEffective` `CommRing.toCommSemiring` `TensorProduct` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing` `NonUnitalCommRing.toNonUnitalNonAssocCommRing` `CommRing.toNonUnitalCommRing` `NonAssocRing.toNonUnitalNonAssocRing` `Ring.toNonAssocRing` `Algebra.toModule` `CommSemiring.toSemiring` `Ring.toSemiring` `Algebra.TensorProduct.instRing` `CommRing.toRing` `Algebra.TensorProduct.leftAlgebra` `Algebra.id` `Algebra.to_smulCommClass`	`Algebra.IsEffective` `CommRing.toCommSemiring`	—	`Algebra.to_smulCommClass` `Module.FaithfullyFlat.lTensor_reflects_exact` `DistribMulActionSemiHomClass.toAddMonoidHomClass` `SemilinearMapClass.distribMulActionSemiHomClass` `LinearMap.semilinearMapClass` `AddMonoidHom.exact_iff_of_surjective_of_bijective_of_injective` `IsScalarTower.to_smulCommClass` `IsScalarTower.left` `RingHomInvPair.ids` `AddMonoidHom.ext` `RingHomCompTriple.ids` `LinearMap.IsScalarTower.compatibleSMul'` `TensorProduct.isScalarTower_left` `IsScalarTower.right` `AddMonoidHomClass.toAddMonoidHom.congr_simp` `AddMonoidHom.id_comp` `AddMonoidHom.comp_id` `Algebra.TensorProduct.distribBaseChange_includeLeftSubRight_apply` `AlgEquiv.surjective` `Function.bijective_id` `LinearEquiv.injective`
`of_section` 📖	mathematical	—	`Algebra.IsEffective`	—	`AlgEquiv.injective` `Algebra.TensorProduct.lid_symm_apply` `mul_one` `Algebra.coe_linearMap` `Algebra.smul_def` `TensorProduct.smul_tmul` `TensorProduct.CompatibleSMul.isScalarTower` `IsScalarTower.right` `IsScalarTower.left` `smul_eq_mul` `AlgHom.id_apply` `IsScalarTower.to_smulCommClass` `Algebra.TensorProduct.map_tmul` `sub_eq_zero` `Algebra.TensorProduct.includeLeftSubRight_apply` `map_one` `MonoidHomClass.toOneHomClass` `MonoidWithZeroHomClass.toMonoidHomClass` `RingHomClass.toMonoidWithZeroHomClass` `AlgHomClass.toRingHomClass` `AlgHom.algHomClass` `Algebra.TensorProduct.includeLeftSubRight_zero_of_mem_range`

Algebra.TensorProduct

Definitions

Name	Category	Theorems
`includeLeftSubRight` 📖	CompOp	5 math math: `includeLeftSubRight_algebraMap_zero`, `distribBaseChange_comp_includeLeftSubRight`, `distribBaseChange_includeLeftSubRight_apply`, `includeLeftSubRight_apply`, `includeLeftSubRight_zero_of_mem_range`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`distribBaseChange_comp_includeLeftSubRight` 📖	mathematical	—	`LinearMap.comp` `TensorProduct` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing` `NonUnitalCommRing.toNonUnitalNonAssocCommRing` `CommRing.toNonUnitalCommRing` `NonAssocRing.toNonUnitalNonAssocRing` `Ring.toNonAssocRing` `Algebra.toModule` `CommSemiring.toSemiring` `CommRing.toCommSemiring` `Ring.toSemiring` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `TensorProduct.addCommMonoid` `TensorProduct.instModule` `TensorProduct.leftModule` `Semiring.toModule` `Algebra.to_smulCommClass` `TensorProduct.smulCommClass_left` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `Module.toDistribMulAction` `IsScalarTower.to_smulCommClass'` `IsScalarTower.right` `RingHom.id` `RingHomCompTriple.ids` `LinearEquiv.toLinearMap` `RingHomInvPair.ids` `LinearEquiv.restrictScalars` `LinearMap.IsScalarTower.compatibleSMul` `SMulZeroClass.toSMul` `AddZero.toZero` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `AddCommMonoid.toAddMonoid` `DistribSMul.toSMulZeroClass` `DistribMulAction.toDistribSMul` `Algebra.toSMul` `TensorProduct.isScalarTower_left` `TensorProduct.isScalarTower` `TensorProduct.AlgebraTensorModule.distribBaseChange` `LinearMap.lTensor` `includeLeftSubRight` `LinearMap.restrictScalars` `instRing` `CommRing.toRing` `leftAlgebra` `Algebra.id`	—	`TensorProduct.AlgebraTensorModule.curry_injective` `Algebra.to_smulCommClass` `IsScalarTower.left` `TensorProduct.smulCommClass_left` `IsScalarTower.to_smulCommClass'` `IsScalarTower.right` `TensorProduct.isScalarTower_right` `TensorProduct.CompatibleSMul.isScalarTower` `TensorProduct.isScalarTower_left` `TensorProduct.isScalarTower` `RingHomCompTriple.ids` `RingHomInvPair.ids` `LinearMap.IsScalarTower.compatibleSMul` `LinearMap.ext` `IsScalarTower.to_smulCommClass` `TensorProduct.tmul_sub` `map_sub` `DistribMulActionSemiHomClass.toAddMonoidHomClass` `SemilinearMapClass.distribMulActionSemiHomClass` `SemilinearEquivClass.instSemilinearMapClass` `LinearEquiv.instSemilinearEquivClass` `tmul_one_tmul_one_tmul`
`distribBaseChange_includeLeftSubRight_apply` 📖	mathematical	—	`DFunLike.coe` `LinearEquiv` `CommSemiring.toSemiring` `CommRing.toCommSemiring` `RingHom.id` `Semiring.toNonAssocSemiring` `RingHomInvPair.ids` `TensorProduct` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonAssocRing.toNonUnitalNonAssocRing` `Ring.toNonAssocRing` `Algebra.toModule` `Ring.toSemiring` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `TensorProduct.addCommMonoid` `TensorProduct.instModule` `TensorProduct.leftModule` `Semiring.toModule` `Algebra.to_smulCommClass` `EquivLike.toFunLike` `DFinsupp.instEquivLikeLinearEquiv` `TensorProduct.AlgebraTensorModule.distribBaseChange` `LinearMap` `NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing` `NonUnitalCommRing.toNonUnitalNonAssocCommRing` `CommRing.toNonUnitalCommRing` `LinearMap.instFunLike` `LinearMap.lTensor` `includeLeftSubRight` `instRing` `CommRing.toRing` `leftAlgebra` `Algebra.id`	—	`Algebra.to_smulCommClass` `RingHomInvPair.ids` `TensorProduct.smulCommClass_left` `IsScalarTower.to_smulCommClass'` `IsScalarTower.right` `RingHomCompTriple.ids` `LinearMap.IsScalarTower.compatibleSMul` `TensorProduct.isScalarTower_left` `TensorProduct.isScalarTower` `distribBaseChange_comp_includeLeftSubRight`
`includeLeftSubRight_algebraMap_zero` 📖	mathematical	—	`DFunLike.coe` `LinearMap` `CommSemiring.toSemiring` `RingHom.id` `Semiring.toNonAssocSemiring` `TensorProduct` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonAssocRing.toNonUnitalNonAssocRing` `Ring.toNonAssocRing` `Algebra.toModule` `Ring.toSemiring` `TensorProduct.addCommMonoid` `TensorProduct.instModule` `LinearMap.instFunLike` `includeLeftSubRight` `RingHom` `RingHom.instFunLike` `algebraMap` `instZeroTensorProduct`	—	`includeLeftSubRight_zero_of_mem_range` `Set.mem_range`
`includeLeftSubRight_apply` 📖	mathematical	—	`DFunLike.coe` `LinearMap` `CommSemiring.toSemiring` `RingHom.id` `Semiring.toNonAssocSemiring` `TensorProduct` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonAssocRing.toNonUnitalNonAssocRing` `Ring.toNonAssocRing` `Algebra.toModule` `Ring.toSemiring` `TensorProduct.addCommMonoid` `TensorProduct.instModule` `LinearMap.instFunLike` `includeLeftSubRight` `SubNegMonoid.toSub` `AddGroup.toSubNegMonoid` `AddGroupWithOne.toAddGroup` `Ring.toAddGroupWithOne` `instRing` `TensorProduct.tmul` `AddMonoidWithOne.toOne` `AddGroupWithOne.toAddMonoidWithOne`	—	—
`includeLeftSubRight_zero_of_mem_range` 📖	mathematical	`Set` `Set.instMembership` `Set.range` `DFunLike.coe` `RingHom` `Semiring.toNonAssocSemiring` `CommSemiring.toSemiring` `Ring.toSemiring` `RingHom.instFunLike` `algebraMap`	`DFunLike.coe` `LinearMap` `CommSemiring.toSemiring` `RingHom.id` `Semiring.toNonAssocSemiring` `TensorProduct` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonAssocRing.toNonUnitalNonAssocRing` `Ring.toNonAssocRing` `Algebra.toModule` `Ring.toSemiring` `TensorProduct.addCommMonoid` `TensorProduct.instModule` `LinearMap.instFunLike` `includeLeftSubRight` `instZeroTensorProduct`	—	`Set.mem_range` `AlgHom.commutes` `sub_self`

Algebra.codRestrictEqLocusPushoutCocone

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`bijective_of_faithfullyFlat` 📖	mathematical	—	`Function.Bijective` `CommRingCat.carrier` `CategoryTheory.Limits.Cone.pt` `CategoryTheory.Limits.WalkingParallelPair` `CategoryTheory.Limits.walkingParallelPairHomCategory` `CommRingCat` `CommRingCat.instCategory` `CategoryTheory.Limits.parallelPair` `CommRingCat.of` `CategoryTheory.Limits.Cocone.pt` `CategoryTheory.Limits.WalkingSpan` `CategoryTheory.Limits.WidePushoutShape.category` `CategoryTheory.Limits.WalkingPair` `CategoryTheory.Limits.span` `CommRingCat.ofHom` `algebraMap` `CommRing.toCommSemiring` `CommSemiring.toSemiring` `CommRingCat.pushoutCocone` `CategoryTheory.Limits.PushoutCocone.inl` `CategoryTheory.Limits.PushoutCocone.inr` `CommRingCat.equalizerFork` `DFunLike.coe` `RingHom` `Semiring.toNonAssocSemiring` `CommRingCat.commRing` `RingHom.instFunLike` `Algebra.codRestrictEqLocusPushoutCocone`	—	`injective_of_faithfulSMul` `Module.FaithfullyFlat.faithfulSMul` `surjective_of_isEffective` `Algebra.IsEffective.of_faithfullyFlat`
`injective_of_faithfulSMul` 📖	mathematical	—	`CommRingCat.carrier` `CategoryTheory.Limits.Cone.pt` `CategoryTheory.Limits.WalkingParallelPair` `CategoryTheory.Limits.walkingParallelPairHomCategory` `CommRingCat` `CommRingCat.instCategory` `CategoryTheory.Limits.parallelPair` `CommRingCat.of` `CategoryTheory.Limits.Cocone.pt` `CategoryTheory.Limits.WalkingSpan` `CategoryTheory.Limits.WidePushoutShape.category` `CategoryTheory.Limits.WalkingPair` `CategoryTheory.Limits.span` `CommRingCat.ofHom` `algebraMap` `CommRing.toCommSemiring` `CommSemiring.toSemiring` `CommRingCat.pushoutCocone` `CategoryTheory.Limits.PushoutCocone.inl` `CategoryTheory.Limits.PushoutCocone.inr` `CommRingCat.equalizerFork` `DFunLike.coe` `RingHom` `Semiring.toNonAssocSemiring` `CommRingCat.commRing` `RingHom.instFunLike` `Algebra.codRestrictEqLocusPushoutCocone`	—	`RingHom.injective_codRestrict` `FaithfulSMul.algebraMap_injective`
`surjective_of_isEffective` 📖	mathematical	`Algebra.IsEffective` `CommRing.toCommSemiring` `CommRing.toRing`	`CommRingCat.carrier` `CategoryTheory.Limits.Cone.pt` `CategoryTheory.Limits.WalkingParallelPair` `CategoryTheory.Limits.walkingParallelPairHomCategory` `CommRingCat` `CommRingCat.instCategory` `CategoryTheory.Limits.parallelPair` `CommRingCat.of` `CategoryTheory.Limits.Cocone.pt` `CategoryTheory.Limits.WalkingSpan` `CategoryTheory.Limits.WidePushoutShape.category` `CategoryTheory.Limits.WalkingPair` `CategoryTheory.Limits.span` `CommRingCat.ofHom` `algebraMap` `CommRing.toCommSemiring` `CommSemiring.toSemiring` `CommRingCat.pushoutCocone` `CategoryTheory.Limits.PushoutCocone.inl` `CategoryTheory.Limits.PushoutCocone.inr` `CommRingCat.equalizerFork` `DFunLike.coe` `RingHom` `Semiring.toNonAssocSemiring` `CommRingCat.commRing` `RingHom.instFunLike` `Algebra.codRestrictEqLocusPushoutCocone`	—	`Set.mem_range` `SetLike.mem_coe` `Algebra.IsEffective.eqLocus_includeLeft_includeRight`

---

← Back to Index