The fibres at units of a filtered coefficient algebra

For an increasing multiplicative family M of submodules of an associative algebra B and a unit a of the base ring, evaluation at a on coeffSubalgebra M has kernel generated by X - a. If the filtration is exhaustive, the quotient is therefore B, and so is the tensor base change along evaluation R[X] → R at a. The algebra B need not be commutative.

This is the specialization at a unit of the Rees construction; see J. Dixmier, Enveloping Algebras, for filtered enveloping algebras and their Rees algebras.

instance TauCeti.coeffSubalgebra.span_X_sub_algebraMap_isTwoSided {R : Type u_1} {B : Type u_2} [CommRing R] [Ring B] [Algebra R B] (M : ℕ → Submodule R B) [SetLike.GradedMonoid M] (h1 : 1 ∈ M 1) (a : R) : (Ideal.span {X M h1 - (algebraMap R ↥(coeffSubalgebra M)) a}).IsTwoSided

The ideal generated by the central element X - a is two-sided.

instance TauCeti.coeffSubalgebra.span_X_sub_one_isTwoSided {R : Type u_1} {B : Type u_2} [CommRing R] [Ring B] [Algebra R B] (M : ℕ → Submodule R B) [SetLike.GradedMonoid M] (h1 : 1 ∈ M 1) : (Ideal.span {X M h1 - 1}).IsTwoSided

The ideal generated by the central element X - 1 is two-sided.

theorem TauCeti.coeffSubalgebra.ker_eval {R : Type u_1} {B : Type u_2} [CommRing R] [Ring B] [Algebra R B] (M : ℕ → Submodule R B) [SetLike.GradedMonoid M] (h1 : 1 ∈ M 1) (hM : Monotone M) {a : R} (ha : IsUnit a) : RingHom.ker (eval M a) = Ideal.span {X M h1 - (algebraMap R ↥(coeffSubalgebra M)) a}

Evaluation at a unit a has kernel exactly the principal ideal generated by X - a.

theorem TauCeti.coeffSubalgebra.eval_surjective {R : Type u_1} {B : Type u_2} [CommRing R] [Ring B] [Algebra R B] (M : ℕ → Submodule R B) [SetLike.GradedMonoid M] (hex : ⨆ (n : ℕ), M n = ⊤) {a : R} (ha : IsUnit a) : Function.Surjective ⇑(eval M a)

Evaluation at a unit is surjective when the filtration is exhaustive.

noncomputable def TauCeti.coeffSubalgebra.quotientSpanXSubAlgebraMapEquiv {R : Type u_1} {B : Type u_2} [CommRing R] [Ring B] [Algebra R B] (M : ℕ → Submodule R B) [SetLike.GradedMonoid M] (h1 : 1 ∈ M 1) (hM : Monotone M) (hex : ⨆ (n : ℕ), M n = ⊤) {a : R} (ha : IsUnit a) : (↥(coeffSubalgebra M) ⧸ Ideal.span {X M h1 - (algebraMap R ↥(coeffSubalgebra M)) a}) ≃ₐ[R] B

The quotient of coeffSubalgebra M by X - a, for a unit a, is B when the filtration is exhaustive and increasing.

@[simp]

theorem TauCeti.coeffSubalgebra.quotientSpanXSubAlgebraMapEquiv_mk {R : Type u_1} {B : Type u_2} [CommRing R] [Ring B] [Algebra R B] (M : ℕ → Submodule R B) [SetLike.GradedMonoid M] (h1 : 1 ∈ M 1) (hM : Monotone M) (hex : ⨆ (n : ℕ), M n = ⊤) {a : R} (ha : IsUnit a) (p : ↥(coeffSubalgebra M)) : (quotientSpanXSubAlgebraMapEquiv M h1 hM hex ha) ((Ideal.Quotient.mk (Ideal.span {X M h1 - (algebraMap R ↥(coeffSubalgebra M)) a})) p) = (eval M a) p

The quotient comparison is evaluation at a on representatives.

@[simp]

theorem TauCeti.coeffSubalgebra.quotientSpanXSubAlgebraMapEquiv_symm_eval {R : Type u_1} {B : Type u_2} [CommRing R] [Ring B] [Algebra R B] (M : ℕ → Submodule R B) [SetLike.GradedMonoid M] (h1 : 1 ∈ M 1) (hM : Monotone M) (hex : ⨆ (n : ℕ), M n = ⊤) {a : R} (ha : IsUnit a) (p : ↥(coeffSubalgebra M)) : (quotientSpanXSubAlgebraMapEquiv M h1 hM hex ha).symm ((eval M a) p) = (Ideal.Quotient.mk (Ideal.span {X M h1 - (algebraMap R ↥(coeffSubalgebra M)) a})) p

The inverse quotient comparison sends the value at a of a representative to its class.

noncomputable def TauCeti.coeffSubalgebra.baseChangeEvalEquiv {R : Type u_1} {B : Type u_2} [CommRing R] [Ring B] [Algebra R B] (M : ℕ → Submodule R B) [SetLike.GradedMonoid M] (h1 : 1 ∈ M 1) (hM : Monotone M) (hex : ⨆ (n : ℕ), M n = ⊤) {a : R} (ha : IsUnit a) : TensorProduct (Polynomial R) R ↥(coeffSubalgebra M) ≃ₐ[R] B

Base change along evaluation R[X] → R at a unit a recovers B. The parameter action on the left tensor factor is evaluation at a.

@[simp]

theorem TauCeti.coeffSubalgebra.baseChangeEvalEquiv_tmul {R : Type u_1} {B : Type u_2} [CommRing R] [Ring B] [Algebra R B] (M : ℕ → Submodule R B) [SetLike.GradedMonoid M] (h1 : 1 ∈ M 1) (hM : Monotone M) (hex : ⨆ (n : ℕ), M n = ⊤) {a : R} (ha : IsUnit a) (r : R) (p : ↥(coeffSubalgebra M)) : (baseChangeEvalEquiv M h1 hM hex ha) (r ⊗ₜ[Polynomial R] p) = r • (eval M a) p

The base-change comparison sends a pure tensor to scalar multiplication of its value at a.

@[simp]

theorem TauCeti.coeffSubalgebra.baseChangeEvalEquiv_symm_eval {R : Type u_1} {B : Type u_2} [CommRing R] [Ring B] [Algebra R B] (M : ℕ → Submodule R B) [SetLike.GradedMonoid M] (h1 : 1 ∈ M 1) (hM : Monotone M) (hex : ⨆ (n : ℕ), M n = ⊤) {a : R} (ha : IsUnit a) (p : ↥(coeffSubalgebra M)) : (baseChangeEvalEquiv M h1 hM hex ha).symm ((eval M a) p) = 1 ⊗ₜ[Polynomial R] p

The inverse base-change comparison sends the value at a of p to 1 ⊗ p.