Free commutative rings

The theory of the free commutative ring generated by a type α. It is isomorphic to the polynomial ring over ℤ with variables in α

Main definitions

• FreeCommRing α : the free commutative ring on a type α
• lift (f : α → R) : the ring hom FreeCommRing α →+* R induced by functoriality from f.
• map (f : α → β) : the ring hom FreeCommRing α →*+ FreeCommRing β induced by functoriality from f.

Main results

FreeCommRing has functorial properties (it is an adjoint to the forgetful functor). In this file we have:

• of : α → FreeCommRing α

• lift (f : α → R) : FreeCommRing α →+* R

• map (f : α → β) : FreeCommRing α →+* FreeCommRing β

• freeCommRingEquivMvPolynomialInt : FreeCommRing α ≃+* MvPolynomial α ℤ : FreeCommRing α is isomorphic to a polynomial ring.

Implementation notes

FreeCommRing α is implemented not using MvPolynomial but directly as the free abelian group on Multiset α, the type of monomials in this free commutative ring.

Tags

free commutative ring, free ring

def FreeCommRing (α : Type u) : Type u

If α is a type, then FreeCommRing α is the free commutative ring generated by α. This is a commutative ring equipped with a function FreeCommRing.of : α → FreeCommRing α which has the following universal property: if R is any commutative ring, and f : α → R is any function, then this function is the composite of FreeCommRing.of and a unique ring homomorphism FreeCommRing.lift f : FreeCommRing α →+* R.

A typical element of FreeCommRing α is a ℤ-linear combination of formal products of elements of α. For example if x and y are terms of type α then 3 * x * x * y - 2 * x * y + 1 is a "typical" element of FreeCommRing α. In particular if α is empty then FreeCommRing α is isomorphic to ℤ, and if α has one term t then FreeCommRing α is isomorphic to the polynomial ring ℤ[t]. One can think of FreeRing α as the free polynomial ring with coefficients in the integers and variables indexed by α.

Equations

• FreeCommRing α = FreeAbelianGroup (Multiplicative (Multiset α))

instance instCommRingFreeCommRing (α : Type u_1) : CommRing (FreeCommRing α)

Equations

• instCommRingFreeCommRing α = FreeAbelianGroup.instCommRingOfCommMonoid (Multiplicative (Multiset α))

instance instInhabitedFreeCommRing (α : Type u_1) : Inhabited (FreeCommRing α)

Equations

• instInhabitedFreeCommRing α = instInhabitedFreeAbelianGroup (Multiplicative (Multiset α))

def FreeCommRing.of {α : Type u} (x : α) : FreeCommRing α

The canonical map from α to the free commutative ring on α.

Equations

• FreeCommRing.of x = FreeAbelianGroup.of (Multiplicative.ofAdd {x})

theorem FreeCommRing.of_injective {α : Type u} : Function.Injective of

@[simp]

theorem FreeCommRing.of_ne_zero {α : Type u} (x : α) : of x ≠ 0

@[simp]

theorem FreeCommRing.zero_ne_of {α : Type u} (x : α) : 0 ≠ of x

@[simp]

theorem FreeCommRing.of_ne_one {α : Type u} (x : α) : of x ≠ 1

@[simp]

theorem FreeCommRing.one_ne_of {α : Type u} (x : α) : 1 ≠ of x

theorem FreeCommRing.of_cons {α : Type u} (a : α) (m : Multiset α) : FreeAbelianGroup.of (Multiplicative.ofAdd (a ::ₘ m)) = of a * FreeAbelianGroup.of (Multiplicative.ofAdd m)

theorem FreeCommRing.induction_on {α : Type u} {motive : FreeCommRing α → Prop} (z : FreeCommRing α) (neg_one : motive (-1)) (of : ∀ (b : α), motive (of b)) (add : ∀ (x y : FreeCommRing α), motive x → motive y → motive (x + y)) (mul : ∀ (x y : FreeCommRing α), motive x → motive y → motive (x * y)) : motive z

def FreeCommRing.lift {α : Type u} {R : Type v} [CommRing R] : (α → R) ≃ (FreeCommRing α →+* R)

Lift a map α → R to an additive group homomorphism FreeCommRing α → R.

Equations

• FreeCommRing.lift = FreeCommRing.liftToMultiset✝.trans FreeAbelianGroup.liftMonoid

@[simp]

theorem FreeCommRing.lift_of {α : Type u} {R : Type v} [CommRing R] (f : α → R) (x : α) : (lift f) (of x) = f x

@[simp]

theorem FreeCommRing.lift_comp_of {α : Type u} {R : Type v} [CommRing R] (f : FreeCommRing α →+* R) : lift (⇑f ∘ of) = f

theorem FreeCommRing.hom_ext {α : Type u} {R : Type v} [CommRing R] ⦃f g : FreeCommRing α →+* R⦄ (h : ∀ (x : α), f (of x) = g (of x)) : f = g

