Étale neighbourhoods of a pair

An étale neighbourhood of a ring and ideal (R, I) is an étale R-algebra whose quotient by I is canonically isomorphic to R ⧸ I. These algebras form the stages in the construction of the henselization of the pair. This file defines their full subcategory and proves closure under localization at an element invertible modulo the ideal, under tensor products, and under base change along maps of pairs. It also shows that two R-algebra maps out of an étale neighbourhood agree once I generates an ideal of the target inside its Jacobson radical.

References

• Stacks Project, Tag 0A02, the construction of the henselization of a pair.

def TauCeti.Henselization.reducedMap {R : Type u} [CommRing R] (I : Ideal R) (B : Type v) [CommRing B] [Algebra R B] : R ⧸ I →+* B ⧸ Ideal.map (algebraMap R B) I

The canonical map on quotients induced by the structure map of an algebra.

@[simp]

theorem TauCeti.Henselization.reducedMap_mk {R : Type u} [CommRing R] (I : Ideal R) (B : Type v) [CommRing B] [Algebra R B] (r : R) : (reducedMap I B) ((Ideal.Quotient.mk I) r) = (Ideal.Quotient.mk (Ideal.map (algebraMap R B) I)) ((algebraMap R B) r)

def TauCeti.Henselization.IsNeighbourhood {R : Type u} [CommRing R] (I : Ideal R) : CategoryTheory.ObjectProperty (CommAlgCat R)

An étale neighbourhood induces an isomorphism on the closed subscheme defined by I.

@[reducible, inline]

abbrev TauCeti.Henselization.Neighbourhood {R : Type u} [CommRing R] (I : Ideal R) : Type (max u (v + 1))

The category of étale neighbourhoods of the pair (R, I).

theorem TauCeti.Henselization.isNeighbourhood_iff {R : Type u} [CommRing R] (I : Ideal R) (B : CommAlgCat R) : IsNeighbourhood I B ↔ Algebra.Etale R ↑B ∧ Function.Bijective ⇑(reducedMap I ↑B)

The two conditions defining an étale neighbourhood.

theorem TauCeti.Henselization.isNeighbourhood_of_algEquiv {R : Type u} [CommRing R] (I : Ideal R) {B : Type v} [CommRing B] [Algebra R B] (e : R ≃ₐ[R] B) : IsNeighbourhood I ↧B

An algebra isomorphic to the base ring is an étale neighbourhood of every ideal.

theorem TauCeti.Henselization.isNeighbourhood_self {R : Type u} [CommRing R] (I : Ideal R) : IsNeighbourhood I ↧R

The identity algebra is an étale neighbourhood.

theorem TauCeti.Henselization.mem_of_algebraMap_mem_map_of_reducedMap_injective {R : Type u} [CommRing R] (I : Ideal R) {B : Type v} [CommRing B] [Algebra R B] (hB : Function.Injective ⇑(reducedMap I B)) {r : R} (hr : (algebraMap R B) r ∈ Ideal.map (algebraMap R B) I) : r ∈ I

If the reduced map is injective, an element of R whose image lies in the extended ideal already lies in I.

theorem TauCeti.Henselization.exists_sub_algebraMap_mem_map_of_reducedMap_surjective {R : Type u} [CommRing R] (I : Ideal R) {B : Type v} [CommRing B] [Algebra R B] (hB : Function.Surjective ⇑(reducedMap I B)) (b : B) : ∃ (r : R), b - (algebraMap R B) r ∈ Ideal.map (algebraMap R B) I

If the reduced map is surjective, every element of the algebra is congruent to the image of an element of R modulo the extended ideal.

theorem TauCeti.Henselization.quotient_mk_eq_of_reducedMap_surjective {R : Type u} [CommRing R] (I : Ideal R) {B : Type v} {C : Type u_1} [CommRing B] [CommRing C] [Algebra R B] [Algebra R C] (hB : Function.Surjective ⇑(reducedMap I B)) (f g : B →ₐ[R] C) (b : B) : (Ideal.Quotient.mk (Ideal.map (algebraMap R C) I)) (f b) = (Ideal.Quotient.mk (Ideal.map (algebraMap R C) I)) (g b)

Two maps out of an algebra whose reduced map is surjective (for instance, a neighbourhood) agree after quotienting their target by the extended ideal.

theorem TauCeti.Henselization.IsNeighbourhood.algHom_ext {R : Type u} [CommRing R] {I : Ideal R} {B : CommAlgCat R} (hB : IsNeighbourhood I B) {S : Type u_1} [CommRing S] [Algebra R S] (hI : Ideal.map (algebraMap R S) I ≤ ⊥.jacobson) {f g : ↑B →ₐ[R] S} : f = g

