Documentation

Mathlib.LinearAlgebra.QuadraticForm.QuadraticModuleCat

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.

Instances For
    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
    @[simp]
    theorem QuadraticModuleCat.of_form {R : Type u} [CommRing R] {X : Type v} [AddCommGroup X] [Module R X] (Q : QuadraticForm R X) :

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

    Equations
    Instances For
      theorem QuadraticModuleCat.Hom.ext {R : Type u} :
      ∀ {inst : CommRing R} {V W : QuadraticModuleCat R} (x y : V.Hom W), x.toIsometry = y.toIsometryx = 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

      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

      Instances For
        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
        @[reducible, inline]
        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₂) :

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

        Equations
        Instances For
          @[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 = g.toIsometry.comp f.toIsometry
          Equations
          • One or more equations did not get rendered due to their size.
          Equations
          • One or more equations did not get rendered due to their size.
          @[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)).map f = f.toIsometry.toLinearMap
          @[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 : QuadraticMap.IsometryEquiv Q₁ Q₂) :
          (QuadraticModuleCat.ofIso e).inv.toIsometry = e.symm.toIsometry
          @[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 : QuadraticMap.IsometryEquiv Q₁ Q₂) :
          (QuadraticModuleCat.ofIso e).hom.toIsometry = e.toIsometry
          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 : QuadraticMap.IsometryEquiv Q₁ 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 := }
          Instances For
            @[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 : QuadraticMap.IsometryEquiv Q₁ Q₂) :
            @[simp]
            @[simp]
            theorem CategoryTheory.Iso.toIsometryEquiv_toFun {R : Type u} [CommRing R] {X : QuadraticModuleCat R} {Y : QuadraticModuleCat R} (i : X Y) (a : X.toModuleCat) :
            i.toIsometryEquiv 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) :
            i.toIsometryEquiv.invFun a = i.inv.toIsometry a

            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' := }
            Instances For
              @[simp]
              theorem CategoryTheory.Iso.toIsometryEquiv_symm {R : Type u} [CommRing R] {X : QuadraticModuleCat R} {Y : QuadraticModuleCat R} (e : X Y) :
              e.symm.toIsometryEquiv = e.toIsometryEquiv.symm
              @[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) :
              (e ≪≫ f).toIsometryEquiv = e.toIsometryEquiv.trans f.toIsometryEquiv