Basic

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

Statistics

Metric	Count
Definitions FormallyEtale, FormallyEtale	2
Theorems baseChange, comp, finitePresentation, formallyEtale, instAway, instSmooth, of_equiv, of_isLocalizationAway, of_isLocalization_Away, iff_of_surjective, of_restrictScalars, comp, comp_bijective, iff_comp_bijective, iff_formallyUnramified_and_formallySmooth, iff_of_equiv, iff_of_surjective, iff_restrictScalars, iff_unramified_and_smooth, instFormallySmooth, instFormallyUnramified, instLocalization, instTensorProduct, localization_base, localization_map, of_equiv, of_formallyUnramified_and_formallySmooth, of_isLocalization, of_restrictScalars, of_unramified_and_smooth, subsingleton_h1Cotangent, subsingleton_kaehlerDifferential, iff_restrictScalars, formallyEtale_iff, comp, formallyEtale_algebraMap	36
Total	38

Algebra

Definitions

Name	Category	Theorems
FormallyEtale 📖	CompData	31 math math: FormallyEtale.of_unramified_and_smooth, FormallyEtale.comp, FormallyEtale.of_isSeparable_aux, FormallyEtale.instLocalization, FormallyEtale.of_isLocalization, formallyEtale_iff, Etale.formallyEtale, FormallyEtale.iff_isSeparable, StandardEtalePair.instFormallyEtaleRing, etaleLocus_eq_univ_iff, FormallyEtale.localization_base, RingHom.formallyEtale_algebraMap, FormallyEtale.instTensorProduct, basicOpen_subset_etaleLocus_iff, FormallyEtale.iff_formallyUnramified_of_field, FormallyEtale.Algebra.FormallyEtale.iff_of_surjective, FormallyEtale.iff_comp_bijective, FormallyEtale.of_restrictScalars, FormallyEtale.iff_formallyUnramified_and_formallySmooth, FormallyEtale.pi_iff, FormallyEtale.iff_exists_algEquiv_prod, FormallyEtale.of_formallyUnramified_and_formallySmooth, FormallyEtale.of_isSeparable, FormallyEtale.of_equiv, FormallyEtale.iff_unramified_and_smooth, FormallyEtale.of_formallyUnramified_of_field, FormallyEtale.Algebra.FormallyEtale.of_restrictScalars, FormallyEtale.iff_of_surjective, FormallyEtale.iff_restrictScalars, FormallyEtale.localization_map, FormallyEtale.iff_of_equiv

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
formallyEtale_iff 📖	mathematical	—	FormallyEtale KaehlerDifferential H1Cotangent	—	—

Algebra.Etale

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
baseChange 📖	mathematical	—	Algebra.Etale TensorProduct CommRing.toCommSemiring NonUnitalNonAssocSemiring.toAddCommMonoid NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing Algebra.toModule CommSemiring.toSemiring Algebra.TensorProduct.instCommRing Algebra.TensorProduct.leftAlgebra Algebra.id Algebra.to_smulCommClass	—	Algebra.to_smulCommClass Algebra.FormallyEtale.instTensorProduct formallyEtale Algebra.FinitePresentation.baseChange finitePresentation
comp 📖	mathematical	—	Algebra.Etale	—	Algebra.FormallyEtale.comp formallyEtale Algebra.FinitePresentation.trans finitePresentation
finitePresentation 📖	mathematical	—	Algebra.FinitePresentation CommRing.toCommSemiring CommSemiring.toSemiring	—	—
formallyEtale 📖	mathematical	—	Algebra.FormallyEtale	—	—
instAway 📖	mathematical	—	Algebra.Etale Localization.Away CommRing.toCommMonoid OreLocalization.instCommRing Submonoid.powers CommMonoid.toMonoid OreLocalization.oreSetComm OreLocalization.instAlgebra Ring.toSemiring CommRing.toRing CommRing.toCommSemiring	—	Algebra.FormallyEtale.instLocalization formallyEtale instFinitePresentationAway finitePresentation
instSmooth 📖	mathematical	—	Algebra.Smooth	—	Algebra.FormallyEtale.instFormallySmooth formallyEtale finitePresentation
of_equiv 📖	mathematical	—	Algebra.Etale	—	Algebra.FormallyEtale.of_equiv formallyEtale Algebra.FinitePresentation.equiv finitePresentation
of_isLocalizationAway 📖	mathematical	—	Algebra.Etale	—	Algebra.FormallyEtale.of_isLocalization IsLocalization.Away.finitePresentation
of_isLocalization_Away 📖	mathematical	—	Algebra.Etale	—	of_isLocalizationAway

