Documentation

Mathlib.RingTheory.FreeCommRing

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 #

Main results #

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

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) :

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
def FreeCommRing.of {α : Type u} (x : α) :

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

Equations
@[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.induction_on {α : Type u} {motive : FreeCommRing αProp} (z : FreeCommRing α) (neg_one : motive (-1)) (of : ∀ (b : α), motive (of b)) (add : ∀ (x y : FreeCommRing α), motive xmotive ymotive (x + y)) (mul : ∀ (x y : FreeCommRing α), motive xmotive ymotive (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
@[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 : αβ) :

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

Equations
@[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 α) :

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

Equations
theorem FreeCommRing.isSupported_upwards {α : Type u} {x : FreeCommRing α} {s t : Set α} (hs : x.IsSupported s) (hst : s 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) :
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_int {α : Type u} {i : } {s : Set α} :
(↑i).IsSupported s
def FreeCommRing.restriction {α : Type u} (s : Set α) [DecidablePred fun (x : α) => x s] :

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

Equations
@[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) :
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

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

Equations

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

Equations
@[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 : α) :
@[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_eq (α : Type u) :
castFreeCommRing = Functor.map fun (l : List α) => l

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
Equations

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

Equations