Documentation Verification Report

CotangentBaseChange

📁 Source: Mathlib/RingTheory/Ideal/CotangentBaseChange.lean

Statistics

Metric	Count
Definitions `tensorCotangentEquiv`, `tensorCotangentHom`	2
Theorems `tensorCotangentEquiv_tmul`, `tensorCotangentHom_injective_of_flat`, `tensorCotangentHom_surjective`, `tensorCotangentHom_tmul`	4
Total	6

Ideal

Definitions

Name	Category	Theorems
`tensorCotangentEquiv` 📖	CompOp	1 math math: `tensorCotangentEquiv_tmul`
`tensorCotangentHom` 📖	CompOp	3 math math: `tensorCotangentHom_injective_of_flat`, `tensorCotangentHom_tmul`, `tensorCotangentHom_surjective`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`tensorCotangentEquiv_tmul` 📖	mathematical	—	`DFunLike.coe` `LinearEquiv` `CommSemiring.toSemiring` `CommRing.toCommSemiring` `RingHom.id` `Semiring.toNonAssocSemiring` `RingHomInvPair.ids` `TensorProduct` `Cotangent` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing` `NonUnitalCommRing.toNonUnitalNonAssocCommRing` `CommRing.toNonUnitalCommRing` `AddCommGroup.toAddCommMonoid` `instAddCommGroupCotangent` `Algebra.toModule` `instModuleCotangentOfAlgebra` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Algebra.TensorProduct.instCommRing` `map` `RingHom` `Algebra.TensorProduct.instSemiring` `RingHom.instFunLike` `AlgHom.toRingHom` `Algebra.TensorProduct.instAlgebra` `Algebra.TensorProduct.includeRight` `TensorProduct.addCommMonoid` `TensorProduct.leftModule` `Semiring.toModule` `Algebra.to_smulCommClass` `Algebra.TensorProduct.leftAlgebra` `Algebra.id` `EquivLike.toFunLike` `DFinsupp.instEquivLikeLinearEquiv` `tensorCotangentEquiv` `TensorProduct.tmul` `LinearMap` `Ideal` `SetLike.instMembership` `Submodule.setLike` `Submodule.addCommMonoid` `Submodule.module` `LinearMap.instFunLike` `toCotangent` `SMulZeroClass.toSMul` `AddZero.toZero` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `SubNegMonoid.toAddMonoid` `AddGroup.toSubNegMonoid` `AddCommGroup.toAddGroup` `DistribSMul.toSMulZeroClass` `DistribMulAction.toDistribSMul` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `Module.toDistribMulAction` `AddMonoidWithOne.toOne` `AddCommMonoidWithOne.toAddMonoidWithOne` `NonAssocSemiring.toAddCommMonoidWithOne` `mem_map_of_mem`	—	`RingHomInvPair.ids` `Algebra.to_smulCommClass`
`tensorCotangentHom_injective_of_flat` 📖	mathematical	—	`TensorProduct` `CommRing.toCommSemiring` `Cotangent` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing` `NonUnitalCommRing.toNonUnitalNonAssocCommRing` `CommRing.toNonUnitalCommRing` `AddCommGroup.toAddCommMonoid` `instAddCommGroupCotangent` `Algebra.toModule` `CommSemiring.toSemiring` `instModuleCotangentOfAlgebra` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `Algebra.TensorProduct.instCommRing` `map` `RingHom` `Algebra.TensorProduct.instSemiring` `RingHom.instFunLike` `AlgHom.toRingHom` `Algebra.TensorProduct.instAlgebra` `Algebra.TensorProduct.includeRight` `DFunLike.coe` `LinearMap` `RingHom.id` `TensorProduct.addCommMonoid` `TensorProduct.leftModule` `Semiring.toModule` `Algebra.to_smulCommClass` `Algebra.TensorProduct.leftAlgebra` `Algebra.id` `LinearMap.instFunLike` `tensorCotangentHom`	—	`Algebra.to_smulCommClass` `IsScalarTower.right` `LinearMap.IsScalarTower.compatibleSMul` `Quotient.isScalarTower` `RingHomCompTriple.ids` `IsScalarTower.to_smulCommClass` `smulCommClass_self` `TensorProduct.smulCommClass_left` `IsScalarTower.to_smulCommClass'` `instIsTwoSided_1` `map_pow` `AlgHomClass.toRingHomClass` `AlgHom.algHomClass` `TensorProduct.AlgebraTensorModule.curry_injective` `TensorProduct.isScalarTower_left` `LinearMap.ext_ring` `LinearMap.ext` `toCotangent_surjective` `mem_map_of_mem` `tensorCotangentHom_tmul` `one_smul` `toCotangent_to_quotient_square` `LinearMap.coe_comp` `AlgEquiv.injective` `Module.Flat.lTensor_preserves_injective_linearMap` `cotangentToQuotientSquare_injective` `Function.Injective.of_comp`
`tensorCotangentHom_surjective` 📖	mathematical	—	`TensorProduct` `CommRing.toCommSemiring` `Cotangent` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing` `NonUnitalCommRing.toNonUnitalNonAssocCommRing` `CommRing.toNonUnitalCommRing` `AddCommGroup.toAddCommMonoid` `instAddCommGroupCotangent` `Algebra.toModule` `CommSemiring.toSemiring` `instModuleCotangentOfAlgebra` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `Algebra.TensorProduct.instCommRing` `map` `RingHom` `Algebra.TensorProduct.instSemiring` `RingHom.instFunLike` `AlgHom.toRingHom` `Algebra.TensorProduct.instAlgebra` `Algebra.TensorProduct.includeRight` `DFunLike.coe` `LinearMap` `RingHom.id` `TensorProduct.addCommMonoid` `TensorProduct.leftModule` `Semiring.toModule` `Algebra.to_smulCommClass` `Algebra.TensorProduct.leftAlgebra` `Algebra.id` `LinearMap.instFunLike` `tensorCotangentHom`	—	`Algebra.to_smulCommClass` `IsScalarTower.right` `toCotangent_surjective` `RingHomSurjective.ids` `Eq.le` `map_includeRight_eq` `Eq.ge` `TensorProduct.induction_on` `map_zero` `AddMonoidHomClass.toZeroHomClass` `DistribMulActionSemiHomClass.toAddMonoidHomClass` `SemilinearMapClass.distribMulActionSemiHomClass` `LinearMap.semilinearMapClass` `cotangentToQuotientSquare_injective` `instIsTwoSided_1` `mem_map_of_mem` `tensorCotangentHom_tmul` `LinearMap.map_smul_of_tower` `LinearMap.IsScalarTower.compatibleSMul` `Quotient.isScalarTower` `Algebra.smul_def` `NonUnitalRingHomClass.toMulHomClass` `RingHomClass.toNonUnitalRingHomClass` `RingHom.instRingHomClass` `mul_one` `one_mul` `map_add` `SemilinearMapClass.toAddHomClass`
`tensorCotangentHom_tmul` 📖	mathematical	—	`DFunLike.coe` `LinearMap` `CommSemiring.toSemiring` `CommRing.toCommSemiring` `RingHom.id` `Semiring.toNonAssocSemiring` `TensorProduct` `Cotangent` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing` `NonUnitalCommRing.toNonUnitalNonAssocCommRing` `CommRing.toNonUnitalCommRing` `AddCommGroup.toAddCommMonoid` `instAddCommGroupCotangent` `Algebra.toModule` `instModuleCotangentOfAlgebra` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Algebra.TensorProduct.instCommRing` `map` `RingHom` `Algebra.TensorProduct.instSemiring` `RingHom.instFunLike` `AlgHom.toRingHom` `Algebra.TensorProduct.instAlgebra` `Algebra.TensorProduct.includeRight` `TensorProduct.addCommMonoid` `TensorProduct.leftModule` `Semiring.toModule` `Algebra.to_smulCommClass` `Algebra.TensorProduct.leftAlgebra` `Algebra.id` `LinearMap.instFunLike` `tensorCotangentHom` `TensorProduct.tmul` `Ideal` `SetLike.instMembership` `Submodule.setLike` `Submodule.addCommMonoid` `Submodule.module` `toCotangent` `SMulZeroClass.toSMul` `AddZero.toZero` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `SubNegMonoid.toAddMonoid` `AddGroup.toSubNegMonoid` `AddCommGroup.toAddGroup` `DistribSMul.toSMulZeroClass` `DistribMulAction.toDistribSMul` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `Module.toDistribMulAction` `AddMonoidWithOne.toOne` `AddCommMonoidWithOne.toAddMonoidWithOne` `NonAssocSemiring.toAddCommMonoidWithOne` `mem_map_of_mem`	—	`Algebra.to_smulCommClass`

---

← Back to Index