Basic

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

Statistics

Metric	Count
Definitions equivOfFormallySmooth, equivH1CotangentOfFormallySmooth, homInfinitesimal, FormallySmooth, liftOfSurjective	5
Theorems equivOfFormallySmooth_apply, equivOfFormallySmooth_symm, equivOfFormallySmooth_toLinearMap, cotangentComplex_injective_iff, formallySmooth_iff_split_injection, comp, comp_lift, comp_liftOfSurjective, comp_surjective, exists_lift, iff_comp_surjective, iff_of_equiv, iff_of_surjective, iff_split_injection, iff_split_surjection, iff_subsingleton_and_projective, inst, instFinitePresentationKaehlerDifferentialOfEssFiniteType, instLocalization, instTensorProduct, kerCotangentToTensor_injective_iff, liftOfSurjective_apply, localization_base, localization_map, mk_lift, of_comp_surjective, of_equiv, of_isLocalization, of_restrictScalars, of_split, polynomial, projective_kaehlerDifferential, subsingleton_h1Cotangent, baseChange, comp, finitePresentation, formallySmooth, of_equiv, of_isLocalization_Away, formallySmooth_iff, mvPolynomial, smooth_iff	42
Total	47

Algebra

Definitions

Name	Category	Theorems
FormallySmooth 📖	CompData	41 math math: FormallySmooth.of_algebraicIndependent_of_isSeparable, Smooth.formallySmooth, smooth_iff, Extension.formallySmooth_iff_split_injection, FormallySmooth.adjoin_of_algebraicIndependent, smoothLocus_eq_univ_iff, RingHom.FormallySmooth.toAlgebra, FormallySmooth.of_isLocalization, FormallySmooth.iff_injective_cotangentComplexBaseChange_residueField, FormallySmooth.iff_injective_lTensor_residueField, FormallySmooth.of_pi, FormallySmooth.inst, FormallySmooth.iff_subsingleton_and_projective, FormallySmooth.of_restrictScalars, FormallySmooth.of_equiv, FormallySmooth.iff_of_surjective, FormallySmooth.instTensorProduct, FormallySmooth.localization_base, RingHom.formallySmooth_algebraMap, FormallyEtale.instFormallySmooth, FormallySmooth.of_algebraicIndependent, FormallySmooth.iff_split_surjection, FormallySmooth.of_comp_surjective, FormallySmooth.instLocalization, FormallyEtale.iff_formallyUnramified_and_formallySmooth, FormallySmooth.of_split, FormallySmooth.of_perfectField, FormallySmooth.pi_iff, mvPolynomial, FormallyEtale.iff_unramified_and_smooth, formallySmooth_iff, FormallySmooth.of_formallySmooth_residueField_tensor, FormallySmooth.iff_injective_cotangentComplexBaseChange, FormallySmooth.localization_map, FormallySmooth.polynomial, basicOpen_subset_smoothLocus_iff, FormallySmooth.comp, FormallySmooth.iff_restrictScalars, FormallySmooth.iff_comp_surjective, FormallySmooth.iff_split_injection, FormallySmooth.iff_of_equiv

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
formallySmooth_iff 📖	mathematical	—	FormallySmooth Module.Projective CommSemiring.toSemiring CommRing.toCommSemiring KaehlerDifferential AddCommGroup.toAddCommMonoid instAddCommGroupKaehlerDifferential KaehlerDifferential.module' id to_smulCommClass H1Cotangent	—	to_smulCommClass
mvPolynomial 📖	mathematical	—	FormallySmooth MvPolynomial CommRing.toCommSemiring MvPolynomial.instCommRingMvPolynomial MvPolynomial.algebra id	—	MvPolynomial.aeval_X_left Submodule.subsingleton_iff_eq_bot MvPolynomial.map_id Function.Surjective.subsingleton Extension.Cotangent.mk_surjective Function.Injective.subsingleton Extension.instIsScalarTowerCotangent IsScalarTower.right Extension.h1Cotangentι_injective to_smulCommClass Module.Projective.of_free instFreeMvPolynomialKaehlerDifferential Equiv.subsingleton RingHomInvPair.ids
smooth_iff 📖	mathematical	—	Smooth FormallySmooth FinitePresentation CommRing.toCommSemiring CommSemiring.toSemiring	—	—

