Functoriality of integral closures

An R-algebra map f : A → B restricts to a map f.mapIntegralClosure between the integral closures of R in A and in B. This file records that this restriction is functorial and preserves injectivity, and that primes of the integral closure of R in A are contractions of primes of the integral closure of R in B when f is injective: the integral closure in B is integral over R, so lying over applies along the restricted map.

Main results

• AlgHom.mapIntegralClosure_comp: the restriction to integral closures is functorial.
• AlgHom.mapIntegralClosure_injective: it preserves injectivity.
• Ideal.exists_isPrime_comap_mapIntegralClosure_eq: a prime of the integral closure in A is the contraction of a prime of the integral closure in B along an injective f.

@[simp]

theorem AlgHom.mapIntegralClosure_comp {R : Type u_1} {A : Type u_2} {B : Type u_3} {C : Type u_4} [CommRing R] [CommRing A] [CommRing B] [CommRing C] [Algebra R A] [Algebra R B] [Algebra R C] (f : B →ₐ[R] C) (g : A →ₐ[R] B) : (f.comp g).mapIntegralClosure = f.mapIntegralClosure.comp g.mapIntegralClosure

Restricting a composite algebra homomorphism to integral closures gives the composite of the restricted algebra homomorphisms.

theorem AlgHom.mapIntegralClosure_injective {R : Type u_1} {A : Type u_2} {B : Type u_3} [CommRing R] [CommRing A] [CommRing B] [Algebra R A] [Algebra R B] {f : A →ₐ[R] B} (hf : Function.Injective ⇑f) : Function.Injective ⇑f.mapIntegralClosure

Restricting an injective algebra homomorphism to integral closures preserves injectivity.

theorem Ideal.exists_isPrime_comap_mapIntegralClosure_eq {R : Type u_1} {A : Type u_2} {B : Type u_3} [CommRing R] [CommRing A] [CommRing B] [Algebra R A] [Algebra R B] (P : Ideal ↥(integralClosure R A)) [P.IsPrime] {f : A →ₐ[R] B} (hf : Function.Injective ⇑f) : ∃ (Q : Ideal ↥(integralClosure R B)), Q.IsPrime ∧ comap f.mapIntegralClosure Q = P

Lying over for integral closures: along an injective R-algebra map f : A → B, every prime of the integral closure of R in A is the contraction of a prime of the integral closure of R in B.