OAI/RepresentationTheory/FoulkesHowe/SpanningAgreement.lean

GitHub source file

3 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.Problem346.multilinear_agreement_of_basis line 13

   Source documentation

   Equality on chosen basis generators extends to all generator tuples when each coordinate of the generator function has a linear extension.

   theorem multilinear_agreement_of_basis
       {R I W : Type*} [Field R] [Fintype I] [DecidableEq I]
       {M X K : I → Type*} [∀ i, AddCommGroup (M i)] [∀ i, Module R (M i)]
       [AddCommGroup W] [Module R W]
       (s : ∀ i, X i → M i) (B : ∀ i, Basis (K i) R (M i))
       (t : ∀ i, K i → X i) (ht : ∀ i k, s i (t i k) = B i k)
       (F : (∀ i, X i) → W) (G : MultilinearMap R M W)
       (hlinear : ∀ x : ∀ i, X i, ∀ i,
         ∃ L : M i →ₗ[R] W, ∀ y, L (s i y) = F (Function.update x i y))
       (hbase : ∀ k : ∀ i, K i, F (fun i => t i (k i)) = G (fun i => B i (k i))) :
       ∀ x : ∀ i, X i, F x = G (fun i => s i (x i)) := by
   …

2. theorem OAI.Problem346.exists_multilinear_extension_of_basis line 62

   Source documentation

   Construct the extension when a basis consists of specified generators.

   theorem exists_multilinear_extension_of_basis
       {R I W : Type*} [Field R] [Fintype I] [DecidableEq I]
       {M X K : I → Type*} [∀ i, AddCommGroup (M i)] [∀ i, Module R (M i)]
       [AddCommGroup W] [Module R W]
       (s : ∀ i, X i → M i) (B : ∀ i, Basis (K i) R (M i))
       (t : ∀ i, K i → X i) (ht : ∀ i k, s i (t i k) = B i k)
       (F : (∀ i, X i) → W)
       (hlinear : ∀ x : ∀ i, X i, ∀ i,
         ∃ L : M i →ₗ[R] W, ∀ y, L (s i y) = F (Function.update x i y)) :
       ∃ G : MultilinearMap R M W, ∀ x : ∀ i, X i, F x = G (fun i => s i (x i)) := by
   …

3. theorem OAI.Problem346.exists_multilinear_extension_of_spanning line 83

   Source documentation

   Separate linear extendibility on spanning generators gives a multilinear extension.

   theorem exists_multilinear_extension_of_spanning
       {R I W : Type*} [Field R] [Fintype I] [DecidableEq I]
       {M X : I → Type*} [∀ i, AddCommGroup (M i)] [∀ i, Module R (M i)]
       [AddCommGroup W] [Module R W]
       (s : ∀ i, X i → M i)
       (hspan : ∀ i, Submodule.span R (Set.range (s i)) = ⊤)
       (F : (∀ i, X i) → W)
       (hlinear : ∀ x : ∀ i, X i, ∀ i,
         ∃ L : M i →ₗ[R] W, ∀ y, L (s i y) = F (Function.update x i y)) :
       ∃ G : MultilinearMap R M W, ∀ x : ∀ i, X i, F x = G (fun i => s i (x i)) := by
   …