The integral trace on extended ideals

Mathlib's Algebra.intTrace A B is the trace of a finite extension of integrally closed domains B / A, restricted from the fraction fields to the rings themselves. This file records that it is compatible with the ideals of the base: the trace carries the extended ideal p · B of an ideal p of A back into p. This is the case of the trace of the general fact LinearMap.apply_mem_of_mem_smul_top, that an A-linear functional carries p • B into p, since p • B is the extended ideal p · B.

This is the elementary half of the computation of the trace of an ideal of B. The other half, which reads the exact image off the different ideal, is in TauCeti.RingTheory.DedekindDomain.Different.Trace.

Main results

• Algebra.intTrace_mem_of_mem_map: Tr(p · B) ⊆ p.

theorem Algebra.intTrace_mem_of_mem_map {A : Type u_1} {B : Type u_2} [CommRing A] [CommRing B] [Algebra A B] [IsDomain A] [IsIntegrallyClosed A] [IsDomain B] [IsIntegrallyClosed B] [Module.Finite A B] [Module.IsTorsionFree A B] {p : Ideal A} {x : B} (hx : x ∈ Ideal.map (algebraMap A B) p) : (intTrace A B) x ∈ p

The integral trace carries the extended ideal p · B of an ideal p of the base ring back into p: it is an A-linear functional on B, and p · B = p • B.