The category of quadratic modules

structure QuadraticModuleCat (R : Type u) [CommRing R] extends ModuleCat R : Type (max u (v + 1))

The category of quadratic modules; modules with an associated quadratic form

• carrier : Type v
• isAddCommGroup : AddCommGroup ↑self.toModuleCat
• isModule : Module R ↑self.toModuleCat
• form : QuadraticForm R ↑self.toModuleCat

  The quadratic form associated with the module.

@[instance_reducible]

instance QuadraticModuleCat.instCoeSortType {R : Type u} [CommRing R] : CoeSort (QuadraticModuleCat R) (Type v)

Equations

• QuadraticModuleCat.instCoeSortType = { coe := fun (x : QuadraticModuleCat R) => ↑x.toModuleCat }

@[simp]

theorem QuadraticModuleCat.moduleCat_of_toModuleCat {R : Type u} [CommRing R] (X : QuadraticModuleCat R) : ↧↑X.toModuleCat = X.toModuleCat

@[reducible, inline]

abbrev QuadraticModuleCat.of {R : Type u} [CommRing R] {X : Type v} [AddCommGroup X] [Module R X] (Q : QuadraticForm R X) : QuadraticModuleCat R

The object in the category of quadratic R-modules associated to a quadratic R-module.

Equations

• QuadraticModuleCat.of Q = { toModuleCat := ↧X, form := Q }

structure QuadraticModuleCat.Hom {R : Type u} [CommRing R] (V W : QuadraticModuleCat R) : Type v

A type alias for QuadraticForm.LinearIsometry to avoid confusion between the categorical and algebraic spellings of composition.

• toIsometry' : V.form →qᵢ W.form

  The underlying isometry

