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
def BoolRing :
Type (u_1 + 1)

The category of Boolean rings.

Equations
Instances For
    source
    instance BoolRing.instCoeSortType :
    CoeSort BoolRing (Type u_1)
    Equations
    source
    instance BoolRing.instBooleanRingα (X : BoolRing) :
    BooleanRing ↑X
    Equations
    • X.instBooleanRingα = X.str
    source
    def BoolRing.of (α : Type u_1) [BooleanRing α] :
    BoolRing

    Construct a bundled BoolRing from a BooleanRing.

    Equations
    Instances For
      source
      @[simp]
      theorem BoolRing.coe_of (α : Type u_1) [BooleanRing α] :
      ↑(BoolRing.of α) = α
      source
      instance BoolRing.instInhabited :
      Inhabited BoolRing
      Equations
      source
      instance BoolRing.instParentProjectionCommRingBooleanRingToCommRing :
      CategoryTheory.BundledHom.ParentProjection @BooleanRing.toCommRing
      Equations
      source
      instance BoolRing.instConcreteCategory :
      CategoryTheory.ConcreteCategory BoolRing
      Equations
      source
      instance BoolRing.hasForgetToCommRing :
      CategoryTheory.HasForget₂ BoolRing CommRingCat
      Equations
      • One or more equations did not get rendered due to their size.
      source
      @[simp]
      theorem BoolRing.Iso.mk_inv {α : BoolRing} {β : BoolRing} (e : ↑α ≃+* ↑β) :
      (BoolRing.Iso.mk e).inv = ↑e.symm
      source
      @[simp]
      theorem BoolRing.Iso.mk_hom {α : BoolRing} {β : BoolRing} (e : ↑α ≃+* ↑β) :
      (BoolRing.Iso.mk e).hom = ↑e
      source
      def BoolRing.Iso.mk {α : BoolRing} {β : BoolRing} (e : ↑α ≃+* ↑β) :
      α ≅ β

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

      Equations
      • BoolRing.Iso.mk e = { hom := ↑e, inv := ↑e.symm, hom_inv_id := ⋯, inv_hom_id := ⋯ }
      Instances For

        Equivalence between BoolAlg and BoolRing #

        source
        @[simp]
        theorem BoolRing.hasForgetToBoolAlg_forget₂_map {X : BoolRing} {Y : BoolRing} (f : ↑X →+* ↑Y) :
        CategoryTheory.HasForget₂.forget₂.map f = f.asBoolAlg
        source
        @[simp]
        theorem BoolRing.hasForgetToBoolAlg_forget₂_obj (X : BoolRing) :
        CategoryTheory.HasForget₂.forget₂.obj X = BoolAlg.of (AsBoolAlg ↑X)
        source
        instance BoolRing.hasForgetToBoolAlg :
        CategoryTheory.HasForget₂ BoolRing BoolAlg
        Equations
        • One or more equations did not get rendered due to their size.
        source
        instance instBooleanAlgebraαLatticeToLatToBddLatToBddDistLat {X : BoolAlg} :
        BooleanAlgebra ↑X.toBddDistLat.toBddLat.toLat
        Equations
        • instBooleanAlgebraαLatticeToLatToBddLatToBddDistLat = X.instBooleanAlgebra
        source
        @[simp]
        theorem BoolAlg.hasForgetToBoolRing_forget₂_obj (X : BoolAlg) :
        CategoryTheory.HasForget₂.forget₂.obj X = BoolRing.of (AsBoolRing ↑X)
        source
        @[simp]
        theorem BoolAlg.hasForgetToBoolRing_forget₂_map {X : BoolAlg} {Y : BoolAlg} (f : BoundedLatticeHom ↑X.toBddDistLat.toBddLat.toLat ↑Y.toBddDistLat.toBddLat.toLat) :
        CategoryTheory.HasForget₂.forget₂.map f = f.asBoolRing
        source
        instance BoolAlg.hasForgetToBoolRing :
        CategoryTheory.HasForget₂ BoolAlg BoolRing
        Equations
        • One or more equations did not get rendered due to their size.
        source
        @[simp]
        theorem boolRingCatEquivBoolAlg_functor :
        boolRingCatEquivBoolAlg.functor = CategoryTheory.forget₂ BoolRing BoolAlg
        source
        @[simp]
        theorem boolRingCatEquivBoolAlg_inverse :
        boolRingCatEquivBoolAlg.inverse = CategoryTheory.forget₂ BoolAlg BoolRing
        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