English
A convenient constructor Away.mk builds a homogeneous fraction a/f^n with a in 𝒜 (n•d) and f^n in the appropriate graded piece.
Русский
Удобный конструктор Away.mk строит однородную дробь a/f^n с a в 𝒜 (n•d) и f^n в соответствующей градационной части.
LaTeX
$$$$ \mathrm{Away.mk}: \text{hf} \mapsto \text{mk} \;\langle a, \dots \rangle. $$$$
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 →+* Away 𝒜 x :=
by
let e :=
RingEquiv.ofLeftInverse (f := algebraMap (Away 𝒜 x) (Localization.Away x)) (h :=
(val_injective _).hasLeftInverse.choose_spec)
refine RingHom.comp (e.symm.toRingHom.comp (Subring.inclusion ?_)) (awayMapAux 𝒜 (f := f) ⟨_, hx⟩).rangeRestrict
exact range_awayMapAux_subset 𝒜 hg hx