theorem FreeCommRing.hom_ext_iff {α : Type u} {R : Type v} [CommRing R] {f g : FreeCommRing α →+* R} : f = g ↔ ∀ (x : α), f (of x) = g (of x)

def FreeCommRing.map {α : Type u} {β : Type v} (f : α → β) : FreeCommRing α →+* FreeCommRing β

A map f : α → β produces a ring homomorphism FreeCommRing α →+* FreeCommRing β.

Equations

• FreeCommRing.map f = FreeCommRing.lift (FreeCommRing.of ∘ f)

@[simp]

theorem FreeCommRing.map_of {α : Type u} {β : Type v} (f : α → β) (x : α) : (map f) (of x) = of (f x)

def FreeCommRing.IsSupported {α : Type u} (x : FreeCommRing α) (s : Set α) : Prop

is_supported x s means that all monomials showing up in x have variables in s.

Equations

• x.IsSupported s = (x ∈ Subring.closure (FreeCommRing.of '' s))

theorem FreeCommRing.isSupported_upwards {α : Type u} {x : FreeCommRing α} {s t : Set α} (hs : x.IsSupported s) (hst : s ⊆ t) : x.IsSupported t

theorem FreeCommRing.isSupported_add {α : Type u} {x y : FreeCommRing α} {s : Set α} (hxs : x.IsSupported s) (hys : y.IsSupported s) : (x + y).IsSupported s

theorem FreeCommRing.isSupported_neg {α : Type u} {x : FreeCommRing α} {s : Set α} (hxs : x.IsSupported s) : (-x).IsSupported s

theorem FreeCommRing.isSupported_sub {α : Type u} {x y : FreeCommRing α} {s : Set α} (hxs : x.IsSupported s) (hys : y.IsSupported s) : (x - y).IsSupported s

theorem FreeCommRing.isSupported_mul {α : Type u} {x y : FreeCommRing α} {s : Set α} (hxs : x.IsSupported s) (hys : y.IsSupported s) : (x * y).IsSupported s

theorem FreeCommRing.isSupported_zero {α : Type u} {s : Set α} : IsSupported 0 s

theorem FreeCommRing.isSupported_one {α : Type u} {s : Set α} : IsSupported 1 s

theorem FreeCommRing.isSupported_int {α : Type u} {i : ℤ} {s : Set α} : (↑i).IsSupported s

def FreeCommRing.restriction {α : Type u} (s : Set α) [DecidablePred fun (x : α) => x ∈ s] : FreeCommRing α →+* FreeCommRing ↑s

The restriction map from FreeCommRing α to FreeCommRing s where s : Set α, defined by sending all variables not in s to zero.

Equations

• FreeCommRing.restriction s = FreeCommRing.lift fun (a : α) => if H : a ∈ s then FreeCommRing.of ⟨a, H⟩ else 0

@[simp]

theorem FreeCommRing.restriction_of {α : Type u} (s : Set α) [DecidablePred fun (x : α) => x ∈ s] (p : α) : (restriction s) (of p) = if H : p ∈ s then of ⟨p, H⟩ else 0

theorem FreeCommRing.isSupported_of {α : Type u} {p : α} {s : Set α} : (of p).IsSupported s ↔ p ∈ s

theorem FreeCommRing.map_subtype_val_restriction {α : Type u} {x : FreeCommRing α} (s : Set α) [DecidablePred fun (x : α) => x ∈ s] (hxs : x.IsSupported s) : (map Subtype.val) ((restriction s) x) = x

theorem FreeCommRing.exists_finite_support {α : Type u} (x : FreeCommRing α) : ∃ (s : Set α), s.Finite ∧ x.IsSupported s

theorem FreeCommRing.exists_finset_support {α : Type u} (x : FreeCommRing α) : ∃ (s : Finset α), x.IsSupported ↑s

def FreeRing.toFreeCommRing {α : Type u_1} : FreeRing α →+* FreeCommRing α

The canonical ring homomorphism from the free ring generated by α to the free commutative ring generated by α.

Equations

• FreeRing.toFreeCommRing = FreeRing.lift FreeCommRing.of

def FreeRing.castFreeCommRing {α : Type u_1} : FreeRing α → FreeCommRing α

The coercion defined by the canonical ring homomorphism from the free ring generated by α to the free commutative ring generated by α.

Equations

• FreeRing.castFreeCommRing = ⇑FreeRing.toFreeCommRing

instance FreeRing.FreeCommRing.instCoe (α : Type u) : Coe (FreeRing α) (FreeCommRing α)

Equations

• FreeRing.FreeCommRing.instCoe α = { coe := FreeRing.castFreeCommRing }

def FreeRing.coeRingHom (α : Type u) : FreeRing α →+* FreeCommRing α

The natural map FreeRing α → FreeCommRing α, as a RingHom.

