Base change of homogeneous affine charts

Homogeneous localization away from a homogeneous element commutes with flat extension of the coefficient ring. These are the coordinate rings of the standard affine charts of a projective spectrum, so the comparison is the affine input to projective base change. In particular, extension from a field satisfies the flatness hypothesis automatically.

The comparison uses Mathlib's ordinary-localization base-change equivalence IsLocalization.Away.tensorProductEquivTMulRight and its grading on a scalar extension.

References

• The Stacks Project, Lemma 27.11.6, base change for projective spectra, proved on standard affine opens.

noncomputable def HomogeneousLocalization.Away.baseChangeMap {ι : Type u_1} {R : Type u_2} {A : Type u_3} [AddCommMonoid ι] [DecidableEq ι] [CommRing R] [CommRing A] [Algebra R A] (𝒜 : ι → Submodule R A) [GradedAlgebra 𝒜] (S : Type u_4) [CommRing S] [Algebra R S] (f : A) : Away 𝒜 f →+* Away (fun (i : ι) => Submodule.baseChange S (𝒜 i)) (1 ⊗ₜ[R] f)

The canonical graded coefficient map induces a map on homogeneous charts.

Equations

• One or more equations did not get rendered due to their size.

@[simp]

theorem HomogeneousLocalization.Away.baseChangeMap_mk {ι : Type u_1} {R : Type u_2} {A : Type u_3} [AddCommMonoid ι] [DecidableEq ι] [CommRing R] [CommRing A] [Algebra R A] (𝒜 : ι → Submodule R A) [GradedAlgebra 𝒜] (S : Type u_4) [CommRing S] [Algebra R S] (f : A) {d : ι} (hf : f ∈ 𝒜 d) (n : ℕ) (a : A) (ha : a ∈ 𝒜 (n • d)) : (baseChangeMap 𝒜 S f) (Away.mk 𝒜 hf n a ha) = Away.mk (fun (i : ι) => Submodule.baseChange S (𝒜 i)) ⋯ n (1 ⊗ₜ[R] a) ⋯

Extension of a homogeneous fraction extends its numerator and denominator.

theorem HomogeneousLocalization.Away.baseChangeMap_eq_map {ι : Type u_1} {R : Type u_2} {A : Type u_3} [AddCommMonoid ι] [DecidableEq ι] [CommRing R] [CommRing A] [Algebra R A] (𝒜 : ι → Submodule R A) [GradedAlgebra 𝒜] (S : Type u_4) [CommRing S] [Algebra R S] (f : A) : baseChangeMap 𝒜 S f = Away.map (TauCeti.GradedAlgebra.baseChangeMap S 𝒜) f

The chart coefficient map is the homogeneous-localization map of graded coefficient inclusion.

@[simp]

theorem HomogeneousLocalization.Away.baseChangeMap_algebraMap {ι : Type u_1} {R : Type u_2} {A : Type u_3} [AddCommMonoid ι] [DecidableEq ι] [CommRing R] [CommRing A] [Algebra R A] (𝒜 : ι → Submodule R A) [GradedAlgebra 𝒜] (S : Type u_4) [CommRing S] [Algebra R S] (f : A) (r : R) : (baseChangeMap 𝒜 S f) ((algebraMap R (Away 𝒜 f)) r) = (algebraMap S (Away (fun (i : ι) => Submodule.baseChange S (𝒜 i)) (1 ⊗ₜ[R] f))) ((algebraMap R S) r)

Coefficient extension on a chart respects the structure maps of the base rings.

theorem HomogeneousLocalization.Away.val_baseChangeMap {ι : Type u_1} {R : Type u_2} {A : Type u_3} [AddCommMonoid ι] [DecidableEq ι] [CommRing R] [CommRing A] [Algebra R A] (𝒜 : ι → Submodule R A) [GradedAlgebra 𝒜] (S : Type u_4) [CommRing S] [Algebra R S] (f : A) (z : Away 𝒜 f) : val ((baseChangeMap 𝒜 S f) z) = (Localization.awayMap Algebra.TensorProduct.includeRight.toRingHom f) (val z)

Forgetting the grading identifies coefficient extension with ordinary localization.

noncomputable def HomogeneousLocalization.Away.baseChangeHom {ι : Type u_1} {R : Type u_2} {A : Type u_3} [AddCommMonoid ι] [DecidableEq ι] [CommRing R] [CommRing A] [Algebra R A] (𝒜 : ι → Submodule R A) [GradedAlgebra 𝒜] (S : Type u_4) [CommRing S] [Algebra R S] (f : A) : TensorProduct R S (Away 𝒜 f) →ₐ[S] Away (fun (i : ι) => Submodule.baseChange S (𝒜 i)) (1 ⊗ₜ[R] f)

The canonical comparison from the scalar extension of a homogeneous affine chart to the corresponding chart of the scalar-extended graded algebra.

Equations

• One or more equations did not get rendered due to their size.

@[simp]

theorem HomogeneousLocalization.Away.baseChangeHom_tmul {ι : Type u_1} {R : Type u_2} {A : Type u_3} [AddCommMonoid ι] [DecidableEq ι] [CommRing R] [CommRing A] [Algebra R A] (𝒜 : ι → Submodule R A) [GradedAlgebra 𝒜] (S : Type u_4) [CommRing S] [Algebra R S] (f : A) (s : S) (z : Away 𝒜 f) : (baseChangeHom 𝒜 S f) (s ⊗ₜ[R] z) = s • (baseChangeMap 𝒜 S f) z

On pure tensors, the comparison multiplies by the extended coefficient.

