mk_XYIdeal'_neg_mul — Mathlib

English

In the class group of the coordinate ring, the class of the ideal corresponding to a point and the class of the ideal corresponding to its negation multiply to the identity: class(XYIdeal'(neg h)) · class(XYIdeal'(h)) = 1.

Русский

В группе классов координатного кольца произведение классов идеалов, соответствующих точке и ее противоположности, даёт тождественный элемент: class(XYIdeal'(нег)) · class(XYIdeal'(h)) = 1.

LaTeX

$$$[XYIdeal'((nonsingular\\_neg\\,\\dots)\\, \\text{mpr}\\, h)] \\cdot [XYIdeal'(h)] = 1$$$

Lean4

theorem mk_XYIdeal'_neg_mul {x y : F} (h : W.Nonsingular x y) :
    ClassGroup.mk (XYIdeal' <| (nonsingular_neg ..).mpr h) * ClassGroup.mk (XYIdeal' h) = 1 :=
  by
  rw [← map_mul]
  exact
    (ClassGroup.mk_eq_one_of_coe_ideal <|
          (coeIdeal_mul ..).symm.trans <| FractionalIdeal.coeIdeal_inj.mpr <| XYIdeal_neg_mul h).mpr
      ⟨_, XClass_ne_zero x, rfl⟩

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