Algebra.Extension

Definitions

Name	Category	Theorems
equivH1CotangentOfFormallySmooth 📖	CompOp	—
homInfinitesimal 📖	CompOp	—

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
cotangentComplex_injective_iff 📖	mathematical	—	Cotangent CotangentSpace DFunLike.coe LinearMap CommSemiring.toSemiring CommRing.toCommSemiring RingHom.id Semiring.toNonAssocSemiring AddCommGroup.toAddCommMonoid instAddCommGroupCotangent TensorProduct.addCommMonoid Ring commRing KaehlerDifferential instRingOfIsScalarTower Algebra.id NonUnitalNonAssocSemiring.toAddCommMonoid NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing instAddCommGroupKaehlerDifferential Algebra.toModule algebra₂ KaehlerDifferential.module' instModuleCotangent TensorProduct.leftModule Semiring.toModule Algebra.to_smulCommClass LinearMap.instFunLike cotangentComplex Algebra.H1Cotangent	—	IsScalarTower.left Algebra.to_smulCommClass subsingleton_h1Cotangent Equiv.subsingleton_congr RingHomInvPair.ids instIsScalarTowerCotangent IsScalarTower.right
formallySmooth_iff_split_injection 📖	mathematical	—	Algebra.FormallySmooth LinearMap.comp Cotangent CotangentSpace CommSemiring.toSemiring CommRing.toCommSemiring AddCommGroup.toAddCommMonoid instAddCommGroupCotangent TensorProduct.addCommMonoid Ring commRing KaehlerDifferential instRingOfIsScalarTower Algebra.id NonUnitalNonAssocSemiring.toAddCommMonoid NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing instAddCommGroupKaehlerDifferential Algebra.toModule algebra₂ KaehlerDifferential.module' instModuleCotangent TensorProduct.leftModule Semiring.toModule Algebra.to_smulCommClass RingHom.id Semiring.toNonAssocSemiring RingHomCompTriple.ids cotangentComplex LinearMap.id	—	IsScalarTower.left Algebra.to_smulCommClass RingHom.instRingHomClass RingHomCompTriple.ids Algebra.FormallySmooth.iff_split_injection instIsScalarTowerRing_2 algebraMap_surjective RingHomInvPair.ids AddEquiv.map_add' Cotangent.ext Cotangent.val_smul' Equiv.left_inv Equiv.right_inv TensorProduct.isScalarTower_left IsScalarTower.right instIsScalarTowerCotangent LinearMap.ext DFunLike.congr_fun LinearMap.IsScalarTower.compatibleSMul

Algebra.Extension.H1Cotangent

Definitions

