OAI/Combinatorics/HadwigerCounterexample/LinearExtension.lean

GitHub source file

6 declarations, 0 contain sorry, 0 declared as axioms

1. abbrev OAI.HadwigerCounterexample.dim line 13
2. abbrev OAI.HadwigerCounterexample.rk line 14
3. theorem OAI.HadwigerCounterexample.mem_range_comp line 21
4. theorem OAI.HadwigerCounterexample.equate line 36

   Source documentation

   Transport equal-sized domain embeddings in equal-dimensional spaces.

   theorem equate {f : U →ₗ[F] V} {g : U →ₗ[F] V'} [FiniteDimensional F V]
       [FiniteDimensional F V'] (hf : Injective f) (hg : Injective g)
       (h : dim V = dim V') :
       ∃ A : V ≃ₗ[F] V', ∀ x, A (f x) = g x := by
   …

   Mentions: OAI.HadwigerCounterexample.F, OAI.HadwigerCounterexample.dim

5. theorem OAI.HadwigerCounterexample.lin_split line 67

   Source documentation

   Split projection into kernel plus section.

   theorem lin_split (f : V →ₗ[F] W) (h : Surjective f) :
       ∃ (B : W →ₗ[F] V) (k : V →ₗ[F] ker f), (∀ x, f (B x) = x) ∧
         ∀ x, B (f x) + (k x).val = x := by
   …

   Mentions: OAI.HadwigerCounterexample.F

6. theorem OAI.HadwigerCounterexample.equate_pair line 80

   Source documentation

   Extend simultaneous diagram A' = L A, G = G' L to some change of basis L. Here the two maps A, A' are injective, G, G' are onto, and G A = G' A'.

   theorem equate_pair {A A' : U →ₗ[F] V} {G G' : V →ₗ[F] W}
       [FiniteDimensional F V] (hA : Injective A) (hA' : Injective A')
       (hG : Surjective G) (hG' : Surjective G') (h : G ∘ₗ A = G' ∘ₗ A') :
       ∃ L : V ≃ₗ[F] V, (∀ x, L (A x) = A' x) ∧ (∀ y, G y = G' (L y)) := by
   …

   Mentions: OAI.HadwigerCounterexample.F