Algebra.FormallyEtale

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
comp 📖	mathematical	—	Algebra.FormallyEtale	—	iff_formallyUnramified_and_formallySmooth Algebra.FormallyUnramified.comp instFormallyUnramified Algebra.FormallySmooth.comp instFormallySmooth
comp_bijective 📖	mathematical	Ideal CommSemiring.toSemiring CommRing.toCommSemiring Monoid.toNatPow MonoidWithZero.toMonoid Semiring.toMonoidWithZero IdemSemiring.toSemiring Submodule.idemSemiring Algebra.id Bot.bot Submodule.instBot NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring Semiring.toModule	Function.Bijective AlgHom Ring.toSemiring CommRing.toRing HasQuotient.Quotient Ideal.instHasQuotient Ideal.Quotient.ring Ideal.instIsTwoSided_1 Ideal.Quotient.algebra AlgHom.comp Ideal.Quotient.mkₐ	—	Ideal.instIsTwoSided_1 Algebra.FormallyUnramified.comp_injective instFormallyUnramified Algebra.FormallySmooth.comp_surjective instFormallySmooth
iff_comp_bijective 📖	mathematical	—	Algebra.FormallyEtale Function.Bijective AlgHom CommRing.toCommSemiring CommSemiring.toSemiring Ring.toSemiring CommRing.toRing HasQuotient.Quotient Ideal Ideal.instHasQuotient Ideal.Quotient.ring Ideal.instIsTwoSided_1 Ideal.Quotient.algebra AlgHom.comp Ideal.Quotient.mkₐ	—	Ideal.instIsTwoSided_1 comp_bijective Algebra.FormallyUnramified.iff_comp_injective_of_small UnivLE.small univLE_of_max UnivLE.self Function.Bijective.injective Algebra.FormallySmooth.of_comp_surjective Function.Bijective.surjective of_formallyUnramified_and_formallySmooth
iff_formallyUnramified_and_formallySmooth 📖	mathematical	—	Algebra.FormallyEtale Algebra.FormallyUnramified Algebra.FormallySmooth	—	instFormallyUnramified instFormallySmooth Algebra.FormallyUnramified.subsingleton_kaehlerDifferential Algebra.FormallySmooth.subsingleton_h1Cotangent
iff_of_equiv 📖	mathematical	—	Algebra.FormallyEtale	—	of_equiv
iff_of_surjective 📖	mathematical	DFunLike.coe RingHom Semiring.toNonAssocSemiring CommSemiring.toSemiring CommRing.toCommSemiring RingHom.instFunLike algebraMap	Algebra.FormallyEtale IsIdempotentElem Ideal Submodule.mul Semiring.toModule IsScalarTower.right Algebra.id RingHom.ker RingHom.instRingHomClass	—	IsScalarTower.right RingHom.instRingHomClass iff_formallyUnramified_and_formallySmooth Algebra.FormallySmooth.iff_of_surjective Algebra.FormallyUnramified.of_surjective Algebra.FormallyUnramified.inst
iff_restrictScalars 📖	mathematical	—	Algebra.FormallyEtale	—	of_restrictScalars instFormallyUnramified comp
iff_unramified_and_smooth 📖	mathematical	—	Algebra.FormallyEtale Algebra.FormallyUnramified Algebra.FormallySmooth	—	iff_formallyUnramified_and_formallySmooth
instFormallySmooth 📖	mathematical	—	Algebra.FormallySmooth	—	Algebra.to_smulCommClass Module.Projective.of_free Module.Free.of_subsingleton subsingleton_kaehlerDifferential subsingleton_h1Cotangent
instFormallyUnramified 📖	mathematical	—	Algebra.FormallyUnramified	—	subsingleton_kaehlerDifferential
instLocalization 📖	mathematical	—	Algebra.FormallyEtale Localization CommRing.toCommMonoid OreLocalization.instCommRing OreLocalization.oreSetComm OreLocalization.instAlgebra CommSemiring.toSemiring CommRing.toCommSemiring	—	of_formallyUnramified_and_formallySmooth Algebra.FormallyUnramified.instLocalization instFormallyUnramified Algebra.FormallySmooth.instLocalization instFormallySmooth
instTensorProduct 📖	mathematical	—	Algebra.FormallyEtale TensorProduct CommRing.toCommSemiring NonUnitalNonAssocSemiring.toAddCommMonoid NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing Algebra.toModule CommSemiring.toSemiring Algebra.TensorProduct.instCommRing Algebra.TensorProduct.leftAlgebra Algebra.id Algebra.to_smulCommClass	—	of_formallyUnramified_and_formallySmooth Algebra.to_smulCommClass Algebra.FormallyUnramified.base_change instFormallyUnramified Algebra.FormallySmooth.instTensorProduct instFormallySmooth
localization_base 📖	mathematical	—	Algebra.FormallyEtale	—	iff_formallyUnramified_and_formallySmooth Algebra.FormallyUnramified.localization_base instFormallyUnramified Algebra.FormallySmooth.localization_base instFormallySmooth
localization_map 📖	mathematical	—	Algebra.FormallyEtale	—	MonoidWithZeroHomClass.toMonoidHomClass RingHomClass.toMonoidWithZeroHomClass RingHom.instRingHomClass localization_base comp of_isLocalization
of_equiv 📖	mathematical	—	Algebra.FormallyEtale	—	iff_formallyUnramified_and_formallySmooth Algebra.FormallyUnramified.of_equiv instFormallyUnramified Algebra.FormallySmooth.of_equiv instFormallySmooth
of_formallyUnramified_and_formallySmooth 📖	mathematical	—	Algebra.FormallyEtale	—	iff_formallyUnramified_and_formallySmooth
of_isLocalization 📖	mathematical	—	Algebra.FormallyEtale	—	iff_formallyUnramified_and_formallySmooth Algebra.FormallyUnramified.of_isLocalization Algebra.FormallySmooth.of_isLocalization
of_restrictScalars 📖	mathematical	—	Algebra.FormallyEtale	—	Algebra.FormallyUnramified.of_restrictScalars instFormallyUnramified Algebra.FormallySmooth.of_restrictScalars instFormallySmooth of_formallyUnramified_and_formallySmooth
of_unramified_and_smooth 📖	mathematical	—	Algebra.FormallyEtale	—	of_formallyUnramified_and_formallySmooth
subsingleton_h1Cotangent 📖	mathematical	—	Algebra.H1Cotangent	—	—
subsingleton_kaehlerDifferential 📖	mathematical	—	KaehlerDifferential	—	—

