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 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) : ModuleCat.of R ↑X.toModuleCat = X.toModuleCat

def 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 := ModuleCat.of R X, form := Q }

@[simp]

theorem QuadraticModuleCat.of_form {R : Type u} [CommRing R] {X : Type v} [AddCommGroup X] [Module R X] (Q : QuadraticForm R X) : (of Q).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.toIsometry_injective {R : Type u} [CommRing R] (V W : QuadraticModuleCat R) : Function.Injective toIsometry

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

Equations

• QuadraticModuleCat.category = CategoryTheory.Category.mk ⋯ ⋯ ⋯

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

@[reducible, inline]

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

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

Equations

• QuadraticModuleCat.ofHom f = { toIsometry := f }

@[simp]

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

@[simp]

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

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

Equations

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

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 = ModuleCat.of R ↑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 f.toIsometry.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 := { toIsometry := e.toIsometry }, inv := { toIsometry := e.symm.toIsometry }, hom_inv_id := ⋯, inv_hom_id := ⋯ }

@[simp]

theorem QuadraticModuleCat.ofIso_hom_toIsometry {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.toIsometry = e.toIsometry

@[simp]

theorem QuadraticModuleCat.ofIso_inv_toIsometry {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.toIsometry = e.symm.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

• i.toIsometryEquiv = { toFun := ⇑i.hom.toIsometry, map_add' := ⋯, map_smul' := ⋯, invFun := ⇑i.inv.toIsometry, left_inv := ⋯, right_inv := ⋯, map_app' := ⋯ }

@[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 = i.inv.toIsometry 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 = i.hom.toIsometry 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