idealPowersDiagram — Mathlib

English

Defines a functor from opposite natural numbers to Ideals by mapping t to J^t and arrows by radical containment.

Русский

Определяет функтор от противоположных натуральных чисел в идеалы: t ↦ J^t, стрелки по включению радикала.

LaTeX

$$$\\text{idealPowersDiagram } (J) : \\mathbb{N}^{op} \\to \\text{Ideal } R$ with$ $\\text{obj}(t)=J^{\\text{unop } t}$ and $\\text{map}(w)=\\langle\\langle \\text{Ideal.pow_le_pow_right}\\rangle\\rangle$$$

Lean4

/-- The functor sending a natural number `i` to the `i`-th power of the ideal `J` -/
def idealPowersDiagram (J : Ideal R) : ℕᵒᵖ ⥤ Ideal R
    where
  obj t := J ^ unop t
  map w := ⟨⟨Ideal.pow_le_pow_right w.unop.down.down⟩⟩

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