Pointed étale neighbourhoods

Étale algebras with a map to a fixed commutative algebra form the indexing category for strict henselization. For R : Type u and Ω : Type v, source algebras live in Type (max u v). The target is lifted to this universe, so the base algebra and tensor-product refinements belong to the same category even when the base and target have different universes. The structure map of a neighbourhood therefore lands in ULift Ω, and Neighbourhood.point is the corresponding R-algebra map to Ω.

Localizing a neighbourhood at an element whose point is a unit gives a refinement in which that element is a unit. A monic polynomial with a simple root at the point has a root with that same image in a further neighbourhood.

This file records the underlying R-algebra map to Ω (Neighbourhood.point), constructors Neighbourhood.mk' and Neighbourhood.homMk' from algebra maps compatible with the points, an extensionality lemma for morphisms, and the refinement Neighbourhood.away of a neighbourhood by inverting an element that is a unit at the point.

References

• Stacks Project, Tags 04GP and 04GW.
• Mathlib's StandardEtalePair, for adjoining a root and inverting its derivative.
• Taylor Dupuy, Thomas Tucker, and Zhuoran Wang, pcfawd-formalization at 9a20b3f, StrictHenselizationConstruction.lean, PointedEtaleNeighborhood.

def TauCeti.StrictHenselization.IsPointedNeighbourhood (R : Type u) (Ω : Type v) [CommRing R] [CommRing Ω] [Algebra R Ω] : CategoryTheory.ObjectProperty (CategoryTheory.Over ↧(ULift.{u, v} Ω))

An étale algebra equipped with a point valued in the universe lift of Ω.

@[reducible, inline]

abbrev TauCeti.StrictHenselization.Neighbourhood (R : Type u) (Ω : Type v) [CommRing R] [CommRing Ω] [Algebra R Ω] : Type (max (u + 1) (v + 1))

The category of pointed étale neighbourhoods.

@[simp]

theorem TauCeti.StrictHenselization.isPointedNeighbourhood_iff (R : Type u) (Ω : Type v) [CommRing R] [CommRing Ω] [Algebra R Ω] (point : CategoryTheory.Over ↧(ULift.{u, v} Ω)) : IsPointedNeighbourhood R Ω point ↔ Algebra.Etale R ↑point.left

The defining property of a pointed neighbourhood.

instance TauCeti.StrictHenselization.Neighbourhood.etale (R : Type u) (Ω : Type v) [CommRing R] [CommRing Ω] [Algebra R Ω] (B : Neighbourhood R Ω) : Algebra.Etale R ↑B.obj.left

The source algebra of a pointed neighbourhood is étale over the base.

theorem TauCeti.StrictHenselization.Neighbourhood.ext (R : Type u) (Ω : Type v) [CommRing R] [CommRing Ω] [Algebra R Ω] (first second : Neighbourhood R Ω) (hleft : first.obj.left = second.obj.left) (hpoint : CommAlgCat.Hom.hom first.obj.hom ≍ CommAlgCat.Hom.hom second.obj.hom) : first = second

Pointed neighbourhoods agree when their source algebras and point maps agree.

theorem TauCeti.StrictHenselization.Neighbourhood.ext_iff {R : Type u} {Ω : Type v} [CommRing R] [CommRing Ω] [Algebra R Ω] {first second : Neighbourhood R Ω} : first = second ↔ first.obj.left = second.obj.left ∧ CommAlgCat.Hom.hom first.obj.hom ≍ CommAlgCat.Hom.hom second.obj.hom

def TauCeti.StrictHenselization.Neighbourhood.point {R : Type u} {Ω : Type v} [CommRing R] [CommRing Ω] [Algebra R Ω] (B : Neighbourhood R Ω) : ↑B.obj.left →ₐ[R] Ω

The R-algebra map to Ω underlying the point of a pointed neighbourhood.

theorem TauCeti.StrictHenselization.Neighbourhood.point_apply {R : Type u} {Ω : Type v} [CommRing R] [CommRing Ω] [Algebra R Ω] (B : Neighbourhood R Ω) (x : ↑B.obj.left) : B.point x = ((CommAlgCat.Hom.hom B.obj.hom) x).down

The point of a neighbourhood is the structure map followed by ULift.down.

theorem TauCeti.StrictHenselization.Neighbourhood.hom_ext {R : Type u} {Ω : Type v} [CommRing R] [CommRing Ω] [Algebra R Ω] {B C : Neighbourhood R Ω} {f g : B ⟶ C} (h : CommAlgCat.Hom.hom (CategoryTheory.Over.Hom.left f.hom) = CommAlgCat.Hom.hom (CategoryTheory.Over.Hom.left g.hom)) : f = g

Morphisms of pointed neighbourhoods are determined by their underlying algebra maps.

