mathlib3 documentation

ring_theory.free_comm_ring

Free commutative rings #

THIS FILE IS SYNCHRONIZED WITH MATHLIB4. Any changes to this file require a corresponding PR to mathlib4.

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

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

Equations

free_comm_ring α = free_abelian_group (multiplicative (multiset α))

Instances for free_comm_ring

@[protected, instance]

def free_comm_ring.comm_ring (α : Type u) :

comm_ring (free_comm_ring α)

@[protected, instance]

def free_comm_ring.inhabited (α : Type u) :

inhabited (free_comm_ring α)

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

free_comm_ring α

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

Equations

free_comm_ring.of x = free_abelian_group.of (⇑multiplicative.of_add {x})

theorem free_comm_ring.of_injective {α : Type u} :

function.injective free_comm_ring.of

@[protected]

theorem free_comm_ring.induction_on {α : Type u} {C : free_comm_ring α → Prop} (z : free_comm_ring α) (hn1 : C (-1)) (hb : ∀ (b : α), C (free_comm_ring.of b)) (ha : ∀ (x y : free_comm_ring α), C x → C y → C (x + y)) (hm : ∀ (x y : free_comm_ring α), C x → C y → C (x * y)) :

C z

def free_comm_ring.lift {α : Type u} {R : Type v} [comm_ring R] :

(α → R) ≃ (free_comm_ring α →+* 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

free_comm_ring.lift = lift_to_multiset.trans free_abelian_group.lift_monoid

@[simp]

theorem free_comm_ring.lift_of {α : Type u} {R : Type v} [comm_ring R] (f : α → R) (x : α) :

⇑(⇑free_comm_ring.lift f) (free_comm_ring.of x) = f x

@[simp]

theorem free_comm_ring.lift_comp_of {α : Type u} {R : Type v} [comm_ring R] (f : free_comm_ring α →+* R) :

⇑free_comm_ring.lift (⇑f ∘ free_comm_ring.of) = f

@[ext]

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

f = g

def free_comm_ring.map {α : Type u} {β : Type v} (f : α → β) :

free_comm_ring α →+* free_comm_ring β

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

Equations

free_comm_ring.map f = ⇑free_comm_ring.lift (free_comm_ring.of ∘ f)

@[simp]

theorem free_comm_ring.map_of {α : Type u} {β : Type v} (f : α → β) (x : α) :

⇑(free_comm_ring.map f) (free_comm_ring.of x) = free_comm_ring.of (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

x.is_supported s = (x ∈ subring.closure (free_comm_ring.of '' s))

theorem free_comm_ring.is_supported_upwards {α : Type u} {x : free_comm_ring α} {s t : set α} (hs : x.is_supported s) (hst : s ⊆ t) :

x.is_supported 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) :

(-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 α} :

0.is_supported s

theorem free_comm_ring.is_supported_one {α : Type u} {s : set α} :

1.is_supported s

theorem free_comm_ring.is_supported_int {α : Type u} {i : ℤ} {s : set α} :

↑i.is_supported s

def free_comm_ring.restriction {α : Type u} (s : set α) [decidable_pred (λ (_x : α), _x ∈ s)] :

free_comm_ring α →+* free_comm_ring ↥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

free_comm_ring.restriction s = ⇑free_comm_ring.lift (λ (p : α), dite (p ∈ s) (λ (H : p ∈ s), free_comm_ring.of ⟨p, H⟩) (λ (H : p ∉ s), 0))

@[simp]

theorem free_comm_ring.restriction_of {α : Type u} (s : set α) [decidable_pred (λ (_x : α), _x ∈ s)] (p : α) :

⇑(free_comm_ring.restriction s) (free_comm_ring.of 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 α} :

(free_comm_ring.of p).is_supported s ↔ 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) :

⇑(free_comm_ring.map subtype.val) (⇑(free_comm_ring.restriction s) x) = x

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 α), x.is_supported ↑s

