The colimit algebra of pointed étale neighbourhoods

Pointed étale neighbourhoods form a filtered, essentially small category. Their algebra-valued diagram has a colimit with canonical maps from each stage, identified by algebraIsoColimitDiagram with the colimit of its small-model restriction diagram. The pointings also induce a map from the colimit to the chosen target algebra.

References

• Stacks Project, Tags 04GP, 04GQ, and 04GW.
• Taylor Dupuy, Thomas Tucker, and Zhuoran Wang, pcfawd-formalization at 9a20b3f (Apache 2.0): functor, colimitObj, toColimit, colimitPoint, and colimitPoint_comp_toColimit in StrictHenselizationConstruction.lean; and exists_stage_of_colimit_element and toColimit_naturality in StrictHenselizationStages.lean.

@[reducible, inline]

noncomputable abbrev TauCeti.StrictHenselization.algebraFunctor (R : Type u) (Ω : Type v) [CommRing R] [CommRing Ω] [Algebra R Ω] : CategoryTheory.Functor (Neighbourhood R Ω) (CommAlgCat R)

Forget the point but retain the étale algebra.

noncomputable def TauCeti.StrictHenselization.pointCocone (R : Type u) (Ω : Type v) [CommRing R] [CommRing Ω] [Algebra R Ω] : CategoryTheory.Limits.Cocone (algebraFunctor R Ω)

The cocone on pointed étale algebras with apex ULift Ω whose leg at each neighbourhood is its point.

@[simp]

theorem TauCeti.StrictHenselization.pointCocone_pt (R : Type u) (Ω : Type v) [CommRing R] [CommRing Ω] [Algebra R Ω] : (pointCocone R Ω).pt = ↧(ULift.{u, v} Ω)

The apex of pointCocone is Ω lifted to the universe of the base and target.

@[simp]

theorem TauCeti.StrictHenselization.pointCocone_ι_app (R : Type u) (Ω : Type v) [CommRing R] [CommRing Ω] [Algebra R Ω] (B : Neighbourhood R Ω) : (pointCocone R Ω).ι.app B = B.obj.hom

The leg of pointCocone at a neighbourhood is its point.

@[reducible, inline]

noncomputable abbrev TauCeti.StrictHenselization.diagram (R Ω : Type u) [CommRing R] [CommRing Ω] [Algebra R Ω] : CategoryTheory.Functor (CategoryTheory.SmallModel.{u, u, u + 1} (Neighbourhood R Ω)) (CommAlgCat R)

The restriction of the pointed étale algebras to a small model of the neighbourhood category. Its colimit is identified with algebra R Ω by algebraIsoColimitDiagram.

noncomputable def TauCeti.StrictHenselization.algebra (R Ω : Type u) [CommRing R] [CommRing Ω] [Algebra R Ω] : CommAlgCat R

The colimit of pointed étale algebras. For a local base ring and a separable closure of its residue field as target, this is the strict henselization.

noncomputable def TauCeti.StrictHenselization.stage (R Ω : Type u) [CommRing R] [CommRing Ω] [Algebra R Ω] (B : Neighbourhood R Ω) : ↑B.obj.left →ₐ[R] ↑(algebra R Ω)

The canonical map from a pointed étale algebra to the colimit.

noncomputable def TauCeti.StrictHenselization.algebraIsoColimitDiagram (R Ω : Type u) [CommRing R] [CommRing Ω] [Algebra R Ω] : algebra R Ω ≅ CategoryTheory.Limits.colimit (diagram R Ω)

The colimit over all pointed neighbourhoods is the colimit over the small model.

@[simp]

theorem TauCeti.StrictHenselization.algebraIsoColimitDiagram_inv_comp_ι (R Ω : Type u) [CommRing R] [CommRing Ω] [Algebra R Ω] (smallObject : CategoryTheory.SmallModel.{u, u, u + 1} (Neighbourhood R Ω)) : (CommAlgCat.Hom.hom (algebraIsoColimitDiagram R Ω).inv).comp (CommAlgCat.Hom.hom (CategoryTheory.Limits.colimit.ι (diagram R Ω) smallObject)) = stage R Ω ((CategoryTheory.equivSmallModel (Neighbourhood R Ω)).inverse.obj smallObject)

The comparison with the small-model colimit is compatible with the stage maps.

@[simp]

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

The stage maps commute with morphisms of pointed étale algebras.

@[simp]

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

Naturality of the stage maps on elements.

noncomputable def TauCeti.StrictHenselization.desc (R Ω : Type u) [CommRing R] [CommRing Ω] [Algebra R Ω] (s : CategoryTheory.Limits.Cocone (algebraFunctor R Ω)) : ↑(algebra R Ω) →ₐ[R] ↑s.pt

A cocone on pointed étale algebras induces a map out of their colimit.

@[simp]

theorem TauCeti.StrictHenselization.desc_comp_stage (R Ω : Type u) [CommRing R] [CommRing Ω] [Algebra R Ω] (s : CategoryTheory.Limits.Cocone (algebraFunctor R Ω)) (B : Neighbourhood R Ω) : (desc R Ω s).comp (stage R Ω B) = CommAlgCat.Hom.hom (s.ι.app B)

The map induced by a cocone agrees with it at each stage.

@[simp]

theorem TauCeti.StrictHenselization.desc_stage_apply (R Ω : Type u) [CommRing R] [CommRing Ω] [Algebra R Ω] (s : CategoryTheory.Limits.Cocone (algebraFunctor R Ω)) (B : Neighbourhood R Ω) (b : ↑B.obj.left) : (desc R Ω s) ((stage R Ω B) b) = (CommAlgCat.Hom.hom (s.ι.app B)) b

