mapCotangent_toCotangent — Mathlib

English

The cotangent map commutes with cotangent lift on cotangent spaces under the inclusion of ideals and compatible algebra maps.

Русский

Котантгентовая карта согласуется с отображением котантгентов при включении идеалов и совместимых алгебраических отображений.

LaTeX

$$mapCotangent I1 I2 f h (toCotangent I1 x) = toCotangent I2 (⟨f x, h x.2⟩)$$

Lean4

@[simp]
theorem mapCotangent_toCotangent (I₁ : Ideal A) (I₂ : Ideal B) (f : A →ₐ[R] B) (h : I₁ ≤ I₂.comap f) (x : I₁) :
    Ideal.mapCotangent I₁ I₂ f h (Ideal.toCotangent I₁ x) = Ideal.toCotangent I₂ ⟨f x, h x.2⟩ :=
  rfl

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