Theorems · Theorem · commutative algebra

IsFractionRing.fieldEquivOfAlgEquiv_algebraMap

∀ {A : Type u_8} {B : Type u_9} {C : Type u_10} [inst : CommRing A] [inst_1 : CommRing B] [inst_2 : CommRing C]
  [inst_3 : Algebra A B] [inst_4 : Algebra A C] (FA : Type u_12) (FB : Type u_13) (FC : Type u_14) [inst_5 : Field FA]
  [inst_6 : Field FB] [inst_7 : Field FC] [inst_8 : Algebra A FA] [inst_9 : Algebra B FB] [inst_10 : Algebra C FC]
  [inst_11 : IsFractionRing A FA] [inst_12 : IsFractionRing B FB] [inst_13 : IsFractionRing C FC]
  [inst_14 : Algebra A FB] [inst_15 : IsScalarTower A B FB] [inst_16 : Algebra A FC] [inst_17 : IsScalarTower A C FC]
  [inst_18 : Algebra FA FB] [inst_19 : IsScalarTower A FA FB] [inst_20 : Algebra FA FC]
  [inst_21 : IsScalarTower A FA FC] (f : B ≃ₐ[A] C) (b : B),
  (IsFractionRing.fieldEquivOfAlgEquiv FA FB FC f) ((algebraMap B FB) b) = (algebraMap C FC) (f b)

This says that fieldEquivOfAlgEquiv f is an extension of f (i.e., it agrees with f on B). Whereas (fieldEquivOfAlgEquiv f).commutes says that fieldEquivOfAlgEquiv f fixes K.

Defined in

Mathlib.RingTheory.Localization.FractionRing

Cited by

4 results in Mathlib

Foundations

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

Assumes

CommRingCommRingCommRingAlgebraAlgebraFieldFieldFieldAlgebraAlgebraAlgebraIsFractionRingIsFractionRingIsFractionRingAlgebraIsScalarTowerAlgebraIsScalarTowerAlgebraIsScalarTowerAlgebraIsScalarTower