Name	Category	Theorems
equivOfFormallySmooth 📖	CompOp	3 math math: equivOfFormallySmooth_apply, equivOfFormallySmooth_symm, equivOfFormallySmooth_toLinearMap

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
equivOfFormallySmooth_apply 📖	mathematical	—	DFunLike.coe LinearEquiv CommSemiring.toSemiring CommRing.toCommSemiring RingHom.id Semiring.toNonAssocSemiring RingHomInvPair.ids Algebra.Extension.H1Cotangent AddCommGroup.toAddCommMonoid Algebra.Extension.instAddCommGroupH1Cotangent Algebra.Extension.instModuleH1CotangentOfIsScalarTowerCotangent Algebra.id Algebra.Extension.instModuleCotangent Algebra.Extension.instIsScalarTowerCotangent IsScalarTower.right EquivLike.toFunLike DFinsupp.instEquivLikeLinearEquiv equivOfFormallySmooth LinearMap LinearMap.instFunLike map IsScalarTower.left MonoidWithZero.toMonoid Semiring.toMonoidWithZero DistribMulAction.toMulAction AddCommMonoid.toAddMonoid NonUnitalNonAssocSemiring.toAddCommMonoid NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing Module.toDistribMulAction Algebra.toModule	—	IsScalarTower.left RingHomInvPair.ids Algebra.Extension.instIsScalarTowerCotangent IsScalarTower.right equivOfFormallySmooth_toLinearMap LinearEquiv.coe_coe
equivOfFormallySmooth_symm 📖	mathematical	—	LinearEquiv.symm Algebra.Extension.H1Cotangent CommSemiring.toSemiring CommRing.toCommSemiring AddCommGroup.toAddCommMonoid Algebra.Extension.instAddCommGroupH1Cotangent Algebra.Extension.instModuleH1CotangentOfIsScalarTowerCotangent Algebra.id Algebra.Extension.instModuleCotangent Algebra.Extension.instIsScalarTowerCotangent IsScalarTower.right RingHom.id Semiring.toNonAssocSemiring RingHomInvPair.ids equivOfFormallySmooth	—	IsScalarTower.left RingHomInvPair.ids Algebra.Extension.instIsScalarTowerCotangent IsScalarTower.right
equivOfFormallySmooth_toLinearMap 📖	mathematical	—	LinearEquiv.toLinearMap CommSemiring.toSemiring CommRing.toCommSemiring RingHom.id Semiring.toNonAssocSemiring RingHomInvPair.ids Algebra.Extension.H1Cotangent AddCommGroup.toAddCommMonoid Algebra.Extension.instAddCommGroupH1Cotangent Algebra.Extension.instModuleH1CotangentOfIsScalarTowerCotangent Algebra.id Algebra.Extension.instModuleCotangent Algebra.Extension.instIsScalarTowerCotangent IsScalarTower.right equivOfFormallySmooth map IsScalarTower.left MonoidWithZero.toMonoid Semiring.toMonoidWithZero DistribMulAction.toMulAction AddCommMonoid.toAddMonoid NonUnitalNonAssocSemiring.toAddCommMonoid NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing Module.toDistribMulAction Algebra.toModule	—	IsScalarTower.left LinearMap.ext Algebra.Extension.instIsScalarTowerCotangent IsScalarTower.right RingHomInvPair.ids map_toInfinitesimal_bijective LinearEquiv.symm_apply_eq RingHomCompTriple.ids LinearMap.IsScalarTower.compatibleSMul Algebra.Extension.instIsScalarTowerH1CotangentOfCotangent map_comp map_eq

Algebra.FormallySmooth

Definitions

