diff --git a/Mathlib.lean b/Mathlib.lean index ec30d813df6af..14b5b0c4d7f7a 100644 --- a/Mathlib.lean +++ b/Mathlib.lean @@ -966,6 +966,7 @@ import Mathlib.AlgebraicGeometry.PrimeSpectrum.Module import Mathlib.AlgebraicGeometry.PrimeSpectrum.Noetherian import Mathlib.AlgebraicGeometry.PrimeSpectrum.TensorProduct import Mathlib.AlgebraicGeometry.ProjectiveSpectrum.Basic +import Mathlib.AlgebraicGeometry.ProjectiveSpectrum.Proper import Mathlib.AlgebraicGeometry.ProjectiveSpectrum.Scheme import Mathlib.AlgebraicGeometry.ProjectiveSpectrum.StructureSheaf import Mathlib.AlgebraicGeometry.ProjectiveSpectrum.Topology diff --git a/Mathlib/AlgebraicGeometry/ProjectiveSpectrum/Basic.lean b/Mathlib/AlgebraicGeometry/ProjectiveSpectrum/Basic.lean index b29a137f71eb2..1ebe7c785f7bb 100644 --- a/Mathlib/AlgebraicGeometry/ProjectiveSpectrum/Basic.lean +++ b/Mathlib/AlgebraicGeometry/ProjectiveSpectrum/Basic.lean @@ -166,6 +166,90 @@ lemma awayι_toSpecZero : awayι 𝒜 f f_deg hm ≫ toSpecZero 𝒜 = ← Spec.map_comp, ← Spec.map_comp, ← Spec.map_comp] rfl +variable {f} +variable {m' : ℕ} {g : A} (g_deg : g ∈ 𝒜 m') (hm' : 0 < m') {x : A} (hx : x = f * g) + +@[reassoc] +lemma awayMap_awayToSection : + CommRingCat.ofHom (awayMap 𝒜 g_deg hx) ≫ awayToSection 𝒜 x = + awayToSection 𝒜 f ≫ (Proj 𝒜).presheaf.map (homOfLE (basicOpen_mono _ _ _ ⟨_, hx⟩)).op := by + ext a + apply Subtype.ext + ext ⟨i, hi⟩ + obtain ⟨⟨n, a, ⟨b, hb'⟩, i, rfl : _ = b⟩, rfl⟩ := mk_surjective a + simp only [CommRingCat.forget_obj, CommRingCat.coe_of, CommRingCat.ofHom, CommRingCat.coe_comp_of, + RingHom.coe_comp, Function.comp_apply, homOfLE_leOfHom] + erw [ProjectiveSpectrum.Proj.awayToSection_apply] + rw [val_awayMap_mk, Localization.mk_eq_mk', IsLocalization.map_mk', + ← Localization.mk_eq_mk'] + refine Localization.mk_eq_mk_iff.mpr ?_ + rw [Localization.r_iff_exists] + use 1 + simp only [OneMemClass.coe_one, RingHom.id_apply, one_mul, hx] + ring + +@[reassoc] +lemma basicOpenToSpec_SpecMap_awayMap : + basicOpenToSpec 𝒜 x ≫ Spec.map (CommRingCat.ofHom (awayMap 𝒜 g_deg hx)) = + (Proj 𝒜).homOfLE (basicOpen_mono _ _ _ ⟨_, hx⟩) ≫ basicOpenToSpec 𝒜 f := by + rw [basicOpenToSpec, Category.assoc, ← Spec.map_comp, awayMap_awayToSection, + Spec.map_comp, Scheme.Opens.toSpecΓ_SpecMap_map_assoc] + rfl + +@[reassoc] +lemma SpecMap_awayMap_awayι : + Spec.map (CommRingCat.ofHom (awayMap 𝒜 g_deg hx)) ≫ awayι 𝒜 f f_deg hm = + awayι 𝒜 x (hx ▸ SetLike.mul_mem_graded f_deg g_deg) (hm.trans_le (m.le_add_right m')) := by + rw [awayι, awayι, Iso.eq_inv_comp, basicOpenIsoSpec_hom, basicOpenToSpec_SpecMap_awayMap_assoc, + ← basicOpenIsoSpec_hom _ _ f_deg hm, Iso.hom_inv_id_assoc, Scheme.homOfLE_ι] + +/-- The isomorphism `D₊(f) ×[Proj 𝒜] D₊(g) ≅ D₊(fg)`. -/ +noncomputable +def pullbackAwayιIso : + Limits.pullback (awayι 𝒜 f f_deg hm) (awayι 𝒜 g g_deg hm') ≅ + Spec (CommRingCat.of (Away 𝒜 x)) := + IsOpenImmersion.isoOfRangeEq (Limits.pullback.fst _ _ ≫ awayι 𝒜 f f_deg hm) + (awayι 𝒜 x (hx ▸ SetLike.mul_mem_graded f_deg g_deg) (hm.trans_le (m.le_add_right m'))) <| by + rw [IsOpenImmersion.range_pullback_to_base_of_left] + show ((awayι 𝒜 f _ _).opensRange ⊓ (awayι 𝒜 g _ _).opensRange).1 = (awayι 𝒜 _ _ _).opensRange.1 + rw [opensRange_awayι, opensRange_awayι, opensRange_awayι, ← basicOpen_mul, hx] + +@[reassoc (attr := simp)] +lemma pullbackAwayιIso_hom_awayι : + (pullbackAwayιIso 𝒜 f_deg hm g_deg hm' hx).hom ≫ + awayι 𝒜 x (hx ▸ SetLike.mul_mem_graded f_deg g_deg) (hm.trans_le (m.le_add_right m')) = + Limits.pullback.fst _ _ ≫ awayι 𝒜 f f_deg hm := + IsOpenImmersion.isoOfRangeEq_hom_fac .. + +@[reassoc (attr := simp)] +lemma pullbackAwayιIso_hom_SpecMap_awayMap_left : + (pullbackAwayιIso 𝒜 f_deg hm g_deg hm' hx).hom ≫ + Spec.map (CommRingCat.ofHom (awayMap 𝒜 g_deg hx)) = Limits.pullback.fst _ _ := by + rw [← cancel_mono (awayι 𝒜 f f_deg hm), ← pullbackAwayιIso_hom_awayι, + Category.assoc, SpecMap_awayMap_awayι] + +@[reassoc (attr := simp)] +lemma pullbackAwayιIso_hom_SpecMap_awayMap_right : + (pullbackAwayιIso 𝒜 f_deg hm g_deg hm' hx).hom ≫ + Spec.map (CommRingCat.ofHom (awayMap 𝒜 f_deg (hx.trans (mul_comm _ _)))) = + Limits.pullback.snd _ _ := by + rw [← cancel_mono (awayι 𝒜 g g_deg hm'), ← Limits.pullback.condition, + ← pullbackAwayιIso_hom_awayι 𝒜 f_deg hm g_deg hm' hx, + Category.assoc, SpecMap_awayMap_awayι] + rfl + +@[reassoc (attr := simp)] +lemma pullbackAwayιIso_inv_fst : + (pullbackAwayιIso 𝒜 f_deg hm g_deg hm' hx).inv ≫ Limits.pullback.fst _ _ = + Spec.map (CommRingCat.ofHom (awayMap 𝒜 g_deg hx)) := by + rw [← pullbackAwayιIso_hom_SpecMap_awayMap_left, Iso.inv_hom_id_assoc] + +@[reassoc (attr := simp)] +lemma pullbackAwayιIso_inv_snd : + (pullbackAwayιIso 𝒜 f_deg hm g_deg hm' hx).inv ≫ Limits.pullback.snd _ _ = + Spec.map (CommRingCat.ofHom (awayMap 𝒜 f_deg (hx.trans (mul_comm _ _)))) := by + rw [← pullbackAwayιIso_hom_SpecMap_awayMap_right, Iso.inv_hom_id_assoc] + open TopologicalSpace.Opens in /-- Given a family of homogeneous elements `f` of positive degree that spans the irrelavent ideal, `Spec (A_f)₀ ⟶ Proj A` forms an affine open cover of `Proj A`. -/ diff --git a/Mathlib/AlgebraicGeometry/ProjectiveSpectrum/Proper.lean b/Mathlib/AlgebraicGeometry/ProjectiveSpectrum/Proper.lean new file mode 100644 index 0000000000000..6235852b32c97 --- /dev/null +++ b/Mathlib/AlgebraicGeometry/ProjectiveSpectrum/Proper.lean @@ -0,0 +1,126 @@ +/- +Copyright (c) 2024 Andrew Yang. All rights reserved. +Released under Apache 2.0 license as described in the file LICENSE. +Authors: Patience Ablett, Kevin Buzzard, Harald Carlens, Wayne Ng Kwing King, Michael Schlößer, + Justus Springer, Andrew Yang, Jujian Zhang +-/ +import Mathlib.AlgebraicGeometry.Morphisms.Separated +import Mathlib.AlgebraicGeometry.ProjectiveSpectrum.Basic + +/-! +# Properness of `Proj A` + +We show that `Proj 𝒜` is a separated scheme. + +## TODO +- Show that `Proj 𝒜` satisfies the valuative criterion. + +## Notes +This contribution was created as part of the Durham Computational Algebraic Geometry Workshop + +-/ + +namespace AlgebraicGeometry.Proj + +variable {R A : Type*} +variable [CommRing R] [CommRing A] [Algebra R A] +variable (𝒜 : ℕ → Submodule R A) +variable [GradedAlgebra 𝒜] + +open Scheme CategoryTheory Limits pullback HomogeneousLocalization + +lemma lift_awayMapₐ_awayMapₐ_surjective {d e : ℕ} {f : A} (hf : f ∈ 𝒜 d) + {g : A} (hg : g ∈ 𝒜 e) {x : A} (hx : x = f * g) (hd : 0 < d) : + Function.Surjective + (Algebra.TensorProduct.lift (awayMapₐ 𝒜 hg hx) (awayMapₐ 𝒜 hf (hx.trans (mul_comm _ _))) + (fun _ _ ↦ .all _ _)) := by + intro z + obtain ⟨⟨n, ⟨a, ha⟩, ⟨b, hb'⟩, ⟨j, (rfl : _ = b)⟩⟩, rfl⟩ := mk_surjective z + by_cases hfg : (f * g) ^ j = 0 + · use 0 + have := HomogeneousLocalization.subsingleton 𝒜 (x := Submonoid.powers x) ⟨j, hx ▸ hfg⟩ + exact this.elim _ _ + have : n = j * (d + e) := by + apply DirectSum.degree_eq_of_mem_mem 𝒜 hb' + convert SetLike.pow_mem_graded _ _ using 2 + · infer_instance + · exact hx ▸ SetLike.mul_mem_graded hf hg + · exact hx ▸ hfg + let x0 : NumDenSameDeg 𝒜 (.powers f) := + { deg := j * (d * (e + 1)) + num := ⟨a * g ^ (j * (d - 1)), by + convert SetLike.mul_mem_graded ha (SetLike.pow_mem_graded _ hg) using 2 + rw [this] + cases d + · contradiction + · simp; ring⟩ + den := ⟨f ^ (j * (e + 1)), by convert SetLike.pow_mem_graded _ hf using 2; ring⟩ + den_mem := ⟨_,rfl⟩ } + let y0 : NumDenSameDeg 𝒜 (.powers g) := + { deg := j * (d * e) + num := ⟨f ^ (j * e), by convert SetLike.pow_mem_graded _ hf using 2; ring⟩ + den := ⟨g ^ (j * d), by convert SetLike.pow_mem_graded _ hg using 2; ring⟩ + den_mem := ⟨_,rfl⟩ } + use mk x0 ⊗ₜ mk y0 + ext + simp only [Algebra.TensorProduct.lift_tmul, awayMapₐ_apply, val_mul, + val_awayMap_mk, Localization.mk_mul, val_mk, x0, y0] + rw [Localization.mk_eq_mk_iff, Localization.r_iff_exists] + use 1 + simp only [OneMemClass.coe_one, one_mul, Submonoid.mk_mul_mk] + cases d + · contradiction + · simp only [hx, add_tsub_cancel_right] + ring + +open TensorProduct in +instance isSeparated : IsSeparated (toSpecZero 𝒜) := by + refine ⟨IsLocalAtTarget.of_openCover (Pullback.openCoverOfLeftRight + (affineOpenCover 𝒜).openCover (affineOpenCover 𝒜).openCover _ _) ?_⟩ + intro ⟨i, j⟩ + dsimp [Scheme, Cover.pullbackHom] + refine (MorphismProperty.cancel_left_of_respectsIso (P := @IsClosedImmersion) + (f := (pullbackDiagonalMapIdIso ..).inv) _).mp ?_ + let e₁ : pullback ((affineOpenCover 𝒜).map i ≫ toSpecZero 𝒜) + ((affineOpenCover 𝒜).map j ≫ toSpecZero 𝒜) ≅ + Spec (.of <| TensorProduct (𝒜 0) (Away 𝒜 i.2) (Away 𝒜 j.2)) := by + refine pullback.congrHom ?_ ?_ ≪≫ pullbackSpecIso (𝒜 0) (Away 𝒜 i.2) (Away 𝒜 j.2) + · simp [affineOpenCover, openCoverOfISupEqTop, awayι_toSpecZero]; rfl + · simp [affineOpenCover, openCoverOfISupEqTop, awayι_toSpecZero]; rfl + let e₂ : pullback ((affineOpenCover 𝒜).map i) ((affineOpenCover 𝒜).map j) ≅ + Spec (.of <| (Away 𝒜 (i.2 * j.2))) := + pullbackAwayιIso 𝒜 _ _ _ _ rfl + rw [← MorphismProperty.cancel_right_of_respectsIso (P := @IsClosedImmersion) _ e₁.hom, + ← MorphismProperty.cancel_left_of_respectsIso (P := @IsClosedImmersion) e₂.inv] + let F : Away 𝒜 i.2.1 ⊗[𝒜 0] Away 𝒜 j.2.1 →+* Away 𝒜 (i.2.1 * j.2.1) := + (Algebra.TensorProduct.lift (awayMapₐ 𝒜 j.2.2 rfl) (awayMapₐ 𝒜 i.2.2 (mul_comm _ _)) + (fun _ _ ↦ .all _ _)).toRingHom + have : Function.Surjective F := lift_awayMapₐ_awayMapₐ_surjective 𝒜 i.2.2 j.2.2 rfl i.1.2 + convert IsClosedImmersion.spec_of_surjective + (CommRingCat.ofHom (R := Away 𝒜 i.2.1 ⊗[𝒜 0] Away 𝒜 j.2.1) F) this using 1 + rw [← cancel_mono (pullbackSpecIso ..).inv] + apply pullback.hom_ext + · simp only [Iso.trans_hom, congrHom_hom, Category.assoc, Iso.hom_inv_id, Category.comp_id, + limit.lift_π, id_eq, eq_mpr_eq_cast, PullbackCone.mk_pt, PullbackCone.mk_π_app, e₂, e₁, + pullbackDiagonalMapIdIso_inv_snd_fst, AlgHom.toRingHom_eq_coe, pullbackSpecIso_inv_fst, + ← Spec.map_comp] + erw [pullbackAwayιIso_inv_fst] + congr 1 + ext x + exact DFunLike.congr_fun (Algebra.TensorProduct.lift_comp_includeLeft + (awayMapₐ 𝒜 j.2.2 rfl) (awayMapₐ 𝒜 i.2.2 (mul_comm _ _)) (fun _ _ ↦ .all _ _)).symm x + · simp only [Iso.trans_hom, congrHom_hom, Category.assoc, Iso.hom_inv_id, Category.comp_id, + limit.lift_π, id_eq, eq_mpr_eq_cast, PullbackCone.mk_pt, PullbackCone.mk_π_app, + pullbackDiagonalMapIdIso_inv_snd_snd, AlgHom.toRingHom_eq_coe, pullbackSpecIso_inv_snd, ← + Spec.map_comp, e₂, e₁] + erw [pullbackAwayιIso_inv_snd] + congr 1 + ext x + exact DFunLike.congr_fun (Algebra.TensorProduct.lift_comp_includeRight + (awayMapₐ 𝒜 j.2.2 rfl) (awayMapₐ 𝒜 i.2.2 (mul_comm _ _)) (fun _ _ ↦ .all _ _)).symm x + +@[stacks 01MC] +instance : Scheme.IsSeparated (Proj 𝒜) := + (HasAffineProperty.iff_of_isAffine (P := @IsSeparated)).mp (isSeparated 𝒜) + +end AlgebraicGeometry.Proj diff --git a/Mathlib/AlgebraicGeometry/ProjectiveSpectrum/Scheme.lean b/Mathlib/AlgebraicGeometry/ProjectiveSpectrum/Scheme.lean index 462689531697b..781f0783739f0 100644 --- a/Mathlib/AlgebraicGeometry/ProjectiveSpectrum/Scheme.lean +++ b/Mathlib/AlgebraicGeometry/ProjectiveSpectrum/Scheme.lean @@ -603,6 +603,16 @@ lemma awayToSection_germ (f x hx) : apply (Proj.stalkIso' 𝒜 x).eq_symm_apply.mpr apply Proj.stalkIso'_germ +lemma awayToSection_apply (f : A) (x p) : + (((ProjectiveSpectrum.Proj.awayToSection 𝒜 f).1 x).val p).val = + IsLocalization.map (M := Submonoid.powers f) (T := p.1.1.toIdeal.primeCompl) _ + (RingHom.id _) (Submonoid.powers_le.mpr p.2) x.val := by + obtain ⟨x, rfl⟩ := HomogeneousLocalization.mk_surjective x + show (HomogeneousLocalization.mapId 𝒜 _ _).val = _ + dsimp [HomogeneousLocalization.mapId, HomogeneousLocalization.map] + rw [Localization.mk_eq_mk', Localization.mk_eq_mk', IsLocalization.map_mk'] + rfl + /-- The ring map from `A⁰_ f` to the global sections of the structure sheaf of the projective spectrum of `A` restricted to the basic open set `D(f)`. diff --git a/Mathlib/RingTheory/GradedAlgebra/HomogeneousLocalization.lean b/Mathlib/RingTheory/GradedAlgebra/HomogeneousLocalization.lean index dcab8f6f958a6..af6dc235b4928 100644 --- a/Mathlib/RingTheory/GradedAlgebra/HomogeneousLocalization.lean +++ b/Mathlib/RingTheory/GradedAlgebra/HomogeneousLocalization.lean @@ -6,6 +6,7 @@ Authors: Jujian Zhang, Eric Wieser import Mathlib.Order.Filter.AtTopBot import Mathlib.RingTheory.Localization.AtPrime import Mathlib.RingTheory.GradedAlgebra.Basic +import Mathlib.RingTheory.Localization.Away.Basic /-! # Homogeneous Localization @@ -473,6 +474,11 @@ def fromZeroRingHom : 𝒜 0 →+* HomogeneousLocalization 𝒜 x where map_zero' := rfl map_add' f g := by ext; simp [Localization.add_mk, add_comm f.1 g.1] +instance : Algebra (𝒜 0) (HomogeneousLocalization 𝒜 x) := + (fromZeroRingHom 𝒜 x).toAlgebra + +lemma algebraMap_eq : algebraMap (𝒜 0) (HomogeneousLocalization 𝒜 x) = fromZeroRingHom 𝒜 x := rfl + end HomogeneousLocalization namespace HomogeneousLocalization @@ -627,4 +633,88 @@ lemma map_mk (g : A →+* B) end +section mapAway + +variable [AddCommMonoid ι] [DecidableEq ι] [GradedAlgebra 𝒜] +variable {d e : ι} {f : A} (hf : f ∈ 𝒜 d) {g : A} (hg : g ∈ 𝒜 e) +variable {x : A} (hx : x = f * g) + +variable (𝒜) + +/-- Given `f ∣ x`, this is the map `A_{(f)} → A_f → A_x`. We will lift this to a map +`A_{(f)} → A_{(x)}` in `awayMap`. -/ +private def awayMapAux (hx : f ∣ x) : Away 𝒜 f →+* Localization.Away x := + (Localization.awayLift (algebraMap A _) _ + (isUnit_of_dvd_unit (map_dvd _ hx) (IsLocalization.Away.algebraMap_isUnit x))).comp + (algebraMap (Away 𝒜 f) (Localization.Away f)) + +lemma awayMapAux_mk (n a i hi) : + awayMapAux 𝒜 ⟨_, hx⟩ (mk ⟨n, a, ⟨f ^ i, hi⟩, ⟨i, rfl⟩⟩) = + Localization.mk (a * g ^ i) ⟨x ^ i, (Submonoid.mem_powers_iff _ _).mpr ⟨i, rfl⟩⟩ := by + have : algebraMap A (Localization.Away x) f * + (Localization.mk g ⟨f * g, (Submonoid.mem_powers_iff _ _).mpr ⟨1, by simp [hx]⟩⟩) = 1 := by + rw [← Algebra.smul_def, Localization.smul_mk] + exact Localization.mk_self ⟨f*g, _⟩ + simp [awayMapAux] + rw [Localization.awayLift_mk (hv := this), ← Algebra.smul_def, + Localization.mk_pow, Localization.smul_mk] + subst hx + rfl + +include hg in +lemma range_awayMapAux_subset : + Set.range (awayMapAux 𝒜 (f := f) ⟨_, hx⟩) ⊆ Set.range (val (𝒜 := 𝒜)) := by + rintro _ ⟨z, rfl⟩ + obtain ⟨⟨n, ⟨a, ha⟩, ⟨b, hb'⟩, j, rfl : _ = b⟩, rfl⟩ := mk_surjective z + use mk ⟨n+j•e,⟨a*g^j, ?_⟩ ,⟨x^j, ?_⟩, j, rfl⟩ + · simp [awayMapAux_mk 𝒜 (hx := hx)] + · apply SetLike.mul_mem_graded ha + exact SetLike.pow_mem_graded _ hg + · rw [hx, mul_pow] + apply SetLike.mul_mem_graded hb' + exact SetLike.pow_mem_graded _ hg + +/-- 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 + +lemma val_awayMap_eq_aux (a) : (awayMap 𝒜 hg hx a).val = awayMapAux 𝒜 ⟨_, hx⟩ a := by + let e := RingEquiv.ofLeftInverse (f := algebraMap (Away 𝒜 x) (Localization.Away x)) + (h := (val_injective _).hasLeftInverse.choose_spec) + dsimp [awayMap] + convert_to (e (e.symm ⟨awayMapAux 𝒜 (f := f) ⟨_, hx⟩ a, + range_awayMapAux_subset 𝒜 hg hx ⟨_, rfl⟩⟩)).1 = _ + rw [e.apply_symm_apply] + +lemma val_awayMap (a) : (awayMap 𝒜 hg hx a).val = Localization.awayLift (algebraMap A _) _ + (isUnit_of_dvd_unit (map_dvd _ ⟨_, hx⟩) (IsLocalization.Away.algebraMap_isUnit x)) a.val := by + rw [val_awayMap_eq_aux] + rfl + +lemma awayMap_fromZeroRingHom (a) : + awayMap 𝒜 hg hx (fromZeroRingHom 𝒜 _ a) = fromZeroRingHom 𝒜 _ a := by + ext + simp only [fromZeroRingHom, RingHom.coe_mk, MonoidHom.coe_mk, OneHom.coe_mk, + val_awayMap, val_mk, SetLike.GradeZero.coe_one] + convert IsLocalization.lift_eq _ _ + +lemma val_awayMap_mk (n a i hi) : (awayMap 𝒜 hg hx (mk ⟨n, a, ⟨f ^ i, hi⟩, ⟨i, rfl⟩⟩)).val = + Localization.mk (a * g ^ i) ⟨x ^ i, (Submonoid.mem_powers_iff _ _).mpr ⟨i, rfl⟩⟩ := by + rw [val_awayMap_eq_aux, awayMapAux_mk 𝒜 (hx := hx)] + +/-- 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 .. + +@[simp] lemma awayMapₐ_apply (a) : awayMapₐ 𝒜 hg hx a = awayMap 𝒜 hg hx a := rfl + +end mapAway + end HomogeneousLocalization diff --git a/Mathlib/RingTheory/Localization/Away/Basic.lean b/Mathlib/RingTheory/Localization/Away/Basic.lean index d587619c72796..01a01a331e08b 100644 --- a/Mathlib/RingTheory/Localization/Away/Basic.lean +++ b/Mathlib/RingTheory/Localization/Away/Basic.lean @@ -361,6 +361,15 @@ noncomputable abbrev awayLift (f : R →+* P) (r : R) (hr : IsUnit (f r)) : Localization.Away r →+* P := IsLocalization.Away.lift r hr +lemma awayLift_mk {A : Type*} [CommRing A] (f : R →+* A) (r : R) + (a : R) (v : A) (hv : f r * v = 1) (j : ℕ) : + Localization.awayLift f r (isUnit_iff_exists_inv.mpr ⟨v, hv⟩) + (Localization.mk a ⟨r ^ j, j, rfl⟩) = f a * v ^ j := by + rw [Localization.mk_eq_mk'] + erw [IsLocalization.lift_mk'] + rw [Units.mul_inv_eq_iff_eq_mul] + simp [IsUnit.liftRight, mul_assoc, ← mul_pow, (mul_comm _ _).trans hv] + /-- Given a map `f : R →+* S` and an element `r : R`, we may construct a map `Rᵣ →+* Sᵣ`. -/ noncomputable abbrev awayMap (f : R →+* P) (r : R) : Localization.Away r →+* Localization.Away (f r) :=