ModuleFormallyEtaleNilpotent.lean
Nyll.SchemeTheory.FiniteEtale.Algebra.FormallyEtaleNilpotent
3 declarations indexed from sourceView source ↗ Module documentation
Formally étale lifting across nilpotent thickenings
Formal smoothness gives existence of lifts across nilpotent ideals, while formal unramifiedness gives uniqueness. This file combines the two halves for formally étale algebras and records the resulting rigidity of two nilpotent thickenings of the same algebra.
Imports1
- Mathlib.RingTheory.Etale.Basic
Imported by2
Declarations
Algebra.FormallyEtale.comp_bijective_of_isNilpotent
DocumentationFor a formally étale algebra, reduction modulo any nilpotent ideal is bijective on algebra homomorphisms.
Source context 5 commands
Surrounding namespaces, section variables, and local commands at this declaration.
noncomputable section
universe u v w x
namespace Algebra.FormallyEtale
variable {R : Type u} {A : Type v} {B : Type w}
variable [CommRing R] [CommRing A] [CommRing B] [Algebra R A] [Algebra R B]
Algebra.FormallyEtale.existsUnique_lift
DocumentationA map from a formally étale algebra to a nilpotent quotient has a unique lift.
Source context 5 commands
Surrounding namespaces, section variables, and local commands at this declaration.
noncomputable section
universe u v w x
namespace Algebra.FormallyEtale
variable {R : Type u} {A : Type v} {B : Type w}
variable [CommRing R] [CommRing A] [CommRing B] [Algebra R A] [Algebra R B]
Algebra.FormallyEtale.existsUnique_algEquiv_of_surjective
DocumentationTwo formally étale nilpotent thickenings of the same algebra are uniquely isomorphic over the common quotient.
Source context 6 commands
Surrounding namespaces, section variables, and local commands at this declaration.
noncomputable section
universe u v w x
namespace Algebra.FormallyEtale
variable {R : Type u} {A : Type v} {B : Type w}
variable [CommRing R] [CommRing A] [CommRing B] [Algebra R A] [Algebra R B]
variable {C : Type x} [CommRing C] [Algebra R C]