Theorems · Definition · commutative algebra

Algebra.intTrace

(A : Type u_1) →
  (B : Type u_6) →
    [inst : CommRing A] →
      [inst_1 : CommRing B] →
        [inst_2 : Algebra A B] →
          [IsDomain A] →
            [IsIntegrallyClosed A] →
              [IsDomain B] → [IsIntegrallyClosed B] → [Module.Finite A B] → [Module.IsTorsionFree A B] → B →ₗ[A] A

The trace of a finite extension of integrally closed domains B/A is the restriction of the trace on Frac(B)/Frac(A) onto B/A. See Algebra.algebraMap_intTrace.

Defined in

Mathlib.RingTheory.IntegralClosure.IntegralRestrict

Cited by

9 results in Mathlib

Foundations

Depth 183 from the axioms · uses propext, Classical.choice, Quot.sound

Assumes

CommRingCommRingAlgebraIsDomainIsIntegrallyClosedIsDomainIsIntegrallyClosedModule.FiniteModule.IsTorsionFree