Structures · Algebra
Algebra.FormallyEtale
An R-algebra A is formally etale if both Ω[A⁄R] and H¹(L_{A/R}) are zero.
For the infinitesimal lifting definition, see FormallyEtale.iff_comp_bijective.
- Defined in
- Mathlib.RingTheory.Etale.Basic
- Shape
- 2 explicit arguments · adds subsingleton_kaehlerDifferential, subsingleton_h1Cotangent
Extends0
Extends nothing: this is a root of the hierarchy.
Extended by1
Forgetful instances
Provided automatically by
Concrete types that are instances0
No instance on a concrete type; it is reached through other classes.
How is a type an instance?
Loading the hierarchy index…
Assumed by25
- Algebra.FormallyEtale.comp
- KaehlerDifferential.tensorKaehlerEquivOfFormallyEtale
- Algebra.FormallyEtale.of_restrictScalars
- Algebra.FormallyEtale.equivPiOfIsSepClosed
- Algebra.FormallyEtale.of_equiv
- Algebra.FormallyEtale.localization_base
- Algebra.FormallyEtale.comp_bijective
- KaehlerDifferential.tensorKaehlerEquivOfFormallyEtale_apply
- Algebra.FormallySmooth.iff_restrictScalars
- Algebra.FormallyEtale.equivPiOfIsSepClosed_comap
- KaehlerDifferential.tensorKaehlerEquivOfFormallyEtale_symm_D_algebraMap
- Algebra.FormallyEtale.subsingleton_h1Cotangent
- KaehlerDifferential.isBaseChange_of_formallyEtale
- Algebra.FormallyEtale.instTensorProduct
- Algebra.FormallyEtale.instFormallyUnramified
- Algebra.FormallyEtale.instForallOfFinite
- Algebra.FormallyEtale.instFormallySmooth
- Algebra.IsFiniteSplit.instOfIsSepClosedOfEssFiniteTypeOfFormallyEtale
- Algebra.FormallyEtale.iff_restrictScalars
- KaehlerDifferential.tensorKaehlerEquivOfFormallyEtale.congr_simp
- Algebra.FormallyEtale.subsingleton_kaehlerDifferential
- Algebra.FormallyEtale.equivPiOfIsSepClosed.congr_simp
- Algebra.FormallyEtale.instLocalization
- Algebra.FormallyEtale.instIsSeparableQuotientIdealOfEssFiniteTypeOfIsPrime
- Algebra.FormallyEtale.localization_map
Ancestors0
No ancestors.