The map induced by a cocone, evaluated at a stage element.

noncomputable def TauCeti.StrictHenselization.descOfCompatible (R Ω : Type u) [CommRing R] [CommRing Ω] [Algebra R Ω] {T : Type w} [CommRing T] [Algebra R T] (stageMap : (B : Neighbourhood R Ω) → ↑B.obj.left →ₐ[R] T) (hcompat : ∀ {B C : Neighbourhood R Ω} (f : B ⟶ C), (stageMap C).comp (CommAlgCat.Hom.hom (CategoryTheory.Over.Hom.left f.hom)) = stageMap B) : ↑(algebra R Ω) →ₐ[R] T

A compatible family of algebra maps from the pointed étale algebras into a target in any universe descends to the colimit.

@[simp]

theorem TauCeti.StrictHenselization.descOfCompatible_comp_stage (R Ω : Type u) [CommRing R] [CommRing Ω] [Algebra R Ω] {T : Type w} [CommRing T] [Algebra R T] (stageMap : (B : Neighbourhood R Ω) → ↑B.obj.left →ₐ[R] T) (hcompat : ∀ {B C : Neighbourhood R Ω} (f : B ⟶ C), (stageMap C).comp (CommAlgCat.Hom.hom (CategoryTheory.Over.Hom.left f.hom)) = stageMap B) (B : Neighbourhood R Ω) : (descOfCompatible R Ω stageMap ⋯).comp (stage R Ω B) = stageMap B

The descent of a compatible family restricts to the family at every stage.

@[simp]

theorem TauCeti.StrictHenselization.descOfCompatible_stage_apply (R Ω : Type u) [CommRing R] [CommRing Ω] [Algebra R Ω] {T : Type w} [CommRing T] [Algebra R T] (stageMap : (B : Neighbourhood R Ω) → ↑B.obj.left →ₐ[R] T) (hcompat : ∀ {B C : Neighbourhood R Ω} (f : B ⟶ C), (stageMap C).comp (CommAlgCat.Hom.hom (CategoryTheory.Over.Hom.left f.hom)) = stageMap B) (B : Neighbourhood R Ω) (b : ↑B.obj.left) : (descOfCompatible R Ω stageMap ⋯) ((stage R Ω B) b) = (stageMap B) b

The descent of a compatible family, evaluated at a stage element.

theorem TauCeti.StrictHenselization.exists_stage_eq (R Ω : Type u) [CommRing R] [CommRing Ω] [Algebra R Ω] (x : ↑(algebra R Ω)) : ∃ (B : Neighbourhood R Ω) (b : ↑B.obj.left), (stage R Ω B) b = x

Every element of the colimit comes from a pointed étale neighbourhood.

theorem TauCeti.StrictHenselization.exists_stage_family (R Ω : Type u) [CommRing R] [CommRing Ω] [Algebra R Ω] {ι : Type u_1} [Finite ι] (x : ι → ↑(algebra R Ω)) : ∃ (B : Neighbourhood R Ω) (b : ι → ↑B.obj.left), ∀ (i : ι), (stage R Ω B) (b i) = x i

Finitely many elements of the colimit come from a common pointed étale neighbourhood.

theorem TauCeti.StrictHenselization.hom_ext (R Ω : Type u) [CommRing R] [CommRing Ω] [Algebra R Ω] {S : Type w} [Semiring S] [Algebra R S] {f g : ↑(algebra R Ω) →ₐ[R] S} (h : ∀ (B : Neighbourhood R Ω), f.comp (stage R Ω B) = g.comp (stage R Ω B)) : f = g

Algebra maps out of the colimit agree if they agree on every stage.

theorem TauCeti.StrictHenselization.hom_ext_iff {R Ω : Type u} [CommRing R] [CommRing Ω] [Algebra R Ω] {S : Type w} [Semiring S] [Algebra R S] {f g : ↑(algebra R Ω) →ₐ[R] S} : f = g ↔ ∀ (B : Neighbourhood R Ω), f.comp (stage R Ω B) = g.comp (stage R Ω B)

noncomputable def TauCeti.StrictHenselization.toTarget (R Ω : Type u) [CommRing R] [CommRing Ω] [Algebra R Ω] : ↑(algebra R Ω) →ₐ[R] Ω

The pointings induce a map from the colimit to the chosen algebra.

theorem TauCeti.StrictHenselization.toTarget_apply (R Ω : Type u) [CommRing R] [CommRing Ω] [Algebra R Ω] (x : ↑(algebra R Ω)) : (toTarget R Ω) x = ULift.algEquiv.{u, u, u} ((desc R Ω (pointCocone R Ω)) x)

toTarget is the descent of pointCocone, followed by the identification of ULift Ω with Ω.

@[simp]

theorem TauCeti.StrictHenselization.toTarget_comp_stage (R Ω : Type u) [CommRing R] [CommRing Ω] [Algebra R Ω] (B : Neighbourhood R Ω) : (toTarget R Ω).comp (stage R Ω B) = B.point

Composing a stage map with toTarget recovers the point of that neighbourhood.

@[simp]

theorem TauCeti.StrictHenselization.toTarget_stage_apply (R Ω : Type u) [CommRing R] [CommRing Ω] [Algebra R Ω] (B : Neighbourhood R Ω) (b : ↑B.obj.left) : (toTarget R Ω) ((stage R Ω B) b) = B.point b

Elementwise form of toTarget_comp_stage.