Documentation

Q2Presentation.Lifting.SimpleDuality

source
theorem Q2Presentation.Lifting.char2_add_self {A : Type} [AddCommGroup A] [Module (ZMod 2) A] (a : A) :
a + a = 0

a + a = 0 in an F₂-module.

source
theorem Q2Presentation.Lifting.char2_add_eq_zero_iff {A : Type} [AddCommGroup A] [Module (ZMod 2) A] (a b : A) :
a + b = 0 ↔ a = b

a + b = 0 ↔ a = b in an F₂-module.

source
theorem Q2Presentation.Lifting.one_add_one_eq_zero_End {A : Type} [AddCommGroup A] [Module (ZMod 2) A] :
1 + 1 = 0

1 + 1 = 0 in End of an F₂-module.

source
theorem Q2Presentation.Lifting.eq_zero_of_unit_apply {A : Type} [AddCommGroup A] [Module (ZMod 2) A] {f : Module.End (ZMod 2) A} (hf : IsUnit f) {a : A} (ha : f a = 0) :
a = 0

Kernel-triviality from a unit endomorphism.

source
theorem Q2Presentation.Lifting.unit_apply_inj {A : Type} [AddCommGroup A] [Module (ZMod 2) A] {f : Module.End (ZMod 2) A} (hf : IsUnit f) {a b : A} (h : f a = f b) :
a = b

Value-injectivity from a unit endomorphism.

source
theorem Q2Presentation.Lifting.mem_Z1_iff {A : Type} [AddCommGroup A] [Module (ZMod 2) A] (Sinv T P : Module.End (ZMod 2) A) (w : A × A × A × A) :
w ∈ Z1 Sinv T P ↔ (Sinv * (1 + T)) w.1 + (Sinv + 1 + T) w.2.1 = 0 ∧ P w.2.1 + (P + Sinv) w.2.2.2 = 0

Membership in Z¹ unfolded to the two rows.

Case (i): trivial inertia (T = 1, P = 1) #

source
theorem Q2Presentation.Lifting.mem_Z1_case_i {A : Type} [AddCommGroup A] [Module (ZMod 2) A] (Sinv : Module.End (ZMod 2) A) (hSinv_unit : IsUnit Sinv) (hSone_unit : IsUnit (Sinv + 1)) (w : A × A × A × A) :
w ∈ Z1 Sinv 1 1 ↔ w.2.1 = 0 ∧ w.2.2.2 = 0

Case (i) cocycles: (a,b,c,d) ∈ Z¹ ↔ b = 0 ∧ d = 0.

source
def Q2Presentation.Lifting.Z1_case_i_equiv {A : Type} [AddCommGroup A] [Module (ZMod 2) A] (Sinv : Module.End (ZMod 2) A) (hSinv_unit : IsUnit Sinv) (hSone_unit : IsUnit (Sinv + 1)) :
↥(Z1 Sinv 1 1) ≃ₗ[ZMod 2] A × A

Case (i) cocycles are a free rank-two A-space.

Equations
  • One or more equations did not get rendered due to their size.
