Local

📁 Source: Mathlib/RingTheory/Smooth/Local.lean

Statistics

Metric	Count
Definitions	0
Theorems iff_injective_cotangentComplexBaseChange, iff_injective_cotangentComplexBaseChange_residueField, iff_injective_lTensor_residueField	3
Total	3

Algebra.FormallySmooth

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
iff_injective_cotangentComplexBaseChange 📖	mathematical	DFunLike.coe RingHom Semiring.toNonAssocSemiring CommSemiring.toSemiring CommRing.toCommSemiring RingHom.instFunLike algebraMap Ideal.FG RingHom.ker RingHom.instRingHomClass Ideal Preorder.toLE PartialOrder.toPreorder Submodule.instPartialOrder NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toModule IsLocalRing.maximalIdeal DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield	Algebra.FormallySmooth TensorProduct SetLike.instMembership Submodule.setLike NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing EuclideanDomain.toCommRing Field.toEuclideanDomain Submodule.addCommMonoid Algebra.toModule Submodule.module KaehlerDifferential AddCommGroup.toAddCommMonoid instAddCommGroupKaehlerDifferential KaehlerDifferential.module' Algebra.id Algebra.to_smulCommClass LinearMap RingHom.id TensorProduct.addCommMonoid TensorProduct.leftModule LinearMap.instFunLike KaehlerDifferential.cotangentComplexBaseChange	—	Algebra.to_smulCommClass RingHom.instRingHomClass Ideal.instIsTwoSided_1 IsScalarTower.of_algebraMap_eq' AlgHomClass.toRingHomClass AlgHom.algHomClass AlgHom.comp_algebraMap IsScalarTower.to₁₃₄ IsLocalRing.instIsScalarTowerResidueField IsScalarTower.right iff_injective_cotangentComplexBaseChange_residueField Module.FaithfullyFlat.lTensor_injective_iff_injective Module.FaithfullyFlat.instOfNontrivialOfFree IsLocalRing.toNontrivial Field.instIsLocalRing Module.Free.of_divisionRing IsScalarTower.to_smulCommClass RingHomCompTriple.ids RingHomInvPair.ids TensorProduct.AlgebraTensorModule.curry_injective TensorProduct.isScalarTower_left LinearMap.ext_ring LinearMap.ext one_smul Equiv.injective_comp Equiv.comp_injective
iff_injective_cotangentComplexBaseChange_residueField 📖	mathematical	DFunLike.coe RingHom Semiring.toNonAssocSemiring CommSemiring.toSemiring CommRing.toCommSemiring RingHom.instFunLike algebraMap Ideal.FG RingHom.ker RingHom.instRingHomClass	Algebra.FormallySmooth TensorProduct IsLocalRing.ResidueField Ideal SetLike.instMembership Submodule.setLike NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toModule NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing IsLocalRing.instCommRingResidueField Submodule.addCommMonoid Algebra.toModule IsLocalRing.ResidueField.algebra Submodule.module KaehlerDifferential AddCommGroup.toAddCommMonoid instAddCommGroupKaehlerDifferential KaehlerDifferential.module' Algebra.id Algebra.to_smulCommClass LinearMap RingHom.id TensorProduct.addCommMonoid TensorProduct.leftModule LinearMap.instFunLike KaehlerDifferential.cotangentComplexBaseChange IsLocalRing.instIsScalarTowerResidueField IsScalarTower.right	—	Algebra.to_smulCommClass RingHom.instRingHomClass Function.surjInv_eq IsLocalRing.instIsScalarTowerResidueField IsScalarTower.right iff_injective_lTensor_residueField IsScalarTower.left RingHomCompTriple.ids RingHomInvPair.ids IsScalarTower.to_smulCommClass Algebra.Extension.cotangentComplexBaseChange_eq_lTensor_cotangentComplex Equiv.injective_comp Equiv.comp_injective
iff_injective_lTensor_residueField 📖	mathematical	Ideal.FG Algebra.Extension.Ring CommSemiring.toSemiring CommRing.toCommSemiring Algebra.Extension.commRing Algebra.Extension.ker	Algebra.FormallySmooth TensorProduct IsLocalRing.ResidueField Algebra.Extension.Cotangent NonUnitalNonAssocSemiring.toAddCommMonoid NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing IsLocalRing.instCommRingResidueField AddCommGroup.toAddCommMonoid Algebra.Extension.instAddCommGroupCotangent Algebra.toModule DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield IsLocalRing.ResidueField.field IsLocalRing.ResidueField.algebra Algebra.id Algebra.Extension.instModuleCotangent Algebra.Extension.CotangentSpace TensorProduct.addCommMonoid KaehlerDifferential Algebra.Extension.instRingOfIsScalarTower instAddCommGroupKaehlerDifferential Algebra.Extension.algebra₂ KaehlerDifferential.module' TensorProduct.leftModule Semiring.toModule Algebra.to_smulCommClass DFunLike.coe LinearMap RingHom.id Semiring.toNonAssocSemiring TensorProduct.instModule LinearMap.instFunLike LinearMap.lTensor Algebra.Extension.cotangentComplex	—	IsScalarTower.left Algebra.to_smulCommClass Module.Finite.of_fg Module.Finite.of_surjective RingHomSurjective.ids Algebra.Extension.Cotangent.mk_surjective Module.Finite.of_restrictScalars_finite Algebra.Extension.instIsScalarTowerCotangent IsScalarTower.right RingHomCompTriple.ids IsLocalRing.split_injective_iff_lTensor_residueField_injective Module.Finite.base_change Algebra.TensorProduct.instFree Algebra.Extension.formallySmooth_iff_split_injection

---

← Back to Index