Presentations on subrings

In this file we establish the API for realising a presentation over a subring of R. We define a property HasCoeffs R₀ for a presentation P to mean the (sub)ring R₀ contains the coefficients of the relations of P. subring R₀ of R that contains the coefficients of the relations In this case there exists a model of S over R₀, i.e., there exists an R₀-algebra S₀ such that S is isomorphic to R ⊗[R₀] S₀.

If the presentation is finite, R₀ may be chosen as a Noetherian ring. In this case, this API can be used to remove Noetherian hypothesis in certain cases.

def Algebra.Presentation.coeffs {R : Type u_1} {S : Type u_2} {ι : Type u_3} {σ : Type u_4} [CommRing R] [CommRing S] [Algebra R S] (P : Presentation R S ι σ) : Set R

The coefficients of a presentation are the coefficients of the relations.

Equations

• P.coeffs = ⋃ (i : σ), ↑(MvPolynomial.coeffs (P.relation i))

theorem Algebra.Presentation.coeffs_relation_subset_coeffs {R : Type u_1} {S : Type u_2} {ι : Type u_3} {σ : Type u_4} [CommRing R] [CommRing S] [Algebra R S] {P : Presentation R S ι σ} (x : σ) : ↑(MvPolynomial.coeffs (P.relation x)) ⊆ P.coeffs

theorem Algebra.Presentation.finite_coeffs {R : Type u_1} {S : Type u_2} {ι : Type u_3} {σ : Type u_4} [CommRing R] [CommRing S] [Algebra R S] {P : Presentation R S ι σ} [Finite σ] : P.coeffs.Finite

def Algebra.Presentation.core {R : Type u_1} {S : Type u_2} {ι : Type u_3} {σ : Type u_4} [CommRing R] [CommRing S] [Algebra R S] (P : Presentation R S ι σ) : Subalgebra ℤ R

The core of a presentation is the subalgebra generated by the coefficients of the relations.

Equations

• P.core = Algebra.adjoin ℤ P.coeffs

theorem Algebra.Presentation.coeffs_subset_core {R : Type u_1} {S : Type u_2} {ι : Type u_3} {σ : Type u_4} [CommRing R] [CommRing S] [Algebra R S] (P : Presentation R S ι σ) : P.coeffs ⊆ ↑P.core

theorem Algebra.Presentation.coeffs_relation_subset_core {R : Type u_1} {S : Type u_2} {ι : Type u_3} {σ : Type u_4} [CommRing R] [CommRing S] [Algebra R S] {P : Presentation R S ι σ} (x : σ) : ↑(MvPolynomial.coeffs (P.relation x)) ⊆ ↑P.core

def Algebra.Presentation.Core {R : Type u_1} {S : Type u_2} {ι : Type u_3} {σ : Type u_4} [CommRing R] [CommRing S] [Algebra R S] (P : Presentation R S ι σ) : Type u_1

The core coerced to a type for performance reasons.

Equations

• P.Core = ↥P.core

instance Algebra.Presentation.instCommRingCore {R : Type u_1} {S : Type u_2} {ι : Type u_3} {σ : Type u_4} [CommRing R] [CommRing S] [Algebra R S] {P : Presentation R S ι σ} : CommRing P.Core

Equations

• Algebra.Presentation.instCommRingCore = P.core.toCommRing

instance Algebra.Presentation.instCore {R : Type u_1} {S : Type u_2} {ι : Type u_3} {σ : Type u_4} [CommRing R] [CommRing S] [Algebra R S] {P : Presentation R S ι σ} : Algebra P.Core R

Equations

• Algebra.Presentation.instCore = P.core.toAlgebra

instance Algebra.Presentation.instFaithfulSMulCore {R : Type u_1} {S : Type u_2} {ι : Type u_3} {σ : Type u_4} [CommRing R] [CommRing S] [Algebra R S] {P : Presentation R S ι σ} : FaithfulSMul P.Core R

instance Algebra.Presentation.instCore_1 {R : Type u_1} {S : Type u_2} {ι : Type u_3} {σ : Type u_4} [CommRing R] [CommRing S] [Algebra R S] {P : Presentation R S ι σ} : Algebra P.Core S

Equations

• Algebra.Presentation.instCore_1 = P.core.toAlgebra

instance Algebra.Presentation.instIsScalarTowerCore {R : Type u_1} {S : Type u_2} {ι : Type u_3} {σ : Type u_4} [CommRing R] [CommRing S] [Algebra R S] {P : Presentation R S ι σ} : IsScalarTower P.Core R S

