Theorems · Inductive type · commutative algebra
Algebra.FormallyEtale
(R : Type u) → (A : Type v) → [inst : CommRing R] → [inst_1 : CommRing A] → [Algebra R A] → Prop
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
- Cited by
- 37 results in Mathlib
- Foundations
- Depth 6 from the axioms · uses no axioms
Around this declaration
Dashed lines are statement dependencies; solid lines are citations in proofs.
Cites2
Mathlib declarations this one mentions in its statement or cites explicitly in its proof. Plumbing is filtered out.
Cited by45
Results whose statement or proof uses this declaration.
- Algebra.FormallyEtale.iff_formallyUnramified_and_formallySmoothstatement and proof · cited by 8
- Algebra.FormallyEtale.compstatement and proof · cited by 5
- Algebra.IsEtaleAtproof · cited by 5
- KaehlerDifferential.tensorKaehlerEquivOfFormallyEtalestatement and proof · cited by 5
- Algebra.FormallyEtale.of_restrictScalarsstatement and proof · cited by 4
- RingHom.FormallyEtaleproof · cited by 3
- Algebra.basicOpen_subset_etaleLocus_iffstatement and proof · cited by 3
- Algebra.FormallyEtale.equivPiOfIsSepClosedstatement and proof · cited by 3
- Algebra.FormallyEtale.of_equivstatement and proof · cited by 3
- Algebra.FormallyEtale.of_formallyUnramified_and_formallySmoothstatement · cited by 3
- Algebra.FormallyEtale.of_isLocalizationstatement · cited by 3
- Algebra.FormallyEtale.of_isSeparablestatement and proof · cited by 3