Instances For
    source
    theorem Q2Presentation.Lifting.Z1_card_case_i {A : Type} [AddCommGroup A] [Module (ZMod 2) A] (Sinv : Module.End (ZMod 2) A) (hSinv_unit : IsUnit Sinv) (hSone_unit : IsUnit (Sinv + 1)) :
    Nat.card ↥(Z1 Sinv 1 1) = Nat.card A * Nat.card A

    Case (i) count: |Z¹| = |A|².

    Case (ii): vanishing inertia fixed space (P = 0) #

    source
    def Q2Presentation.Lifting.caseIISol {A : Type} [AddCommGroup A] [Module (ZMod 2) A] (Sinv T : Module.End (ZMod 2) A) (hSinv_unit : IsUnit Sinv) (hTone_unit : IsUnit (1 + T)) :
    Module.End (ZMod 2) A

    The tame-row solution operator.

    Equations
    Instances For
      source
      theorem Q2Presentation.Lifting.caseIISol_spec {A : Type} [AddCommGroup A] [Module (ZMod 2) A] (Sinv T : Module.End (ZMod 2) A) (hSinv_unit : IsUnit Sinv) (hTone_unit : IsUnit (1 + T)) (b : A) :
      (Sinv * (1 + T)) ((caseIISol Sinv T hSinv_unit hTone_unit) b) = (Sinv + 1 + T) b
      source
      theorem Q2Presentation.Lifting.mem_Z1_case_ii {A : Type} [AddCommGroup A] [Module (ZMod 2) A] (Sinv T : Module.End (ZMod 2) A) (hSinv_unit : IsUnit Sinv) (hTone_unit : IsUnit (1 + T)) (w : A × A × A × A) :
      w ∈ Z1 Sinv T 0 ↔ w.1 = (caseIISol Sinv T hSinv_unit hTone_unit) w.2.1 ∧ w.2.2.2 = 0

      Case (ii) cocycles: d = 0 and a solves the tame row against b.

      source
      def Q2Presentation.Lifting.Z1_case_ii_equiv {A : Type} [AddCommGroup A] [Module (ZMod 2) A] (Sinv T : Module.End (ZMod 2) A) (hSinv_unit : IsUnit Sinv) (hTone_unit : IsUnit (1 + T)) :
      ↥(Z1 Sinv T 0) ≃ₗ[ZMod 2] A × A

      Case (ii) cocycles are a free rank-two A-space (coordinates (b, c)).

      Equations
      • One or more equations did not get rendered due to their size.
      Instances For
        source
        theorem Q2Presentation.Lifting.Z1_card_case_ii {A : Type} [AddCommGroup A] [Module (ZMod 2) A] (Sinv T : Module.End (ZMod 2) A) (hSinv_unit : IsUnit Sinv) (hTone_unit : IsUnit (1 + T)) :
        Nat.card ↥(Z1 Sinv T 0) = Nat.card A * Nat.card A

        Case (ii) count: |Z¹| = |A|².

        The trivial module (all operators 1, P = 1): |Z¹| = |A|³ #

        source
        theorem Q2Presentation.Lifting.mem_Z1_trivial {A : Type} [AddCommGroup A] [Module (ZMod 2) A] (w : A × A × A × A) :
        w ∈ Z1 1 1 1 ↔ w.2.1 = 0

        Trivial-case cocycles: (a,b,c,d) ∈ Z¹ ↔ b = 0.

        source
        def Q2Presentation.Lifting.Z1_trivial_equiv {A : Type} [AddCommGroup A] [Module (ZMod 2) A] :
        ↥(Z1 1 1 1) ≃ₗ[ZMod 2] A × A × A

        Trivial-case cocycles are free of rank three.

        Equations
        • One or more equations did not get rendered due to their size.
        Instances For
          source
          theorem Q2Presentation.Lifting.Z1_card_trivial {A : Type} [AddCommGroup A] [Module (ZMod 2) A] :
          Nat.card ↥(Z1 1 1 1) = Nat.card A * (Nat.card A * Nat.card A)

          Trivial-case count: |Z¹| = |A|³.

          The H²-side: surjective d¹ kills the obstruction group #

          source
          theorem Q2Presentation.Lifting.H2_card_eq_one_of_surjective {A : Type} [AddCommGroup A] [Module (ZMod 2) A] (S₀ T₀ P₀ : Module.End (ZMod 2) A) (hsurj : Function.Surjective ⇑(d1 S₀ T₀ P₀)) :
          Nat.card (H2 S₀ T₀ P₀) = 1

          Surjective d¹ forces |H²| = 1.

          d¹-surjectivity in the two simple cases #

          source
          theorem Q2Presentation.Lifting.d1_surjective_case_i {A : Type} [AddCommGroup A] [Module (ZMod 2) A] (Sinv : Module.End (ZMod 2) A) (hSinv_unit : IsUnit Sinv) (hSone_unit : IsUnit (Sinv + 1)) :
          Function.Surjective ⇑(d1 Sinv 1 1)

          Case (i) (T = 1, P = 1): d¹ is surjective.

          source
          theorem Q2Presentation.Lifting.H2_card_case_i {A : Type} [AddCommGroup A] [Module (ZMod 2) A] (Sinv : Module.End (ZMod 2) A) (hSinv_unit : IsUnit Sinv) (hSone_unit : IsUnit (Sinv + 1)) :
          Nat.card (H2 Sinv 1 1) = 1

          Case (i): |H²| = 1.

          source
          theorem Q2Presentation.Lifting.d1_surjective_case_ii {A : Type} [AddCommGroup A] [Module (ZMod 2) A] (Sinv T : Module.End (ZMod 2) A) (hSinv_unit : IsUnit Sinv) (hTone_unit : IsUnit (1 + T)) :
          Function.Surjective ⇑(d1 Sinv T 0)

          Case (ii) (P = 0): d¹ is surjective.

          source
          theorem Q2Presentation.Lifting.H2_card_case_ii {A : Type} [AddCommGroup A] [Module (ZMod 2) A] (Sinv T : Module.End (ZMod 2) A) (hSinv_unit : IsUnit Sinv) (hTone_unit : IsUnit (1 + T)) :
          Nat.card (H2 Sinv T 0) = 1

          Case (ii): |H²| = 1.

          Trivial-case H²: the obstruction group is A itself #

          source
          theorem Q2Presentation.Lifting.d1_trivial_apply {A : Type} [AddCommGroup A] [Module (ZMod 2) A] (a b c d : A) :
          (d1 1 1 1) (a, b, c, d) = (b, b)

          d¹ at the trivial module: (a,b,c,d) ↦ (b, b).

          source
          def Q2Presentation.Lifting.trivialSum {A : Type} [AddCommGroup A] [Module (ZMod 2) A] :
          A × A →ₗ[ZMod 2] A

          The fold map (u,v) ↦ u + v.

          Equations
          Instances For
            source
            theorem Q2Presentation.Lifting.trivialSum_apply {A : Type} [AddCommGroup A] [Module (ZMod 2) A] (u v : A) :
            trivialSum (u, v) = u + v
            source
            theorem Q2Presentation.Lifting.trivialSum_surjective {A : Type} [AddCommGroup A] [Module (ZMod 2) A] :
            Function.Surjective ⇑trivialSum
            source
            theorem Q2Presentation.Lifting.range_d1_trivial {A : Type} [AddCommGroup A] [Module (ZMod 2) A] :
            (d1 1 1 1).range = trivialSum.ker

            The image of d¹ at the trivial module is the antidiagonal (= diagonal, char 2), i.e. the kernel of the fold.

            source
            noncomputable def Q2Presentation.Lifting.H2_trivial_equiv {A : Type} [AddCommGroup A] [Module (ZMod 2) A] :
            H2 1 1 1 ≃ₗ[ZMod 2] A

            Trivial-case H²: the obstruction group is A.

            Equations
            • One or more equations did not get rendered due to their size.
            Instances For
              source
              theorem Q2Presentation.Lifting.H2_card_trivial {A : Type} [AddCommGroup A] [Module (ZMod 2) A] :
              Nat.card (H2 1 1 1) = Nat.card A

              Trivial-case count: |H²| = |A|.

              Rank–nullity: |Z¹|·|A|² = |A|⁴·|H²| #

              source
              theorem Q2Presentation.Lifting.card_submodule_mul_card_quotient {M : Type} [AddCommGroup M] [Module (ZMod 2) M] (p : Submodule (ZMod 2) M) :
              Nat.card ↥p * Nat.card (M ⧸ p) = Nat.card M

              Cardinality splits across a submodule and its quotient (vector-space case).

              source
              theorem Q2Presentation.Lifting.Z1_card_mul_H2 {A : Type} [AddCommGroup A] [Module (ZMod 2) A] (S₀ T₀ P₀ : Module.End (ZMod 2) A) :
              Nat.card ↥(Z1 S₀ T₀ P₀) * Nat.card A ^ 2 = Nat.card A ^ 4 * Nat.card (H2 S₀ T₀ P₀)

              Rank–nullity for the word complex (multiplicative, unconditional): |Z¹|·|A|² = |A|⁴·|H²|. With the case-computed |H²| this yields the manuscript count |Z¹| = 2^{2·dim A + dim (A^∨)^C} module-by-module.

              source
              theorem Q2Presentation.Lifting.Z1_card_eq_of_finite {A : Type} [AddCommGroup A] [Module (ZMod 2) A] [Finite A] (S₀ T₀ P₀ : Module.End (ZMod 2) A) :
              Nat.card ↥(Z1 S₀ T₀ P₀) = Nat.card A ^ 2 * Nat.card (H2 S₀ T₀ P₀)

              Rank–nullity, divided form (finite A): |Z¹| = |A|²·|H²|.