theorem finrank_quotient_polynomial_eq_natDegree (k : Type u_1) [Field k] (f : Polynomial k) : Module.finrank k (Polynomial k ⧸ Ideal.span {f}) = f.natDegree

The k-dimension of k[X] / ⟨f⟩ equals the degree of f.

theorem finrank_quotient_X (k : Type u_1) [Field k] : Module.finrank k (Polynomial k ⧸ Ideal.span {Polynomial.X}) = 1

The quotient k[X] / ⟨X⟩ has k-dimension 1.

theorem finrank_quotient_X_sub_C (k : Type u_1) [Field k] (c : k) : Module.finrank k (Polynomial k ⧸ Ideal.span {Polynomial.X - Polynomial.C c}) = 1

The quotient k[X] / ⟨X - c⟩ has k-dimension 1 for any scalar c.

theorem line_line_intersection_dim (k : Type u_1) [Field k] : Module.finrank k (Polynomial (Polynomial k) ⧸ Ideal.span {Polynomial.C Polynomial.X, Polynomial.X}) = 1

Two transverse lines Y = 0 and X = 0 in the affine plane meet in a single point: the quotient k[X][Y] / ⟨C X, X⟩ has k-dimension 1.

noncomputable def lineConicQuotientEquiv (k : Type u_1) [Field k] : (Polynomial (Polynomial k) ⧸ Ideal.span {Polynomial.C (Polynomial.X ^ 2 + 1), Polynomial.X}) ≃ₐ[Polynomial k] Polynomial k ⧸ Ideal.span {Polynomial.X ^ 2 + 1}

Algebra isomorphism relating the bivariate quotient k[X][Y] / ⟨C(X² + 1), Y⟩ to the univariate quotient k[X] / ⟨X² + 1⟩, used to compute the line/conic intersection dimension.

theorem line_conic_intersection_dim (k : Type u_1) [Field k] : Module.finrank k (Polynomial (Polynomial k) ⧸ Ideal.span {Polynomial.C (Polynomial.X ^ 2 + 1), Polynomial.X}) = 2

A line meets a conic (the conic X² + 1 = 0) in 2 points: the corresponding bivariate quotient has k-dimension 2.

theorem finrank_quotient_coprime_product (k : Type u_1) [Field k] (f g : Polynomial k) (hf : f ≠ 0) (hg : g ≠ 0) : Module.finrank k (Polynomial k ⧸ Ideal.span {f * g}) = f.natDegree + g.natDegree

The k-dimension of k[X] / ⟨f · g⟩ is the sum of the degrees of f and g.

noncomputable def coprime_polynomial_CRT (k : Type u_1) [Field k] (f g : Polynomial k) (hfg : IsCoprime f g) : Polynomial k ⧸ Ideal.span {f * g} ≃+* (Polynomial k ⧸ Ideal.span {f}) × Polynomial k ⧸ Ideal.span {g}

Chinese remainder theorem for coprime polynomials: k[X] / ⟨f g⟩ ≅ k[X]/⟨f⟩ × k[X]/⟨g⟩.

theorem finrank_quotient_algebraMap (k : Type u_1) [Field k] {S : Type u_2} [CommRing S] [IsDomain S] {ι : Type u_3} [Fintype ι] [Algebra (Polynomial k) S] [Algebra k S] [IsScalarTower k (Polynomial k) S] (b : Module.Basis ι (Polynomial k) S) (p : Polynomial k) (hp : (algebraMap (Polynomial k) S) p ≠ 0) : Module.finrank k (S ⧸ Ideal.span {(algebraMap (Polynomial k) S) p}) = Fintype.card ι * p.natDegree

Norm-based degree formula: for a free k[X]-algebra S with basis indexed by ι, dim_k (S / ⟨algebraMap p⟩) = |ι| · deg(p).

theorem principal_divisor_degree_one (k : Type u_1) [Field k] {S : Type u_2} [CommRing S] [IsDomain S] {ι : Type u_3} [Fintype ι] [Algebra (Polynomial k) S] [Algebra k S] [IsScalarTower k (Polynomial k) S] (b : Module.Basis ι (Polynomial k) S) (c : k) : Module.finrank k (S ⧸ Ideal.span {(algebraMap (Polynomial k) S) (Polynomial.X - Polynomial.C c)}) = Fintype.card ι

A degree-one principal divisor X - c cuts out a fibre of length |ι| in any free k[X]-algebra S with basis indexed by ι.

theorem quotient_polynomial_module_finite (R : Type u_1) [CommRing R] (g : Polynomial R) (hg : g.Monic) : Module.Finite R (Polynomial R ⧸ Ideal.span {g})

For a monic polynomial g ∈ R[X], the quotient R[X] / ⟨g⟩ is a finitely generated R-module.

noncomputable def quotient_polynomial_powerBasis (R : Type u_1) [CommRing R] (g : Polynomial R) (hg : g.Monic) : PowerBasis R (AdjoinRoot g)

The canonical power basis 1, X, X², …, X^{deg g - 1} of R[X] / ⟨g⟩ over R when g is monic.

theorem bezout_algebraic (k : Type u_1) [Field k] (g : Polynomial (Polynomial k)) (hg : g.Monic) [IsDomain (AdjoinRoot g)] (f : Polynomial k) (hf : (algebraMap (Polynomial k) (AdjoinRoot g)) f ≠ 0) : Module.finrank k (AdjoinRoot g ⧸ Ideal.span {(algebraMap (Polynomial k) (AdjoinRoot g)) f}) = g.natDegree * f.natDegree

Algebraic form of Bezout: dim_k (AdjoinRoot g / ⟨f⟩) = deg(g) · deg(f) when g is monic and the image of f is nonzero.

