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 #

Main results #

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

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 α.

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

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

    Equations
    Instances For
      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 xC yC (x + y)) (hm : ∀ (x y : FreeCommRing α), C xC yC (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
      Instances For
        @[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_iff {α : Type u} {R : Type v} [CommRing R] {f : FreeCommRing α →+* R} {g : FreeCommRing α →+* R} :
        f = g ∀ (x : α), f (FreeCommRing.of x) = g (FreeCommRing.of x)
        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 : αβ) :

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

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

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

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

            Equations
            Instances For
              @[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 p, H else 0
              theorem FreeCommRing.isSupported_of {α : Type u} {p : α} {s : Set α} :
              (FreeCommRing.of p).IsSupported s p s
              theorem FreeCommRing.map_subtype_val_restriction {α : Type u} {x : FreeCommRing α} (s : Set α) [DecidablePred fun (x : α) => x s] (hxs : x.IsSupported s) :
              theorem FreeCommRing.exists_finite_support {α : Type u} (x : FreeCommRing α) :
              ∃ (s : Set α), s.Finite x.IsSupported s
              theorem FreeCommRing.exists_finset_support {α : Type u} (x : FreeCommRing α) :
              ∃ (s : Finset α), x.IsSupported s

              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

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

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

                    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

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

                      Equations
                      Instances For

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

                        Equations
                        Instances For