# 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 #

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

FreeCommRing α is the free commutative ring on the type α.

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

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

Instances For
theorem FreeCommRing.of_injective {α : Type u} :
Function.Injective FreeCommRing.of
theorem FreeCommRing.of_cons {α : Type u} (a : α) (m : ) :
theorem FreeCommRing.induction_on {α : Type u} {C : } (z : ) (hn1 : C (-1)) (hb : (b : α) → C ()) (ha : (x y : ) → C xC yC (x + y)) (hm : (x y : ) → C xC yC (x * y)) :
C z
def FreeCommRing.lift {α : Type u} {R : Type v} [] :
(αR) ()

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

Instances For
@[simp]
theorem FreeCommRing.lift_of {α : Type u} {R : Type v} [] (f : αR) (x : α) :
↑(FreeCommRing.lift f) () = f x
@[simp]
theorem FreeCommRing.lift_comp_of {α : Type u} {R : Type v} [] (f : ) :
FreeCommRing.lift (f FreeCommRing.of) = f
theorem FreeCommRing.hom_ext {α : Type u} {R : Type v} [] ⦃f : ⦃g : (h : ∀ (x : α), f () = g ()) :
f = g
def FreeCommRing.map {α : Type u} {β : Type v} (f : αβ) :

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

Instances For
@[simp]
theorem FreeCommRing.map_of {α : Type u} {β : Type v} (f : αβ) (x : α) :
↑() () = FreeCommRing.of (f x)
def FreeCommRing.IsSupported {α : Type u} (x : ) (s : Set α) :

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

Instances For
theorem FreeCommRing.isSupported_upwards {α : Type u} {x : } {s : Set α} {t : Set α} (hs : ) (hst : s t) :
theorem FreeCommRing.isSupported_add {α : Type u} {x : } {y : } {s : Set α} (hxs : ) (hys : ) :
theorem FreeCommRing.isSupported_neg {α : Type u} {x : } {s : Set α} (hxs : ) :
theorem FreeCommRing.isSupported_sub {α : Type u} {x : } {y : } {s : Set α} (hxs : ) (hys : ) :
theorem FreeCommRing.isSupported_mul {α : Type u} {x : } {y : } {s : Set α} (hxs : ) (hys : ) :
theorem FreeCommRing.isSupported_zero {α : Type u} {s : Set α} :
theorem FreeCommRing.isSupported_one {α : Type u} {s : Set α} :
theorem FreeCommRing.isSupported_int {α : Type u} {i : } {s : Set α} :
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.

Instances For
@[simp]
theorem FreeCommRing.restriction_of {α : Type u} (s : Set α) [DecidablePred fun x => x s] (p : α) :
↑() () = if H : p s then FreeCommRing.of { val := p, property := H } else 0
theorem FreeCommRing.isSupported_of {α : Type u} {p : α} {s : Set α} :
p s
theorem FreeCommRing.map_subtype_val_restriction {α : Type u} {x : } (s : Set α) [DecidablePred fun x => x s] (hxs : ) :
↑(FreeCommRing.map Subtype.val) (↑() x) = x
theorem FreeCommRing.exists_finite_support {α : Type u} (x : ) :
s,
theorem FreeCommRing.exists_finset_support {α : Type u} (x : ) :
s,
def FreeRing.toFreeCommRing {α : Type u_1} :

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

Instances For
def FreeRing.castFreeCommRing {α : Type u_1} :

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

Instances For
def FreeRing.coeRingHom (α : Type u) :

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

Instances For
@[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 : ) :
↑(-x) = -x
@[simp]
theorem FreeRing.coe_add {α : Type u} (x : ) (y : ) :
↑(x + y) = x + y
@[simp]
theorem FreeRing.coe_sub {α : Type u} (x : ) (y : ) :
↑(x - y) = x - y
@[simp]
theorem FreeRing.coe_mul {α : Type u} (x : ) (y : ) :
↑(x * y) = x * y
theorem FreeRing.coe_surjective (α : Type u) :
Function.Surjective FreeRing.castFreeCommRing
theorem FreeRing.coe_eq (α : Type u) :
FreeRing.castFreeCommRing = Functor.map fun l => 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.

Instances For
instance FreeRing.instCommRing (α : Type u) [] :

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

Instances For

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

Instances For

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

Instances For

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

Instances For

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

Instances For