Structures · Algebra
Algebra.FormallySmooth
An R-algebra A is formally smooth if Ω[A⁄R] is A-projective and H¹(L_{A/R}) = 0.
For the infinitesimal lifting definition,
see FormallySmooth.lift and FormallySmooth.iff_comp_surjective.
- Defined in
- Mathlib.RingTheory.Smooth.Basic
- Shape
- 2 explicit arguments · adds projective_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 by44
- Algebra.FormallySmooth.comp
- Algebra.FormallySmooth.of_equiv
- Algebra.FormallySmooth.comp_surjective
- Algebra.FormallySmooth.iff_split_surjection
- Algebra.FormallySmooth.lift
- Algebra.Extension.H1Cotangent.equivOfFormallySmooth
- Algebra.FormallySmooth.iff_split_injection
- Algebra.FormallyEtale.of_formallyUnramified_and_formallySmooth
- Algebra.FormallySmooth.localization_base
- Algebra.FormallySmooth.of_restrictScalars
- Algebra.FormallySmooth.exists_adicCompletionEvalOneₐ_comp_eq
- Algebra.FormallySmooth.liftOfSurjective
- Algebra.FormallySmooth.of_split
- Algebra.FormallySmooth.mk_lift
- Algebra.FormallySmooth.comp_lift
- Algebra.IsSmoothAt.of_formallySmooth_fiber
- Algebra.FormallySmooth.liftOfSurjective_apply
- Algebra.FormallySmooth.exists_lift
- Algebra.Extension.homInfinitesimal
- Algebra.FormallySmooth.iff_injective_lTensor_residueField
- Algebra.Extension.cotangentComplex_injective_iff
- Algebra.FormallySmooth.flat_of_algHom_of_isNoetherianRing
- Algebra.FormallySmooth.kerCotangentToTensor_injective_iff
- Algebra.Extension.equivH1CotangentOfFormallySmooth
- Algebra.Extension.H1Cotangent.equivOfFormallySmooth_symm
- Algebra.FormallySmooth.of_pi
- Algebra.Extension.H1Cotangent.equivOfFormallySmooth_toLinearMap
- Algebra.FormallySmooth.iff_injective_cotangentComplexBaseChange_residueField
- Algebra.FormallySmooth.of_formallySmooth_residueField_tensor
- Algebra.Extension.H1Cotangent.equivOfFormallySmooth_apply
- Algebra.Extension.formallySmooth_iff_split_injection
- Algebra.FormallySmooth.exists_kerProj_comp_eq_id
- Algebra.FormallySmooth.projective_kaehlerDifferential
- Algebra.FormallySmooth.exists_mkₐ_comp_eq_of_isAdicComplete
- Algebra.Extension.H1Cotangent.equivOfFormallySmooth.congr_simp
- Algebra.FormallySmooth.subsingleton_h1Cotangent
- Algebra.FormallySmooth.instLocalization
- Algebra.FormallySmooth.iff_injective_cotangentComplexBaseChange
- Algebra.FormallySmooth.comp_liftOfSurjective
- Algebra.FormallySmooth.localization_map
- Algebra.FormallySmooth.instTensorProduct
- Algebra.FormallySmooth.lift.congr_simp
- Algebra.FormallySmooth.instForallOfFinite
- Algebra.FormallySmooth.instFinitePresentationKaehlerDifferentialOfEssFiniteType
Ancestors0
No ancestors.