Documentation

Mathlib.Algebra.Category.BoolRing

The category of Boolean rings #

This file defines BoolRing, the category of Boolean rings.

TODO #

Finish the equivalence with BoolAlg.

structure BoolRing :
Type (u + 1)

The category of Boolean rings.

Instances For
    @[reducible, inline]
    abbrev BoolRing.of (α : Type u_1) [BooleanRing α] :

    Construct a bundled BoolRing from a BooleanRing.

    Equations
    Instances For
      theorem BoolRing.coe_of (α : Type u_1) [BooleanRing α] :
      (BoolRing.of α) = α
      structure BoolRing.Hom (R : BoolRing) (S : BoolRing) :
      Type (max u_1 u_2)

      The type of morphisms in BoolRing.

      • hom : R →+* S

        The underlying ring hom.

      Instances For
        theorem BoolRing.Hom.ext {R : BoolRing} {S : BoolRing} {x y : R.Hom S} (hom : x.hom = y.hom) :
        x = y
        theorem BoolRing.hom_ext {R S : BoolRing} {f g : R S} (hf : f.hom = g.hom) :
        f = g
        @[reducible, inline]
        abbrev BoolRing.ofHom {R S : Type u} [BooleanRing R] [BooleanRing S] (f : R →+* S) :

        Typecheck a RingHom as a morphism in BoolRing.

        Equations
        Instances For
          Equations
          • One or more equations did not get rendered due to their size.
          Equations
          • One or more equations did not get rendered due to their size.
          def BoolRing.Iso.mk {α β : BoolRing} (e : α ≃+* β) :
          α β

          Constructs an isomorphism of Boolean rings from a ring isomorphism between them.

          Equations
          • BoolRing.Iso.mk e = { hom := { hom := e }, inv := { hom := e.symm }, hom_inv_id := , inv_hom_id := }
          Instances For
            @[simp]
            theorem BoolRing.Iso.mk_hom_hom {α β : BoolRing} (e : α ≃+* β) :
            (BoolRing.Iso.mk e).hom.hom = e
            @[simp]
            theorem BoolRing.Iso.mk_inv_hom {α β : BoolRing} (e : α ≃+* β) :
            (BoolRing.Iso.mk e).inv.hom = e.symm

            Equivalence between BoolAlg and BoolRing #

            instance instBooleanAlgebraαLatticeToLatToBddLatToBddDistLat {X : BoolAlg} :
            BooleanAlgebra X.toBddDistLat.toBddLat.toLat
            Equations
            • instBooleanAlgebraαLatticeToLatToBddLatToBddDistLat = X.instBooleanAlgebra
            Equations
            Equations
            • One or more equations did not get rendered due to their size.
            @[simp]
            theorem BoolRing.hasForgetToBoolAlg_forget₂_map {R S : BoolRing} (f : R S) :
            CategoryTheory.HasForget₂.forget₂.map f = f.hom.asBoolAlg
            @[simp]
            theorem BoolRing.hasForgetToBoolAlg_forget₂_obj (X : BoolRing) :
            CategoryTheory.HasForget₂.forget₂.obj X = BoolAlg.of (AsBoolAlg X)
            Equations
            • One or more equations did not get rendered due to their size.
            @[simp]
            theorem BoolAlg.hasForgetToBoolRing_forget₂_obj_carrier (X : BoolAlg) :
            (CategoryTheory.HasForget₂.forget₂.obj X) = AsBoolRing X
            @[simp]
            theorem BoolAlg.hasForgetToBoolRing_forget₂_map_hom {x✝ x✝¹ : BoolAlg} (f : x✝ x✝¹) :
            (CategoryTheory.HasForget₂.forget₂.map f).hom = BoundedLatticeHom.asBoolRing f

            The equivalence between Boolean rings and Boolean algebras. This is actually an isomorphism.

            Equations
            • One or more equations did not get rendered due to their size.
            Instances For