instance Algebra.Presentation.instFiniteTypeIntCoreOfFinite {R : Type u_1} {S : Type u_2} {ι : Type u_3} {σ : Type u_4} [CommRing R] [CommRing S] [Algebra R S] {P : Presentation R S ι σ} [Finite σ] : FiniteType ℤ P.Core

class Algebra.Presentation.HasCoeffs {R : Type u_1} {S : Type u_2} {ι : Type u_3} {σ : Type u_4} [CommRing R] [CommRing S] [Algebra R S] (P : Presentation R S ι σ) (R₀ : Type u_5) [CommRing R₀] [Algebra R₀ R] [Algebra R₀ S] [IsScalarTower R₀ R S] : Prop

A ring R₀ has the coefficients of the presentation P if the coefficients of the relations of P lie in the image of R₀ in R. The smallest subring of R satisfying this is given by Algebra.Presentation.Core P.

• coeffs_subset_range : P.coeffs ⊆ Set.range ⇑(algebraMap R₀ R)

instance Algebra.Presentation.instHasCoeffsCore {R : Type u_1} {S : Type u_2} {ι : Type u_3} {σ : Type u_4} [CommRing R] [CommRing S] [Algebra R S] {P : Presentation R S ι σ} : P.HasCoeffs P.Core

theorem Algebra.Presentation.coeffs_subset_range {R : Type u_1} {S : Type u_2} {ι : Type u_3} {σ : Type u_4} [CommRing R] [CommRing S] [Algebra R S] {P : Presentation R S ι σ} (R₀ : Type u_5) [CommRing R₀] [Algebra R₀ R] [Algebra R₀ S] [IsScalarTower R₀ R S] [P.HasCoeffs R₀] : P.coeffs ⊆ Set.range ⇑(algebraMap R₀ R)

theorem Algebra.Presentation.HasCoeffs.of_isScalarTower {R : Type u_1} {S : Type u_2} {ι : Type u_3} {σ : Type u_4} [CommRing R] [CommRing S] [Algebra R S] {P : Presentation R S ι σ} (R₀ : Type u_5) [CommRing R₀] [Algebra R₀ R] [Algebra R₀ S] [IsScalarTower R₀ R S] [P.HasCoeffs R₀] {R₁ : Type u_6} [CommRing R₁] [Algebra R₀ R₁] [Algebra R₁ R] [IsScalarTower R₀ R₁ R] [Algebra R₁ S] [IsScalarTower R₁ R S] : P.HasCoeffs R₁

instance Algebra.Presentation.instHasCoeffsSubtypeMemSubalgebraAdjoin {R : Type u_1} {S : Type u_2} {ι : Type u_3} {σ : Type u_4} [CommRing R] [CommRing S] [Algebra R S] {P : Presentation R S ι σ} (R₀ : Type u_5) [CommRing R₀] [Algebra R₀ R] [Algebra R₀ S] [IsScalarTower R₀ R S] [P.HasCoeffs R₀] (s : Set R) : P.HasCoeffs ↥(adjoin R₀ s)

theorem Algebra.Presentation.HasCoeffs.coeffs_relation_mem_range {R : Type u_1} {S : Type u_2} {ι : Type u_3} {σ : Type u_4} [CommRing R] [CommRing S] [Algebra R S] {P : Presentation R S ι σ} (R₀ : Type u_5) [CommRing R₀] [Algebra R₀ R] [Algebra R₀ S] [IsScalarTower R₀ R S] [P.HasCoeffs R₀] (x : σ) : ↑(MvPolynomial.coeffs (P.relation x)) ⊆ Set.range ⇑(algebraMap R₀ R)

theorem Algebra.Presentation.HasCoeffs.relation_mem_range_map {R : Type u_1} {S : Type u_2} {ι : Type u_3} {σ : Type u_4} [CommRing R] [CommRing S] [Algebra R S] {P : Presentation R S ι σ} (R₀ : Type u_5) [CommRing R₀] [Algebra R₀ R] [Algebra R₀ S] [IsScalarTower R₀ R S] [P.HasCoeffs R₀] (x : σ) : P.relation x ∈ Set.range ⇑(MvPolynomial.map (algebraMap R₀ R))

noncomputable def Algebra.Presentation.relationOfHasCoeffs {R : Type u_1} {S : Type u_2} {ι : Type u_3} {σ : Type u_4} [CommRing R] [CommRing S] [Algebra R S] {P : Presentation R S ι σ} (R₀ : Type u_5) [CommRing R₀] [Algebra R₀ R] [Algebra R₀ S] [IsScalarTower R₀ R S] [P.HasCoeffs R₀] (r : σ) : MvPolynomial ι R₀

