Locus

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

Statistics

Metric	Count
Definitions IsSmoothAt, smoothLocus	2
Theorems exists_notMem_smooth, basicOpen_subset_smoothLocus_iff, basicOpen_subset_smoothLocus_iff_smooth, isOpen_smoothLocus, smoothLocus_comap_of_isLocalization, smoothLocus_eq_compl_support_inter, smoothLocus_eq_univ, smoothLocus_eq_univ_iff	8
Total	10

Algebra

Definitions

Name	Category	Theorems
IsSmoothAt 📖	MathDef	1 math math: IsSmoothAt.of_formallySmooth_fiber
smoothLocus 📖	CompOp	9 math math: smoothLocus_eq_univ_iff, basicOpen_subset_smoothLocus_iff_smooth, AlgebraicGeometry.formallySmooth_stalkMap_iff, smoothLocus_comap_of_isLocalization, smoothLocus_eq_univ, isOpen_smoothLocus, smoothLocus_eq_compl_support_inter, basicOpen_subset_smoothLocus_iff, etaleLocus_eq_unramfiedLocus_inter_smoothLocus

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
basicOpen_subset_smoothLocus_iff 📖	mathematical	—	Set PrimeSpectrum CommRing.toCommSemiring Set.instHasSubset SetLike.coe TopologicalSpace.Opens PrimeSpectrum.zariskiTopology TopologicalSpace.Opens.instSetLike PrimeSpectrum.basicOpen smoothLocus FormallySmooth Localization.Away CommRing.toCommMonoid OreLocalization.instCommRing Submonoid.powers CommMonoid.toMonoid OreLocalization.oreSetComm OreLocalization.instAlgebra Ring.toSemiring CommRing.toRing	—	Extension.instIsScalarTowerCotangent IsScalarTower.right to_smulCommClass smoothLocus_eq_compl_support_inter EssFiniteType.of_finiteType FiniteType.of_finitePresentation Set.subset_inter_iff Set.subset_compl_comm PrimeSpectrum.basicOpen_eq_zeroLocus_compl compl_compl LocalizedModule.subsingleton_iff_support_subset formallySmooth_iff RingHomInvPair.ids IsScalarTower.left OreLocalization.instIsScalarTower H1Cotangent.isLocalizedModule Localization.isLocalization Equiv.subsingleton_congr Module.basicOpen_subset_freeLocus_iff instFinitePresentationKaehlerDifferentialOfFinitePresentation OreLocalization.instSMulCommClass KaehlerDifferential.isLocalizedModule_map OreLocalization.instIsScalarTower_1 KaehlerDifferential.isScalarTower_of_tower Module.Projective.of_equiv
basicOpen_subset_smoothLocus_iff_smooth 📖	mathematical	—	Set PrimeSpectrum CommRing.toCommSemiring Set.instHasSubset SetLike.coe TopologicalSpace.Opens PrimeSpectrum.zariskiTopology TopologicalSpace.Opens.instSetLike PrimeSpectrum.basicOpen smoothLocus Smooth Localization.Away CommRing.toCommMonoid OreLocalization.instCommRing Submonoid.powers CommMonoid.toMonoid OreLocalization.oreSetComm OreLocalization.instAlgebra Ring.toSemiring CommRing.toRing	—	IsLocalization.Away.finitePresentation Localization.isLocalization basicOpen_subset_smoothLocus_iff FinitePresentation.trans OreLocalization.instIsScalarTower IsScalarTower.right Smooth.formallySmooth
isOpen_smoothLocus 📖	mathematical	—	IsOpen PrimeSpectrum CommRing.toCommSemiring PrimeSpectrum.zariskiTopology smoothLocus	—	isOpen_iff_forall_mem_open to_smulCommClass TopologicalSpace.IsTopologicalBasis.exists_subset_of_mem_open PrimeSpectrum.isBasis_basic_opens Extension.instIsScalarTowerCotangent IsScalarTower.right Eq.le smoothLocus_eq_compl_support_inter EssFiniteType.of_finiteType FiniteType.of_finitePresentation Module.isOpen_freeLocus instFinitePresentationKaehlerDifferentialOfFinitePresentation IsLocalization.Away.finitePresentation Localization.isLocalization FinitePresentation.trans OreLocalization.instIsScalarTower RingHomInvPair.ids IsScalarTower.left OreLocalization.instSMulCommClass KaehlerDifferential.isLocalizedModule_map OreLocalization.instIsScalarTower_1 KaehlerDifferential.isScalarTower_of_tower Module.Projective.of_equiv Module.basicOpen_subset_freeLocus_iff instEssFiniteTypeLocalization Module.support_eq_zeroLocus instFiniteH1CotangentOfFinitePresentationOfProjectiveKaehlerDifferential IsOpen.inter IsClosed.isOpen_compl PrimeSpectrum.isClosed_zeroLocus Topology.IsOpenEmbedding.isOpenMap PrimeSpectrum.localization_away_isOpenEmbedding smoothLocus_comap_of_isLocalization Set.inter_subset_left PrimeSpectrum.localization_away_comap_range Set.image_preimage_eq_inter_range
smoothLocus_comap_of_isLocalization 📖	mathematical	—	Set.preimage PrimeSpectrum CommRing.toCommSemiring PrimeSpectrum.comap algebraMap CommSemiring.toSemiring smoothLocus	—	Set.ext PrimeSpectrum.isPrime IsLocalization.isLocalization_isLocalization_atPrime_isLocalization OreLocalization.instIsScalarTower IsScalarTower.right Localization.isLocalization FormallySmooth.iff_of_equiv
smoothLocus_eq_compl_support_inter 📖	mathematical	—	smoothLocus Set PrimeSpectrum CommRing.toCommSemiring Set.instInter Compl.compl Set.instCompl Module.support H1Cotangent Extension.instAddCommGroupH1Cotangent Generators.toExtension Generators.self Extension.instModuleH1CotangentOfIsScalarTowerCotangent id Extension.instModuleCotangent Extension.instIsScalarTowerCotangent IsScalarTower.right CommSemiring.toSemiring Module.freeLocus KaehlerDifferential instAddCommGroupKaehlerDifferential KaehlerDifferential.module' to_smulCommClass	—	Set.ext Extension.instIsScalarTowerCotangent IsScalarTower.right to_smulCommClass PrimeSpectrum.isPrime formallySmooth_iff RingHomInvPair.ids IsScalarTower.left OreLocalization.instIsScalarTower H1Cotangent.isLocalizedModule Localization.isLocalization Equiv.subsingleton_congr EssFiniteType.of_isLocalization EssFiniteType.comp Module.free_of_flat_of_isLocalRing Localization.AtPrime.isLocalRing KaehlerDifferential.finite Module.Flat.of_projective Module.Projective.of_free OreLocalization.instSMulCommClass KaehlerDifferential.isLocalizedModule_map OreLocalization.instIsScalarTower_1 KaehlerDifferential.isScalarTower_of_tower Module.Free.of_equiv'
smoothLocus_eq_univ 📖	mathematical	—	smoothLocus Set.univ PrimeSpectrum CommRing.toCommSemiring	—	smoothLocus_eq_univ_iff Smooth.finitePresentation Smooth.formallySmooth
smoothLocus_eq_univ_iff 📖	mathematical	—	smoothLocus Set.univ PrimeSpectrum CommRing.toCommSemiring FormallySmooth	—	Localization.isLocalization Submonoid.powers_one FormallySmooth.iff_of_equiv IsScalarTower.right OreLocalization.instIsScalarTower basicOpen_subset_smoothLocus_iff PrimeSpectrum.basicOpen_one

Algebra.IsSmoothAt

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
exists_notMem_smooth 📖	mathematical	—	Ideal CommSemiring.toSemiring CommRing.toCommSemiring SetLike.instMembership Submodule.setLike NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring Semiring.toModule Algebra.Smooth Localization.Away CommRing.toCommMonoid OreLocalization.instCommRing Submonoid.powers CommMonoid.toMonoid OreLocalization.oreSetComm OreLocalization.instAlgebra Ring.toSemiring CommRing.toRing	—	TopologicalSpace.IsTopologicalBasis.exists_subset_of_mem_open PrimeSpectrum.isBasis_basic_opens Algebra.isOpen_smoothLocus PrimeSpectrum.basicOpen_eq_zeroLocus_compl Algebra.basicOpen_subset_smoothLocus_iff instFinitePresentationAway

---

← Back to Index