Name	Category	Theorems
liftOfSurjective 📖	CompOp	2 math math: liftOfSurjective_apply, comp_liftOfSurjective

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
comp 📖	mathematical	—	Algebra.FormallySmooth	—	of_comp_surjective Ideal.instIsTwoSided_1 comp_surjective AlgHom.congr_fun IsScalarTower.of_algHom Ideal.Quotient.isScalarTower AlgHom.ext
comp_lift 📖	mathematical	IsNilpotent Ideal CommSemiring.toSemiring CommRing.toCommSemiring Submodule.pointwiseZero NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring Semiring.toModule Submodule.instPowNat IsScalarTower.right Algebra.id	AlgHom.comp HasQuotient.Quotient Ring.toSemiring CommRing.toRing Ideal.instHasQuotient Ideal.Quotient.ring Ideal.instIsTwoSided_1 Ideal.Quotient.algebra Ideal.Quotient.mkₐ lift	—	IsScalarTower.right Ideal.instIsTwoSided_1 exists_lift
comp_liftOfSurjective 📖	mathematical	DFunLike.coe AlgHom CommRing.toCommSemiring CommSemiring.toSemiring AlgHom.funLike IsNilpotent Ideal Submodule.pointwiseZero NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring Semiring.toModule Submodule.instPowNat IsScalarTower.right Algebra.id RingHom.ker RingHom RingHom.instFunLike RingHom.instRingHomClass RingHomClass.toRingHom AlgHomClass.toRingHomClass AlgHom.algHomClass	AlgHom.comp liftOfSurjective	—	IsScalarTower.right RingHom.instRingHomClass AlgHomClass.toRingHomClass AlgHom.algHomClass AlgHom.ext liftOfSurjective_apply
comp_surjective 📖	mathematical	Ideal CommSemiring.toSemiring CommRing.toCommSemiring Monoid.toNatPow MonoidWithZero.toMonoid Semiring.toMonoidWithZero IdemSemiring.toSemiring Submodule.idemSemiring Algebra.id Bot.bot Submodule.instBot NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring Semiring.toModule	AlgHom Ring.toSemiring CommRing.toRing HasQuotient.Quotient Ideal.instHasQuotient Ideal.Quotient.ring Ideal.instIsTwoSided_1 Ideal.Quotient.algebra AlgHom.comp Ideal.Quotient.mkₐ	—	Ideal.instIsTwoSided_1 Algebra.to_smulCommClass LinearMap.ker_eq_bot Submodule.subsingleton_iff_eq_bot subsingleton_h1Cotangent RingHomCompTriple.ids List.TFAE.out RingHomInvPair.ids Function.Exact.split_tfae' Algebra.Extension.exact_cotangentComplex_toKaehler Algebra.Extension.subsingleton_h1Cotangent Module.projective_lifting_property projective_kaehlerDifferential Algebra.Extension.toKaehler_surjective RingHom.instRingHomClass Algebra.Generators.instIsScalarTowerRing IsScalarTower.left Algebra.Generators.algebraMap_surjective Algebra.Extension.Cotangent.val_smul' LinearMap.IsScalarTower.compatibleSMul TensorProduct.isScalarTower_left IsScalarTower.right Algebra.Extension.instIsScalarTowerCotangent LinearMap.ext Ideal.Quotient.mk_surjective Ideal.Quotient.algebraMap_eq MvPolynomial.aeval_algebraMap_apply Ideal.Quotient.isScalarTower AlgHomClass.toRingHomClass AlgHom.algHomClass Algebra.Generators.algebraMap_eq AlgHom.coe_toRingHom MvPolynomial.comp_aeval_apply Function.comp_assoc Function.comp_surjInv CompTriple.comp_eq CompTriple.instId_comp CompTriple.instIsIdId Ideal.Quotient.eq_zero_iff_mem Algebra.Generators.algebraMap_apply map_zero MonoidWithZeroHomClass.toZeroHomClass RingHomClass.toMonoidWithZeroHomClass LE.le.trans Ideal.pow_right_mono LE.le.trans_eq Ideal.le_comap_pow Ideal.Quotient.algHom_ext MvPolynomial.algHom_ext MvPolynomial.aeval_X Function.surjInv_eq AlgHom.comp_assoc AlgHom.comp_id
exists_lift 📖	mathematical	IsNilpotent Ideal CommSemiring.toSemiring CommRing.toCommSemiring Submodule.pointwiseZero NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring Semiring.toModule Submodule.instPowNat IsScalarTower.right Algebra.id	AlgHom.comp HasQuotient.Quotient Ring.toSemiring CommRing.toRing Ideal.instHasQuotient Ideal.Quotient.ring Ideal.instIsTwoSided_1 Ideal.Quotient.algebra Ideal.Quotient.mkₐ	—	IsScalarTower.right Ideal.instIsTwoSided_1 Ideal.IsNilpotent.induction_on comp_surjective sup_eq_right RingEquiv.map_mul' RingEquiv.map_add' AlgHom.comp_assoc AlgEquivClass.toAlgHomClass AlgEquiv.instAlgEquivClass AlgEquiv.toAlgHom_eq_coe AlgEquiv.comp_symm AlgHom.id_comp
iff_comp_surjective 📖	mathematical	—	Algebra.FormallySmooth AlgHom CommRing.toCommSemiring CommSemiring.toSemiring Ring.toSemiring CommRing.toRing HasQuotient.Quotient Ideal Ideal.instHasQuotient Ideal.Quotient.ring Ideal.instIsTwoSided_1 Ideal.Quotient.algebra AlgHom.comp Ideal.Quotient.mkₐ	—	Ideal.instIsTwoSided_1 comp_surjective of_comp_surjective
iff_of_equiv 📖	mathematical	—	Algebra.FormallySmooth	—	of_equiv
iff_of_surjective 📖	mathematical	DFunLike.coe RingHom Semiring.toNonAssocSemiring CommSemiring.toSemiring CommRing.toCommSemiring RingHom.instFunLike algebraMap	Algebra.FormallySmooth IsIdempotentElem Ideal Submodule.mul Semiring.toModule IsScalarTower.right Algebra.id RingHom.ker RingHom.instRingHomClass	—	IsScalarTower.right RingHom.instRingHomClass iff_split_surjection inst Ideal.Quotient.algHom_ext Ideal.instIsTwoSided_1 Algebra.ext_id IsIdempotentElem.eq_1 pow_two Ideal.mk_ker Ideal.Quotient.algebraMap_eq AlgHomClass.toRingHomClass AlgHom.algHomClass AlgHom.comp_algebraMap RingHom.ker_comp_of_injective AlgEquiv.injective AlgHom.ext Function.Surjective.forall AlgHom.commutes AlgEquivClass.toAlgHomClass AlgEquiv.instAlgEquivClass
iff_split_injection 📖	mathematical	DFunLike.coe RingHom Semiring.toNonAssocSemiring CommSemiring.toSemiring CommRing.toCommSemiring RingHom.instFunLike algebraMap	Algebra.FormallySmooth LinearMap.comp Ideal.Cotangent RingHom.ker RingHom.instRingHomClass TensorProduct KaehlerDifferential NonUnitalNonAssocSemiring.toAddCommMonoid NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing AddCommGroup.toAddCommMonoid instAddCommGroupKaehlerDifferential Algebra.toModule KaehlerDifferential.module' Algebra.id Algebra.to_smulCommClass Ideal.instAddCommGroupCotangent TensorProduct.addCommMonoid Ideal.instModuleCotangentOfAlgebra TensorProduct.instModule RingHom.id RingHomCompTriple.ids KaehlerDifferential.kerCotangentToTensor LinearMap.id	—	Algebra.to_smulCommClass RingHom.instRingHomClass RingHomCompTriple.ids Algebra.formallySmooth_iff Module.Projective.iff_split_of_projective Module.Projective.tensorProduct IsScalarTower.right Module.Projective.of_free Module.Free.self projective_kaehlerDifferential KaehlerDifferential.mapBaseChange_surjective kerCotangentToTensor_injective_iff IsScalarTower.to_smulCommClass LinearMap.IsScalarTower.compatibleSMul TensorProduct.isScalarTower_left KaehlerDifferential.isScalarTower_of_tower RingHomInvPair.ids smulCommClass_self IsScalarTower.to_smulCommClass' Equiv.exists_congr_right List.TFAE.out Function.Exact.split_tfae' KaehlerDifferential.exact_kerCotangentToTensor_mapBaseChange
iff_split_surjection 📖	mathematical	DFunLike.coe AlgHom CommRing.toCommSemiring CommSemiring.toSemiring AlgHom.funLike	Algebra.FormallySmooth AlgHom.comp HasQuotient.Quotient Ideal Ideal.instHasQuotient_1 Monoid.toNatPow MonoidWithZero.toMonoid Semiring.toMonoidWithZero IdemSemiring.toSemiring Submodule.idemSemiring Algebra.id RingHom.ker RingHom Semiring.toNonAssocSemiring RingHom.instFunLike RingHom.instRingHomClass AlgHom.toRingHom Ideal.Quotient.semiring Ideal.instAlgebraQuotient AlgHom.kerSquareLift AlgHom.id	—	RingHom.instRingHomClass Algebra.to_smulCommClass RingHomCompTriple.ids iff_split_injection IsScalarTower.of_algHom nonempty_subtype Equiv.nonempty_congr
iff_subsingleton_and_projective 📖	mathematical	—	Algebra.FormallySmooth Module.Projective CommSemiring.toSemiring CommRing.toCommSemiring KaehlerDifferential AddCommGroup.toAddCommMonoid instAddCommGroupKaehlerDifferential KaehlerDifferential.module' Algebra.id Algebra.to_smulCommClass Algebra.H1Cotangent	—	Algebra.formallySmooth_iff
inst 📖	mathematical	—	Algebra.FormallySmooth Algebra.id CommRing.toCommSemiring	—	of_equiv Algebra.mvPolynomial Empty.instIsEmpty
instFinitePresentationKaehlerDifferentialOfEssFiniteType 📖	mathematical	—	Module.FinitePresentation KaehlerDifferential CommSemiring.toSemiring CommRing.toCommSemiring AddCommGroup.toAddCommMonoid instAddCommGroupKaehlerDifferential KaehlerDifferential.module' Algebra.id Algebra.to_smulCommClass	—	Module.finitePresentation_of_projective Algebra.to_smulCommClass projective_kaehlerDifferential KaehlerDifferential.finite
instLocalization 📖	mathematical	—	Algebra.FormallySmooth Localization CommRing.toCommMonoid OreLocalization.instCommRing OreLocalization.oreSetComm OreLocalization.instAlgebra CommSemiring.toSemiring CommRing.toCommSemiring	—	of_isLocalization Localization.isLocalization comp OreLocalization.instIsScalarTower IsScalarTower.right
instTensorProduct 📖	mathematical	—	Algebra.FormallySmooth TensorProduct CommRing.toCommSemiring NonUnitalNonAssocSemiring.toAddCommMonoid NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing Algebra.toModule CommSemiring.toSemiring Algebra.TensorProduct.instCommRing Algebra.TensorProduct.leftAlgebra Algebra.id Algebra.to_smulCommClass	—	of_comp_surjective Algebra.to_smulCommClass Ideal.instIsTwoSided_1 IsScalarTower.right IsScalarTower.of_algebraMap_eq' TensorProduct.isScalarTower_left Ideal.Quotient.isScalarTower AlgHom.restrictScalars_injective Algebra.TensorProduct.ext' IsScalarTower.left Algebra.smul_def map_smul SemilinearMapClass.toMulActionSemiHomClass NonUnitalAlgHomClass.instLinearMapClass AlgHom.instNonUnitalAlgHomClassOfAlgHomClass AlgHom.algHomClass TensorProduct.smul_tmul' smul_eq_mul mul_one IsScalarTower.to_smulCommClass map_mul NonUnitalRingHomClass.toMulHomClass RingHomClass.toNonUnitalRingHomClass RingHom.instRingHomClass mk_lift
kerCotangentToTensor_injective_iff 📖	mathematical	DFunLike.coe RingHom Semiring.toNonAssocSemiring CommSemiring.toSemiring CommRing.toCommSemiring RingHom.instFunLike algebraMap	Ideal.Cotangent RingHom.ker RingHom.instRingHomClass TensorProduct KaehlerDifferential NonUnitalNonAssocSemiring.toAddCommMonoid NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing AddCommGroup.toAddCommMonoid instAddCommGroupKaehlerDifferential Algebra.toModule KaehlerDifferential.module' Algebra.id Algebra.to_smulCommClass LinearMap RingHom.id Ideal.instAddCommGroupCotangent TensorProduct.addCommMonoid Ideal.instModuleCotangentOfAlgebra TensorProduct.instModule LinearMap.instFunLike KaehlerDifferential.kerCotangentToTensor Algebra.H1Cotangent	—	Function.surjInv_eq Algebra.Extension.cotangentComplex_injective_iff
liftOfSurjective_apply 📖	mathematical	DFunLike.coe AlgHom CommRing.toCommSemiring CommSemiring.toSemiring AlgHom.funLike IsNilpotent Ideal Submodule.pointwiseZero NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring Semiring.toModule Submodule.instPowNat IsScalarTower.right Algebra.id RingHom.ker AlgHomClass.toRingHomClass AlgHom.algHomClass	liftOfSurjective	—	IsScalarTower.right AlgHomClass.toRingHomClass AlgHom.algHomClass AlgEquiv.injective RingHom.instIsTwoSidedKer Ideal.instIsTwoSided_1 AlgEquivClass.toAlgHomClass AlgEquiv.instAlgEquivClass AlgHom.coe_coe AlgHom.comp_apply mk_lift AlgEquiv.apply_symm_apply Ideal.quotientKerAlgEquivOfSurjective_apply RingHom.instRingHomClass
localization_base 📖	mathematical	—	Algebra.FormallySmooth	—	of_comp_surjective Ideal.instIsTwoSided_1 IsScalarTower.right Ideal.Quotient.isScalarTower IsScalarTower.of_algebraMap_eq' AlgHomClass.toRingHomClass AlgHom.algHomClass IsLocalization.ringHom_ext RingHom.comp_assoc IsScalarTower.algebraMap_eq AlgHom.comp_algebraMap AlgHom.ext mk_lift
localization_map 📖	mathematical	—	Algebra.FormallySmooth	—	MonoidWithZeroHomClass.toMonoidHomClass RingHomClass.toMonoidWithZeroHomClass RingHom.instRingHomClass localization_base comp of_isLocalization
mk_lift 📖	mathematical	IsNilpotent Ideal CommSemiring.toSemiring CommRing.toCommSemiring Submodule.pointwiseZero NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring Semiring.toModule Submodule.instPowNat IsScalarTower.right Algebra.id	DFunLike.coe RingHom HasQuotient.Quotient Ring.toSemiring CommRing.toRing Ideal.instHasQuotient Ideal.Quotient.ring Ideal.instIsTwoSided_1 RingHom.instFunLike AlgHom AlgHom.funLike lift Ideal.instHasQuotient_1 Ideal.Quotient.semiring Ideal.instAlgebraQuotient	—	IsScalarTower.right AlgHom.congr_fun Ideal.instIsTwoSided_1 comp_lift
of_comp_surjective 📖	mathematical	AlgHom CommRing.toCommSemiring CommSemiring.toSemiring Ring.toSemiring CommRing.toRing HasQuotient.Quotient Ideal Ideal.instHasQuotient Ideal.Quotient.ring Ideal.instIsTwoSided_1 Ideal.Quotient.algebra AlgHom.comp Ideal.Quotient.mkₐ	Algebra.FormallySmooth	—	Ideal.instIsTwoSided_1 Algebra.Generators.instIsScalarTowerRing IsScalarTower.left RingHom.instRingHomClass iff_split_surjection Algebra.mvPolynomial Algebra.Generators.algebraMap_surjective Ideal.Quotient.lift_surjective_of_surjective AlgHom.ker_kerSquareLift Ideal.cotangentIdeal_square AlgHomClass.toRingHomClass AlgHom.algHomClass RingHom.instIsTwoSidedKer AlgHom.ext AlgEquiv.surjective Ideal.Quotient.mk_surjective AlgEquiv.symm_apply_apply
of_equiv 📖	mathematical	—	Algebra.FormallySmooth	—	RingHom.instRingHomClass iff_split_surjection AlgEquiv.surjective Ideal.instIsTwoSided_1 AlgEquivClass.toAlgHomClass AlgEquiv.instAlgEquivClass AlgHom.ext AlgEquiv.apply_symm_apply
of_isLocalization 📖	mathematical	—	Algebra.FormallySmooth	—	of_comp_surjective Ideal.instIsTwoSided_1 IsNilpotent.isUnit_quotient_mk_iff IsScalarTower.right AlgHom.commutes IsUnit.map MonoidWithZeroHomClass.toMonoidHomClass RingHomClass.toMonoidWithZeroHomClass AlgHomClass.toRingHomClass AlgHom.algHomClass IsLocalization.map_units IsLocalization.lift_eq AlgHom.coe_ringHom_injective IsLocalization.ringHom_ext RingHom.ext AlgHom.comp_algebraMap_of_tower IsScalarTower.left Ideal.Quotient.isScalarTower
of_restrictScalars 📖	mathematical	—	Algebra.FormallySmooth	—	Ideal.instIsTwoSided_1 iff_comp_surjective IsScalarTower.of_algebraMap_eq' Ideal.Quotient.isScalarTower comp_surjective Algebra.FormallyUnramified.comp_injective AlgHom.comp_assoc AlgHom.ext AlgHom.commutes
of_split 📖	mathematical	AlgHom.comp HasQuotient.Quotient Ideal CommSemiring.toSemiring CommRing.toCommSemiring Ideal.instHasQuotient_1 Monoid.toNatPow MonoidWithZero.toMonoid Semiring.toMonoidWithZero IdemSemiring.toSemiring Submodule.idemSemiring Algebra.id RingHom.ker RingHom Semiring.toNonAssocSemiring RingHom.instFunLike RingHom.instRingHomClass AlgHom.toRingHom Ideal.Quotient.semiring Ideal.instAlgebraQuotient AlgHom.kerSquareLift AlgHom.id	Algebra.FormallySmooth	—	RingHom.instRingHomClass iff_split_surjection Ideal.instIsTwoSided_1 Ideal.Quotient.mk_surjective
polynomial 📖	mathematical	—	Algebra.FormallySmooth Polynomial CommSemiring.toSemiring CommRing.toCommSemiring Polynomial.commRing Polynomial.algebraOfAlgebra Algebra.id	—	of_equiv Algebra.mvPolynomial
projective_kaehlerDifferential 📖	mathematical	—	Module.Projective CommSemiring.toSemiring CommRing.toCommSemiring KaehlerDifferential AddCommGroup.toAddCommMonoid instAddCommGroupKaehlerDifferential KaehlerDifferential.module' Algebra.id Algebra.to_smulCommClass	—	—
subsingleton_h1Cotangent 📖	mathematical	—	Algebra.H1Cotangent	—	—