noncomputable def bivariate_quotient_equiv (k : Type u_1) [Field k] (f g : Polynomial (Polynomial k)) : (Polynomial (Polynomial k) ⧸ Ideal.span {g} ⊔ Ideal.span {f}) ≃ₐ[k] AdjoinRoot g ⧸ Ideal.span {(AdjoinRoot.mk g) f}

Algebra isomorphism k[X][Y] / (⟨g⟩ + ⟨f⟩) ≅ AdjoinRoot g / ⟨[f]⟩ obtained via the quotient-of-quotients construction.

theorem bezout_bivariate_norm (k : Type u_1) [Field k] (g : Polynomial (Polynomial k)) (hg : g.Monic) [IsDomain (AdjoinRoot g)] (f : Polynomial (Polynomial k)) (hf : (AdjoinRoot.mk g) f ≠ 0) : Module.finrank k (Polynomial (Polynomial k) ⧸ Ideal.span {g} ⊔ Ideal.span {f}) = ((Algebra.norm (Polynomial k)) ((AdjoinRoot.mk g) f)).natDegree

Norm form of bivariate Bezout: the k-dimension of k[X][Y] / (⟨g⟩ + ⟨f⟩) equals the degree of Norm_{k[X]} ([f]).

theorem bezout_bivariate_base (k : Type u_1) [Field k] (g : Polynomial (Polynomial k)) (hg : g.Monic) [IsDomain (AdjoinRoot g)] (p : Polynomial k) (hp : (algebraMap (Polynomial k) (AdjoinRoot g)) p ≠ 0) : Module.finrank k (Polynomial (Polynomial k) ⧸ Ideal.span {g} ⊔ Ideal.span {Polynomial.C p}) = g.natDegree * p.natDegree

Bivariate Bezout for constant C p: dim_k (k[X][Y] / (⟨g⟩ + ⟨C p⟩)) = deg(g) · deg(p).

theorem bezout_algebraic_irreducible (k : Type u_1) [Field k] (g : Polynomial (Polynomial k)) (hg : g.Monic) (hirr : Irreducible g) (f : Polynomial k) (hf : (algebraMap (Polynomial k) (AdjoinRoot g)) f ≠ 0) : Module.finrank k (AdjoinRoot g ⧸ Ideal.span {(algebraMap (Polynomial k) (AdjoinRoot g)) f}) = g.natDegree * f.natDegree

Variant of bezout_algebraic that derives the integral-domain hypothesis from irreducibility of g.

theorem ideal_span_pair_eq_sup {R : Type u_1} [Semiring R] (a b : R) : Ideal.span {a, b} = Ideal.span {a} ⊔ Ideal.span {b}

The ideal spanned by a pair {a, b} equals the supremum of the singleton ideals.

theorem bezout_bivariate_product (k : Type u_1) [Field k] (g : Polynomial (Polynomial k)) (hg : g.Monic) (hirr : Irreducible g) (p : Polynomial k) (hp : (algebraMap (Polynomial k) (AdjoinRoot g)) p ≠ 0) : Module.finrank k (Polynomial (Polynomial k) ⧸ Ideal.span {g, Polynomial.C p}) = g.natDegree * p.natDegree

Bivariate Bezout, span-of-pair form: dim_k (k[X][Y] / ⟨g, C p⟩) = deg(g) · deg(p).

theorem bezout_bivariate_norm_irreducible (k : Type u_1) [Field k] (g : Polynomial (Polynomial k)) (hg : g.Monic) (hirr : Irreducible g) (f : Polynomial (Polynomial k)) (hf : (AdjoinRoot.mk g) f ≠ 0) : Module.finrank k (Polynomial (Polynomial k) ⧸ Ideal.span {g, f}) = ((Algebra.norm (Polynomial k)) ((AdjoinRoot.mk g) f)).natDegree

Norm form of bivariate Bezout for an irreducible monic g, using the span-of-pair presentation of the ideal.

theorem bezout_full (k : Type u_1) [Field k] (g : Polynomial (Polynomial k)) (hg : g.Monic) (hirr : Irreducible g) (f : Polynomial (Polynomial k)) (hf : (AdjoinRoot.mk g) f ≠ 0) {n : ℕ} (hnorm : ((Algebra.norm (Polynomial k)) ((AdjoinRoot.mk g) f)).natDegree = n) : Module.finrank k (Polynomial (Polynomial k) ⧸ Ideal.span {g, f}) = n

Full Bezout statement: given the degree of the norm of [f], the k-dimension of k[X][Y] / ⟨g, f⟩ is precisely that degree.

theorem bezout_norm_degree_base (k : Type u_1) [Field k] (g : Polynomial (Polynomial k)) (hg : g.Monic) (p : Polynomial k) : ((Algebra.norm (Polynomial k)) ((AdjoinRoot.mk g) (Polynomial.C p))).natDegree = g.natDegree * p.natDegree

Norm-degree base computation: deg (Norm_{k[X]} (C p mod g)) = deg(g) · deg(p).

theorem conic_conic_intersection_dim (k : Type u_1) [Field k] [IsDomain (AdjoinRoot (Polynomial.X ^ 2 + Polynomial.C 1))] (hne : (algebraMap (Polynomial k) (AdjoinRoot (Polynomial.X ^ 2 + Polynomial.C 1))) (Polynomial.X ^ 2 + 1) ≠ 0) : Module.finrank k (Polynomial (Polynomial k) ⧸ Ideal.span {Polynomial.X ^ 2 + Polynomial.C 1, Polynomial.C (Polynomial.X ^ 2 + 1)}) = 4

Two conics defined by Y² + 1 and X² + 1 meet in 2 · 2 = 4 points: the bivariate quotient has k-dimension 4.