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

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

Equations

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

instance FreeCommRing.instCommRing (α : Type u) : CommRing (FreeCommRing α)

Equations

• FreeCommRing.instCommRing α = id inferInstance

instance FreeCommRing.instInhabited (α : Type u) : Inhabited (FreeCommRing α)

Equations

• FreeCommRing.instInhabited α = id inferInstance

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 FreeCommRing.of

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

theorem FreeCommRing.induction_on {α : Type u} {C : FreeCommRing α → Prop} (z : FreeCommRing α) (hn1 : C (-1)) (hb : ∀ (b : α), C (FreeCommRing.of b)) (ha : ∀ (x y : FreeCommRing α), C x → C y → C (x + y)) (hm : ∀ (x y : FreeCommRing α), C x → C y → C (x * y)) : C 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 : α) : (FreeCommRing.lift f) (FreeCommRing.of x) = f x

@[simp]

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

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

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 : α) : (FreeCommRing.map f) (FreeCommRing.of x) = FreeCommRing.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

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

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

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

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

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

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

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

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

theorem FreeCommRing.isSupported_int {α : Type u} {i : ℤ} {s : Set α} : FreeCommRing.IsSupported (↑i) 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 { val := a, property := H } else 0

@[simp]

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

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

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

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

theorem FreeCommRing.exists_finset_support {α : Type u} (x : FreeCommRing α) : ∃ (s : Finset α), FreeCommRing.IsSupported x ↑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 : α) : ↑(FreeRing.of a) = FreeCommRing.of a

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

theorem FreeRing.coe_mul {α : Type u} (x : FreeRing α) (y : FreeRing α) : ↑(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 : 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 α = let __src := inferInstanceAs (Ring (FreeRing α)); CommRing.mk ⋯

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

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

Equations

• freeCommRingEquivMvPolynomialInt α = RingEquiv.ofHomInv (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 = RingEquiv.trans (freeCommRingEquivMvPolynomialInt PEmpty.{u + 1} ) (MvPolynomial.isEmptyRingEquiv ℤ PEmpty.{u + 1} )

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

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

Equations

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

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

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

Equations

• freeRingPemptyEquivInt = RingEquiv.trans (FreeRing.subsingletonEquivFreeCommRing PEmpty.{u + 1} ) freeCommRingPemptyEquivInt

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

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

Equations

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