Two R-algebra maps out of an étale neighbourhood of (R, I) agree as soon as I generates an ideal of the target inside its Jacobson radical.

theorem TauCeti.Henselization.reducedMap_bijective_of_isLocalization {R : Type u} [CommRing R] (I : Ideal R) (M : Submonoid R) (B : Type v) [CommRing B] [Algebra R B] [IsLocalization M B] (hM : Submonoid.map (Ideal.Quotient.mk I) M ≤ IsUnit.submonoid (R ⧸ I)) : Function.Bijective ⇑(reducedMap I B)

Localization at elements which are units modulo I preserves the quotient by I.

theorem TauCeti.Henselization.isNeighbourhood_localization {R : Type u} [CommRing R] (I : Ideal R) {x : R} (hx : IsUnit ((Ideal.Quotient.mk I) x)) (B : Type v) [CommRing B] [Algebra R B] [IsLocalization.Away x B] : IsNeighbourhood I ↧B

Inverting an element that is a unit modulo the ideal gives an étale neighbourhood.

theorem TauCeti.Henselization.reducedMap_bijective_of_tower {R : Type u} [CommRing R] (I : Ideal R) (B C : Type v) [CommRing B] [CommRing C] [Algebra R B] [Algebra R C] [Algebra B C] [IsScalarTower R B C] (hB : Function.Bijective ⇑(reducedMap I B)) (hC : Function.Bijective ⇑(reducedMap (Ideal.map (algebraMap R B) I) C)) : Function.Bijective ⇑(reducedMap I C)

Bijectivity on quotients composes in a tower of algebras.

theorem TauCeti.Henselization.isNeighbourhood_localization_of_isNeighbourhood {R : Type u} [CommRing R] (I : Ideal R) (B : CommAlgCat R) (hB : IsNeighbourhood I B) {x : ↑B} (hx : IsUnit ((Ideal.Quotient.mk (Ideal.map (algebraMap R ↑B) I)) x)) : IsNeighbourhood I ↧(Localization.Away x)

An étale neighbourhood can be further localized at any element invertible on its quotient.

theorem TauCeti.Henselization.reducedMap_bijective_of_le {R : Type u} [CommRing R] (I : Ideal R) {J : Ideal R} (hIJ : I ≤ J) (B : Type v) [CommRing B] [Algebra R B] (hB : Function.Bijective ⇑(reducedMap I B)) : Function.Bijective ⇑(reducedMap J B)

Enlarging the ideal preserves bijectivity of the reduced map.

theorem TauCeti.Henselization.reducedMap_bijective_baseChange {R : Type u} [CommRing R] (I : Ideal R) (S : Type u_1) [CommRing S] [Algebra R S] (B : Type v) [CommRing B] [Algebra R B] (hB : Function.Bijective ⇑(reducedMap I B)) : Function.Bijective ⇑(reducedMap (Ideal.map (algebraMap R S) I) (TensorProduct R S B))

Base change along any algebra preserves bijectivity of the reduced map, for the extended ideal.

theorem TauCeti.Henselization.reducedMap_bijective_tensor {R : Type u} [CommRing R] (I : Ideal R) (B C : Type v) [CommRing B] [CommRing C] [Algebra R B] [Algebra R C] (hB : Function.Bijective ⇑(reducedMap I B)) (hC : Function.Bijective ⇑(reducedMap I C)) : Function.Bijective ⇑(reducedMap I (TensorProduct R B C))

The tensor product of two algebras inducing isomorphisms modulo I has the same property.

theorem TauCeti.Henselization.isNeighbourhood_tensor {R : Type u} [CommRing R] (I : Ideal R) (B C : CommAlgCat R) (hB : IsNeighbourhood I B) (hC : IsNeighbourhood I C) : IsNeighbourhood I ↧(TensorProduct R ↑B ↑C)

Tensor products provide common refinements of étale neighbourhoods.

theorem TauCeti.Henselization.isNeighbourhood_baseChange {R : Type u} [CommRing R] (I : Ideal R) {S : Type v} [CommRing S] [Algebra R S] {J : Ideal S} (hIJ : Ideal.map (algebraMap R S) I ≤ J) (B : CommAlgCat R) (hB : IsNeighbourhood I B) : IsNeighbourhood J ↧(TensorProduct R S ↑B)

Base change along a map of pairs (R, I) → (S, J), that is an R-algebra S with an ideal J containing the image of I, carries étale neighbourhoods of (R, I) to étale neighbourhoods of (S, J).

theorem TauCeti.Henselization.exists_common_target {R : Type u} [CommRing R] (I : Ideal R) (B C : Neighbourhood I) : ∃ (D : Neighbourhood I), Nonempty (B ⟶ D) ∧ Nonempty (C ⟶ D)

Any two étale neighbourhoods admit maps to a common étale neighbourhood.