Documentation

Mathlib.LinearAlgebra.QuadraticForm.QuadraticModuleCat

The category of quadratic modules #

source
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
    source
    instance QuadraticModuleCat.instCoeSortQuadraticModuleCatType {R : Type u} [CommRing R] :
    CoeSort (QuadraticModuleCat R) (Type v)
    Equations
    • QuadraticModuleCat.instCoeSortQuadraticModuleCatType = { coe := fun (x : QuadraticModuleCat R) => ↑x.toModuleCat }
    source
    @[simp]
    theorem QuadraticModuleCat.moduleCat_of_toModuleCat {R : Type u} [CommRing R] (X : QuadraticModuleCat R) :
    ModuleCat.of R ↑X.toModuleCat = X.toModuleCat
    source
    @[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
    source
    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
    Instances For
      source
      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
      source
      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
      source
      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

      Instances For
        source
        theorem QuadraticModuleCat.Hom.toIsometry_injective {R : Type u} [CommRing R] (V : QuadraticModuleCat R) (W : QuadraticModuleCat R) :
        Function.Injective QuadraticModuleCat.Hom.toIsometry
        source
        instance QuadraticModuleCat.category {R : Type u} [CommRing R] :
        CategoryTheory.Category.{v, max (v + 1) u} (QuadraticModuleCat R)
        Equations
        source
        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
        source
        @[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
        Instances For
          source
          @[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
          source
          @[simp]
          theorem QuadraticModuleCat.toIsometry_id {R : Type u} [CommRing R] {M : QuadraticModuleCat R} :
          (CategoryTheory.CategoryStruct.id M).toIsometry = QuadraticForm.Isometry.id M.form
          source
          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.
          source
          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.
          source
          @[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
          source
          @[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
          source
          @[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)
          source
          @[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
          source
          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.
          Instances For
            source
            @[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₁)
            source
            @[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
            source
            @[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
            source
            @[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
            source
            @[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).invFun a = i.inv.toIsometry a
            source
            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.
            Instances For
              source
              @[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
              source
              @[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)
              source
              @[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)