theorem QuadraticModuleCat.Hom.ext {R : Type u} {inst✝ : CommRing R} {V W : QuadraticModuleCat R} {x y : V.Hom W} (toIsometry' : x.toIsometry' = y.toIsometry') : x = y

theorem QuadraticModuleCat.Hom.ext_iff {R : Type u} {inst✝ : CommRing R} {V W : QuadraticModuleCat R} {x y : V.Hom W} : x = y ↔ x.toIsometry' = y.toIsometry'

@[instance_reducible]

instance QuadraticModuleCat.category {R : Type u} [CommRing R] : CategoryTheory.Category.{v, max (v + 1) u} (QuadraticModuleCat R)

Equations

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

@[instance_reducible]

instance QuadraticModuleCat.concreteCategory {R : Type u} [CommRing R] : CategoryTheory.ConcreteCategory (QuadraticModuleCat R) fun (V W : QuadraticModuleCat R) => V.form →qᵢ W.form

Equations

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

@[reducible, inline]

abbrev QuadraticModuleCat.Hom.toIsometry {R : Type u} [CommRing R] {X Y : QuadraticModuleCat R} (f : X.Hom Y) : X.form →qᵢ Y.form

Turn a morphism in QuadraticModuleCat back into a Isometry.

Equations

• f.toIsometry = CategoryTheory.ConcreteCategory.hom f

@[reducible, inline]

abbrev QuadraticModuleCat.ofHom {R : Type u} [CommRing R] {X Y : Type v} [AddCommGroup X] [Module R X] [AddCommGroup Y] [Module R Y] {Q₁ : QuadraticForm R X} {Q₂ : QuadraticForm R Y} (f : Q₁ →qᵢ Q₂) : of Q₁ ⟶ of Q₂

Typecheck a QuadraticForm.Isometry as a morphism in Module R.

Equations

• QuadraticModuleCat.ofHom f = CategoryTheory.ConcreteCategory.ofHom f

theorem QuadraticModuleCat.Hom.toIsometry_injective {R : Type u} [CommRing R] (V W : QuadraticModuleCat R) : Function.Injective toIsometry

theorem QuadraticModuleCat.hom_ext {R : Type u} [CommRing R] {M N : QuadraticModuleCat R} (f g : M ⟶ N) (h : Hom.toIsometry f = Hom.toIsometry g) : f = g

theorem QuadraticModuleCat.hom_ext_iff {R : Type u} [CommRing R] {M N : QuadraticModuleCat R} {f g : M ⟶ N} : f = g ↔ Hom.toIsometry f = Hom.toIsometry g

@[simp]

theorem QuadraticModuleCat.toIsometry_comp {R : Type u} [CommRing R] {M N U : QuadraticModuleCat R} (f : M ⟶ N) (g : N ⟶ U) : Hom.toIsometry (CategoryTheory.CategoryStruct.comp f g) = (Hom.toIsometry g).comp (Hom.toIsometry f)

@[simp]

theorem QuadraticModuleCat.toIsometry_id {R : Type u} [CommRing R] {M : QuadraticModuleCat R} : Hom.toIsometry (CategoryTheory.CategoryStruct.id M) = QuadraticMap.Isometry.id M.form

@[instance_reducible]

instance QuadraticModuleCat.hasForgetToModule {R : Type u} [CommRing R] : CategoryTheory.HasForget₂ (QuadraticModuleCat R) (ModuleCat R)

Equations

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

@[simp]

theorem QuadraticModuleCat.forget₂_obj {R : Type u} [CommRing R] (X : QuadraticModuleCat R) : (CategoryTheory.forget₂ (QuadraticModuleCat R) (ModuleCat R)).obj X = ↧↑X.toModuleCat

@[simp]

theorem QuadraticModuleCat.forget₂_map {R : Type u} [CommRing R] (X Y : QuadraticModuleCat R) (f : X ⟶ Y) : (CategoryTheory.forget₂ (QuadraticModuleCat R) (ModuleCat R)).map f = ModuleCat.ofHom (Hom.toIsometry f).toLinearMap

def QuadraticModuleCat.ofIso {R : Type u} [CommRing R] {X Y : Type v} [AddCommGroup X] [Module R X] [AddCommGroup Y] [Module R Y] {Q₁ : QuadraticForm R X} {Q₂ : QuadraticForm R Y} (e : QuadraticMap.IsometryEquiv Q₁ Q₂) : of Q₁ ≅ of Q₂

Build an isomorphism in the category QuadraticModuleCat R from a QuadraticForm.IsometryEquiv.

Equations

• QuadraticModuleCat.ofIso e = { hom := QuadraticModuleCat.ofHom e.toIsometry, inv := QuadraticModuleCat.ofHom e.symm.toIsometry, hom_inv_id := ⋯, inv_hom_id := ⋯ }

@[simp]

theorem QuadraticModuleCat.ofIso_inv {R : Type u} [CommRing R] {X Y : Type v} [AddCommGroup X] [Module R X] [AddCommGroup Y] [Module R Y] {Q₁ : QuadraticForm R X} {Q₂ : QuadraticForm R Y} (e : QuadraticMap.IsometryEquiv Q₁ Q₂) : (ofIso e).inv = ofHom e.symm.toIsometry

@[simp]

theorem QuadraticModuleCat.ofIso_hom {R : Type u} [CommRing R] {X Y : Type v} [AddCommGroup X] [Module R X] [AddCommGroup Y] [Module R Y] {Q₁ : QuadraticForm R X} {Q₂ : QuadraticForm R Y} (e : QuadraticMap.IsometryEquiv Q₁ Q₂) : (ofIso e).hom = ofHom e.toIsometry

@[simp]

theorem QuadraticModuleCat.ofIso_refl {R : Type u} [CommRing R] {X : Type v} [AddCommGroup X] [Module R X] {Q₁ : QuadraticForm R X} : ofIso (QuadraticMap.IsometryEquiv.refl Q₁) = CategoryTheory.Iso.refl (of Q₁)

@[simp]

theorem QuadraticModuleCat.ofIso_symm {R : Type u} [CommRing R] {X Y : Type v} [AddCommGroup X] [Module R X] [AddCommGroup Y] [Module R Y] {Q₁ : QuadraticForm R X} {Q₂ : QuadraticForm R Y} (e : QuadraticMap.IsometryEquiv Q₁ Q₂) : ofIso e.symm = (ofIso e).symm

@[simp]

theorem QuadraticModuleCat.ofIso_trans {R : Type u} [CommRing R] {X Y Z : Type v} [AddCommGroup X] [Module R X] [AddCommGroup Y] [Module R Y] [AddCommGroup Z] [Module R Z] {Q₁ : QuadraticForm R X} {Q₂ : QuadraticForm R Y} {Q₃ : QuadraticForm R Z} (e : QuadraticMap.IsometryEquiv Q₁ Q₂) (f : QuadraticMap.IsometryEquiv Q₂ Q₃) : ofIso (e.trans f) = ofIso e ≪≫ ofIso f

def CategoryTheory.Iso.toIsometryEquiv {R : Type u} [CommRing R] {X Y : QuadraticModuleCat R} (i : X ≅ Y) : QuadraticMap.IsometryEquiv X.form Y.form

Build a QuadraticForm.IsometryEquiv from an isomorphism in the category QuadraticModuleCat R.

Equations

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

@[simp]

theorem CategoryTheory.Iso.toIsometryEquiv_invFun {R : Type u} [CommRing R] {X Y : QuadraticModuleCat R} (i : X ≅ Y) (a : ↑Y.toModuleCat) : i.toIsometryEquiv.invFun a = (QuadraticModuleCat.Hom.toIsometry i.inv) a

@[simp]

theorem CategoryTheory.Iso.toIsometryEquiv_toFun {R : Type u} [CommRing R] {X Y : QuadraticModuleCat R} (i : X ≅ Y) (a : ↑X.toModuleCat) : i.toIsometryEquiv a = (QuadraticModuleCat.Hom.toIsometry i.hom) a

@[simp]

theorem CategoryTheory.Iso.toIsometryEquiv_refl {R : Type u} [CommRing R] {X : QuadraticModuleCat R} : (refl X).toIsometryEquiv = QuadraticMap.IsometryEquiv.refl X.form

@[simp]

theorem CategoryTheory.Iso.toIsometryEquiv_symm {R : Type u} [CommRing R] {X Y : QuadraticModuleCat R} (e : X ≅ Y) : e.symm.toIsometryEquiv = e.toIsometryEquiv.symm

@[simp]

theorem CategoryTheory.Iso.toIsometryEquiv_trans {R : Type u} [CommRing R] {X Y Z : QuadraticModuleCat R} (e : X ≅ Y) (f : Y ≅ Z) : (e ≪≫ f).toIsometryEquiv = e.toIsometryEquiv.trans f.toIsometryEquiv