English
Given a graded algebra homomorphism g respecting degrees and suitable submonoid inclusions, there is a canonical ring homomorphism between the corresponding homogeneous localizations.
Русский
Для градуированной алгебры с гомоморфизмом, сохраняющим степени, и подходящими включениями подпомножидков, существует канонический кольцевый гомоморфизм между соответствующими однородными локализациями.
LaTeX
$$$$ \mathrm{map}: \mathrm{HomogeneousLocalization}(\mathcal{A}, P) \to \mathrm{HomogeneousLocalization}(\mathcal{B}, Q). $$$$
Lean4
/-- Let `A, B` be two graded algebras with the same indexing set and `g : A → B` be a graded algebra
homomorphism (i.e. `g(Aₘ) ⊆ Bₘ`). Let `P ≤ A` be a submonoid and `Q ≤ B` be a submonoid such that
`P ≤ g⁻¹ Q`, then `g` induce a map from the homogeneous localizations `A⁰_P` to the homogeneous
localizations `B⁰_Q`.
-/
def map (g : A →+* B) (comap_le : P ≤ Q.comap g) (hg : ∀ i, ∀ a ∈ 𝒜 i, g a ∈ ℬ i) :
HomogeneousLocalization 𝒜 P →+* HomogeneousLocalization ℬ Q
where
toFun :=
Quotient.map' (fun x ↦ ⟨x.1, ⟨_, hg _ _ x.2.2⟩, ⟨_, hg _ _ x.3.2⟩, comap_le x.4⟩)
fun x y (e : x.embedding = y.embedding) ↦
by
apply_fun IsLocalization.map (Localization Q) g comap_le at e
simp_rw [HomogeneousLocalization.NumDenSameDeg.embedding, Localization.mk_eq_mk', IsLocalization.map_mk', ←
Localization.mk_eq_mk'] at e
exact e
map_add' :=
Quotient.ind₂' fun x y ↦ by simp only [← mk_add, Quotient.map'_mk'', num_add, map_add, map_mul, den_add]; rfl
map_mul' := Quotient.ind₂' fun x y ↦ by simp only [← mk_mul, Quotient.map'_mk'', num_mul, map_mul, den_mul]; rfl
map_zero' := by
simp only [← mk_zero (𝒜 := 𝒜), Quotient.map'_mk'', deg_zero, num_zero, ZeroMemClass.coe_zero, map_zero, den_zero,
map_one];
rfl
map_one' := by simp only [← mk_one (𝒜 := 𝒜), Quotient.map'_mk'', num_one, den_one, map_one]; rfl
