Sections of unramified algebras

A section of an essentially finite type, formally unramified algebra selects an open-and-closed component. Its kernel is generated by the complement of an idempotent, and the section is localization at that idempotent. The same selector also gives a product decomposition into the section component and its complement.

A section ψ : S → R ⧸ J modulo an ideal J of R base changes to a section of (R ⧸ J) ⊗[R] S, and a lift g ∈ S of its idempotent selector satisfies ψ g = 1 and kills the kernel of ψ modulo J S (exists_mul_mem_map_of_eq_zero).

The diagonal idempotent is supplied by exists_isIdempotentElem_ker_lmul_eq_span.

References

• The Stacks Project, Tag 02FL (the diagonal of an unramified morphism).

theorem TauCeti.Algebra.FormallyUnramified.exists_isIdempotentElem_ker_eq_span (R : Type u_1) (S : Type u_2) [CommRing R] [CommRing S] [Algebra R S] [Algebra.EssFiniteType R S] [Algebra.FormallyUnramified R S] (σ : S →ₐ[R] R) : ∃ (e : S), IsIdempotentElem e ∧ σ e = 1 ∧ RingHom.ker σ = Ideal.span {1 - e}

A section of an essentially finite type unramified algebra selects an idempotent component. The kernel is generated by the complement of the selector, which maps to one.

theorem TauCeti.Algebra.FormallyUnramified.isLocalizationAway_of_ker_eq_span {R : Type u_1} {S : Type u_2} [CommRing R] [CommRing S] [Algebra R S] (σ : S →ₐ[R] R) {e : S} (he : IsIdempotentElem e) (hker : RingHom.ker σ = Ideal.span {1 - e}) : have x := σ.toAlgebra; IsLocalization.Away e R

A section is localization at any idempotent selector whose complement generates its kernel. The algebra structure on the target is the one induced by the section.

noncomputable def TauCeti.Algebra.FormallyUnramified.prodOfKerEqSpan {R : Type u_1} {S : Type u_2} [CommRing R] [CommRing S] [Algebra R S] (σ : S →ₐ[R] R) {e : S} (he : IsIdempotentElem e) (hker : RingHom.ker σ = Ideal.span {1 - e}) : S ≃ₐ[R] R × S ⧸ Ideal.span {e}

An idempotent selector whose complement generates the kernel of a section splits the algebra as a product. The first factor is the section component, and the second is its complement.

@[simp]

theorem TauCeti.Algebra.FormallyUnramified.prodOfKerEqSpan_apply {R : Type u_1} {S : Type u_2} [CommRing R] [CommRing S] [Algebra R S] (σ : S →ₐ[R] R) {e : S} (he : IsIdempotentElem e) (hker : RingHom.ker σ = Ideal.span {1 - e}) (s : S) : (prodOfKerEqSpan σ he hker) s = (σ s, (Ideal.Quotient.mk (Ideal.span {e})) s)

The product decomposition has the given section and quotient map as its projections.

theorem TauCeti.Algebra.FormallyUnramified.exists_mul_mem_map_of_eq_zero {R : Type u_1} {S : Type u_2} [CommRing R] [CommRing S] [Algebra R S] [Algebra.EssFiniteType R S] [Algebra.FormallyUnramified R S] (J : Ideal R) (ψ : S →ₐ[R] R ⧸ J) : ∃ (g : S), ψ g = 1 ∧ ∀ (s : S), ψ s = 0 → g * s ∈ Ideal.map (algebraMap R S) J

For an R-algebra map ψ : S → R ⧸ J out of an essentially finite type unramified R-algebra, there is g ∈ S with ψ g = 1 and g s ∈ J S for every s in the kernel of ψ. Base changed to R ⧸ J, the section ψ is localization at an idempotent, and g lifts that idempotent.