theorem TauCeti.StrictHenselization.Neighbourhood.hom_ext_iff {R : Type u} {Ω : Type v} [CommRing R] [CommRing Ω] [Algebra R Ω] {B C : Neighbourhood R Ω} {f g : B ⟶ C} : f = g ↔ CommAlgCat.Hom.hom (CategoryTheory.Over.Hom.left f.hom) = CommAlgCat.Hom.hom (CategoryTheory.Over.Hom.left g.hom)

@[simp]

theorem TauCeti.StrictHenselization.Neighbourhood.point_comp_hom {R : Type u} {Ω : Type v} [CommRing R] [CommRing Ω] [Algebra R Ω] {B C : Neighbourhood R Ω} (f : B ⟶ C) : C.point.comp (CommAlgCat.Hom.hom (CategoryTheory.Over.Hom.left f.hom)) = B.point

Morphisms of pointed neighbourhoods are compatible with the points.

@[simp]

theorem TauCeti.StrictHenselization.Neighbourhood.point_hom_apply {R : Type u} {Ω : Type v} [CommRing R] [CommRing Ω] [Algebra R Ω] {B C : Neighbourhood R Ω} (f : B ⟶ C) (x : ↑B.obj.left) : C.point ((CommAlgCat.Hom.hom (CategoryTheory.Over.Hom.left f.hom)) x) = B.point x

The elementwise form of point_comp_hom.

def TauCeti.StrictHenselization.Neighbourhood.mk' {R : Type u} {Ω : Type v} [CommRing R] [CommRing Ω] [Algebra R Ω] (A : Type (max u v)) [CommRing A] [Algebra R A] [Algebra.Etale R A] (pt : A →ₐ[R] Ω) : Neighbourhood R Ω

The pointed neighbourhood given by an étale R-algebra A and an R-algebra map A → Ω.

@[simp]

theorem TauCeti.StrictHenselization.Neighbourhood.point_mk' {R : Type u} {Ω : Type v} [CommRing R] [CommRing Ω] [Algebra R Ω] (A : Type (max u v)) [CommRing A] [Algebra R A] [Algebra.Etale R A] (pt : A →ₐ[R] Ω) : (mk' A pt).point = pt

The point of mk' A pt is pt.

def TauCeti.StrictHenselization.Neighbourhood.homMk' {R : Type u} {Ω : Type v} [CommRing R] [CommRing Ω] [Algebra R Ω] {B C : Neighbourhood R Ω} (f : ↑B.obj.left →ₐ[R] ↑C.obj.left) (h : C.point.comp f = B.point) : B ⟶ C

A morphism of pointed neighbourhoods given by an algebra map compatible with the points.

@[simp]

theorem TauCeti.StrictHenselization.Neighbourhood.homMk'_hom_left_hom {R : Type u} {Ω : Type v} [CommRing R] [CommRing Ω] [Algebra R Ω] {B C : Neighbourhood R Ω} (f : ↑B.obj.left →ₐ[R] ↑C.obj.left) (h : C.point.comp f = B.point) : CommAlgCat.Hom.hom (CategoryTheory.Over.Hom.left (homMk' f h).hom) = f

The underlying algebra map of homMk' f h is f.

noncomputable def TauCeti.StrictHenselization.Neighbourhood.away {R : Type u} {Ω : Type v} [CommRing R] [CommRing Ω] [Algebra R Ω] (B : Neighbourhood R Ω) (y : ↑B.obj.left) (hy : IsUnit (B.point y)) : Neighbourhood R Ω

Inverting an element y of a pointed neighbourhood that is a unit at the point gives a pointed neighbourhood, with the point extended to the localization.

@[simp]

theorem TauCeti.StrictHenselization.Neighbourhood.point_away {R : Type u} {Ω : Type v} [CommRing R] [CommRing Ω] [Algebra R Ω] (B : Neighbourhood R Ω) (y : ↑B.obj.left) (hy : IsUnit (B.point y)) : (B.away y hy).point = IsLocalization.Away.liftAlgHom y hy

The point of away B y hy extends the point of B.

noncomputable def TauCeti.StrictHenselization.Neighbourhood.awayHom {R : Type u} {Ω : Type v} [CommRing R] [CommRing Ω] [Algebra R Ω] (B : Neighbourhood R Ω) (y : ↑B.obj.left) (hy : IsUnit (B.point y)) : B ⟶ B.away y hy

The refinement from a pointed neighbourhood to its inversion at y.

@[simp]

theorem TauCeti.StrictHenselization.Neighbourhood.awayHom_hom_left_hom {R : Type u} {Ω : Type v} [CommRing R] [CommRing Ω] [Algebra R Ω] (B : Neighbourhood R Ω) (y : ↑B.obj.left) (hy : IsUnit (B.point y)) : CommAlgCat.Hom.hom (CategoryTheory.Over.Hom.left (B.awayHom y hy).hom) = IsScalarTower.toAlgHom R (↑B.obj.left) (Localization.Away y)