The r-th relation of P as a polynomial in R₀. This is the (arbitrary) choice of a pre-image under the map R₀[X] → R[X].

Equations

• Algebra.Presentation.relationOfHasCoeffs R₀ r = Exists.choose ⋯

theorem Algebra.Presentation.map_relationOfHasCoeffs {R : Type u_1} {S : Type u_2} {ι : Type u_3} {σ : Type u_4} [CommRing R] [CommRing S] [Algebra R S] {P : Presentation R S ι σ} (R₀ : Type u_5) [CommRing R₀] [Algebra R₀ R] [Algebra R₀ S] [IsScalarTower R₀ R S] [P.HasCoeffs R₀] (r : σ) : (MvPolynomial.map (algebraMap R₀ R)) (relationOfHasCoeffs R₀ r) = P.relation r

@[simp]

theorem Algebra.Presentation.aeval_val_relationOfHasCoeffs {R : Type u_1} {S : Type u_2} {ι : Type u_3} {σ : Type u_4} [CommRing R] [CommRing S] [Algebra R S] {P : Presentation R S ι σ} (R₀ : Type u_5) [CommRing R₀] [Algebra R₀ R] [Algebra R₀ S] [IsScalarTower R₀ R S] [P.HasCoeffs R₀] (r : σ) : (MvPolynomial.aeval P.val) (relationOfHasCoeffs R₀ r) = 0

@[simp]

theorem Algebra.Presentation.algebraTensorAlgEquiv_symm_relation {R : Type u_1} {S : Type u_2} {ι : Type u_3} {σ : Type u_4} [CommRing R] [CommRing S] [Algebra R S] {P : Presentation R S ι σ} (R₀ : Type u_5) [CommRing R₀] [Algebra R₀ R] [Algebra R₀ S] [IsScalarTower R₀ R S] [P.HasCoeffs R₀] (r : σ) : (MvPolynomial.algebraTensorAlgEquiv R₀ R).symm (P.relation r) = 1 ⊗ₜ[R₀] relationOfHasCoeffs R₀ r

@[reducible, inline]

abbrev Algebra.Presentation.ModelOfHasCoeffs {R : Type u_1} {S : Type u_2} {ι : Type u_3} {σ : Type u_4} [CommRing R] [CommRing S] [Algebra R S] {P : Presentation R S ι σ} (R₀ : Type u_5) [CommRing R₀] [Algebra R₀ R] [Algebra R₀ S] [IsScalarTower R₀ R S] [P.HasCoeffs R₀] : Type (max (max u_3 u_5) u_5 u_3)

The model of S over a R₀ that contains the coefficients of P is R₀[X] quotiented by the same relations.

Equations

• Algebra.Presentation.ModelOfHasCoeffs R₀ = (MvPolynomial ι R₀ ⧸ Ideal.span (Set.range (Algebra.Presentation.relationOfHasCoeffs R₀)))

instance Algebra.Presentation.instFinitePresentationModelOfHasCoeffsOfFinite {R : Type u_1} {S : Type u_2} {ι : Type u_3} {σ : Type u_4} [CommRing R] [CommRing S] [Algebra R S] {P : Presentation R S ι σ} (R₀ : Type u_5) [CommRing R₀] [Algebra R₀ R] [Algebra R₀ S] [IsScalarTower R₀ R S] [P.HasCoeffs R₀] [Finite ι] [Finite σ] : FinitePresentation R₀ (ModelOfHasCoeffs R₀)

noncomputable def Algebra.Presentation.tensorModelOfHasCoeffsHom {R : Type u_1} {S : Type u_2} {ι : Type u_3} {σ : Type u_4} [CommRing R] [CommRing S] [Algebra R S] (P : Presentation R S ι σ) (R₀ : Type u_5) [CommRing R₀] [Algebra R₀ R] [Algebra R₀ S] [IsScalarTower R₀ R S] [P.HasCoeffs R₀] : TensorProduct R₀ R (ModelOfHasCoeffs R₀) →ₐ[R] S

(Implementation detail): The underlying AlgHom of tensorModelOfHasCoeffsEquiv.

Equations

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

@[simp]

