Documentation

TauCeti.RingTheory.Henselization.Algebra

The underlying algebra of a henselization #

The henselization of a ring along an ideal is constructed as the filtered colimit of its étale neighbourhoods. This file defines the resulting algebra and provides the canonical map from every étale neighbourhood, together with the small-model diagram diagram and the isomorphism algebraIsoColimitDiagram identifying the algebra with its colimit.

References #

source
@[reducible, inline]
noncomputable abbrev TauCeti.Henselization.diagram {R : Type u} [CommRing R] (I : Ideal R) :
CategoryTheory.Functor (CategoryTheory.SmallModel.{u, u, u + 1} (Neighbourhood I)) (CommAlgCat R)

The restriction of the étale neighbourhoods of (R, I) to a small model of the neighbourhood category. Its colimit is identified with algebra I by algebraIsoColimitDiagram.

Instances For
    source
    noncomputable def TauCeti.Henselization.algebra {R : Type u} [CommRing R] (I : Ideal R) :
    CommAlgCat R

    The henselization algebra of (R, I), constructed as the filtered colimit of its étale neighbourhoods.

    Instances For
      source
      @[reducible, inline]
      noncomputable abbrev TauCeti.Henselization.extended {R : Type u} [CommRing R] (I : Ideal R) :
      Ideal ↑(algebra I)

      The ideal of the henselization algebra extended from I.

      Instances For
        source
        noncomputable def TauCeti.Henselization.stage {R : Type u} [CommRing R] (I : Ideal R) (B : Neighbourhood I) :
        ↑B.obj →ₐ[R] ↑(algebra I)

        The canonical map from an étale neighbourhood to the henselization algebra.

        Instances For
          source
          noncomputable def TauCeti.Henselization.algebraIsoColimitDiagram {R : Type u} [CommRing R] (I : Ideal R) :
          algebra I ≅ CategoryTheory.Limits.colimit (diagram I)

          The colimit over all étale neighbourhoods is the colimit over the small model.

          Instances For
            source
            @[simp]
            theorem TauCeti.Henselization.algebraIsoColimitDiagram_inv_comp_ι {R : Type u} [CommRing R] (I : Ideal R) (smallObject : CategoryTheory.SmallModel.{u, u, u + 1} (Neighbourhood I)) :
            (CommAlgCat.Hom.hom (algebraIsoColimitDiagram I).inv).comp (CommAlgCat.Hom.hom (CategoryTheory.Limits.colimit.ι (diagram I) smallObject)) = stage I ((CategoryTheory.equivSmallModel (Neighbourhood I)).inverse.obj smallObject)

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

            source
            @[simp]
            theorem TauCeti.Henselization.stage_naturality {R : Type u} [CommRing R] (I : Ideal R) {B C : Neighbourhood I} (f : B ⟶ C) :
            (stage I C).comp (CommAlgCat.Hom.hom f.hom) = stage I B

            The stage maps form a cocone over the category of étale neighbourhoods.

            source
            @[simp]
            theorem TauCeti.Henselization.stage_hom_apply {R : Type u} [CommRing R] (I : Ideal R) {B C : Neighbourhood I} (f : B ⟶ C) (b : ↑B.obj) :
            (stage I C) ((CommAlgCat.Hom.hom f.hom) b) = (stage I B) b

            Naturality of the stage maps, evaluated at an element.

            source
            noncomputable def TauCeti.Henselization.desc {R : Type u} [CommRing R] (I : Ideal R) (s : CategoryTheory.Limits.Cocone (IsNeighbourhood I).ι) :
            ↑(algebra I) →ₐ[R] ↑s.pt

            The map from the henselization algebra induced by a cocone on all étale neighbourhoods.

            Instances For
              source
              @[simp]
              theorem TauCeti.Henselization.desc_comp_stage {R : Type u} [CommRing R] (I : Ideal R) (s : CategoryTheory.Limits.Cocone (IsNeighbourhood I).ι) (B : Neighbourhood I) :
              (desc I s).comp (stage I B) = CommAlgCat.Hom.hom (s.ι.app B)

              The map induced by a cocone agrees with that cocone on every stage.

              source
              @[simp]
              theorem TauCeti.Henselization.desc_stage_apply {R : Type u} [CommRing R] (I : Ideal R) (s : CategoryTheory.Limits.Cocone (IsNeighbourhood I).ι) (B : Neighbourhood I) (b : ↑B.obj) :
              (desc I s) ((stage I B) b) = (CommAlgCat.Hom.hom (s.ι.app B)) b

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

              source
              noncomputable def TauCeti.Henselization.descOfCompatible {R : Type u} [CommRing R] (I : Ideal R) {S : Type u_1} [CommRing S] [Algebra R S] (stageMap : (B : Neighbourhood I) → ↑B.obj →ₐ[R] S) (hcompat : ∀ {B C : Neighbourhood I} (f : B ⟶ C), (stageMap C).comp (CommAlgCat.Hom.hom f.hom) = stageMap B) :
              ↑(algebra I) →ₐ[R] S

              A compatible family of R-algebra maps from the étale neighbourhoods of (R, I) to an R-algebra S in any universe descends to the henselization algebra.

              Instances For
                source
                @[simp]
                theorem TauCeti.Henselization.descOfCompatible_comp_stage {R : Type u} [CommRing R] (I : Ideal R) {S : Type u_1} [CommRing S] [Algebra R S] (stageMap : (B : Neighbourhood I) → ↑B.obj →ₐ[R] S) (hcompat : ∀ {B C : Neighbourhood I} (f : B ⟶ C), (stageMap C).comp (CommAlgCat.Hom.hom f.hom) = stageMap B) (B : Neighbourhood I) :
                (descOfCompatible I stageMap ⋯).comp (stage I B) = stageMap B

                The descent of a compatible family restricts to the family on every étale neighbourhood.

                source
                @[simp]
                theorem TauCeti.Henselization.descOfCompatible_stage_apply {R : Type u} [CommRing R] (I : Ideal R) {S : Type u_1} [CommRing S] [Algebra R S] (stageMap : (B : Neighbourhood I) → ↑B.obj →ₐ[R] S) (hcompat : ∀ {B C : Neighbourhood I} (f : B ⟶ C), (stageMap C).comp (CommAlgCat.Hom.hom f.hom) = stageMap B) (B : Neighbourhood I) (b : ↑B.obj) :
                (descOfCompatible I stageMap ⋯) ((stage I B) b) = (stageMap B) b

                Elementwise form of descOfCompatible_comp_stage.

                source
                theorem TauCeti.Henselization.exists_stage_eq {R : Type u} [CommRing R] (I : Ideal R) (x : ↑(algebra I)) :
                ∃ (B : Neighbourhood I) (b : ↑B.obj), (stage I B) b = x

                Every element of the henselization algebra comes from an étale neighbourhood.

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

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

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

                Two maps from the henselization algebra are equal if they agree on every stage.

                source
                theorem TauCeti.Henselization.hom_ext_iff {R : Type u} [CommRing R] {I : Ideal R} {S : Type w} [Semiring S] [Algebra R S] {f g : ↑(algebra I) →ₐ[R] S} :
                f = g ↔ ∀ (B : Neighbourhood I), f.comp (stage I B) = g.comp (stage I B)
                source
                @[simp]
                theorem TauCeti.Henselization.map_stage_map_algebraMap {R : Type u} [CommRing R] (I : Ideal R) (B : Neighbourhood I) :
                Ideal.map (↑(stage I B)) (Ideal.map (algebraMap R ↑B.obj) I) = extended I

                Extending the ideal from a neighbourhood to the henselization agrees with extending it directly from the base ring.

                source
                theorem TauCeti.Henselization.map_extended {R : Type u} [CommRing R] (I : Ideal R) {S : Type u_1} [Semiring S] [Algebra R S] (f : ↑(algebra I) →ₐ[R] S) :
                Ideal.map f (extended I) = Ideal.map (algebraMap R S) I

                Every R-algebra map out of the henselization carries the extended ideal onto the ideal generated by I in the target.