Equations

• FreeRing.coeRingHom α = FreeRing.toFreeCommRing

@[simp]

theorem FreeRing.coe_zero (α : Type u) : ↑0 = 0

@[simp]

theorem FreeRing.coe_one (α : Type u) : ↑1 = 1

@[simp]

theorem FreeRing.coe_of {α : Type u} (a : α) : ↑(of a) = FreeCommRing.of a

@[simp]

theorem FreeRing.coe_neg {α : Type u} (x : FreeRing α) : ↑(-x) = -↑x

@[simp]

theorem FreeRing.coe_add {α : Type u} (x y : FreeRing α) : ↑(x + y) = ↑x + ↑y

@[simp]

theorem FreeRing.coe_sub {α : Type u} (x y : FreeRing α) : ↑(x - y) = ↑x - ↑y

@[simp]

theorem FreeRing.coe_mul {α : Type u} (x y : FreeRing α) : ↑(x * y) = ↑x * ↑y

theorem FreeRing.coe_surjective (α : Type u) : Function.Surjective castFreeCommRing

theorem FreeRing.coe_eq (α : Type u) : castFreeCommRing = Functor.map fun (l : List α) => ↑l

def FreeRing.subsingletonEquivFreeCommRing (α : Type u) [Subsingleton α] : FreeRing α ≃+* FreeCommRing α

If α has size at most 1 then the natural map from the free ring on α to the free commutative ring on α is an isomorphism of rings.

Equations

• FreeRing.subsingletonEquivFreeCommRing α = RingEquiv.ofBijective (FreeRing.coeRingHom α) ⋯

instance FreeRing.instCommRing (α : Type u) [Subsingleton α] : CommRing (FreeRing α)

Equations

• FreeRing.instCommRing α = { toRing := inferInstanceAs (Ring (FreeRing α)), mul_comm := ⋯ }

def freeCommRingEquivMvPolynomialInt (α : Type u) : FreeCommRing α ≃+* MvPolynomial α ℤ

The free commutative ring on α is isomorphic to the polynomial ring over ℤ with variables in α

Equations

• freeCommRingEquivMvPolynomialInt α = RingEquiv.ofRingHom (FreeCommRing.lift fun (a : α) => MvPolynomial.X a) (MvPolynomial.eval₂Hom (Int.castRingHom (FreeCommRing α)) FreeCommRing.of) ⋯ ⋯

def freeCommRingPEmptyEquivInt : FreeCommRing PEmpty.{u + 1} ≃+* ℤ

The free commutative ring on the empty type is isomorphic to ℤ.

Equations

• freeCommRingPEmptyEquivInt = (freeCommRingEquivMvPolynomialInt PEmpty.{?u.2 + 1}).trans (MvPolynomial.isEmptyRingEquiv ℤ PEmpty.{?u.2 + 1})

@[deprecated freeCommRingPEmptyEquivInt (since := "2026-02-08")]

def freeCommRingPemptyEquivInt : FreeCommRing PEmpty.{u + 1} ≃+* ℤ

Alias of freeCommRingPEmptyEquivInt.

---

The free commutative ring on the empty type is isomorphic to ℤ.

Equations

• freeCommRingPemptyEquivInt = freeCommRingPEmptyEquivInt

def freeCommRingPunitEquivPolynomialInt : FreeCommRing PUnit.{u + 1} ≃+* Polynomial ℤ

The free commutative ring on a type with one term is isomorphic to ℤ[X].

Equations

• freeCommRingPunitEquivPolynomialInt = (freeCommRingEquivMvPolynomialInt PUnit.{?u.2 + 1}).trans (MvPolynomial.pUnitAlgEquiv ℤ).toRingEquiv

def freeRingPEmptyEquivInt : FreeRing PEmpty.{u + 1} ≃+* ℤ

The free ring on the empty type is isomorphic to ℤ.

Equations

• freeRingPEmptyEquivInt = (FreeRing.subsingletonEquivFreeCommRing PEmpty.{?u.2 + 1}).trans freeCommRingPEmptyEquivInt

@[deprecated freeRingPEmptyEquivInt (since := "2026-02-08")]

def freeRingPemptyEquivInt : FreeRing PEmpty.{u + 1} ≃+* ℤ

Alias of freeRingPEmptyEquivInt.

---

The free ring on the empty type is isomorphic to ℤ.

Equations

• freeRingPemptyEquivInt = freeRingPEmptyEquivInt

def freeRingPunitEquivPolynomialInt : FreeRing PUnit.{u + 1} ≃+* Polynomial ℤ

The free ring on a type with one term is isomorphic to ℤ[X].

Equations

• freeRingPunitEquivPolynomialInt = (FreeRing.subsingletonEquivFreeCommRing PUnit.{?u.2 + 1}).trans freeCommRingPunitEquivPolynomialInt