lift_apply — Mathlib

English

If f is a monoid hom M → G, then applying lift to x corresponds to the division in the localization determined by sec x.

Русский

Применение lift к x соответствует делению в локализации, определяемому через sec x.

LaTeX

$$$\\text{lift}(f)(x) = f\\bigl((\\mathrm{Localization.monoidOf}(\\top)\\text{.sec } x)\\bigr).1 / f\\bigl((\\mathrm{Localization.monoidOf}(\\top)\\text{.sec } x)\\bigr).2$$$

Lean4

@[to_additive]
theorem lift_apply (f : M →* G) (x : GrothendieckGroup M) :
    lift f x = f ((monoidOf ⊤).sec x).1 / f ((monoidOf ⊤).sec x).2 := by
  simp [lift, (monoidOf ⊤).lift_apply, div_eq_mul_inv]; congr

Похожие утверждения