transitionMap_comp_reduceModIdeal

English

Equality of maps from adic completion can be checked on mk I M a for all Cauchy sequences a.

Русский

Равенство отображений из адического завершения можно проверить на образах mk I M a для всех последовательностей Коши a.

LaTeX

$$$\forall f,g:\mathrm{AdicCompletion}\ I\ M \to N,\ (\forall a:\mathrm{AdicCauchySequence}\ I\ M,\ f(\mathrm{AdicCompletion.mk}\ I\ M\ a) = g(\mathrm{AdicCompletion.mk}\ I\ M\ a)) \Rightarrow f=g$$$

Lean4

theorem transitionMap_comp_reduceModIdeal (f : M →ₗ[R] N) {m n : ℕ} (hmn : m ≤ n) :
    transitionMap I N hmn ∘ₗ f.reduceModIdeal (I ^ n) =
      (f.reduceModIdeal (I ^ m) : _ →ₗ[R] _) ∘ₗ transitionMap I M hmn :=
  by
  ext x
  simp

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