Theorems · Theorem · commutative algebra

IsFractionRing.algHom_commutes

∀ {A : Type u_4} [inst : CommRing A] {B : Type u_6} [inst_1 : CommRing B] [inst_2 : Algebra A B] {K₁ : Type u_8}
  {K₂ : Type u_9} [inst_3 : Field K₁] [inst_4 : Field K₂] [inst_5 : Algebra A K₁] [inst_6 : Algebra A K₂]
  [IsFractionRing A K₁] {L₁ : Type u_10} {L₂ : Type u_11} [inst_8 : Field L₁] [inst_9 : Field L₂]
  [inst_10 : Algebra B L₁] [inst_11 : Algebra B L₂] [inst_12 : Algebra K₁ L₁] [inst_13 : Algebra K₂ L₂]
  [inst_14 : Algebra A L₁] [inst_15 : Algebra A L₂] [IsScalarTower A K₁ L₁] [IsScalarTower A K₂ L₂]
  [IsScalarTower A B L₁] [IsScalarTower A B L₂] (e : K₁ →ₐ[A] K₂) (f : L₁ →ₐ[B] L₂) (x : K₁),
  (algebraMap K₂ L₂) (e x) = f ((algebraMap K₁ L₁) x)

Defined in

Mathlib.RingTheory.Localization.FractionRing

Cited by

1 results in Mathlib

Foundations

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

Assumes

CommRingCommRingAlgebraFieldFieldAlgebraAlgebraIsFractionRingFieldFieldAlgebraAlgebraAlgebraAlgebraAlgebraAlgebraIsScalarTowerIsScalarTowerIsScalarTowerIsScalarTower