Theorems · Theorem · commutative algebra

IsLocalization.ker_map

∀ {R : Type u_1} {S : Type u_2} {P : Type u_3} (Q : Type u_4) [inst : CommSemiring R] [inst_1 : CommSemiring S]
  [inst_2 : CommSemiring P] [inst_3 : CommSemiring Q] {M : Submonoid R} {T : Submonoid P} [inst_4 : Algebra R S]
  [inst_5 : Algebra P Q] [inst_6 : IsLocalization M S] [inst_7 : IsLocalization T Q] (g : R →+* P)
  (hT : Submonoid.map g M = T), RingHom.ker (IsLocalization.map Q g ⋯) = Ideal.map (algebraMap R S) (RingHom.ker g)

Defined in

Mathlib.RingTheory.Localization.Algebra

Cited by

2 results in Mathlib

Foundations

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

Assumes

CommSemiringCommSemiringCommSemiringCommSemiringAlgebraAlgebraIsLocalizationIsLocalization