Smooth

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

Statistics

Metric	Count
Definitions Smooth, FormallySmooth, Smooth	3
Theorems holdsForLocalizationAway, isStableUnderBaseChange, localizationPreserves, of_bijective, respectsIso, stableUnderComposition, toAlgebra, comp, holdsForLocalizationAway, id, isStableUnderBaseChange, ofLocalizationSpanTarget, of_bijective, propertyIsLocal, stableUnderComposition, toAlgebra, formallySmooth_algebraMap, smooth_algebraMap, smooth_def	19
Total	22

Algebra

Definitions

Name	Category	Theorems
Smooth 📖	CompData	15 math math: Smooth.comp, smooth_iff, instSmoothOfIsStandardSmooth, Smooth.of_equiv, basicOpen_subset_smoothLocus_iff_smooth, Smooth.of_formallySmooth_fiber, IsSmoothAt.exists_notMem_smooth, Smooth.baseChange, Smooth.exists_subalgebra_finiteType, Smooth.exists_finiteType, Etale.instSmooth, RingHom.Smooth.toAlgebra, Smooth.of_isLocalization_Away, Smooth.exists_subalgebra_fg, RingHom.smooth_algebraMap

RingHom

Definitions

Name	Category	Theorems
FormallySmooth 📖	MathDef	11 math math: FormallySmooth.isStableUnderBaseChange, FormallySmooth.localizationPreserves, AlgebraicGeometry.formallySmooth_stalkMap_iff, formallySmooth_algebraMap, FormallySmooth.stableUnderComposition, AlgebraicGeometry.Scheme.Hom.mem_smoothLocus, FormallySmooth.holdsForLocalizationAway, FormallySmooth.of_bijective, FormallySmooth.respectsIso, AlgebraicGeometry.Scheme.Hom.isOpen_smoothLocus, smooth_def
Smooth 📖	MathDef	19 math math: Smooth.stableUnderComposition, Etale.eq_formallyUnramified_and_smooth, Smooth.comp, AlgebraicGeometry.Scheme.Hom.smooth_appLE, Smooth.holdsForLocalizationAway, AlgebraicGeometry.smooth_iff, Smooth.propertyIsLocal, IsStandardSmooth.smooth, AlgebraicGeometry.exists_smooth_of_formallySmooth_stalk, Smooth.ofLocalizationSpanTarget, Smooth.of_bijective, Smooth.id, Smooth.isStableUnderBaseChange, smooth_iff_locally_isStandardSmooth, AlgebraicGeometry.Smooth.smooth_appLE, AlgebraicGeometry.instHasRingHomPropertySmoothSmooth, etale_iff_formallyUnramified_and_smooth, smooth_def, smooth_algebraMap

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
formallySmooth_algebraMap 📖	mathematical	—	FormallySmooth algebraMap CommRing.toCommSemiring CommSemiring.toSemiring Algebra.FormallySmooth	—	FormallySmooth.eq_1 toAlgebra_algebraMap
smooth_algebraMap 📖	mathematical	—	Smooth algebraMap CommRing.toCommSemiring CommSemiring.toSemiring Algebra.Smooth	—	Smooth.eq_1 toAlgebra_algebraMap
smooth_def 📖	mathematical	—	Smooth FormallySmooth FinitePresentation	—	Algebra.smooth_iff

