NoetherianDescent

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

Statistics

Metric	Count
Definitions	0
Theorems exists_subalgebra_fg, exists_subalgebra_fg, exists_finiteType, exists_subalgebra_fg, exists_subalgebra_finiteType	5
Total	5

Algebra.Etale

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
exists_subalgebra_fg 📖	mathematical	—	Subalgebra.FG CommRing.toCommSemiring CommSemiring.toSemiring Algebra.Etale Subalgebra SetLike.instMembership Subalgebra.instSetLike Subalgebra.toCommRing AlgEquiv TensorProduct Subalgebra.toCommSemiring NonUnitalNonAssocSemiring.toAddCommMonoid NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing Subalgebra.moduleLeft Semiring.toModule Algebra.toModule Algebra.TensorProduct.instSemiring Subalgebra.toAlgebra Algebra.id Algebra.TensorProduct.leftAlgebra Algebra.to_smulCommClass	—	Algebra.to_smulCommClass Algebra.IsStandardSmoothOfRelativeDimension.exists_subalgebra_fg

Algebra.IsStandardSmoothOfRelativeDimension

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
exists_subalgebra_fg 📖	mathematical	—	Subalgebra.FG CommRing.toCommSemiring CommSemiring.toSemiring Algebra.IsStandardSmoothOfRelativeDimension Subalgebra SetLike.instMembership Subalgebra.instSetLike Subalgebra.toCommRing AlgEquiv TensorProduct Subalgebra.toCommSemiring NonUnitalNonAssocSemiring.toAddCommMonoid NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing Subalgebra.moduleLeft Semiring.toModule Algebra.toModule Algebra.TensorProduct.instSemiring Subalgebra.toAlgebra Algebra.id Algebra.TensorProduct.leftAlgebra Algebra.to_smulCommClass	—	Algebra.to_smulCommClass out IsScalarTower.subalgebra Subalgebra.range_algebraMap Algebra.SubmersivePresentation.instHasCoeffs Algebra.SubmersivePresentation.finite_coeffs Set.Finite.coe_toFinset Subalgebra.instFaithfulSMulSubtypeMem instFaithfulSMul IsScalarTower.right

Algebra.Smooth

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
exists_finiteType 📖	mathematical	—	DFunLike.coe RingHom Semiring.toNonAssocSemiring CommSemiring.toSemiring CommRing.toCommSemiring RingHom.instFunLike algebraMap Algebra.FiniteType Algebra.Smooth AlgEquiv TensorProduct NonUnitalNonAssocSemiring.toAddCommMonoid NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing Algebra.toModule Algebra.TensorProduct.instSemiring Algebra.TensorProduct.leftAlgebra Algebra.id Algebra.to_smulCommClass	—	Algebra.to_smulCommClass exists_subalgebra_fg Subtype.val_injective Subalgebra.fg_top
exists_subalgebra_fg 📖	mathematical	—	Subalgebra.FG CommRing.toCommSemiring CommSemiring.toSemiring Algebra.Smooth Subalgebra SetLike.instMembership Subalgebra.instSetLike Subalgebra.toCommRing AlgEquiv TensorProduct Subalgebra.toCommSemiring NonUnitalNonAssocSemiring.toAddCommMonoid NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing Subalgebra.moduleLeft Semiring.toModule Algebra.toModule Algebra.TensorProduct.instSemiring Subalgebra.toAlgebra Algebra.id Algebra.TensorProduct.leftAlgebra Algebra.to_smulCommClass	—	finitePresentation Algebra.Generators.instIsScalarTowerRing IsScalarTower.left AlgHomClass.toRingHomClass AlgHom.algHomClass Algebra.Presentation.span_range_relation_eq_ker RingHom.instRingHomClass Algebra.to_smulCommClass Algebra.FormallySmooth.iff_split_surjection Algebra.mvPolynomial Algebra.Generators.algebraMap_surjective formallySmooth Ideal.instIsTwoSided_1 Ideal.Quotient.mk_surjective MvPolynomial.algHom_ext MvPolynomial.aeval_X Algebra.Presentation.aeval_val_relation map_zero MonoidWithZeroHomClass.toZeroHomClass RingHomClass.toMonoidWithZeroHomClass Algebra.Generators.algebraMap_apply map_sub DistribMulActionSemiHomClass.toAddMonoidHomClass NonUnitalAlgSemiHomClass.toDistribMulActionSemiHomClass AlgHom.instNonUnitalAlgHomClassOfAlgHomClass Finite.of_fintype Algebra.FormallySmooth.of_split Algebra.Presentation.instFinitePresentationModelOfHasCoeffsOfFinite IsScalarTower.right
exists_subalgebra_finiteType 📖	mathematical	—	Algebra.FiniteType Subalgebra CommRing.toCommSemiring CommSemiring.toSemiring SetLike.instMembership Subalgebra.instSetLike Subalgebra.toSemiring Subalgebra.algebra Algebra.Smooth Subalgebra.toCommRing AlgEquiv TensorProduct Subalgebra.toCommSemiring NonUnitalNonAssocSemiring.toAddCommMonoid NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing Subalgebra.moduleLeft Semiring.toModule Algebra.toModule Algebra.TensorProduct.instSemiring Subalgebra.toAlgebra Algebra.id Algebra.TensorProduct.leftAlgebra Algebra.to_smulCommClass	—	Algebra.to_smulCommClass exists_subalgebra_fg Subalgebra.fg_iff_finiteType

---

← Back to Index