Algebra.Smooth

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
baseChange 📖	mathematical	—	Algebra.Smooth TensorProduct CommRing.toCommSemiring NonUnitalNonAssocSemiring.toAddCommMonoid NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing Algebra.toModule CommSemiring.toSemiring Algebra.TensorProduct.instCommRing Algebra.TensorProduct.leftAlgebra Algebra.id Algebra.to_smulCommClass	—	Algebra.to_smulCommClass Algebra.FormallySmooth.instTensorProduct formallySmooth Algebra.FinitePresentation.baseChange finitePresentation
comp 📖	mathematical	—	Algebra.Smooth	—	Algebra.FormallySmooth.comp formallySmooth Algebra.FinitePresentation.trans finitePresentation
finitePresentation 📖	mathematical	—	Algebra.FinitePresentation CommRing.toCommSemiring CommSemiring.toSemiring	—	—
formallySmooth 📖	mathematical	—	Algebra.FormallySmooth	—	—
of_equiv 📖	mathematical	—	Algebra.Smooth	—	Algebra.FormallySmooth.of_equiv formallySmooth Algebra.FinitePresentation.equiv finitePresentation
of_isLocalization_Away 📖	mathematical	—	Algebra.Smooth	—	Algebra.FormallySmooth.of_isLocalization IsLocalization.Away.finitePresentation

---

← Back to Index