RingHom.FormallySmooth

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
holdsForLocalizationAway 📖	mathematical	—	RingHom.HoldsForLocalizationAway RingHom.FormallySmooth	—	RingHom.formallySmooth_algebraMap Algebra.FormallySmooth.of_isLocalization
isStableUnderBaseChange 📖	mathematical	—	RingHom.IsStableUnderBaseChange RingHom.FormallySmooth	—	respectsIso Algebra.to_smulCommClass RingHom.formallySmooth_algebraMap Algebra.FormallySmooth.instTensorProduct
localizationPreserves 📖	mathematical	—	RingHom.LocalizationPreserves RingHom.FormallySmooth	—	RingHom.IsStableUnderBaseChange.localizationPreserves isStableUnderBaseChange
of_bijective 📖	mathematical	Function.Bijective DFunLike.coe RingHom Semiring.toNonAssocSemiring CommSemiring.toSemiring CommRing.toCommSemiring RingHom.instFunLike	RingHom.FormallySmooth	—	Algebra.FormallySmooth.of_equiv Algebra.FormallySmooth.inst
respectsIso 📖	mathematical	—	RingHom.RespectsIso RingHom.FormallySmooth	—	RingHom.StableUnderComposition.respectsIso stableUnderComposition RingHom.HoldsForLocalizationAway.of_bijective holdsForLocalizationAway RingEquiv.bijective
stableUnderComposition 📖	mathematical	—	RingHom.StableUnderComposition RingHom.FormallySmooth	—	IsScalarTower.of_algebraMap_eq' Algebra.FormallySmooth.comp toAlgebra
toAlgebra 📖	mathematical	—	Algebra.FormallySmooth RingHom.toAlgebra CommRing.toCommSemiring	—	—

RingHom.Smooth

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
comp 📖	mathematical	—	RingHom.Smooth RingHom.comp Semiring.toNonAssocSemiring CommSemiring.toSemiring CommRing.toCommSemiring	—	IsScalarTower.of_algebraMap_eq' Algebra.Smooth.comp toAlgebra
holdsForLocalizationAway 📖	mathematical	—	RingHom.HoldsForLocalizationAway RingHom.Smooth	—	RingHom.smooth_algebraMap Algebra.FormallySmooth.of_isLocalization IsLocalization.Away.finitePresentation
id 📖	mathematical	—	RingHom.Smooth RingHom.id Semiring.toNonAssocSemiring CommSemiring.toSemiring CommRing.toCommSemiring	—	RingHom.HoldsForLocalizationAway.containsIdentities holdsForLocalizationAway
isStableUnderBaseChange 📖	mathematical	—	RingHom.IsStableUnderBaseChange RingHom.Smooth	—	RingHom.smooth_def RingHom.IsStableUnderBaseChange.and RingHom.FormallySmooth.isStableUnderBaseChange RingHom.finitePresentation_isStableUnderBaseChange
ofLocalizationSpanTarget 📖	mathematical	—	RingHom.OfLocalizationSpanTarget RingHom.Smooth	—	RingHom.finitePresentation_ofLocalizationSpanTarget Algebra.Smooth.finitePresentation Algebra.smoothLocus_eq_univ_iff Set.univ_subset_iff TopologicalSpace.Opens.coe_top PrimeSpectrum.iSup_basicOpen_eq_top_iff' TopologicalSpace.Opens.coe_iSup Algebra.Smooth.formallySmooth
of_bijective 📖	mathematical	Function.Bijective DFunLike.coe RingHom Semiring.toNonAssocSemiring CommSemiring.toSemiring CommRing.toCommSemiring RingHom.instFunLike	RingHom.Smooth	—	RingHom.smooth_def RingHom.FormallySmooth.of_bijective RingHom.FinitePresentation.of_bijective
propertyIsLocal 📖	mathematical	—	RingHom.PropertyIsLocal RingHom.Smooth	—	RingHom.LocalizationPreserves.away RingHom.IsStableUnderBaseChange.localizationPreserves isStableUnderBaseChange ofLocalizationSpanTarget RingHom.OfLocalizationSpanTarget.ofLocalizationSpan RingHom.StableUnderComposition.stableUnderCompositionWithLocalizationAway stableUnderComposition holdsForLocalizationAway
stableUnderComposition 📖	mathematical	—	RingHom.StableUnderComposition RingHom.Smooth	—	comp
toAlgebra 📖	mathematical	—	Algebra.Smooth RingHom.toAlgebra CommRing.toCommSemiring	—	—

---

← Back to Index