StandardSmoothOfFree

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

Statistics

Metric	Count
Definitions	0
Theorems iff_isStandardSmoothOfRelativeDimension_zero, exists_notMem_isStandardSmooth, iff_exists_basis_kaehlerDifferential, of_basis_kaehlerDifferential, exists_span_eq_top_isStandardSmooth	5
Total	5

Algebra.Etale

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
iff_isStandardSmoothOfRelativeDimension_zero 📖	mathematical	—	Algebra.Etale Algebra.IsStandardSmoothOfRelativeDimension	—	Mathlib.Tactic.Nontriviality.subsingleton_or_nontrivial_elim Algebra.instIsStandardSmoothOfRelativeDimensionOfNatNatOfSubsingleton Algebra.to_smulCommClass smulCommClass_self Algebra.IsStandardSmooth.iff_exists_basis_kaehlerDifferential finitePresentation Algebra.FormallyEtale.subsingleton_h1Cotangent formallyEtale Algebra.FormallyEtale.subsingleton_kaehlerDifferential Empty.instIsEmpty rank_subsingleton' CharP.cast_eq_zero CharP.ofCharZero Cardinal.instCharZero Algebra.instEtaleOfIsStandardSmoothOfRelativeDimensionOfNatNat

Algebra.IsSmoothAt

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
exists_notMem_isStandardSmooth 📖	mathematical	—	Ideal CommSemiring.toSemiring CommRing.toCommSemiring SetLike.instMembership Submodule.setLike NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring Semiring.toModule Algebra.IsStandardSmooth Localization.Away CommRing.toCommMonoid OreLocalization.instCommRing Submonoid.powers CommMonoid.toMonoid OreLocalization.oreSetComm OreLocalization.instAlgebra Ring.toSemiring CommRing.toRing	—	Algebra.to_smulCommClass IsScalarTower.to_smulCommClass OreLocalization.instIsScalarTower IsScalarTower.right IsScalarTower.left smulCommClass_self Module.exists_basis_of_span_of_flat Localization.AtPrime.isLocalRing Algebra.FormallySmooth.instFinitePresentationKaehlerDifferentialOfEssFiniteType Algebra.instEssFiniteTypeLocalization Algebra.EssFiniteType.of_finiteType Algebra.FiniteType.of_finitePresentation Module.Flat.of_projective Algebra.FormallySmooth.projective_kaehlerDifferential KaehlerDifferential.span_range_map_derivation_of_isLocalization Localization.isLocalization OreLocalization.instSMulCommClass IsScalarTower.to_smulCommClass' KaehlerDifferential.isScalarTower_of_tower instIsLocalizedModuleFinsuppLinearMap instIsLocalizedModuleLinearMapOfIsLocalization KaehlerDifferential.isLocalizedModule_map Finsupp.isScalarTower RingHomInvPair.ids Finsupp.lhom_ext' LinearMap.ext_ring RingHomCompTriple.ids LinearMap.map_zero Finsupp.mapRange_single map_one MonoidHomClass.toOneHomClass MonoidWithZeroHomClass.toMonoidHomClass RingHomClass.toMonoidWithZeroHomClass RingHom.instRingHomClass IsLocalizedModule.map_apply Finsupp.linearCombination_single one_smul KaehlerDifferential.map_D LinearMap.comp.congr_simp Module.Basis.coe_repr_symm LinearEquiv.bijective Module.Finite.finite_basis IsLocalRing.toNontrivial KaehlerDifferential.finite OreLocalization.instIsScalarTower_1 Module.FinitePresentation.exists_notMem_bijective Module.Finite.finsupp Module.Finite.self Algebra.Smooth.formallySmooth Algebra.IsStandardSmooth.of_basis_kaehlerDifferential instFinitePresentationAway Algebra.FormallySmooth.subsingleton_h1Cotangent Algebra.FormallySmooth.instLocalization IsLocalizedModule.map_bijective_iff_localizedModuleMap_bijective LinearMap.CompatibleSMul.finsupp_dom LinearMap.IsScalarTower.compatibleSMul' IsLocalizedModule.map_linearCombination exists_notMem_smooth IsLocalization.isPrime_of_isPrime_disjoint Ideal.disjoint_powers_iff_notMem Ideal.IsPrime.isRadical IsLocalization.Away.mul_of_associated IsLocalization.Away.associated_sec_fst Ideal.IsPrime.mul_notMem Ideal.mem_iff_of_associated Associated.symm Ideal.mem_map_of_mem Algebra.IsStandardSmooth.of_algEquiv