Algebra.FormallyEtale.Algebra.FormallyEtale

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
iff_of_surjective 📖	mathematical	DFunLike.coe RingHom Semiring.toNonAssocSemiring CommSemiring.toSemiring CommRing.toCommSemiring RingHom.instFunLike algebraMap	Algebra.FormallyEtale IsIdempotentElem Ideal Submodule.mul Semiring.toModule IsScalarTower.right Algebra.id RingHom.ker RingHom.instRingHomClass	—	Algebra.FormallyEtale.iff_of_surjective
of_restrictScalars 📖	mathematical	—	Algebra.FormallyEtale	—	Algebra.FormallyEtale.of_restrictScalars

Algebra.FormallySmooth

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
iff_restrictScalars 📖	mathematical	—	Algebra.FormallySmooth	—	of_restrictScalars Algebra.FormallyEtale.instFormallyUnramified comp Algebra.FormallyEtale.instFormallySmooth

RingHom

Definitions

Name	Category	Theorems
FormallyEtale 📖	MathDef	3 math math: formallyEtale_algebraMap, FormallyEtale.comp, FormallyEtale.of_comp

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
formallyEtale_algebraMap 📖	mathematical	—	FormallyEtale algebraMap CommRing.toCommSemiring CommSemiring.toSemiring Algebra.FormallyEtale	—	FormallyEtale.eq_1 toAlgebra_algebraMap

RingHom.FormallyEtale

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
comp 📖	mathematical	—	RingHom.FormallyEtale RingHom.comp Semiring.toNonAssocSemiring CommSemiring.toSemiring CommRing.toCommSemiring	—	IsScalarTower.of_algebraMap_eq' Algebra.FormallyEtale.comp

---

← Back to Index