Documentation

BrauerGroup.FieldCat

Category instances for Field. #

source
structure FieldCat :
Type (u + 1)

The category of fields.

  • carrier : Type u

    The underlying type.

  • field : Field ↑self
Instances For
    source
    instance FieldCat.instCoeSortType :
    CoeSort FieldCat (Type u)
    Equations
    source
    @[reducible, inline]
    abbrev FieldCat.of (R : Type u) [Field R] :
    FieldCat

    The object in the category of R-algebras associated to a type equipped with the appropriate typeclasses. This is the preferred way to construct a term of FieldCat.

    Equations
    Instances For
      source
      theorem FieldCat.coe_of (R : Type u) [Field R] :
      ↑(of R) = R
      source
      theorem FieldCat.of_carrier (R : FieldCat) :
      of ↑R = R
      source
      structure FieldCat.Hom (R : FieldCat) (S : FieldCat) :
      Type (max u_1 u_2)

      The type of morphisms in FieldCat.

      • hom : ↑R →+* ↑S

        The underlying ring hom.

      Instances For
        source
        theorem FieldCat.Hom.ext {R : FieldCat} {S : FieldCat} {x y : R.Hom S} (hom : x.hom = y.hom) :
        x = y
        source
        instance FieldCat.instCategory :
        CategoryTheory.Category.{u_1, u_1 + 1} FieldCat
        Equations
        source
        instance FieldCat.instCoeFunHomForallCarrier {R S : FieldCat} :
        CoeFun (R ⟶ S) fun (x : R ⟶ S) => ↑R → ↑S
        Equations
        source
        @[simp]
        theorem FieldCat.hom_id {R : FieldCat} :
        (CategoryTheory.CategoryStruct.id R).hom = RingHom.id ↑R
        source
        theorem FieldCat.id_apply (R : FieldCat) (r : ↑R) :
        (CategoryTheory.CategoryStruct.id R).hom r = r
        source
        @[simp]
        theorem FieldCat.hom_comp {R S T : FieldCat} (f : R ⟶ S) (g : S ⟶ T) :
        (CategoryTheory.CategoryStruct.comp f g).hom = g.hom.comp f.hom
        source
        theorem FieldCat.comp_apply {R S T : FieldCat} (f : R ⟶ S) (g : S ⟶ T) (r : ↑R) :
        (CategoryTheory.CategoryStruct.comp f g).hom r = g.hom (f.hom r)
        source
        theorem FieldCat.hom_ext {R S : FieldCat} {f g : R ⟶ S} (hf : f.hom = g.hom) :
        f = g
        source
        @[reducible, inline]
        abbrev FieldCat.ofHom {R S : Type u} [Field R] [Field S] (f : R →+* S) :
        of R ⟶ of S

        Typecheck a RingHom as a morphism in FieldCat.

        Equations
        Instances For
          source
          theorem FieldCat.hom_ofHom {R S : Type u} [Field R] [Field S] (f : R →+* S) :
          (ofHom f).hom = f
          source
          @[simp]
          theorem FieldCat.ofHom_hom {R S : FieldCat} (f : R ⟶ S) :
          ofHom f.hom = f
          source
          @[simp]
          theorem FieldCat.ofHom_id {R : Type u} [Field R] :
          ofHom (RingHom.id R) = CategoryTheory.CategoryStruct.id (of R)
          source
          @[simp]
          theorem FieldCat.ofHom_comp {R S T : Type u} [Field R] [Field S] [Field T] (f : R →+* S) (g : S →+* T) :
          ofHom (g.comp f) = CategoryTheory.CategoryStruct.comp (ofHom f) (ofHom g)
          source
          theorem FieldCat.ofHom_apply {R S : Type u} [Field R] [Field S] (f : R →+* S) (r : R) :
          (ofHom f).hom r = f r
          source
          @[simp]
          theorem FieldCat.inv_hom_apply {R S : FieldCat} (e : R ≅ S) (r : ↑R) :
          e.inv.hom (e.hom.hom r) = r
          source
          @[simp]
          theorem FieldCat.hom_inv_apply {R S : FieldCat} (e : R ≅ S) (s : ↑S) :
          e.hom.hom (e.inv.hom s) = s
          source
          instance FieldCat.instHasForget :
          CategoryTheory.HasForget FieldCat
          Equations
          • One or more equations did not get rendered due to their size.
          source
          def FieldCat.forget_obj_eq_coe (R R' : FieldCat) :
          Prop

          This unification hint helps with problems of the form (forget ?C).obj R =?= carrier R'.

          An example where this is needed is in applying PresheafOfModules.Sheafify.app_eq_of_isLocallyInjective.

          Equations
          Instances For
            source
            theorem FieldCat.forget_obj {R : FieldCat} :
            (CategoryTheory.forget FieldCat).obj R = ↑R
            source
            theorem FieldCat.forget_map {R S : FieldCat} (f : R ⟶ S) :
            (CategoryTheory.forget FieldCat).map f = ⇑f.hom
            source
            instance FieldCat.instFieldObjForget {R : FieldCat} :
            Field ((CategoryTheory.forget FieldCat).obj R)
            Equations
            source
            instance FieldCat.hasForgetToSemiRingCat :
            CategoryTheory.HasForget₂ FieldCat CommRingCat
            Equations
            • One or more equations did not get rendered due to their size.
            source
            instance FieldCat.hasForgetToAddCommGrp :
            CategoryTheory.HasForget₂ FieldCat RingCat
            Equations
            • One or more equations did not get rendered due to their size.
            source
            def FieldCat.RingEquiv.toRingCatIso {R S : Type u} [Field R] [Field S] (e : R ≃+* S) :
            of R ≅ of S

            Field equivalence are isomorphisms in category of semirings

            Equations
            Instances For
              source
              @[simp]
              theorem FieldCat.RingEquiv.toRingCatIso_hom_hom {R S : Type u} [Field R] [Field S] (e : R ≃+* S) :
              (toRingCatIso e).hom.hom = ↑e
              source
              @[simp]
              theorem FieldCat.RingEquiv.toRingCatIso_inv_hom {R S : Type u} [Field R] [Field S] (e : R ≃+* S) :
              (toRingCatIso e).inv.hom = ↑e.symm
              source
              instance FieldCat.forgetReflectIsos :
              (CategoryTheory.forget FieldCat).ReflectsIsomorphisms