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 homFreeCommRing α →+* R
induced by functoriality fromf
.map (f : α → β)
: the ring homFreeCommRing α →*+ 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
Equations
- FreeCommRing.instCommRing α = id inferInstance
Equations
- FreeCommRing.instInhabited α = id inferInstance
The canonical map from α
to the free commutative ring on α
.
Equations
- FreeCommRing.of x = FreeAbelianGroup.of (Multiplicative.ofAdd {x})
Instances For
Lift a map α → R
to an additive group homomorphism FreeCommRing α → R
.
Equations
- FreeCommRing.lift = FreeCommRing.liftToMultiset✝.trans FreeAbelianGroup.liftMonoid
Instances For
A map f : α → β
produces a ring homomorphism FreeCommRing α →+* FreeCommRing β
.
Equations
- FreeCommRing.map f = FreeCommRing.lift (FreeCommRing.of ∘ f)
Instances For
is_supported x s
means that all monomials showing up in x
have variables in s
.
Equations
- x.IsSupported s = (x ∈ Subring.closure (FreeCommRing.of '' s))
Instances For
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 ⟨a, H⟩ else 0
Instances For
The canonical ring homomorphism from the free ring generated by α
to the free commutative ring
generated by α
.
Equations
- FreeRing.toFreeCommRing = FreeRing.lift FreeCommRing.of
Instances For
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
Instances For
Equations
- FreeRing.FreeCommRing.instCoe α = { coe := FreeRing.castFreeCommRing }
The natural map FreeRing α → FreeCommRing α
, as a RingHom
.
Equations
- FreeRing.coeRingHom α = FreeRing.toFreeCommRing
Instances For
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
Instances For
Equations
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) ⋯ ⋯
Instances For
The free commutative ring on the empty type is isomorphic to ℤ
.
Equations
Instances For
The free commutative ring on a type with one term is isomorphic to ℤ[X]
.
Equations
- freeCommRingPunitEquivPolynomialInt = (freeCommRingEquivMvPolynomialInt PUnit.{?u.3 + 1} ).trans (MvPolynomial.pUnitAlgEquiv ℤ).toRingEquiv
Instances For
The free ring on the empty type is isomorphic to ℤ
.
Equations
Instances For
The free ring on a type with one term is isomorphic to ℤ[X]
.