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.

source
structure BoolRing :
Type (u + 1)

The category of Boolean rings.

Instances For
    source
    instance BoolRing.instCoeSortType :
    CoeSort BoolRing (Type u_1)
    Equations
    source
    @[reducible, inline]
    abbrev BoolRing.of (α : Type u_1) [BooleanRing α] :
    BoolRing

    Construct a bundled BoolRing from a BooleanRing.

    Equations
    Instances For
      source
      theorem BoolRing.coe_of (α : Type u_1) [BooleanRing α] :
      ↑(BoolRing.of α) = α
      source
      instance BoolRing.instInhabited :
      Inhabited BoolRing
      Equations
      source
      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
        source
        theorem BoolRing.Hom.ext {R : BoolRing} {S : BoolRing} {x y : R.Hom S} (hom : x.hom = y.hom) :
        x = y
        source
        instance BoolRing.instCategory :
        CategoryTheory.Category.{u_1, u_1 + 1} BoolRing
        Equations
        source
        theorem BoolRing.hom_ext {R S : BoolRing} {f g : R ⟶ S} (hf : f.hom = g.hom) :
        f = g
        source
        @[reducible, inline]
        abbrev BoolRing.ofHom {R S : Type u} [BooleanRing R] [BooleanRing S] (f : R →+* S) :
        BoolRing.of R ⟶ BoolRing.of S

        Typecheck a RingHom as a morphism in BoolRing.

        Equations
        Instances For
          source
          instance BoolRing.instConcreteCategory :
          CategoryTheory.ConcreteCategory BoolRing
          Equations
          • One or more equations did not get rendered due to their size.
          source
          instance BoolRing.hasForgetToCommRing :
          CategoryTheory.HasForget₂ BoolRing CommRingCat
          Equations
          • One or more equations did not get rendered due to their size.
          source
          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
            source
            @[simp]
            theorem BoolRing.Iso.mk_hom_hom {α β : BoolRing} (e : ↑α ≃+* ↑β) :
            (BoolRing.Iso.mk e).hom.hom = ↑e
            source
            @[simp]
            theorem BoolRing.Iso.mk_inv_hom {α β : BoolRing} (e : ↑α ≃+* ↑β) :
            (BoolRing.Iso.mk e).inv.hom = ↑e.symm

            Equivalence between BoolAlg and BoolRing #

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

            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
              source
              @[simp]
              theorem boolRingCatEquivBoolAlg_functor :
              boolRingCatEquivBoolAlg.functor = CategoryTheory.forget₂ BoolRing BoolAlg
              source
              @[simp]
              theorem boolRingCatEquivBoolAlg_inverse :
              boolRingCatEquivBoolAlg.inverse = CategoryTheory.forget₂ BoolAlg BoolRing