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

@[implicit_reducible]

instance FieldCat.instCoeSortType :

CoeSort FieldCat (Type u)

Equations

FieldCat.instCoeSortType = { coe := FieldCat.carrier }

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

FieldCat.of R = { carrier := R, field := inst✝ }

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_iff {R : FieldCat} {S : FieldCat} {x y : R.Hom S} :

x = y ↔ x.hom = y.hom

source

theorem FieldCat.Hom.ext {R : FieldCat} {S : FieldCat} {x y : R.Hom S} (hom : x.hom = y.hom) :

x = y

source

@[implicit_reducible]

instance FieldCat.instCategory :

CategoryTheory.Category.{u_1, u_1 + 1} FieldCat

Equations

One or more equations did not get rendered due to their size.

source

@[implicit_reducible]

instance FieldCat.instCoeFunHomForallCarrier {R S : FieldCat} :

CoeFun (R ⟶ S) fun (x : R ⟶ S) => ↑R → ↑S

Equations

FieldCat.instCoeFunHomForallCarrier = { coe := fun (f : R ⟶ S) => ⇑f.hom }

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

theorem FieldCat.hom_ext_iff {R S : FieldCat} {f g : R ⟶ S} :

f = g ↔ f.hom = g.hom

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

FieldCat.ofHom f = { hom := f }

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

@[implicit_reducible]

instance FieldCat.instConcreteCategoryRingHomCarrier :

CategoryTheory.ConcreteCategory FieldCat fun (R S : FieldCat) => ↑R →+* ↑S

Equations

One or more equations did not get rendered due to their size.

source

def FieldCat.forgetObjEqCoe (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

R.forgetObjEqCoe R' = (R = R' → (CategoryTheory.forget FieldCat).obj R = ↑R')

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.ConcreteCategory.hom ((CategoryTheory.forget FieldCat).map f)) = ⇑f.hom

source

@[implicit_reducible]

instance FieldCat.instFieldObjForgetRingHomCarrier {R : FieldCat} :

Field ((CategoryTheory.forget FieldCat).obj R)

Equations

FieldCat.instFieldObjForgetRingHomCarrier = inferInstance

source

@[implicit_reducible]

instance FieldCat.hasForgetToSemiRingCat :

CategoryTheory.HasForget₂ FieldCat CommRingCat

Equations

One or more equations did not get rendered due to their size.

source

@[implicit_reducible]

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

FieldCat.RingEquiv.toRingCatIso e = { hom := { hom := ↑e }, inv := { hom := ↑e.symm }, hom_inv_id := ⋯, inv_hom_id := ⋯ }

Instances For

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

@[simp]

theorem FieldCat.RingEquiv.toRingCatIso_hom_hom {R S : Type u} [Field R] [Field S] (e : R ≃+* S) :

(toRingCatIso e).hom.hom = ↑e

source

instance FieldCat.forgetReflectIsos :

(CategoryTheory.forget FieldCat).ReflectsIsomorphisms

Documentation

LeanPool.BrauerGroupNew.FieldCat

Category instances for `Field`. #

Category instances for Field. #

Category instances for `Field`. #