fromZeroRingHom — Mathlib

English

There is an algebra structure on the degree-zero part 𝒜0 into the homogeneous localization.

Русский

Существует алгебраическая структура над нулевым степенным компонентом 𝒜0 внутри однородной локализации.

LaTeX

$$$\\text{Algebra}(\\mathcal{A}_0, \\mathrm{HomogeneousLocalization}(\\mathcal{A},x))$$$

Lean4

/-- The map from `𝒜 0` to the degree `0` part of `𝒜ₓ` sending `f ↦ f/1`. -/
def fromZeroRingHom : 𝒜 0 →+* HomogeneousLocalization 𝒜 x
    where
  toFun f := .mk ⟨0, f, 1, one_mem _⟩
  map_one' := rfl
  map_mul' f g := by ext; simp [Localization.mk_mul]
  map_zero' := rfl
  map_add' f g := by ext; simp [Localization.add_mk, add_comm f.1 g.1]

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