awayMapₐ — Mathlib

English

Applying awayMap to mk yields a canonical mk in the target away.

Русский

Применение awayMap к mk дает канонический mk в целевой away.

LaTeX

$$$$ \text{awayMap}(\mathcal{A}, hg, hx)(\mathrm{Away.mk}(\mathcal{A}, hf, n, a, ha)) = \mathrm{Away.mk}(\mathcal{A}, (hx \Rightarrow \cdot), n, a) $$$$

Lean4

/-- Given `x = f * g` with `g` homogeneous of positive degree,
this is the map `A_{(f)} → A_{(x)}` taking `a/f^i` to `ag^i/(fg)^i`. -/
def awayMapₐ : Away 𝒜 f →ₐ[𝒜 0] Away 𝒜 x where
  __ := awayMap 𝒜 hg hx
  commutes' _ := awayMap_fromZeroRingHom ..

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