Multiplicative bases

MultiplicativeBasisDeformations.Foundations.ZModFour

The coefficient ring π’ͺ = β„€/4 (Section 10) #

integral-deformations.tex: "Let π’ͺ = β„€/4. […] the coefficient sequence 0 β†’ 𝔽₂ β†’ π’ͺ β†’ 𝔽₂ β†’ 0."

The reduction red : β„€/4 β†’ 𝔽₂, the set-theoretic section lift, and the additive embedding tw : 𝔽₂ β†’ 2π’ͺ, a ↦ 2Γ£. Every statement is a finite check.

source
def MultiplicativeBasisDeformations.term𝔽₂ :
Lean.ParserDescr

𝔽₂.

Instances For
    source
    instance MultiplicativeBasisDeformations.instFactLtOfNat_multiplicativeBasisDeformations :
    Fact (1 < 4)
    source
    def MultiplicativeBasisDeformations.Z4.red :
    ZMod 4 β†’+* ZMod 2

    The reduction π’ͺ β†’ 𝔽₂.

    Instances For
      source
      def MultiplicativeBasisDeformations.Z4.lift (a : ZMod 2) :
      ZMod 4

      The section 𝔽₂ β†’ π’ͺ (not additive).

      Instances For
        source
        @[simp]
        theorem MultiplicativeBasisDeformations.Z4.red_lift (a : ZMod 2) :
        red (lift a) = a
        source
        theorem MultiplicativeBasisDeformations.Z4.lift_zero :
        lift 0 = 0
        source
        theorem MultiplicativeBasisDeformations.Z4.four_eq_zero :
        2 * 2 = 0
        source
        theorem MultiplicativeBasisDeformations.Z4.two_mul_two_mul (a : ZMod 4) :
        2 * (2 * a) = 0
        source
        theorem MultiplicativeBasisDeformations.Z4.two_mul_eq_of_red {a b : ZMod 4} (h : red a = red b) :
        2 * a = 2 * b

        2a depends only on the reduction of a.

        source
        theorem MultiplicativeBasisDeformations.Z4.two_ne_zero :
        2 β‰  0
        source
        theorem MultiplicativeBasisDeformations.Z4.two_mul_eq_zero_iff (a : ZMod 4) :
        2 * a = 0 ↔ red a = 0

        The annihilator of 2 is the kernel of the reduction.

        source
        theorem MultiplicativeBasisDeformations.Z4.exists_two_mul_of_red {a : ZMod 4} (h : red a = 0) :
        βˆƒ (b : ZMod 4), a = 2 * b

        The kernel of the reduction is 2π’ͺ.

        source
        theorem MultiplicativeBasisDeformations.Z4.exists_eq_add_two_mul {a b : ZMod 4} (h : red a = red b) :
        βˆƒ (c : ZMod 4), a = b + 2 * c

        Two lifts of the same element differ by an element of 2π’ͺ.

        source
        theorem MultiplicativeBasisDeformations.Z4.isUnit_of_red_ne_zero {a : ZMod 4} (h : red a β‰  0) :
        IsUnit a

        An element with nonzero reduction is a unit.

        source
        def MultiplicativeBasisDeformations.Z4.tw :
        ZMod 2 β†’+ ZMod 4

        The additive embedding 𝔽₂ β†’ 2π’ͺ, a ↦ 2Γ£.

        Instances For
          source
          theorem MultiplicativeBasisDeformations.Z4.tw_apply (a : ZMod 2) :
          tw a = 2 * lift a
          source
          theorem MultiplicativeBasisDeformations.Z4.tw_red (a : ZMod 4) :
          tw (red a) = 2 * a
          source
          theorem MultiplicativeBasisDeformations.Z4.tw_injective :
          Function.Injective ⇑tw
          source
          theorem MultiplicativeBasisDeformations.Z4.red_surjective :
          Function.Surjective ⇑red
          source
          theorem MultiplicativeBasisDeformations.Z4.red_two :
          red 2 = 0