Congruence subalgebras of a product ring

For a commutative ring R and s : R, the subalgebra productSubalgebra s of R × R consists of the pairs whose difference is divisible by s. It is generated by (s, 0) and is the image of QuadraticAlgebra R 0 s under evaluation at the roots s and 0. This evaluation is injective when s is left-regular, giving the basis (1, 1), (s, 0). The subalgebra is a finite R-module; over ℤ, Mathlib's PID instance supplies freeness.

The conductor of (s, 0) in R × R is the product of the two ideals generated by s. This also characterizes the ideals of the full product ring that lie in the congruence subalgebra. Units are exactly the contained pairs of units. Over ℤ there are four when s divides 2 and two otherwise; modulus 1 gives the full product ring.

def TauCeti.QuadraticOrder.productSubalgebra {R : Type u_1} [CommRing R] (s : R) : Subalgebra R (R × R)

The product subalgebra with coordinates congruent modulo s.

@[simp]

theorem TauCeti.QuadraticOrder.mem_productSubalgebra {R : Type u_1} [CommRing R] (s : R) (z : R × R) : z ∈ productSubalgebra s ↔ s ∣ z.1 - z.2

Membership is divisibility of the difference of the two coordinates.

def TauCeti.QuadraticOrder.productLift {R : Type u_1} [CommRing R] (s : R) : QuadraticAlgebra R 0 s →ₐ[R] R × R

Evaluation of the quadratic model at the roots s and 0.

@[simp]

theorem TauCeti.QuadraticOrder.productLift_apply {R : Type u_1} [CommRing R] (s : R) (z : QuadraticAlgebra R 0 s) : (productLift s) z = (z.re + s * z.im, z.re)

The evaluation map in coordinates.

theorem TauCeti.QuadraticOrder.range_productLift {R : Type u_1} [CommRing R] (s : R) : (productLift s).range = productSubalgebra s

The quadratic model maps onto the congruence subalgebra.

theorem TauCeti.QuadraticOrder.productSubalgebra_eq_adjoin {R : Type u_1} [CommRing R] (s : R) : productSubalgebra s = R[(s, 0)]

The congruence subalgebra is generated by (s, 0).

theorem TauCeti.QuadraticOrder.productLift_injective {R : Type u_1} [CommRing R] (s : R) (hs : IsLeftRegular s) : Function.Injective ⇑(productLift s)

A left-regular congruence modulus makes the evaluation map injective.

instance TauCeti.QuadraticOrder.instFiniteProductSubalgebra {R : Type u_1} [CommRing R] (s : R) : Module.Finite R ↥(productSubalgebra s)

The congruence subalgebra is a finite module.

noncomputable def TauCeti.QuadraticOrder.equivProductSubalgebra {R : Type u_1} [CommRing R] (s : R) (hs : IsLeftRegular s) : QuadraticAlgebra R 0 s ≃ₐ[R] ↥(productSubalgebra s)

The quadratic model is isomorphic to the congruence product subalgebra.

@[simp]

theorem TauCeti.QuadraticOrder.coe_equivProductSubalgebra_apply {R : Type u_1} [CommRing R] (s : R) (hs : IsLeftRegular s) (z : QuadraticAlgebra R 0 s) : ↑((equivProductSubalgebra s hs) z) = (productLift s) z

The equivalence retains the evaluated pair.

noncomputable def TauCeti.QuadraticOrder.productBasis {R : Type u_1} [CommRing R] (s : R) (hs : IsLeftRegular s) : Module.Basis (Fin 2) R ↥(productSubalgebra s)

The basis consists of the diagonal unit and (s, 0).

@[simp]

theorem TauCeti.QuadraticOrder.coe_productBasis_zero {R : Type u_1} [CommRing R] (s : R) (hs : IsLeftRegular s) : ↑((productBasis s hs) 0) = (1, 1)

The first basis vector is the diagonal unit.

@[simp]

theorem TauCeti.QuadraticOrder.coe_productBasis_one {R : Type u_1} [CommRing R] (s : R) (hs : IsLeftRegular s) : ↑((productBasis s hs) 1) = (s, 0)

The second basis vector is (s, 0).

theorem TauCeti.QuadraticOrder.conductor_eq_prod_span {R : Type u_1} [CommRing R] (s : R) : conductor R (s, 0) = (Ideal.span {s}).prod (Ideal.span {s})

The conductor is the product of the two principal ideals generated by s.

@[simp]

theorem TauCeti.QuadraticOrder.productSubalgebra_one {R : Type u_1} [CommRing R] : productSubalgebra 1 = ⊤

The full product algebra is the congruence subalgebra of modulus one.

@[simp]

theorem TauCeti.QuadraticOrder.isUnit_productSubalgebra_iff {R : Type u_1} [CommRing R] (s : R) (z : ↥(productSubalgebra s)) : IsUnit z ↔ IsUnit (↑z).1 ∧ IsUnit (↑z).2

Units of the congruence subalgebra are exactly the pairs of units it contains.

theorem TauCeti.QuadraticOrder.ideal_le_productSubalgebra_iff {R : Type u_1} [CommRing R] (s : R) (I : Ideal (R × R)) : (∀ z ∈ I, z ∈ productSubalgebra s) ↔ I ≤ (Ideal.span {s}).prod (Ideal.span {s})

An ideal of the full product ring lies in the congruence subalgebra exactly when both its coordinates are divisible by the modulus.

theorem TauCeti.QuadraticOrder.units_eq_one_or_neg_one_of_not_dvd_two (s : ℤ) (hs : ¬s ∣ 2) (u : (↥(productSubalgebra s))ˣ) : u = 1 ∨ u = -1

Unless the modulus divides two, every unit is the diagonal unit or its negative.

theorem TauCeti.QuadraticOrder.card_units_productSubalgebra (s : ℤ) : Nat.card (↥(productSubalgebra s))ˣ = if s ∣ 2 then 4 else 2

An integer congruence subalgebra has four units when its modulus divides two, and two otherwise.