theorem
lifted_linearMap_first_tail
{n m : ℕ}
(A : EuclideanSpace ℝ (Fin n) →ₗ[ℝ] EuclideanSpace ℝ (Fin m))
:
have coords₁ := ⇑(EuclideanSpace.equiv (Fin (1 + n)) ℝ);
have first₁ := fun (v : EuclideanSpace ℝ (Fin (1 + n))) => coords₁ v 0;
have tail₁ := fun (v : EuclideanSpace ℝ (Fin (1 + n))) =>
(EuclideanSpace.equiv (Fin n) ℝ).symm fun (i : Fin n) => coords₁ v (Fin.natAdd 1 i);
have coords₂ := ⇑(EuclideanSpace.equiv (Fin (1 + m)) ℝ);
have first₂ := fun (v : EuclideanSpace ℝ (Fin (1 + m))) => coords₂ v 0;
have tail₂ := fun (v : EuclideanSpace ℝ (Fin (1 + m))) =>
(EuclideanSpace.equiv (Fin m) ℝ).symm fun (i : Fin m) => coords₂ v (Fin.natAdd 1 i);
have B :=
have lift :=
(LinearMap.fst ℝ (EuclideanSpace ℝ (Fin 1)) (EuclideanSpace ℝ (Fin n))).prod
(A ∘ₗ LinearMap.snd ℝ (EuclideanSpace ℝ (Fin 1)) (EuclideanSpace ℝ (Fin n)));
↑(appendAffineEquiv 1 m).linear ∘ₗ lift ∘ₗ ↑(appendAffineEquiv 1 n).symm.linear;
∀ (v : EuclideanSpace ℝ (Fin (1 + n))), first₂ (B v) = first₁ v ∧ tail₂ (B v) = A (tail₁ v)
The lifted linear map preserves first coordinate and applies A to the tail.
theorem
image_cone_eq_cone_image
{n m : ℕ}
{C : Set (EuclideanSpace ℝ (Fin n))}
(hCconv : Convex ℝ C)
(A : EuclideanSpace ℝ (Fin n) →ₗ[ℝ] EuclideanSpace ℝ (Fin m))
:
have coords₁ := ⇑(EuclideanSpace.equiv (Fin (1 + n)) ℝ);
have first₁ := fun (v : EuclideanSpace ℝ (Fin (1 + n))) => coords₁ v 0;
have tail₁ := fun (v : EuclideanSpace ℝ (Fin (1 + n))) =>
(EuclideanSpace.equiv (Fin n) ℝ).symm fun (i : Fin n) => coords₁ v (Fin.natAdd 1 i);
have coords₂ := ⇑(EuclideanSpace.equiv (Fin (1 + m)) ℝ);
have first₂ := fun (v : EuclideanSpace ℝ (Fin (1 + m))) => coords₂ v 0;
have tail₂ := fun (v : EuclideanSpace ℝ (Fin (1 + m))) =>
(EuclideanSpace.equiv (Fin m) ℝ).symm fun (i : Fin m) => coords₂ v (Fin.natAdd 1 i);
have S := {v : EuclideanSpace ℝ (Fin (1 + n)) | first₁ v = 1 ∧ tail₁ v ∈ C};
have K := ↑(ConvexCone.hull ℝ S);
have S' := {v : EuclideanSpace ℝ (Fin (1 + m)) | first₂ v = 1 ∧ tail₂ v ∈ ⇑A '' C};
have K' := ↑(ConvexCone.hull ℝ S');
have B :=
have lift :=
(LinearMap.fst ℝ (EuclideanSpace ℝ (Fin 1)) (EuclideanSpace ℝ (Fin n))).prod
(A ∘ₗ LinearMap.snd ℝ (EuclideanSpace ℝ (Fin 1)) (EuclideanSpace ℝ (Fin n)));
↑(appendAffineEquiv 1 m).linear ∘ₗ lift ∘ₗ ↑(appendAffineEquiv 1 n).symm.linear;
⇑B '' K = K'
The lifted map sends the cone over C to the cone over A '' C.
theorem
kernel_lineality_for_cone
{n m : ℕ}
{C : Set (EuclideanSpace ℝ (Fin n))}
(hCne : C.Nonempty)
(hCconv : Convex ℝ C)
(A : EuclideanSpace ℝ (Fin n) →ₗ[ℝ] EuclideanSpace ℝ (Fin m))
(hlineal :
∀ (z : EuclideanSpace ℝ (Fin n)), z ≠ 0 → z ∈ (closure C).recessionCone → A z = 0 → z ∈ (closure C).linealitySpace)
:
have Cbar := closure C;
have coords₁ := ⇑(EuclideanSpace.equiv (Fin (1 + n)) ℝ);
have first₁ := fun (v : EuclideanSpace ℝ (Fin (1 + n))) => coords₁ v 0;
have tail₁ := fun (v : EuclideanSpace ℝ (Fin (1 + n))) =>
(EuclideanSpace.equiv (Fin n) ℝ).symm fun (i : Fin n) => coords₁ v (Fin.natAdd 1 i);
have S := {v : EuclideanSpace ℝ (Fin (1 + n)) | first₁ v = 1 ∧ tail₁ v ∈ Cbar};
have K := ↑(ConvexCone.hull ℝ S);
have B :=
have lift :=
(LinearMap.fst ℝ (EuclideanSpace ℝ (Fin 1)) (EuclideanSpace ℝ (Fin n))).prod
(A ∘ₗ LinearMap.snd ℝ (EuclideanSpace ℝ (Fin 1)) (EuclideanSpace ℝ (Fin n)));
↑(appendAffineEquiv 1 m).linear ∘ₗ lift ∘ₗ ↑(appendAffineEquiv 1 n).symm.linear;
∀ (v : EuclideanSpace ℝ (Fin (1 + n))), v ≠ 0 → v ∈ (closure K).recessionCone → B v = 0 → v ∈ (closure K).linealitySpace
Kernel-lineality for the lifted cone over closure C.
theorem
linearMap_closure_image_eq_image_closure_of_recessionCone_kernel_lineality
{n m : ℕ}
{C : Set (EuclideanSpace ℝ (Fin n))}
(hCne : C.Nonempty)
(hCconv : Convex ℝ C)
(A : EuclideanSpace ℝ (Fin n) →ₗ[ℝ] EuclideanSpace ℝ (Fin m))
(hlineal :
∀ (z : EuclideanSpace ℝ (Fin n)), z ≠ 0 → z ∈ (closure C).recessionCone → A z = 0 → z ∈ (closure C).linealitySpace)
: