theorem
Q2Presentation.Lifting.add_self_eq_zero_V
{V : Type}
[AddCommGroup V]
[Module (ZMod 2) V]
(x : V)
:
Char 2 in any F₂-module.
Generic single-slot tuples.
Instances For
@[simp]
theorem
Q2Presentation.Lifting.famSingle_same
{V : Type}
[AddCommGroup V]
[Module (ZMod 2) V]
(a : Gen)
(x : V)
:
theorem
Q2Presentation.Lifting.foxShadowGen_single_of_not_mentions
{Yt : BoundaryFramedTarget}
[Finite Yt.Y]
{V : Type}
[AddCommGroup V]
[Module (ZMod 2) V]
(Φ : OperatorFamily Yt V)
(q : Marking Yt.Y)
(a : Gen)
(x : V)
(w : GExpr)
(hw : mentions w a = false)
:
Support vanishing at family level.
theorem
Q2Presentation.Lifting.foxShadowGen_tameRelator
{Yt : BoundaryFramedTarget}
[Finite Yt.Y]
{V : Type}
[AddCommGroup V]
[Module (ZMod 2) V]
(Φ : OperatorFamily Yt V)
(q : Marking Yt.Y)
(n : Gen → V)
:
The tame shadow, unfolded (definitional recursion).
theorem
Q2Presentation.Lifting.foxShadowGen_tameRelator_factored
{Yt : BoundaryFramedTarget}
[Finite Yt.Y]
{V : Type}
[AddCommGroup V]
[Module (ZMod 2) V]
(Φ : OperatorFamily Yt V)
(q : Marking Yt.Y)
(n : Gen → V)
:
Tame-row factorization at family level.
theorem
Q2Presentation.Lifting.foxShadowGen_wild_x1_column
{Yt : BoundaryFramedTarget}
[Finite Yt.Y]
{V : Type}
[AddCommGroup V]
[Module (ZMod 2) V]
(Φ : OperatorFamily Yt V)
(q : Marking Yt.Y)
(d : V)
:
foxShadowGen Φ.op q (famSingle Gen.x1 d) Q2Word.wildRelator = (Φ.op (Q2Word.c0.eval q))
((Φ.op ((Q2Word.rconjExpr Q2Word.x1 Q2Word.sigma).eval q))
((Φ.op (Q2Word.u1.eval q)⁻¹)
((∑ i ∈ Finset.range (omega2Mod (Nat.card Yt.Y)).val, Φ.op ((Q2Word.x1.mul Q2Word.tau).eval q) ^ i)
((Φ.op (q Gen.tau)) d))) + (Φ.op (q Gen.sigma)) d)
The wild x₁-column at family level.
theorem
Q2Presentation.Lifting.foxShadowGen_add
{Yt : BoundaryFramedTarget}
[Finite Yt.Y]
{V : Type}
[AddCommGroup V]
[Module (ZMod 2) V]
(Φ : OperatorFamily Yt V)
(q : Marking Yt.Y)
(n₁ n₂ : Gen → V)
(w : GExpr)
:
Additivity of the family shadow in the perturbation.
theorem
Q2Presentation.Lifting.sum_range_one_pow_of_odd_V
{V : Type}
[AddCommGroup V]
[Module (ZMod 2) V]
{R : ℕ}
(hodd : Odd R)
:
Odd sums of the identity collapse (char 2).
theorem
Q2Presentation.Lifting.fam_rconj_collapse
{Yt : BoundaryFramedTarget}
[Finite Yt.Y]
{V : Type}
[AddCommGroup V]
[Module (ZMod 2) V]
(Φ : OperatorFamily Yt V)
(q : Marking Yt.Y)
(hx1 : Φ.op (q Gen.x1) = 1)
:
theorem
Q2Presentation.Lifting.fam_pop_collapse
{Yt : BoundaryFramedTarget}
[Finite Yt.Y]
{V : Type}
[AddCommGroup V]
[Module (ZMod 2) V]
(Φ : OperatorFamily Yt V)
(q : Marking Yt.Y)
(hx1 : Φ.op (q Gen.x1) = 1)
(hT : Φ.op (q Gen.tau) = 1)
(htwo : 2 ∣ Nat.card Yt.Y)
:
theorem
Q2Presentation.Lifting.fam_wild_x1_column_case_i
{Yt : BoundaryFramedTarget}
[Finite Yt.Y]
{V : Type}
[AddCommGroup V]
[Module (ZMod 2) V]
(Φ : OperatorFamily Yt V)
(q : Marking Yt.Y)
(hx1 : Φ.op (q Gen.x1) = 1)
(hT : Φ.op (q Gen.tau) = 1)
(htwo : 2 ∣ Nat.card Yt.Y)
(d : V)
:
theorem
Q2Presentation.Lifting.famRows_surjective_case_i
{Yt : BoundaryFramedTarget}
[Finite Yt.Y]
{V : Type}
[AddCommGroup V]
[Module (ZMod 2) V]
(Φ : OperatorFamily Yt V)
(q : Marking Yt.Y)
(htwo : 2 ∣ Nat.card Yt.Y)
(hx1 : Φ.op (q Gen.x1) = 1)
(hT : Φ.op (q Gen.tau) = 1)
(hSone : IsUnit (1 + Φ.op (q Gen.sigma)))
(uv : V × V)
:
∃ (n : Gen → V), (foxShadowGen Φ.op q n Q2Word.tameRelator, foxShadowGen Φ.op q n Q2Word.wildRelator) = uv
Family case (i) surjectivity, in the five-lemma's head shape.
theorem
Q2Presentation.Lifting.famRows_surjective_case_ii
{Yt : BoundaryFramedTarget}
[Finite Yt.Y]
{V : Type}
[AddCommGroup V]
[Module (ZMod 2) V]
(Φ : OperatorFamily Yt V)
(q : Marking Yt.Y)
(hPop : ∑ i ∈ Finset.range (omega2Mod (Nat.card Yt.Y)).val, Φ.op ((Q2Word.x1.mul Q2Word.tau).eval q) ^ i = 0)
(hTone : IsUnit (1 + Φ.op (q Gen.tau)))
(uv : V × V)
:
∃ (n : Gen → V), (foxShadowGen Φ.op q n Q2Word.tameRelator, foxShadowGen Φ.op q n Q2Word.wildRelator) = uv
Family case (ii) surjectivity, in the five-lemma's head shape.