Etale

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

Statistics

Metric	Count
Definitions Etale, Etale	2
Theorems containsIdentities, eq_formallyUnramified_and_smooth, formallyUnramified, iff_flat_and_formallyUnramified, isStableUnderBaseChange, ofLocalizationSpan, ofLocalizationSpanTarget, of_bijective, propertyIsLocal, respectsIso, stableUnderComposition, toAlgebra, etale_algebraMap, etale_iff_formallyUnramified_and_smooth	14
Total	16

Algebra

Definitions

Name	Category	Theorems
Etale 📖	CompData	24 math math: basicOpen_subset_etaleLocus_iff_etale, Etale.of_equiv, etaleLocus_eq_univ_iff_etale, Etale.of_formallyUnramified_of_flat, instEtaleOfIsStandardEtale, Etale.of_isLocalizationAway, Etale.iff_isStandardSmoothOfRelativeDimension_zero, RingHom.Etale.toAlgebra, Etale.of_isLocalization_Away, exists_etale_isIdempotentElem_forall_liesOver_eq, Etale.exists_subalgebra_fg, FormallyEtale.instEtaleForallOfFinite, RingHom.etale_algebraMap, exists_etale_bijective_residueFieldMap_and_map_eq_mul_and_isCoprime, exists_etale_of_isEtaleAt, Etale.baseChange, Etale.comp, exists_etale_isIdempotentElem_forall_liesOver_eq_aux, instEtaleOfIsStandardSmoothOfRelativeDimensionOfNatNat, Etale.iff_exists_algEquiv_prod, StandardEtalePair.instEtaleRing, Etale.instAway, Polynomial.instEtaleUniversalCoprimeFactorizationRing, IsFiniteSplit.instEtale

RingHom

Definitions

Name	Category	Theorems
Etale 📖	MathDef	20 math math: AlgebraicGeometry.Etale.etale_appLE, Etale.eq_formallyUnramified_and_smooth, Etale.stableUnderComposition, etale_iff_isStandardSmoothOfRelativeDimension_zero, Etale.iff_flat_and_formallyUnramified, Etale.propertyIsLocal, Etale.ofLocalizationSpan, Etale.isStableUnderBaseChange, AlgebraicGeometry.Scheme.Hom.etale_appLE, IsStandardSmooth.exists_etale_mvPolynomial, etale_algebraMap, AlgebraicGeometry.Etale.instHasRingHomPropertyEtale, Etale.respectsIso, AlgebraicGeometry.etale_iff, etale_iff_formallyUnramified_and_smooth, IsStandardSmoothOfRelativeDimension.exists_etale_mvPolynomial, Etale.ofLocalizationSpanTarget, Algebra.IsStandardSmoothOfRelativeDimension.exists_etale_mvPolynomial, Etale.containsIdentities, Etale.of_bijective

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
etale_algebraMap 📖	mathematical	—	Etale algebraMap CommRing.toCommSemiring CommSemiring.toSemiring Algebra.Etale	—	Etale.eq_1 toAlgebra_algebraMap
etale_iff_formallyUnramified_and_smooth 📖	mathematical	—	Etale FormallyUnramified Smooth	—	Algebra.FormallyEtale.instFormallyUnramified Algebra.Etale.formallyEtale Algebra.Smooth.formallySmooth Algebra.Etale.instSmooth Algebra.Etale.finitePresentation Algebra.FormallyEtale.of_formallyUnramified_and_formallySmooth Algebra.Smooth.finitePresentation

RingHom.Etale

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
containsIdentities 📖	mathematical	—	RingHom.ContainsIdentities RingHom.Etale	—	of_bijective Function.bijective_id
eq_formallyUnramified_and_smooth 📖	mathematical	—	RingHom.Etale RingHom.FormallyUnramified RingHom.Smooth	—	RingHom.etale_iff_formallyUnramified_and_smooth
formallyUnramified 📖	mathematical	—	RingHom.FormallyUnramified	—	RingHom.etale_iff_formallyUnramified_and_smooth
iff_flat_and_formallyUnramified 📖	mathematical	—	RingHom.Etale RingHom.Flat RingHom.FormallyUnramified RingHom.FinitePresentation	—	Algebra.Smooth.flat Algebra.Etale.instSmooth Algebra.FormallyEtale.instFormallyUnramified Algebra.Etale.formallyEtale Algebra.Etale.finitePresentation Algebra.Etale.of_formallyUnramified_of_flat
isStableUnderBaseChange 📖	mathematical	—	RingHom.IsStableUnderBaseChange RingHom.Etale	—	eq_formallyUnramified_and_smooth RingHom.IsStableUnderBaseChange.and RingHom.FormallyUnramified.isStableUnderBaseChange RingHom.Smooth.isStableUnderBaseChange
ofLocalizationSpan 📖	mathematical	—	RingHom.OfLocalizationSpan RingHom.Etale	—	RingHom.PropertyIsLocal.ofLocalizationSpan propertyIsLocal
ofLocalizationSpanTarget 📖	mathematical	—	RingHom.OfLocalizationSpanTarget RingHom.Etale	—	RingHom.PropertyIsLocal.ofLocalizationSpanTarget propertyIsLocal
of_bijective 📖	mathematical	Function.Bijective DFunLike.coe RingHom Semiring.toNonAssocSemiring CommSemiring.toSemiring CommRing.toCommSemiring RingHom.instFunLike	RingHom.Etale	—	RingHom.etale_iff_formallyUnramified_and_smooth RingHom.FormallyUnramified.of_surjective RingHom.Smooth.of_bijective
propertyIsLocal 📖	mathematical	—	RingHom.PropertyIsLocal RingHom.Etale	—	eq_formallyUnramified_and_smooth RingHom.PropertyIsLocal.and RingHom.FormallyUnramified.propertyIsLocal RingHom.Smooth.propertyIsLocal
respectsIso 📖	mathematical	—	RingHom.RespectsIso RingHom.Etale	—	RingHom.PropertyIsLocal.respectsIso propertyIsLocal
stableUnderComposition 📖	mathematical	—	RingHom.StableUnderComposition RingHom.Etale	—	eq_formallyUnramified_and_smooth RingHom.StableUnderComposition.and RingHom.FormallyUnramified.stableUnderComposition RingHom.Smooth.stableUnderComposition
toAlgebra 📖	mathematical	—	Algebra.Etale RingHom.toAlgebra CommRing.toCommSemiring	—	—

---

← Back to Index