fromUnit — Mathlib

English

There is a lift of the fromUnit map to a map from R/n into the Selmer group over the empty place set, compatible with lift via kerLift.

Русский

Существует подъем отображения fromUnit на отображение из R/n в Selmer-группу над пустым множеством мест, совместимый с подъемом через kerLift.

LaTeX

$$fromUnitLift : (R / n) →* K⟮∅,n⟯$$

Lean4

/-- The natural homomorphism from `Rˣ` to `K⟮∅, n⟯`. -/
def fromUnit {n : ℕ} : Rˣ →* K⟮(∅ : Set <| HeightOneSpectrum R),n⟯
    where
  toFun x := ⟨QuotientGroup.mk <| Units.map (algebraMap R K).toMonoidHom x, fun v _ => v.valuation_of_unit_mod_eq n x⟩
  map_one' := by simp only [map_one, QuotientGroup.mk_one, Subgroup.mk_eq_one]
  map_mul' _ _ := by simp only [RingHom.toMonoidHom_eq_coe, map_mul, QuotientGroup.mk_mul, MulMemClass.mk_mul_mk]

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