theorem Algebra.Presentation.tensorModelOfHasCoeffsHom_tmul {R : Type u_1} {S : Type u_2} {ι : Type u_3} {σ : Type u_4} [CommRing R] [CommRing S] [Algebra R S] {P : Presentation R S ι σ} (R₀ : Type u_5) [CommRing R₀] [Algebra R₀ R] [Algebra R₀ S] [IsScalarTower R₀ R S] [P.HasCoeffs R₀] (x : R) (y : MvPolynomial ι R₀) : (P.tensorModelOfHasCoeffsHom R₀) (x ⊗ₜ[R₀] (Ideal.Quotient.mk (Ideal.span (Set.range (relationOfHasCoeffs R₀)))) y) = (algebraMap R S) x * (MvPolynomial.aeval P.val) y

noncomputable def Algebra.Presentation.tensorModelOfHasCoeffsInv {R : Type u_1} {S : Type u_2} {ι : Type u_3} {σ : Type u_4} [CommRing R] [CommRing S] [Algebra R S] (P : Presentation R S ι σ) (R₀ : Type u_5) [CommRing R₀] [Algebra R₀ R] [Algebra R₀ S] [IsScalarTower R₀ R S] [P.HasCoeffs R₀] : S →ₐ[R] TensorProduct R₀ R (ModelOfHasCoeffs R₀)

(Implementation detail): The inverse of tensorModelOfHasCoeffsHom.

Equations

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

@[simp]

theorem Algebra.Presentation.tensorModelOfHasCoeffsInv_aeval_val {R : Type u_1} {S : Type u_2} {ι : Type u_3} {σ : Type u_4} [CommRing R] [CommRing S] [Algebra R S] {P : Presentation R S ι σ} (R₀ : Type u_5) [CommRing R₀] [Algebra R₀ R] [Algebra R₀ S] [IsScalarTower R₀ R S] [P.HasCoeffs R₀] (x : MvPolynomial ι R₀) : (P.tensorModelOfHasCoeffsInv R₀) ((MvPolynomial.aeval P.val) x) = 1 ⊗ₜ[R₀] (Ideal.Quotient.mk (Ideal.span (Set.range (relationOfHasCoeffs R₀)))) x

noncomputable def Algebra.Presentation.tensorModelOfHasCoeffsEquiv {R : Type u_1} {S : Type u_2} {ι : Type u_3} {σ : Type u_4} [CommRing R] [CommRing S] [Algebra R S] {P : Presentation R S ι σ} (R₀ : Type u_5) [CommRing R₀] [Algebra R₀ R] [Algebra R₀ S] [IsScalarTower R₀ R S] [P.HasCoeffs R₀] : TensorProduct R₀ R (ModelOfHasCoeffs R₀) ≃ₐ[R] S

The natural isomorphism R ⊗[R₀] S₀ ≃ₐ[R] S.

Equations

• Algebra.Presentation.tensorModelOfHasCoeffsEquiv R₀ = AlgEquiv.ofAlgHom (P.tensorModelOfHasCoeffsHom R₀) (P.tensorModelOfHasCoeffsInv R₀) ⋯ ⋯

@[simp]

theorem Algebra.Presentation.tensorModelOfHasCoeffsEquiv_tmul {R : Type u_1} {S : Type u_2} {ι : Type u_3} {σ : Type u_4} [CommRing R] [CommRing S] [Algebra R S] {P : Presentation R S ι σ} (R₀ : Type u_5) [CommRing R₀] [Algebra R₀ R] [Algebra R₀ S] [IsScalarTower R₀ R S] [P.HasCoeffs R₀] (x : R) (y : MvPolynomial ι R₀) : (tensorModelOfHasCoeffsEquiv R₀) (x ⊗ₜ[R₀] (Ideal.Quotient.mk (Ideal.span (Set.range (relationOfHasCoeffs R₀)))) y) = (algebraMap R S) x * (MvPolynomial.aeval P.val) y

@[simp]

theorem Algebra.Presentation.tensorModelOfHasCoeffsEquiv_symm_tmul {R : Type u_1} {S : Type u_2} {ι : Type u_3} {σ : Type u_4} [CommRing R] [CommRing S] [Algebra R S] {P : Presentation R S ι σ} (R₀ : Type u_5) [CommRing R₀] [Algebra R₀ R] [Algebra R₀ S] [IsScalarTower R₀ R S] [P.HasCoeffs R₀] (x : MvPolynomial ι R₀) : (tensorModelOfHasCoeffsEquiv R₀).symm ((MvPolynomial.aeval P.val) x) = 1 ⊗ₜ[R₀] (Ideal.Quotient.mk (Ideal.span (Set.range (relationOfHasCoeffs R₀)))) x