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.

  • of :: (
  • )
Instances For
    source
    instance BoolRing.instCoeSortType :
    CoeSort BoolRing (Type u_1)
    Equations
    source
    theorem BoolRing.coe_of (α : Type u_1) [BooleanRing α] :
    ↑{ carrier := α, booleanRing := inst✝ } = α
    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
      theorem BoolRing.Hom.ext_iff {R : BoolRing} {S : BoolRing} {x y : R.Hom S} :
      x = y ↔ x.hom' = y.hom'
      source
      instance BoolRing.instCategory :
      CategoryTheory.Category.{u_1, u_1 + 1} BoolRing
      Equations
      • One or more equations did not get rendered due to their size.
      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) :
        { carrier := R, booleanRing := inst✝ } ⟶ { carrier := S, booleanRing := inst✝¹ }

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

            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 ↑{ carrier := AsBoolAlg R, str := instBooleanAlgebraAsBoolAlg }.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