The category of quadratic modules

structure QuadraticModuleCat (R : Type u) [CommRing R] extends ModuleCat : 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.instCoeSortQuadraticModuleCatType {R : Type u} [CommRing R] : CoeSort (QuadraticModuleCat R) (Type v)

Equations

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

@[simp]

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

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.mk X, form := Q }

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

theorem QuadraticModuleCat.Hom.ext_iff {R : Type u} : ∀ {inst : CommRing R} {V W : QuadraticModuleCat R} (x y : QuadraticModuleCat.Hom V W), x = y ↔ x.toIsometry = y.toIsometry

structure QuadraticModuleCat.Hom {R : Type u} [CommRing R] (V : QuadraticModuleCat R) (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.toIsometry_injective {R : Type u} [CommRing R] (V : QuadraticModuleCat R) (W : QuadraticModuleCat R) : Function.Injective QuadraticModuleCat.Hom.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 : QuadraticModuleCat R} {N : QuadraticModuleCat R} (f : M ⟶ N) (g : M ⟶ N) (h : f.toIsometry = g.toIsometry) : f = g

@[inline, reducible]

abbrev QuadraticModuleCat.ofHom {R : Type u} [CommRing R] {X : Type v} [AddCommGroup X] [Module R X] {Q₁ : QuadraticForm R X} {Q₂ : QuadraticForm R X} (f : Q₁ →qᵢ Q₂) : QuadraticModuleCat.of Q₁ ⟶ QuadraticModuleCat.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 : QuadraticModuleCat R} {N : QuadraticModuleCat R} {U : QuadraticModuleCat R} (f : M ⟶ N) (g : N ⟶ U) : (CategoryTheory.CategoryStruct.comp f g).toIsometry = QuadraticForm.Isometry.comp g.toIsometry f.toIsometry

@[simp]

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

instance QuadraticModuleCat.concreteCategory {R : Type u} [CommRing R] : CategoryTheory.ConcreteCategory (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)).toPrefunctor.obj X = ModuleCat.of R ↑X.toModuleCat

@[simp]

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

@[simp]

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

@[simp]

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

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

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

Equations

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

@[simp]

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

@[simp]

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

@[simp]

theorem QuadraticModuleCat.ofIso_trans {R : Type u} [CommRing R] {X : Type v} {Y : Type v} {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 : QuadraticForm.IsometryEquiv Q₁ Q₂) (f : QuadraticForm.IsometryEquiv Q₂ Q₃) : QuadraticModuleCat.ofIso (QuadraticForm.IsometryEquiv.trans e f) = QuadraticModuleCat.ofIso e ≪≫ QuadraticModuleCat.ofIso f

@[simp]

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

@[simp]

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

def CategoryTheory.Iso.toIsometryEquiv {R : Type u} [CommRing R] {X : QuadraticModuleCat R} {Y : QuadraticModuleCat R} (i : X ≅ Y) : QuadraticForm.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_refl {R : Type u} [CommRing R] {X : QuadraticModuleCat R} : CategoryTheory.Iso.toIsometryEquiv (CategoryTheory.Iso.refl X) = QuadraticForm.IsometryEquiv.refl X.form

@[simp]

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

@[simp]

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