OAI/NumberTheory/Ostmann/Construction/ArrangementProducts.lean

GitHub source file

3 declarations, 0 contain sorry, 0 declared as axioms

Component products for the two arrangements of the same bulk variables

  1. def OAI.Ostmann.bulkBlockProduct line 12
  2. theorem OAI.Ostmann.component_block_product line 15
  3. theorem OAI.Ostmann.arrangement_partition_products line 25

    Source documentation

    Multiplying leaf products inside an actual overlap component gives the same answer on both sides of the permutation.

    theorem arrangement_partition_products {L G : Type*} [Fintype L] [CommGroup G]
    {m : ℕ} (e : Equiv.Perm (L × Fin m)) (x : L × Fin m → G) :
    partitionProduct (arrangementLeft e) (bulkBlockProduct x) =
      partitionProduct (arrangementRight e) (bulkBlockProduct (x ∘ e.symm)) := by
…

    Mentions: OAI.Ostmann.partitionProduct, OAI.Ostmann.arrangementLeft, OAI.Ostmann.bulkBlockProduct, OAI.Ostmann.arrangementRight