Multiplicative bases

MultiplicativeBasisDeformations.Foundations.Bockstein

Supported representatives through the connecting map (Corollary 10.5, coefficient form) #

cor:zero-supported-coverage (integral-deformations.tex) on the coefficient complexes of CharComplex, with ๐’ช = โ„ค/4 and the sequence 0 โ†’ ๐”ฝโ‚‚ โ†’ ๐’ช โ†’ ๐”ฝโ‚‚ โ†’ 0: Lemma 10.4 (supported_bockstein) applies to Cยน โ†’ Cยฒ โ†’ Cยณ of character ฯ‡ with U the pairs (u, v) with uv = 0 whose stem product is the ray wโ‚‚(u, v). Condition (2) is Theorem 9.1(3): a derivation modulo two has nonzero-product Leibniz coefficients (IsSol), which lift to โ„ค by integral_lifting; the lifted coboundary vanishes on nonzero products and lands in the stem lines at zero products (d1_isSol_mem_U). Condition (1) is Proposition 10.3 (IStar). This gives the corollary over ๐”ฝโ‚‚ (cor105_coeffโ‚‚); "It may be chosen over ๐”ฝโ‚‚ and then extended to k": a class over k has a coordinate class over ๐”ฝโ‚‚ which is not a coboundary, and a retraction k โ†’ ๐”ฝโ‚‚ shows that its supported representative stays a non-coboundary over k (cor105_coeff).

source
theorem MultiplicativeBasisDeformations.GExt.isHCocycle_hcobdry {R : Type u_1} [CommRing R] {ฮ› : Type u_2} [Ring ฮ›] [Algebra R ฮ›] (h : ฮ› โ†’โ‚—[R] ฮ›) :
IsHCocycle (hcobdry h)

A coboundary is a cocycle.

The complex as linear maps #

source
@[reducible, inline]
abbrev MultiplicativeBasisDeformations.RaySys.Sys.T3 {V R L : Type} [AddCommGroup L] [DecidableEq L] [DecidableEq V] [Fintype R] (S : Sys V R L) (ฯ‡ : L) :
Type

The index set of three-cochain coefficients.