Algebra.IsStandardSmooth

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
iff_exists_basis_kaehlerDifferential 📖	mathematical	—	Algebra.IsStandardSmooth Algebra.H1Cotangent Set KaehlerDifferential Set.instHasSubset Set.range DFunLike.coe Module.Basis CommSemiring.toSemiring CommRing.toCommSemiring AddCommGroup.toAddCommMonoid instAddCommGroupKaehlerDifferential KaehlerDifferential.module' Algebra.id Algebra.to_smulCommClass Module.Basis.instFunLike Derivation smulCommClass_self CommRing.toCommMonoid DistribMulAction.toMulAction CommMonoid.toMonoid AddCommMonoid.toAddMonoid NonUnitalNonAssocSemiring.toAddCommMonoid NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing Module.toDistribMulAction Ring.toSemiring CommRing.toRing Algebra.toModule Derivation.instFunLike KaehlerDifferential.D	—	Algebra.to_smulCommClass smulCommClass_self subsingleton_h1Cotangent out Algebra.SubmersivePresentation.basisKaehler_apply of_basis_kaehlerDifferential
of_basis_kaehlerDifferential 📖	mathematical	Set KaehlerDifferential Set.instHasSubset Set.range DFunLike.coe Module.Basis CommSemiring.toSemiring CommRing.toCommSemiring AddCommGroup.toAddCommMonoid instAddCommGroupKaehlerDifferential KaehlerDifferential.module' Algebra.id Algebra.to_smulCommClass Module.Basis.instFunLike Derivation smulCommClass_self CommRing.toCommMonoid DistribMulAction.toMulAction CommMonoid.toMonoid AddCommMonoid.toAddMonoid NonUnitalNonAssocSemiring.toAddCommMonoid NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing Module.toDistribMulAction Ring.toSemiring CommRing.toRing Algebra.toModule Derivation.instFunLike KaehlerDifferential.D	Algebra.IsStandardSmooth	—	Algebra.to_smulCommClass smulCommClass_self Mathlib.Tactic.Nontriviality.subsingleton_or_nontrivial_elim Algebra.instIsStandardSmoothOfSubsingleton Algebra.FiniteType.iff_exists_generators Algebra.FiniteType.of_finitePresentation Sum.inl_injective Algebra.Generators.cotangentRestrict_bijective_of_basis_kaehlerDifferential IsCompl.symm Set.isCompl_range_inl_range_inr RingHomInvPair.ids Module.Finite.finite_basis KaehlerDifferential.finite Algebra.EssFiniteType.of_finiteType Algebra.Presentation.relation_mem_ker Algebra.Generators.exists_presentation_of_basis_cotangent Finite.instSum Finite.of_fintype Sum.map_injective Algebra.PreSubmersivePresentation.isUnit_jacobian_of_cotangentRestrict_bijective Algebra.SubmersivePresentation.isStandardSmooth

Algebra.Smooth

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
exists_span_eq_top_isStandardSmooth 📖	mathematical	—	Ideal.span CommSemiring.toSemiring CommRing.toCommSemiring Top.top Ideal Submodule.instTop NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring Semiring.toModule Algebra.IsStandardSmooth Localization.Away CommRing.toCommMonoid OreLocalization.instCommRing Submonoid.powers CommMonoid.toMonoid OreLocalization.oreSetComm OreLocalization.instAlgebra Ring.toSemiring CommRing.toRing	—	PrimeSpectrum.isPrime Algebra.FormallySmooth.instLocalization formallySmooth isOpen_iUnion TopologicalSpace.Opens.is_open' PrimeSpectrum.basicOpen_eq_zeroLocus_compl Algebra.IsSmoothAt.exists_notMem_isStandardSmooth finitePresentation

---

← Back to Index