InflatedParityFaces.lean`

15 declarations, 0 contain sorry, 0 declared as axioms

def OAI.DerivedBar.ParityBridge.inflatedModule line 17
Source documentation
The original D module is inflated by the actual projection, without a new action hypothesis.
```
@[instance_reducible] def inflatedModule : Module A N := Module.compHom N
…
```

def OAI.DerivedBar.ParityBridge.baseEmbed line 28

Source documentation

Literal insertion of D slots into square-zero-extension slots.

def baseEmbed : (n : ℕ) → term k D N n →ₗ[k] term k A N n
  | 0 => LinearMap.id
  | n+1 => TensorProduct.map (inlAlgHom k D X).toLinearMap (baseEmbed n)

omit [Module D N] [IsScalarTower k D N] [Module A N] [IsScalarTower k A N] in

Mentions: OAI.DerivedBar.term

theorem OAI.DerivedBar.ParityBridge.baseEmbed_tmul line 33
theorem OAI.DerivedBar.ParityBridge.baseEmbed_smul line 39
Source documentation
D-equivariance of insertion, including the inflated module endpoint.
```
theorem baseEmbed_smul (n : ℕ) (d : D) (v : term k D N n) :
    baseEmbed k D X N n (d • v) = (inl d : A) • baseEmbed k D X N n v := by
…
```
Mentions: OAI.DerivedBar.term, OAI.DerivedBar.ParityBridge.baseEmbed
theorem OAI.DerivedBar.ParityBridge.parity_baseEmbed line 54
Source documentation
All-D faces in the independently defined parity recursion are exactly ordinary D-bar faces. This is an equality of actual maps on tensors.
```
theorem parity_baseEmbed (n : ℕ) (v : term k D N (n+1)) :
    SquareZero.multibarAugmentedDifferential k D X N n (baseEmbed k D X N (n+1) v) =
      baseEmbed k D X N n (DerivedBar.differential k D N n v) := by
…
```
Mentions: OAI.DerivedBar.term, OAI.DerivedBar.SquareZero.multibarAugmentedDifferential, OAI.DerivedBar.ParityBridge.baseEmbed, OAI.DerivedBar.differential
def OAI.DerivedBar.ParityBridge.idealEmbed line 74
Source documentation
Literal insertion of a leading X and its following D block.
```
def idealEmbed (n : ℕ) : X ⊗[k] term k D N n →ₗ[k] term k A N (n+1) :=
…
```
Mentions: OAI.DerivedBar.term
theorem OAI.DerivedBar.ParityBridge.idealEmbed_tmul line 78
theorem OAI.DerivedBar.ParityBridge.idealEmbed_base_smul line 83
Source documentation
The D action on a leading X is its original left bimodule action.
```
theorem idealEmbed_base_smul (n : ℕ) (d : D) (v : X ⊗[k] term k D N n) :
    idealEmbed k D X N n (d • v) = (inl d : A) • idealEmbed k D X N n v := by
…
```
Mentions: OAI.DerivedBar.term, OAI.DerivedBar.ParityBridge.idealEmbed
theorem OAI.DerivedBar.ParityBridge.idealEmbed_ideal_smul line 95
Source documentation
An inner bar beginning with X is annihilated by the square-zero ideal. This is the boundary fact needed when the following D block has length zero.
```
theorem idealEmbed_ideal_smul (n : ℕ) (x : X) (v : X ⊗[k] term k D N n) :
    (inr x : A) • idealEmbed k D X N n v = 0 := by
…
```
Mentions: OAI.DerivedBar.term, OAI.DerivedBar.ParityBridge.idealEmbed
theorem OAI.DerivedBar.ParityBridge.ideal_action_baseEmbed line 106
Source documentation
Multiplying X by the first D entry is precisely the original right D action used by the two-sided bar collapse map.
```
theorem ideal_action_baseEmbed (n : ℕ) (x : X) (v : term k D N (n+1)) :
    (inr x : A) • baseEmbed k D X N (n+1) v =
      idealEmbed k D X N n
        (BimoduleTensor.collapse k D X (term k D N n) (x ⊗ₜ[k] v)) := by
…
```
Mentions: OAI.DerivedBar.term, OAI.DerivedBar.ParityBridge.baseEmbed, OAI.DerivedBar.ParityBridge.idealEmbed, OAI.DerivedBar.BimoduleTensor.collapse
theorem OAI.DerivedBar.ParityBridge.parity_idealEmbed line 121
Source documentation
The inner X bar is minus the augmented slot-parity recursion. The leading D two-sided differential contributes the other minus sign in the full multibar.
```
theorem parity_idealEmbed (n : ℕ) (v : X ⊗[k] term k D N (n+1)) :
    SquareZero.multibarAugmentedDifferential k D X N (n+1) (idealEmbed k D X N (n+1) v) =
      -idealEmbed k D X N n (BimoduleTensor.barDifferential k D X N n v) := by
…
```
Mentions: OAI.DerivedBar.term, OAI.DerivedBar.SquareZero.multibarAugmentedDifferential, OAI.DerivedBar.ParityBridge.idealEmbed, OAI.DerivedBar.BimoduleTensor.barDifferential
theorem OAI.DerivedBar.ParityBridge.parity_idealEmbed_zero line 138
Source documentation
The missing outgoing face at the module end of an empty X bar is zero.
```
theorem parity_idealEmbed_zero
    (hN : ∀ (x : X) (v : N), (inr x : A) • v = 0) (v : X ⊗[k] N) :
    SquareZero.multibarAugmentedDifferential k D X N 0 (idealEmbed k D X N 0 v) = 0 := by
…
```
Mentions: OAI.DerivedBar.SquareZero.multibarAugmentedDifferential, OAI.DerivedBar.ParityBridge.idealEmbed
theorem OAI.DerivedBar.ParityBridge.inflated_parity_idealEmbed line 151
Source documentation
Direct specialization to the original module inflated along A -> D. The inflation is a local instance for this N, never a blanket action on bar terms.
```
theorem inflated_parity_idealEmbed (n : ℕ) (v : X ⊗[k] term k D N (n+1)) :
    letI : Module A N := inflatedModule D X N
…
```
Mentions: OAI.DerivedBar.term, OAI.DerivedBar.ParityBridge.inflatedModule
theorem OAI.DerivedBar.ParityBridge.inflated_parity_baseEmbed line 162
theorem OAI.DerivedBar.ParityBridge.inflated_parity_idealEmbed_zero line 173