OAI/NumberTheory/Ostmann/Tree/ComponentFibers.lean

GitHub source file

7 declarations, 0 contain sorry, 0 declared as axioms

Uniform product fibers for a nonempty component

Fixing one distinguished leaf identifies every component-product fiber with independent values on the remaining leaves. The fiber cardinality therefore does not depend on its total.

  1. def OAI.Ostmann.completeComponentProduct line 18
  2. theorem OAI.Ostmann.completeComponentProduct_pivot line 22
  3. theorem OAI.Ostmann.completeComponentProduct_other line 27
  4. theorem OAI.Ostmann.completeComponentProduct_total line 32
  5. def OAI.Ostmann.componentProductEquiv line 39

    Source documentation

    All but one coordinate can be chosen freely in a fixed product fiber.

    noncomputable def componentProductEquiv {I G : Type*} [Fintype I] [DecidableEq I]
    [CommGroup G] (i₀ : I) (P : G) :
    {m : I → G // ∏ i, m i = P} ≃ ({i : I // i ≠ i₀} → G) where
…
  6. theorem OAI.Ostmann.card_componentProduct line 63
  7. theorem OAI.Ostmann.sum_componentProduct line 69