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 α] :
      ↑(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
        instance BoolRing.instConcreteCategoryRingHomCarrier :
        CategoryTheory.ConcreteCategory BoolRing fun (x1 x2 : BoolRing) => ↑x1 →+* ↑x2
        Equations
        • One or more equations did not get rendered due to their size.
        source
        @[reducible, inline]
        abbrev BoolRing.Hom.hom {X Y : BoolRing} (f : X.Hom Y) :
        ↑X →+* ↑Y

        Turn a morphism in BoolRing back into a RingHom.

        Equations
        Instances For
          source
          @[reducible, inline]
          abbrev BoolRing.ofHom {R S : Type u} [BooleanRing R] [BooleanRing S] (f : R →+* S) :
          of R ⟶ of S

          Typecheck a RingHom as a morphism in BoolRing.

          Equations
          Instances For
            source
            theorem BoolRing.hom_ext {R S : BoolRing} {f g : R ⟶ S} (hf : Hom.hom f = Hom.hom g) :
            f = g
            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 : ↑α ≃+* ↑β) :
              (mk e).hom.hom' = ↑e
              source
              @[simp]
              theorem BoolRing.Iso.mk_inv_hom' {α β : BoolRing} (e : ↑α ≃+* ↑β) :
              (mk e).inv.hom' = ↑e.symm

              Equivalence between BoolAlg and BoolRing #

              source
              instance instBooleanAlgebraCarrierToBddLatToBddDistLat {X : BoolAlg} :
              BooleanAlgebra ↑X.toBddDistLat.toBddLat.toLat
              Equations
              source
              instance instBooleanRingCarrierToBddLatToBddDistLatOfAsBoolAlg {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 {X✝ Y✝ : BoolRing} (f : X✝ ⟶ Y✝) :
              CategoryTheory.HasForget₂.forget₂.map f = BoolAlg.ofHom (Hom.hom f).asBoolAlg
              source
              @[simp]
              theorem BoolRing.hasForgetToBoolAlg_forget₂_obj_coe (X : BoolRing) :
              ↑(CategoryTheory.HasForget₂.forget₂.obj X) = 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₂_map {X✝ Y✝ : BoolAlg} (f : X✝ ⟶ Y✝) :
              CategoryTheory.HasForget₂.forget₂.map f = BoolRing.ofHom (Hom.hom f).asBoolRing
              source
              @[simp]
              theorem BoolAlg.hasForgetToBoolRing_forget₂_obj_carrier (X : BoolAlg) :
              ↑(CategoryTheory.HasForget₂.forget₂.obj X) = AsBoolRing ↑X
              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