theorem HomogeneousLocalization.Away.baseChangeHom_tmul_mk {ι : Type u_1} {R : Type u_2} {A : Type u_3} [AddCommMonoid ι] [DecidableEq ι] [CommRing R] [CommRing A] [Algebra R A] (𝒜 : ι → Submodule R A) [GradedAlgebra 𝒜] (S : Type u_4) [CommRing S] [Algebra R S] (f : A) {d : ι} (hf : f ∈ 𝒜 d) (n : ℕ) (s : S) (a : A) (ha : a ∈ 𝒜 (n • d)) : (baseChangeHom 𝒜 S f) (s ⊗ₜ[R] Away.mk 𝒜 hf n a ha) = Away.mk (fun (i : ι) => Submodule.baseChange S (𝒜 i)) ⋯ n (s ⊗ₜ[R] a) ⋯

The scalar-extended fraction s ⊗ (a/fⁿ) has numerator s ⊗ a.

theorem HomogeneousLocalization.Away.baseChangeHom_surjective {ι : Type u_1} {R : Type u_2} {A : Type u_3} [AddCommMonoid ι] [DecidableEq ι] [CommRing R] [CommRing A] [Algebra R A] (𝒜 : ι → Submodule R A) [GradedAlgebra 𝒜] (S : Type u_4) [CommRing S] [Algebra R S] (f : A) {d : ι} (hf : f ∈ 𝒜 d) : Function.Surjective ⇑(baseChangeHom 𝒜 S f)

Every homogeneous fraction after scalar extension comes from the scalar extension of the original chart. No flatness is required for surjectivity.

theorem HomogeneousLocalization.Away.val_baseChangeHom {ι : Type u_1} {R : Type u_2} {A : Type u_3} [AddCommMonoid ι] [DecidableEq ι] [CommRing R] [CommRing A] [Algebra R A] (𝒜 : ι → Submodule R A) [GradedAlgebra 𝒜] (S : Type u_4) [CommRing S] [Algebra R S] (f : A) (z : TensorProduct R S (Away 𝒜 f)) : val ((baseChangeHom 𝒜 S f) z) = (IsLocalization.Away.tensorProductEquivTMulRight R S f (Localization.Away f)) ((LinearMap.baseChange S (IsScalarTower.toAlgHom R (Away 𝒜 f) (Localization.Away f)).toLinearMap) z)

The homogeneous comparison agrees with ordinary-localization base change after the canonical embeddings into ordinary localizations.

theorem HomogeneousLocalization.Away.baseChangeHom_injective {ι : Type u_1} {R : Type u_2} {A : Type u_3} [AddCommMonoid ι] [DecidableEq ι] [CommRing R] [CommRing A] [Algebra R A] (𝒜 : ι → Submodule R A) [GradedAlgebra 𝒜] (S : Type u_4) [CommRing S] [Algebra R S] (f : A) [Module.Flat R S] : Function.Injective ⇑(baseChangeHom 𝒜 S f)

Flat coefficient extension makes the homogeneous chart comparison injective.

noncomputable def HomogeneousLocalization.Away.baseChangeEquiv {ι : Type u_1} {R : Type u_2} {A : Type u_3} [AddCommMonoid ι] [DecidableEq ι] [CommRing R] [CommRing A] [Algebra R A] (𝒜 : ι → Submodule R A) [GradedAlgebra 𝒜] (S : Type u_4) [CommRing S] [Algebra R S] (f : A) [Module.Flat R S] {d : ι} (hf : f ∈ 𝒜 d) : TensorProduct R S (Away 𝒜 f) ≃ₐ[S] Away (fun (i : ι) => Submodule.baseChange S (𝒜 i)) (1 ⊗ₜ[R] f)

Homogeneous localization away from a homogeneous element commutes with flat extension of the coefficient ring.

Equations

• HomogeneousLocalization.Away.baseChangeEquiv 𝒜 S f hf = AlgEquiv.ofBijective (HomogeneousLocalization.Away.baseChangeHom 𝒜 S f) ⋯

@[simp]

theorem HomogeneousLocalization.Away.baseChangeEquiv_apply {ι : Type u_1} {R : Type u_2} {A : Type u_3} [AddCommMonoid ι] [DecidableEq ι] [CommRing R] [CommRing A] [Algebra R A] (𝒜 : ι → Submodule R A) [GradedAlgebra 𝒜] (S : Type u_4) [CommRing S] [Algebra R S] (f : A) [Module.Flat R S] {d : ι} (hf : f ∈ 𝒜 d) (z : TensorProduct R S (Away 𝒜 f)) : (baseChangeEquiv 𝒜 S f hf) z = (baseChangeHom 𝒜 S f) z

The chart isomorphism has the canonical comparison as its underlying map.

@[simp]

theorem HomogeneousLocalization.Away.baseChangeEquiv_symm_mk {ι : Type u_1} {R : Type u_2} {A : Type u_3} [AddCommMonoid ι] [DecidableEq ι] [CommRing R] [CommRing A] [Algebra R A] (𝒜 : ι → Submodule R A) [GradedAlgebra 𝒜] (S : Type u_4) [CommRing S] [Algebra R S] (f : A) [Module.Flat R S] {d : ι} (hf : f ∈ 𝒜 d) (n : ℕ) (s : S) (a : A) (ha : a ∈ 𝒜 (n • d)) : (baseChangeEquiv 𝒜 S f hf).symm (Away.mk (fun (i : ι) => Submodule.baseChange S (𝒜 i)) ⋯ n (s ⊗ₜ[R] a) ⋯) = s ⊗ₜ[R] Away.mk 𝒜 hf n a ha

The inverse chart isomorphism recovers scalar-extended homogeneous fractions.