def free_ring.to_free_comm_ring {α : Type u_1} :

free_ring α →+* free_comm_ring α

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

Equations

free_ring.to_free_comm_ring = ⇑free_ring.lift free_comm_ring.of

@[protected, instance]

def free_ring.free_comm_ring.has_coe (α : Type u) :

has_coe (free_ring α) (free_comm_ring α)

Equations

free_ring.free_comm_ring.has_coe α = {coe := ⇑free_ring.to_free_comm_ring}

def free_ring.coe_ring_hom (α : Type u) :

free_ring α →+* free_comm_ring α

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

Equations

free_ring.coe_ring_hom α = free_ring.to_free_comm_ring

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

↑(free_ring.of a) = free_comm_ring.of 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) :

function.surjective coe

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 α] :

free_ring α ≃+* free_comm_ring α

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

free_ring.subsingleton_equiv_free_comm_ring α = ring_equiv.of_bijective (free_ring.coe_ring_hom α) _

@[protected, instance]

def free_ring.comm_ring (α : Type u) [subsingleton α] :

comm_ring (free_ring α)

Equations

free_ring.comm_ring α = {add := ring.add (free_ring.ring α), add_assoc := _, zero := ring.zero (free_ring.ring α), zero_add := _, add_zero := _, nsmul := ring.nsmul (free_ring.ring α), nsmul_zero' := _, nsmul_succ' := _, neg := ring.neg (free_ring.ring α), sub := ring.sub (free_ring.ring α), sub_eq_add_neg := _, zsmul := ring.zsmul (free_ring.ring α), zsmul_zero' := _, zsmul_succ' := _, zsmul_neg' := _, add_left_neg := _, add_comm := _, int_cast := ring.int_cast (free_ring.ring α), nat_cast := ring.nat_cast (free_ring.ring α), one := ring.one (free_ring.ring α), nat_cast_zero := _, nat_cast_succ := _, int_cast_of_nat := _, int_cast_neg_succ_of_nat := _, mul := ring.mul (free_ring.ring α), mul_assoc := _, one_mul := _, mul_one := _, npow := ring.npow (free_ring.ring α), npow_zero' := _, npow_succ' := _, left_distrib := _, right_distrib := _, mul_comm := _}

noncomputable def free_comm_ring_equiv_mv_polynomial_int (α : Type u) :

free_comm_ring α ≃+* mv_polynomial α ℤ

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

Equations

free_comm_ring_equiv_mv_polynomial_int α = ring_equiv.of_hom_inv (⇑free_comm_ring.lift (λ (a : α), mv_polynomial.X a)) (mv_polynomial.eval₂_hom (int.cast_ring_hom (free_comm_ring α)) free_comm_ring.of) _ _

noncomputable def free_comm_ring_pempty_equiv_int :

free_comm_ring pempty ≃+* ℤ

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

Equations

free_comm_ring_pempty_equiv_int = (free_comm_ring_equiv_mv_polynomial_int pempty).trans (mv_polynomial.is_empty_ring_equiv ℤ pempty)

noncomputable def free_comm_ring_punit_equiv_polynomial_int :

free_comm_ring punit ≃+* polynomial ℤ

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

Equations

free_comm_ring_punit_equiv_polynomial_int = (free_comm_ring_equiv_mv_polynomial_int punit).trans (mv_polynomial.punit_alg_equiv ℤ).to_ring_equiv

noncomputable def free_ring_pempty_equiv_int :

free_ring pempty ≃+* ℤ

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

Equations

free_ring_pempty_equiv_int = (free_ring.subsingleton_equiv_free_comm_ring pempty).trans free_comm_ring_pempty_equiv_int

noncomputable def free_ring_punit_equiv_polynomial_int :

free_ring punit ≃+* polynomial ℤ

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

Equations

free_ring_punit_equiv_polynomial_int = (free_ring.subsingleton_equiv_free_comm_ring punit).trans free_comm_ring_punit_equiv_polynomial_int