Theorems · Theorem · group theory

Submonoid.LocalizationMap.lift_comp_lift

∀ {M : Type u_1} [inst : CommMonoid M] {S : Submonoid M} {N : Type u_2} [inst_1 : CommMonoid N]
  (f : S.LocalizationMap N) {T : Submonoid M} (hST : S ≤ T) {Q : Type u_4} [inst_2 : CommMonoid Q]
  (k : T.LocalizationMap Q) {A : Type u_5} [inst_3 : CommMonoid A] {l : M →* A} (hl : ∀ (w : ↥T), IsUnit (l ↑w)),
  (k.lift hl).comp (f.lift ⋯) = f.lift ⋯

Given Localization maps f : M →* N for a Submonoid S ⊆ M and k : M →* Q for a Submonoid T ⊆ M, such that S ≤ T, and we have l : M →* A, the composition of the induced map f.lift for k with the induced map k.lift for l is equal to the induced map f.lift for l.

Defined in

Mathlib.GroupTheory.MonoidLocalization.Maps

Cited by

1 results in Mathlib

Foundations

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

Assumes

CommMonoidCommMonoidCommMonoidCommMonoid