DipoleChain.lean`

5 declarations, 0 contain sorry, 0 declared as axioms

def OAI.HyperbolicObstruction.PictureSwitch.faceChain line 19
Source documentation
The total lifted cellular chain (or any additive face statistic). A face is counted once, independent of its number of independently indexed sides.
```
def faceChain (f : Perm D) (w : D → A) (hw : ∀ x, w (f x) = w x) : A :=
…
```
lemma OAI.HyperbolicObstruction.PictureSwitch.faceChain_subtype line 23
lemma OAI.HyperbolicObstruction.PictureSwitch.faceChain_split line 35
lemma OAI.HyperbolicObstruction.PictureSwitch.PictureMap.OppositeFaces.faceChain_dipole line 54
theorem OAI.HyperbolicObstruction.PictureSwitch.PictureMap.removeDipole_chain line 74
Source documentation
Cancellation preserves the exact signed chain in an arbitrary additive coefficient group, not just its homology class or its unsigned face count.
```
theorem removeDipole_chain (hF : OppositeFaces M.face q a b) (hp : ∀ i, M.edge (a i) = b i)
    (i₀ : I) (w : D → A) (hw : ∀ x, w (M.face x) = w x)
    (hc : w (a i₀) + w (b i₀) = 0) :
    faceChain (M.removeDipole hF hp).face (w ∘ Subtype.val) (fun x => hw x.val) =
      faceChain M.face w hw := by
…
```
Mentions: OAI.HyperbolicObstruction.PictureSwitch.PictureMap.OppositeFaces, OAI.HyperbolicObstruction.PictureSwitch.faceChain