mathlibdocumentation

ring_theory.free_comm_ring

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 #

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

Main results #

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

• of : α → free_comm_ring α

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

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

• free_comm_ring_equiv_mv_polynomial_int : free_comm_ring α ≃+* mv_polynomial α ℤ : free_comm_ring α is isomorphic to a polynomial ring.

Implementation notes #

free_comm_ring α is implemented not using mv_polynomial 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 free_comm_ring (α : Type u) :
Type u

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

Equations
Instances for free_comm_ring
@[protected, instance]
def free_comm_ring.comm_ring (α : Type u) :
@[protected, instance]
def free_comm_ring.inhabited (α : Type u) :
def free_comm_ring.of {α : Type u} (x : α) :

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

Equations
theorem free_comm_ring.of_injective {α : Type u} :
@[protected]
theorem free_comm_ring.induction_on {α : Type u} {C : → Prop} (z : free_comm_ring α) (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 free_comm_ring.lift {α : Type u} {R : Type v} [comm_ring R] :
(α → R) →+* R)

Lift a map α → R to a additive group homomorphism free_comm_ring α → R. For a version producing a bundled homomorphism, see lift_hom.

Equations
@[simp]
theorem free_comm_ring.lift_of {α : Type u} {R : Type v} [comm_ring R] (f : α → R) (x : α) :
= f x
@[simp]
theorem free_comm_ring.lift_comp_of {α : Type u} {R : Type v} [comm_ring R] (f : →+* R) :
@[ext]
theorem free_comm_ring.hom_ext {α : Type u} {R : Type v} [comm_ring R] ⦃f g : →+* R⦄ (h : ∀ (x : α), f = g ) :
f = g
def free_comm_ring.map {α : Type u} {β : Type v} (f : α → β) :

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

Equations
@[simp]
theorem free_comm_ring.map_of {α : Type u} {β : Type v} (f : α → β) (x : α) :
def free_comm_ring.is_supported {α : Type u} (x : free_comm_ring α) (s : set α) :
Prop

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

Equations
theorem free_comm_ring.is_supported_upwards {α : Type u} {x : free_comm_ring α} {s t : set α} (hs : x.is_supported s) (hst : s t) :
theorem free_comm_ring.is_supported_add {α : Type u} {x y : free_comm_ring α} {s : set α} (hxs : x.is_supported s) (hys : y.is_supported s) :
(x + y).is_supported s
theorem free_comm_ring.is_supported_neg {α : Type u} {x : free_comm_ring α} {s : set α} (hxs : x.is_supported s) :
theorem free_comm_ring.is_supported_sub {α : Type u} {x y : free_comm_ring α} {s : set α} (hxs : x.is_supported s) (hys : y.is_supported s) :
(x - y).is_supported s
theorem free_comm_ring.is_supported_mul {α : Type u} {x y : free_comm_ring α} {s : set α} (hxs : x.is_supported s) (hys : y.is_supported s) :
(x * y).is_supported s
theorem free_comm_ring.is_supported_zero {α : Type u} {s : set α} :
theorem free_comm_ring.is_supported_one {α : Type u} {s : set α} :
theorem free_comm_ring.is_supported_int {α : Type u} {i : } {s : set α} :
def free_comm_ring.restriction {α : Type u} (s : set α) [decidable_pred (λ (_x : α), _x s)] :

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

Equations
@[simp]
theorem free_comm_ring.restriction_of {α : Type u} (s : set α) [decidable_pred (λ (_x : α), _x s)] (p : α) :
= dite (p s) (λ (H : p s), free_comm_ring.of p, H⟩) (λ (H : p s), 0)
theorem free_comm_ring.is_supported_of {α : Type u} {p : α} {s : set α} :
p s
theorem free_comm_ring.map_subtype_val_restriction {α : Type u} {x : free_comm_ring α} (s : set α) [decidable_pred (λ (_x : α), _x s)] (hxs : x.is_supported s) :
theorem free_comm_ring.exists_finite_support {α : Type u} (x : free_comm_ring α) :
∃ (s : set α), s.finite x.is_supported s
theorem free_comm_ring.exists_finset_support {α : Type u} (x : free_comm_ring α) :
∃ (s : finset α),
def free_ring.to_free_comm_ring {α : Type u_1} :

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

Equations
@[protected, instance]
Equations
def free_ring.coe_ring_hom (α : Type u) :

The natural map free_ring α → free_comm_ring α, as a ring_hom.

Equations
@[protected, simp, norm_cast]
theorem free_ring.coe_zero (α : Type u) :
0 = 0
@[protected, simp, norm_cast]
theorem free_ring.coe_one (α : Type u) :
1 = 1
@[protected, simp]
theorem free_ring.coe_of {α : Type u} (a : α) :
@[protected, simp, norm_cast]
theorem free_ring.coe_neg {α : Type u} (x : free_ring α) :
@[protected, simp, norm_cast]
theorem free_ring.coe_add {α : Type u} (x y : free_ring α) :
(x + y) = x + y
@[protected, simp, norm_cast]
theorem free_ring.coe_sub {α : Type u} (x y : free_ring α) :
(x - y) = x - y
@[protected, simp, norm_cast]
theorem free_ring.coe_mul {α : Type u} (x y : free_ring α) :
(x * y) = x * y
@[protected]
theorem free_ring.coe_surjective (α : Type u) :
theorem free_ring.coe_eq (α : Type u) :
coe = functor.map (λ (l : list α), l)
noncomputable def free_ring.subsingleton_equiv_free_comm_ring (α : Type u) [subsingleton α] :

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
@[protected, instance]
def free_ring.comm_ring (α : Type u) [subsingleton α] :
Equations
noncomputable def free_comm_ring_equiv_mv_polynomial_int (α : Type u) :

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

Equations
noncomputable def free_comm_ring_pempty_equiv_int  :

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

Equations

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

Equations
noncomputable def free_ring_pempty_equiv_int  :

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

Equations
noncomputable def free_ring_punit_equiv_polynomial_int  :

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

Equations