Instances For
    source
    noncomputable def MultiplicativeBasisDeformations.RaySys.Sys.d1L {V R L : Type} [AddCommGroup L] [DecidableEq L] [Fintype V] [DecidableEq V] [Fintype R] [DecidableEq R] (S : Sys V R L) (ฯ‡ : L) (O : Type u) [CommRing O] [Nontrivial O] :
    S.C1 ฯ‡ O โ†’โ‚—[O] S.C2 ฯ‡ O

    dโ‚ as a linear map.

    Instances For
      source
      noncomputable def MultiplicativeBasisDeformations.RaySys.Sys.d2L {V R L : Type} [AddCommGroup L] [DecidableEq L] [Fintype V] [DecidableEq V] [Fintype R] [DecidableEq R] (S : Sys V R L) (ฯ‡ : L) (O : Type u) [CommRing O] [Nontrivial O] :
      S.C2 ฯ‡ O โ†’โ‚—[O] S.T3 ฯ‡ โ†’ O

      dโ‚‚ as a linear map.

      Instances For
        source
        theorem MultiplicativeBasisDeformations.RaySys.Sys.d1L_apply {V R L : Type} [AddCommGroup L] [DecidableEq L] [Fintype V] [DecidableEq V] [Fintype R] [DecidableEq R] (S : Sys V R L) (ฯ‡ : L) (O : Type u) [CommRing O] [Nontrivial O] (f : S.C1 ฯ‡ O) :
        (S.d1L ฯ‡ O) f = S.d1 ฯ‡ O f
        source
        theorem MultiplicativeBasisDeformations.RaySys.Sys.d2L_apply {V R L : Type} [AddCommGroup L] [DecidableEq L] [Fintype V] [DecidableEq V] [Fintype R] [DecidableEq R] (S : Sys V R L) (ฯ‡ : L) (O : Type u) [CommRing O] [Nontrivial O] (c : S.C2 ฯ‡ O) (t : S.T3 ฯ‡) :
        (S.d2L ฯ‡ O) c t = S.d2raw ฯ‡ O c (โ†‘t).1 (โ†‘t).2.1 (โ†‘t).2.2
        source
        theorem MultiplicativeBasisDeformations.RaySys.Sys.d2L_d1L {V R L : Type} [AddCommGroup L] [DecidableEq L] [Fintype V] [DecidableEq V] [Fintype R] [DecidableEq R] (S : Sys V R L) (ฯ‡ : L) (O : Type u) [CommRing O] [Nontrivial O] (f : S.C1 ฯ‡ O) :
        (S.d2L ฯ‡ O) ((S.d1L ฯ‡ O) f) = 0
        source
        def MultiplicativeBasisDeformations.RaySys.Sys.UC {V R L : Type} [AddCommGroup L] [DecidableEq L] [DecidableEq V] [Fintype R] [DecidableEq R] (S : Sys V R L) (ฯ‡ : L) (p : R ร— R) :
        Prop

        The coordinates of U: zero products whose stem product is the ray wโ‚‚.

        Instances For
          source
          def MultiplicativeBasisDeformations.RaySys.Sys.Usub {V R L : Type} [AddCommGroup L] [DecidableEq L] [DecidableEq V] [Fintype R] [DecidableEq R] (S : Sys V R L) (ฯ‡ : L) (O : Type u) [CommRing O] :
          Submodule O (S.C2 ฯ‡ O)

          The supported cochains.

          Instances For

            Solutions of the Leibniz equations #

            source
            theorem MultiplicativeBasisDeformations.RaySys.Sys.IsSol.map {V R L : Type} [AddCommGroup L] [DecidableEq L] [Fintype V] [DecidableEq V] [Fintype R] [DecidableEq R] (S : Sys V R L) {ฯ‡ : L} {M : Type u_1} {N : Type u_2} [AddCommGroup M] [AddCommGroup N] {d : R โ†’ M} (hd : S.IsSol ฯ‡ d) (ฯ† : M โ†’+ N) :
            S.IsSol ฯ‡ (โ‡‘ฯ† โˆ˜ d)
            source
            theorem MultiplicativeBasisDeformations.RaySys.Sys.IsSol.add {V R L : Type} [AddCommGroup L] [DecidableEq L] [Fintype V] [DecidableEq V] [Fintype R] [DecidableEq R] (S : Sys V R L) {ฯ‡ : L} {M : Type u_1} [AddCommGroup M] {d d' : R โ†’ M} (hd : S.IsSol ฯ‡ d) (hd' : S.IsSol ฯ‡ d') :
            S.IsSol ฯ‡ (d + d')
            source
            theorem MultiplicativeBasisDeformations.RaySys.Sys.IsSol.zero {V R L : Type} [AddCommGroup L] [DecidableEq L] [Fintype V] [DecidableEq V] [Fintype R] [DecidableEq R] (S : Sys V R L) {ฯ‡ : L} {M : Type u_1} [AddCommGroup M] :
            S.IsSol ฯ‡ 0
            source
            theorem MultiplicativeBasisDeformations.RaySys.Sys.IsSol.sum {V R L : Type} [AddCommGroup L] [DecidableEq L] [Fintype V] [DecidableEq V] [Fintype R] [DecidableEq R] (S : Sys V R L) {ฯ‡ : L} {M : Type u_1} [AddCommGroup M] {ฮน : Type u_2} (s : Finset ฮน) {d : ฮน โ†’ R โ†’ M} (hd : โˆ€ i โˆˆ s, S.IsSol ฯ‡ (d i)) :
            S.IsSol ฯ‡ (โˆ‘ i โˆˆ s, d i)

            The lifted coboundary is supported on stem lines #

            source
            theorem MultiplicativeBasisDeformations.RaySys.Sys.stem_eq_of_q {V R L : Type} [AddCommGroup L] [DecidableEq L] [Fintype V] [DecidableEq V] [Fintype R] [DecidableEq R] (S : Sys V R L) {r s : R} (h0 : S.rr r * S.rr s = 0) (h1 : S.rr r * S.q (S.P.tgt r) * S.rr s โ‰  0) :
            S.stem r s = S.rr r * S.q (S.P.tgt r) * S.rr s
            source
            theorem MultiplicativeBasisDeformations.RaySys.Sys.UC_of_right {V R L : Type} [AddCommGroup L] [DecidableEq L] [Fintype V] [DecidableEq V] [Fintype R] [DecidableEq R] (S : Sys V R L) {ฯ‡ : L} (hฯ‡ : 0 < S.P.deg ฯ‡) (hprim : Prim ฯ‡) {u v t : R} (hmid : S.P.tgt u = S.P.src v) (h0 : S.rr u * S.rr v = 0) (hv : S.Shift ฯ‡ v) (ht : S.P.mul u (S.succ ฯ‡ v) = some t) :
            S.UC ฯ‡ (u, v)

            A nonzero substitution u vโบ at a zero product lies on the stem line.

            source
            theorem MultiplicativeBasisDeformations.RaySys.Sys.UC_of_left {V R L : Type} [AddCommGroup L] [DecidableEq L] [Fintype V] [DecidableEq V] [Fintype R] [DecidableEq R] (S : Sys V R L) {ฯ‡ : L} (hฯ‡ : 0 < S.P.deg ฯ‡) (hprim : Prim ฯ‡) {u v t : R} (h0 : S.rr u * S.rr v = 0) (hu : S.Shift ฯ‡ u) (ht : S.P.mul (S.succ ฯ‡ u) v = some t) :
            S.UC ฯ‡ (u, v)

            A nonzero substitution uโบ v at a zero product lies on the stem line.

            source
            theorem MultiplicativeBasisDeformations.RaySys.Sys.d1_isSol_mem_U {V R L : Type} [AddCommGroup L] [DecidableEq L] [Fintype V] [DecidableEq V] [Fintype R] [DecidableEq R] (S : Sys V R L) {ฯ‡ : L} (hฯ‡ : 0 < S.P.deg ฯ‡) (hprim : Prim ฯ‡) (O : Type u) [CommRing O] [Nontrivial O] {ฮด : R โ†’ O} (hฮด : S.IsSol ฯ‡ ฮด) :
            (S.d1 ฯ‡ O fun (r : { r : R // S.Shift ฯ‡ r }) => ฮด โ†‘r) โˆˆ S.Usub ฯ‡ O

            The coboundary of a solution of the nonzero-product Leibniz equations is supported on the stem lines of zero products (cor:zero-supported-coverage, proof).

            source
            theorem MultiplicativeBasisDeformations.RaySys.Sys.shift_succ_iff {V R L : Type} [AddCommGroup L] [DecidableEq L] [Fintype V] [DecidableEq V] [Fintype R] [DecidableEq R] (S : Sys V R L) {ฯ‡ : L} {u v t : R} (hp : S.rr u * S.rr v = S.rr t) :
            S.Shift ฯ‡ u โˆง (S.P.mul (S.succ ฯ‡ u) v).isSome = true โ†” S.EL ฯ‡ u v t
            source
            theorem MultiplicativeBasisDeformations.RaySys.Sys.shift_succ_iff' {V R L : Type} [AddCommGroup L] [DecidableEq L] [Fintype V] [DecidableEq V] [Fintype R] [DecidableEq R] (S : Sys V R L) {ฯ‡ : L} {u v t : R} (hu0 : u โ‰  S.P.e (S.P.src u)) (hp : S.rr u * S.rr v = S.rr t) :
            S.Shift ฯ‡ v โˆง (S.P.mul u (S.succ ฯ‡ v)).isSome = true โ†” S.ER ฯ‡ u v t
            source
            noncomputable def MultiplicativeBasisDeformations.RaySys.Sys.ext1 {V R L : Type} [AddCommGroup L] (S : Sys V R L) (ฯ‡ : L) {O : Type u} [Zero O] (f : { r : R // S.Shift ฯ‡ r } โ†’ O) (r : R) :
            O

            A one-cochain as a function on all rays (zero on unshiftable rays).

            Instances For
              source
              theorem MultiplicativeBasisDeformations.RaySys.Sys.isSol_of_d1 {V R L : Type} [AddCommGroup L] [DecidableEq L] [Fintype V] [DecidableEq V] [Fintype R] [DecidableEq R] (S : Sys V R L) {ฯ‡ : L} (O : Type u) [CommRing O] [Nontrivial O] (f : S.C1 ฯ‡ O) (hf : S.d1 ฯ‡ O f = 0) :
              S.IsSol ฯ‡ (S.ext1 ฯ‡ f)

              A one-cocycle gives a solution of the nonzero-product Leibniz equations.

              Condition (2): lifting derivations to โ„ค/4 #

              source
              theorem MultiplicativeBasisDeformations.RaySys.Sys.exists_Z4_isSol {V R L : Type} [AddCommGroup L] [DecidableEq L] [Fintype V] [DecidableEq V] [Fintype R] [DecidableEq R] (S : Sys V R L) {ฯ‡ : L} (k : Type u) [Field k] [IsAlgClosed k] (hfin : IsRepresentationFinite k โ†ฅ(S.P.Lin k)) (hฯ‡ : 0 < S.P.deg ฯ‡) (hprim : Prim ฯ‡) (hW : โˆ€ (w : R โ†’ ZMod 2), (โˆ€ (r s t : R), S.TB ฯ‡ r โ†’ S.TB ฯ‡ s โ†’ S.TB ฯ‡ t โ†’ S.rr r * S.rr s = S.rr t โ†’ w t = w r + w s) โ†’ โˆƒ (ฯ‰ : R โ†’ โ„ค), (โˆ€ (r s t : R), S.TB ฯ‡ r โ†’ S.TB ฯ‡ s โ†’ S.TB ฯ‡ t โ†’ S.rr r * S.rr s = S.rr t โ†’ ฯ‰ t = ฯ‰ r + ฯ‰ s) โˆง โˆ€ (r : R), S.TB ฯ‡ r โ†’ โ†‘(ฯ‰ r) = w r) {d : R โ†’ ZMod 2} (hd : S.IsSol ฯ‡ d) :
              โˆƒ (D : R โ†’ ZMod 4), S.IsSol ฯ‡ D โˆง โˆ€ (r : R), Z4.red (D r) = d r

              Solutions with values in ๐”ฝโ‚‚ lift to ๐’ช = โ„ค/4: Theorem 9.1(3).

              source
              theorem MultiplicativeBasisDeformations.RaySys.Sys.cond2 {V R L : Type} [AddCommGroup L] [DecidableEq L] [Fintype V] [DecidableEq V] [Fintype R] [DecidableEq R] (S : Sys V R L) (ฯ‡ : L) (k : Type u) [Field k] [IsAlgClosed k] (hfin : IsRepresentationFinite k โ†ฅ(S.P.Lin k)) (hฯ‡ : 0 < S.P.deg ฯ‡) (hprim : Prim ฯ‡) (hW : โˆ€ (w : R โ†’ ZMod 2), (โˆ€ (r s t : R), S.TB ฯ‡ r โ†’ S.TB ฯ‡ s โ†’ S.TB ฯ‡ t โ†’ S.rr r * S.rr s = S.rr t โ†’ w t = w r + w s) โ†’ โˆƒ (ฯ‰ : R โ†’ โ„ค), (โˆ€ (r s t : R), S.TB ฯ‡ r โ†’ S.TB ฯ‡ s โ†’ S.TB ฯ‡ t โ†’ S.rr r * S.rr s = S.rr t โ†’ ฯ‰ t = ฯ‰ r + ฯ‰ s) โˆง โˆ€ (r : R), S.TB ฯ‡ r โ†’ โ†‘(ฯ‰ r) = w r) (ฮด : S.C1 ฯ‡ (ZMod 4)) (hฮด : โˆƒ (m : S.C2 ฯ‡ (ZMod 4)), (S.d1L ฯ‡ (ZMod 4)) ฮด = 2 โ€ข m) :
              โˆƒ (ฮต : S.C1 ฯ‡ (ZMod 4)), (S.d1L ฯ‡ (ZMod 4)) (ฮด + 2 โ€ข ฮต) โˆˆ S.Usub ฯ‡ (ZMod 4)

              Condition (2) of Lemma 10.4.

              source
              def MultiplicativeBasisDeformations.RaySys.Sys.IStar {V R L : Type} [AddCommGroup L] [DecidableEq L] [Fintype V] [DecidableEq V] [Fintype R] [DecidableEq R] (S : Sys V R L) (ฯ‡ : L) :
              Prop

              Proposition 10.3 in coefficients (prop:integral-bockstein, i_* = 0): twice a cochain over ๐’ช = โ„ค/4 whose reduction is a cocycle is a coboundary.

              Instances For
                source
                theorem MultiplicativeBasisDeformations.RaySys.Sys.beta_surjective {V R L : Type} [AddCommGroup L] [DecidableEq L] [Fintype V] [DecidableEq V] [Fintype R] [DecidableEq R] (S : Sys V R L) (ฯ‡ : L) (hI : S.IStar ฯ‡) (c : S.C2 ฯ‡ (ZMod 2)) (hc : (S.d2L ฯ‡ (ZMod 2)) c = 0) :
                โˆƒ (ฮด : S.C1 ฯ‡ (ZMod 4)), (S.d1L ฯ‡ (ZMod 4)) ฮด = 2 โ€ข Z4.lift โˆ˜ c โˆง S.d1 ฯ‡ (ZMod 2) (โ‡‘Z4.red โˆ˜ ฮด) = 0

                Proposition 10.3, surjectivity of the connecting map (prop:integral-bockstein): every two-cocycle c over ๐”ฝโ‚‚ of character ฯ‡ is ฮฒ of a derivation: there is a one-cochain ฮด over ๐’ช = โ„ค/4 with dฮด = 2cฬƒ whose reduction is a cocycle, i.e. c = (dฮด)/2.

                source
                theorem MultiplicativeBasisDeformations.RaySys.Sys.ann_two {ฮน : Type u_1} (m : ฮน โ†’ ZMod 4) (h : 2 โ€ข m = 0) :
                โˆƒ (m' : ฮน โ†’ ZMod 4), m = 2 โ€ข m'
                source
                theorem MultiplicativeBasisDeformations.RaySys.Sys.cor105_coeffโ‚‚ {V R L : Type} [AddCommGroup L] [DecidableEq L] [Fintype V] [DecidableEq V] [Fintype R] [DecidableEq R] (S : Sys V R L) (ฯ‡ : L) (k : Type u) [Field k] [IsAlgClosed k] (hfin : IsRepresentationFinite k โ†ฅ(S.P.Lin k)) (hฯ‡ : 0 < S.P.deg ฯ‡) (hprim : Prim ฯ‡) (hW : โˆ€ (w : R โ†’ ZMod 2), (โˆ€ (r s t : R), S.TB ฯ‡ r โ†’ S.TB ฯ‡ s โ†’ S.TB ฯ‡ t โ†’ S.rr r * S.rr s = S.rr t โ†’ w t = w r + w s) โ†’ โˆƒ (ฯ‰ : R โ†’ โ„ค), (โˆ€ (r s t : R), S.TB ฯ‡ r โ†’ S.TB ฯ‡ s โ†’ S.TB ฯ‡ t โ†’ S.rr r * S.rr s = S.rr t โ†’ ฯ‰ t = ฯ‰ r + ฯ‰ s) โˆง โˆ€ (r : R), S.TB ฯ‡ r โ†’ โ†‘(ฯ‰ r) = w r) (hI : S.IStar ฯ‡) (c : S.C2 ฯ‡ (ZMod 2)) (hc : (S.d2L ฯ‡ (ZMod 2)) c = 0) (hnc : ยฌโˆƒ (f : S.C1 ฯ‡ (ZMod 2)), c = S.d1 ฯ‡ (ZMod 2) f) :
                โˆƒ u โˆˆ S.Usub ฯ‡ (ZMod 2), (S.d2L ฯ‡ (ZMod 2)) u = 0 โˆง ยฌโˆƒ (f : S.C1 ฯ‡ (ZMod 2)), u = S.d1 ฯ‡ (ZMod 2) f

                Corollary 10.5 over ๐”ฝโ‚‚ (cor:zero-supported-coverage): given Proposition 10.3, a cocycle of character ฯ‡ which is not a coboundary yields one supported on the stem lines of zero products which is not a coboundary.

                source
                theorem MultiplicativeBasisDeformations.RaySys.Sys.cor105_coeff {V R L : Type} [AddCommGroup L] [DecidableEq L] [Fintype V] [DecidableEq V] [Fintype R] [DecidableEq R] (S : Sys V R L) (ฯ‡ : L) (k : Type u) [Field k] [IsAlgClosed k] [CharP k 2] (hfin : IsRepresentationFinite k โ†ฅ(S.P.Lin k)) (hฯ‡ : 0 < S.P.deg ฯ‡) (hprim : Prim ฯ‡) (hW : โˆ€ (w : R โ†’ ZMod 2), (โˆ€ (r s t : R), S.TB ฯ‡ r โ†’ S.TB ฯ‡ s โ†’ S.TB ฯ‡ t โ†’ S.rr r * S.rr s = S.rr t โ†’ w t = w r + w s) โ†’ โˆƒ (ฯ‰ : R โ†’ โ„ค), (โˆ€ (r s t : R), S.TB ฯ‡ r โ†’ S.TB ฯ‡ s โ†’ S.TB ฯ‡ t โ†’ S.rr r * S.rr s = S.rr t โ†’ ฯ‰ t = ฯ‰ r + ฯ‰ s) โˆง โˆ€ (r : R), S.TB ฯ‡ r โ†’ โ†‘(ฯ‰ r) = w r) (hI : S.IStar ฯ‡) (c : S.C2 ฯ‡ k) (hc : (S.d2L ฯ‡ k) c = 0) (hnc : ยฌโˆƒ (f : S.C1 ฯ‡ k), c = S.d1 ฯ‡ k f) :
                โˆƒ u โˆˆ S.Usub ฯ‡ k, (S.d2L ฯ‡ k) u = 0 โˆง ยฌโˆƒ (f : S.C1 ฯ‡ k), u = S.d1 ฯ‡ k f

                Corollary 10.5 in coefficients (cor:zero-supported-coverage), over k: the corollary over ๐”ฝโ‚‚, extended to k.