def Q2Presentation.Lifting.foxShadowGen {Yt : BoundaryFramedTarget} [Finite Yt.Y] {V : Type} [AddCommGroup V] [Module (ZMod 2) V] (Φ : Yt.Y → Module.End (ZMod 2) V) (q : Marking Yt.Y) (n : Gen → V) : GExpr → V

The shadow recursion over an abstract operator family.

Equations

• Q2Presentation.Lifting.foxShadowGen Φ q n Q2Presentation.GExpr.one = 0
• Q2Presentation.Lifting.foxShadowGen Φ q n (Q2Presentation.GExpr.gen a) = n a
• Q2Presentation.Lifting.foxShadowGen Φ q n (u.mul v) = (Φ (v.eval q)) (Q2Presentation.Lifting.foxShadowGen Φ q n u) + Q2Presentation.Lifting.foxShadowGen Φ q n v
• Q2Presentation.Lifting.foxShadowGen Φ q n u.inv = (Φ (u.eval q)⁻¹) (Q2Presentation.Lifting.foxShadowGen Φ q n u)
• Q2Presentation.Lifting.foxShadowGen Φ q n (u.powNat k) = (∑ i ∈ Finset.range k, Φ (u.eval q) ^ i) (Q2Presentation.Lifting.foxShadowGen Φ q n u)
• Q2Presentation.Lifting.foxShadowGen Φ q n u.powOmega2 = (∑ i ∈ Finset.range (Q2Presentation.omega2Mod (Nat.card Yt.Y)).val, Φ (u.eval q) ^ i) (Q2Presentation.Lifting.foxShadowGen Φ q n u)

theorem Q2Presentation.Lifting.foxShadow_eq_gen {Yt : BoundaryFramedTarget} [Finite Yt.Y] (E : ElementaryKernel Yt) (q : Marking Yt.Y) (n : Gen → NAdd E) (w : GExpr) : foxShadow E q n w = foxShadowGen (conjEndN E) q n w

The concrete shadow is the generalized one at the conjugation family.

theorem Q2Presentation.Lifting.foxShadowGen_natural {Yt : BoundaryFramedTarget} [Finite Yt.Y] {V V' : Type} [AddCommGroup V] [Module (ZMod 2) V] [AddCommGroup V'] [Module (ZMod 2) V'] (Φ : Yt.Y → Module.End (ZMod 2) V) (Ψ : Yt.Y → Module.End (ZMod 2) V') (f : V →ₗ[ZMod 2] V') (hcomm : ∀ (y : Yt.Y) (v : V), f ((Φ y) v) = (Ψ y) (f v)) (q : Marking Yt.Y) (n : Gen → V) (w : GExpr) : f (foxShadowGen Φ q n w) = foxShadowGen Ψ q (fun (a : Gen) => f (n a)) w

Naturality of the shadow: a linear map intertwining two operator families intertwines their shadows.