Theorems · Theorem · commutative algebra

Subalgebra.LinearDisjoint.norm_algebraMap

∀ {R : Type u} {S : Type v} [inst : CommRing R] [inst_1 : CommRing S] [inst_2 : Algebra R S] {A B : Subalgebra R S},
  A.LinearDisjoint B →
    A ⊔ B = ⊤ →
      ∀ [Module.Free R ↥B] [Module.Finite R ↥B] (x : ↥B),
        (Algebra.norm ↥A) ((algebraMap (↥B) S) x) = (algebraMap R ↥A) ((Algebra.norm R) x)

If A and B are subalgebras in a commutative algebra S over R, and if they are linearly disjoint and such that A ⊔ B = S, then norm and algebraMap commutes.

Defined in

Mathlib.RingTheory.LinearDisjoint

Cited by

1 results in Mathlib

Foundations

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

Assumes

CommRingCommRingAlgebraModule.FreeModule.Finite