Algebra_norm_algebraMap_eq_of_isPushout_of_isFractionRing.lean

theorem isLocalization_of_finite (A B L : Type*) [CommRing A] [IsDomain A] [CommRing B] [IsDomain
  B] [Algebra A B]
    [Module.Finite A B] [Field L] [Algebra B L] [IsFractionRing B L] (h : Function.Injective
      (algebraMap A B)) :
    IsLocalization (Algebra.algebraMapSubmonoid B (nonZeroDivisors A)) L

theorem isPushout_of_finite (A B K L : Type*) [CommRing A] [IsDomain A] [CommRing B] [IsDomain B]
  [Algebra A B]
    [Module.Finite A B] [Field K] [Algebra A K] [IsFractionRing A K] [Field L] [Algebra B L]
      [IsFractionRing B L]
    [Algebra K L] [Algebra A L] [IsScalarTower A K L] [IsScalarTower A B L] (h :
      Function.Injective (algebraMap A B)) :
    Algebra.IsPushout A K B L

theorem _root_.Algebra.norm_algebraMap_eq_of_isPushout_of_isFractionRing
    {A B A' B' : Type u} [CommRing A] [CommRing B] [CommRing A'] [CommRing B']
    [IsDomain A] [IsDomain B] [IsDomain A'] [IsDomain B']
    [Algebra A B] [Algebra A A'] [Algebra B B'] [Algebra A' B'] [Algebra A B']
    [IsScalarTower A B B'] [IsScalarTower A A' B'] [Algebra.IsPushout A B A' B']
    [Module.Finite A B] (hAB : Function.Injective (algebraMap A B)) (hA'B' : Function.Injective
      (algebraMap A' B'))
    (K L K' L' : Type u) [Field K] [Field L] [Field K'] [Field L']
    [Algebra A K] [IsFractionRing A K] [Algebra B L] [IsFractionRing B L]
    [Algebra A' K'] [IsFractionRing A' K'] [Algebra B' L'] [IsFractionRing B' L']
    [Algebra K L] [Algebra A L] [IsScalarTower A K L] [IsScalarTower A B L]
    [Algebra K' L'] [Algebra A' L'] [IsScalarTower A' K' L'] [IsScalarTower A' B' L']
    (φ : K →+* K') (hφ : φ.comp (algebraMap A K) = (algebraMap A' K').comp (algebraMap A A'))
    (b : B) :
    φ (Algebra.norm K (algebraMap B L b)) = Algebra.norm K' (algebraMap B' L' (algebraMap B B' b))