English
The lift constructions for localization maps are compatible with composition: given S ≤ T and localizations f, k, l, the composition of the induced map f.lift and k.lift equals the induced map f.lift with hl, i.e., lift(hl) ∘ lift_f = lift_f(hl).
Русский
Лифтинг локализаций совместим с композициями: при S ≤ T и локализациях f, k, l выполняется равенство последовательностей лифтов, эквивалентное композиции лифтов.
LaTeX
$$$ (k.lift\\; hl) \\circ (f.lift (map\\_units\\, k\\, \\langle\\_, hST\\,\\rangle)) = f.lift (hl \\langle\\_, hST\\,\\rangle). $$$
Lean4
/-- 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`. -/
@[to_additive /-- 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` -/
]
theorem lift_comp_lift {T : Submonoid M} (hST : S ≤ T) {Q : Type*} [CommMonoid Q] (k : LocalizationMap T Q) {A : Type*}
[CommMonoid A] {l : M →* A} (hl : ∀ w : T, IsUnit (l w)) :
(k.lift hl).comp (f.lift (map_units k ⟨_, hST ·.2⟩)) = f.lift (hl ⟨_, hST ·.2⟩) :=
.symm <|
lift_unique _ _ fun x ↦ by
rw [← toMonoidHom_apply, ← MonoidHom.comp_apply, MonoidHom.comp_assoc, lift_comp, lift_comp]