The refinement awayHom is the localization map.

theorem TauCeti.StrictHenselization.Neighbourhood.isUnit_awayHom {R : Type u} {Ω : Type v} [CommRing R] [CommRing Ω] [Algebra R Ω] (B : Neighbourhood R Ω) (y : ↑B.obj.left) (hy : IsUnit (B.point y)) : IsUnit ((CommAlgCat.Hom.hom (CategoryTheory.Over.Hom.left (B.awayHom y hy).hom)) y)

The refinement awayHom sends y to a unit.

noncomputable def TauCeti.StrictHenselization.Neighbourhood.awayLift {R : Type u} {Ω : Type v} [CommRing R] [CommRing Ω] [Algebra R Ω] {B C : Neighbourhood R Ω} (y : ↑B.obj.left) (hy : IsUnit (B.point y)) (f : B ⟶ C) (hf : IsUnit ((CommAlgCat.Hom.hom (CategoryTheory.Over.Hom.left f.hom)) y)) : B.away y hy ⟶ C

The universal property of away: a morphism f : B ⟶ C that sends y to a unit factors through awayHom B y hy.

@[simp]

theorem TauCeti.StrictHenselization.Neighbourhood.awayLift_hom_left_hom {R : Type u} {Ω : Type v} [CommRing R] [CommRing Ω] [Algebra R Ω] {B C : Neighbourhood R Ω} (y : ↑B.obj.left) (hy : IsUnit (B.point y)) (f : B ⟶ C) (hf : IsUnit ((CommAlgCat.Hom.hom (CategoryTheory.Over.Hom.left f.hom)) y)) : CommAlgCat.Hom.hom (CategoryTheory.Over.Hom.left (awayLift y hy f hf).hom) = IsLocalization.Away.liftAlgHom y hf

The underlying algebra map of awayLift is the localization lift of the underlying map of f.

@[simp]

theorem TauCeti.StrictHenselization.Neighbourhood.awayHom_comp_awayLift {R : Type u} {Ω : Type v} [CommRing R] [CommRing Ω] [Algebra R Ω] {B C : Neighbourhood R Ω} (y : ↑B.obj.left) (hy : IsUnit (B.point y)) (f : B ⟶ C) (hf : IsUnit ((CommAlgCat.Hom.hom (CategoryTheory.Over.Hom.left f.hom)) y)) : CategoryTheory.CategoryStruct.comp (B.awayHom y hy) (awayLift y hy f hf) = f

The factorization awayLift composed with awayHom is the original morphism.

theorem TauCeti.StrictHenselization.Neighbourhood.away_hom_ext {R : Type u} {Ω : Type v} [CommRing R] [CommRing Ω] [Algebra R Ω] {B C : Neighbourhood R Ω} {y : ↑B.obj.left} {hy : IsUnit (B.point y)} {g h : B.away y hy ⟶ C} (H : CategoryTheory.CategoryStruct.comp (B.awayHom y hy) g = CategoryTheory.CategoryStruct.comp (B.awayHom y hy) h) : g = h

Morphisms out of away B y hy are determined by their composite with awayHom.

theorem TauCeti.StrictHenselization.Neighbourhood.exists_refinement_isUnit {R : Type u} {Ω : Type v} [CommRing R] [CommRing Ω] [Algebra R Ω] (B : Neighbourhood R Ω) (b : ↑B.obj.left) (hpoint : IsUnit (B.point b)) : ∃ (target : Neighbourhood R Ω) (refinement : B ⟶ target), IsUnit ((CommAlgCat.Hom.hom (CategoryTheory.Over.Hom.left refinement.hom)) b)

A stage element whose point is a unit becomes a unit in a further pointed étale neighbourhood, obtained by localizing at that element.

theorem TauCeti.StrictHenselization.Neighbourhood.exists_refinement_isRoot (R : Type u) (Ω : Type v) [CommRing R] [CommRing Ω] [Algebra R Ω] (B : Neighbourhood R Ω) (p : Polynomial ↑B.obj.left) (hp : p.Monic) (a : ULift.{u, v} Ω) (ha : Polynomial.eval₂ (CommAlgCat.Hom.hom B.obj.hom).toRingHom a p = 0) (hderiv : IsUnit (Polynomial.eval₂ (CommAlgCat.Hom.hom B.obj.hom).toRingHom a (Polynomial.derivative p))) : ∃ (C : Neighbourhood R Ω) (f : B ⟶ C) (c : ↑C.obj.left), (Polynomial.map (CommAlgCat.Hom.hom (CategoryTheory.Over.Hom.left f.hom)).toRingHom p).IsRoot c ∧ (CommAlgCat.Hom.hom C.obj.hom) c = a

A simple root at the point of a pointed étale neighbourhood lifts to a root in a further pointed étale neighbourhood, with exactly the prescribed image under its point.