Piecewise linear maps

Stream: maths

[GENNARO PORPORA]

Hi, im a math student at the university of Salerno (Italy). Im trying to implement piecewise linear maps between simplicial complexes in lean togheter with my logic professor. Neither I nor my supervisor are very experienced with lean. This is the code I have written so far

import Mathlib.Analysis.Convex.Hull
import Mathlib.Analysis.Convex.Combination
import Mathlib.LinearAlgebra.AffineSpace.Independent
import Mathlib.LinearAlgebra.AffineSpace.AffineSubspace.Basic
import Mathlib.Analysis.Convex.SimplicialComplex.Basic
import Mathlib.Data.Real.Basic

open Set Finset
open Geometry
open SimplicialComplex

variable {𝕜 : Type*} [LinearOrderedField 𝕜]
variable {V: Type*} [AddCommGroup V] [Module 𝕜 V]
variable {W : Type*} [AddCommGroup W] [Module 𝕜 W]


/- piecewise linear map -/
structure PLMap (K: SimplicialComplex 𝕜 V) (L: SimplicialComplex 𝕜 W) where
  toFun : V → W
  face2face : ∀ sk ∈ K.faces, ∃ sl ∈ L.faces, MapsTo toFun sk sl
  isLin : ∀ s ∈ K.faces, ∀ (w: V → 𝕜), toFun (∑ y ∈ s, w y • y) = ∑ y ∈ s, w y • toFun y

namespace PLMap

variable {K : SimplicialComplex 𝕜 V}
variable {L : SimplicialComplex 𝕜 W}
variable {f: PLMap K L}

instance : CoeFun (PLMap K L) (fun g => V → W) where
  coe g := g.toFun


/- vertices are mapped to vertices -/
theorem v2v: MapsTo f K.vertices L.vertices := by
  intro x xink
  rw [mem_vertices] at xink
  have : ∃ sl ∈ L.faces, MapsTo f ({x}: Finset V) sl := f.face2face {x} xink
  rcases this with ⟨sl,⟨slinl,x2sl⟩⟩
  have xinx : x ∈ ({x}: Finset V) := by exact mem_singleton.mpr rfl
  have fxinsl : f x ∈ sl := by apply x2sl xinx
  have : ∃z ∈ sl, f x = z := by
    exact exists_eq_right'.mpr (x2sl xinx)
  rcases this with ⟨z,⟨zinsl,fxeqz⟩⟩
  rw [fxeqz]
  apply mem_vertices.mpr
  apply L.down_closed slinl
  exact Finset.singleton_subset_iff.mpr zinsl
  exact Finset.singleton_ne_empty z


/- the convex hull of a face is mapped to the convex hull of another face -/
lemma hull2hull (sk: Finset V) (hs: sk ∈ K.faces): ∃sl ∈ L.faces,
  MapsTo f (convexHull 𝕜 ↑sk) (convexHull 𝕜 ↑sl) := by
  rcases f.face2face sk hs with ⟨sl, ⟨slinl,sk2sl⟩⟩
  use sl; constructor
  exact slinl
  intro x hx
  rw [mem_convexHull'] at hx
  rcases hx with ⟨w,⟨wnng,sum1,xeq⟩⟩
  have fxeq : ∑ y ∈ sk, w y • f y = f x := by
    rw [Eq.comm,<-xeq]
    apply f.isLin sk hs w
  have hullconv : Convex 𝕜 ((convexHull 𝕜) ↑sl : Set W) := by
    apply convex_convexHull
  have fyinsl : ∀ y ∈ sk, f y ∈ (convexHull 𝕜 sl) := by
    intro y yinsk
    have := by apply sk2sl yinsk
    apply subset_convexHull 𝕜 sl
    exact this
    apply Set.mem_range.mpr
    simp
    constructor
    apply subset_convexHull 𝕜 (sl: Set W)
    apply convex_convexHull
  rw [<-fxeq]
  apply Convex.sum_mem hullconv wnng sum1 fyinsl


/- the underlying space of K is mapped to the underlying space of L -/
theorem space2space: MapsTo f K.space L.space := by
  intro x xink
  rcases (mem_space_iff.mp xink) with ⟨sk,⟨skink,xinsk⟩⟩
  rcases (f.hull2hull sk skink) with ⟨sl,⟨slinl,sk2sl⟩⟩
  have fxinsl := sk2sl xinsk
  have hullinsp := convexHull_subset_space slinl
  exact hullinsp fxinsl


theorem linear_pieces: ∀ sk ∈ K.faces, ∃ (fsk: V → W), IsLinearMap 𝕜 fsk ∧
  EqOn f fsk sk := by
  intro sk skink
  sorry

Sorry if my code is not very readable, im not a good at coding :smiling_face_with_tear:
But now im stuck with the last theorem. I want to build a linear map from V to W that coincide with the map f on the convex hull of the face sk of the simplicial complex K. In other words i want to restrict f to (convex hull sk) and then extend the restriction to a linear map V -> W. How can i do this , any idea ? Thak you !!

[Ben Eltschig]

This is not an answer to your quesiton, but - are you sure your definition of PLMap actually does what you want it to do? As far as I can see it currently is a map between the ambient spaces, not just the simplicial complexes, and your isLin condition forces it to be linear on every linear linear subspace spanned by one of the faces

[Ben Eltschig]

I assume what you actually want is a map that is affine-linear on each of the faces

[GENNARO PORPORA]

Thank you for your answer. Initially I defined plmap to be a map from K.space to L.space but I faced a lot of type mismatch problems so I tought well lets define it from V to W and then prove that it maps k.space to L.space. You are right it should be affine linear but the mathlib version of simplicial complex I found actually lives in a Module not in an Affine Space and unless I want to define my own version of simplicial complex (and I dont want xD) I have to adapt the definition somehow.

[GENNARO PORPORA]

I changed my strategy, now isLin says that f coincides with a linear map on each face. And everything works but I have a new problem. I want to define a barycentric subdivision of a simplicial complex. I defined Bcenter but when I use it in isSubdive it tells me typeclass problem Module ??? V

import Mathlib.Analysis.Convex.Hull
import Mathlib.Analysis.Convex.Combination
import Mathlib.LinearAlgebra.AffineSpace.Independent
import Mathlib.LinearAlgebra.AffineSpace.AffineSubspace.Basic
import Mathlib.Analysis.Convex.SimplicialComplex.Basic
import Mathlib.Data.Real.Basic

open Set Finset
open Geometry
open SimplicialComplex

variable {𝕜 : Type*} [LinearOrderedField 𝕜]
variable {V: Type*} [AddCommGroup V] [Module 𝕜 V] [DecidableEq V]
variable {W : Type*} [AddCommGroup W] [Module 𝕜 W]

/- piecewise linear map -/
structure PLMap (K: SimplicialComplex 𝕜 V) (L: SimplicialComplex 𝕜 W) where
  toFun : V → W
  face2face : ∀ sk ∈ K.faces, ∃ sl ∈ L.faces, MapsTo toFun sk sl
  isLin : ∀ sk ∈ K.faces, ∃ (fsk: V →ₗ[𝕜] W), IsLinearMap 𝕜 fsk ∧
          EqOn toFun fsk (convexHull 𝕜 sk)
  -- isLin : ∀ s ∈ K.faces, ∀ (w: V → 𝕜), toFun (∑ y ∈ s, w y • y) = ∑ y ∈ s, w y • toFun y

namespace PLMap

variable {K : SimplicialComplex 𝕜 V}
variable {L : SimplicialComplex 𝕜 W}
variable {f: PLMap K L}

variable (s : Finset V)
variable (v : V → V)
variable (c : V → 𝕜)

variable (f1 f2 : V → W)
def idV : V →ₗ[𝕜] V := LinearMap.id

instance : CoeFun (PLMap K L) (fun g => V → W) where
  coe g := g.toFun

theorem _linear_map_sum (g:V →ₗ[𝕜] W): g (∑ i ∈ s, c i • v i) = ∑ i ∈ s, c i • g (v i) := by
  induction s using Finset.induction with
  | empty =>
    simp [Finset.sum_empty]
  | insert i ih =>
    simp

theorem _sum_rewrite (h: EqOn f1 f2 s ):
  ∑ a ∈ s, c a • f1 a = ∑ a ∈ s, c a • f2 ((idV : V →ₗ[𝕜] V) a) := by
  -- Usa l'induzione su s
  induction s using Finset.induction with
  | empty =>
    -- Caso base: s è vuoto
    simp [sum_empty]
  | insert a s' =>
    exact sum_congr rfl fun x a ↦ congrArg (HSMul.hSMul (c x)) (h a)



/- vertices are mapped to vertices -/
theorem v2v: MapsTo f K.vertices L.vertices := by
  intro x xink
  rw [mem_vertices] at xink
  have : ∃ sl ∈ L.faces, MapsTo f ({x}: Finset V) sl := f.face2face {x} xink
  rcases this with ⟨sl,⟨slinl,x2sl⟩⟩
  have xinx : x ∈ ({x}: Finset V) := by exact mem_singleton.mpr rfl
  have fxinsl : f x ∈ sl := by apply x2sl xinx
  have : ∃z ∈ sl, f x = z := by
    exact exists_eq_right'.mpr (x2sl xinx)
  rcases this with ⟨z,⟨zinsl,fxeqz⟩⟩
  rw [fxeqz]
  apply mem_vertices.mpr
  apply L.down_closed slinl
  exact Finset.singleton_subset_iff.mpr zinsl
  exact Finset.singleton_ne_empty z


/- the convex hull of a face is mapped to the convex hull of another face -/
lemma hull2hull (sk: Finset V) (hs: sk ∈ K.faces): ∃sl ∈ L.faces,
  MapsTo f (convexHull 𝕜 ↑sk) (convexHull 𝕜 ↑sl) := by
  rcases f.face2face sk hs with ⟨sl, ⟨slinl,sk2sl⟩⟩
  use sl; constructor
  exact slinl
  intro x hx
  rw [mem_convexHull'] at hx
  rcases hx with ⟨w,⟨wnng,sum1,xeq⟩⟩
  have := f.isLin sk hs
  rcases this with ⟨fsk,⟨fsklin,eqonhull⟩⟩

  have hullconvsk : Convex 𝕜 ((convexHull 𝕜) ↑sk : Set V) := by
    apply convex_convexHull

  have fxeq : ∑ y ∈ sk, w y • f y = f x := by
    rw [Eq.comm,<-xeq]
    --rcases fsklin with ⟨fskadd,fskmul⟩

    have := _linear_map_sum sk (idV : V →ₗ[𝕜] V) w fsk
    have eqonsk : EqOn f fsk sk := by
      intro z zinsk
      apply eqonhull
      exact mem_convexHull_iff.mpr fun t a a_1 ↦ a zinsk
    rw [_sum_rewrite sk w f fsk eqonsk, eqonhull]
    exact this
    apply Convex.sum_mem hullconvsk wnng sum1
    apply subset_convexHull 𝕜 (sk: Set V)

  have hullconv : Convex 𝕜 ((convexHull 𝕜) ↑sl : Set W) := by
    apply convex_convexHull
  have fyinsl : ∀ y ∈ sk, f y ∈ (convexHull 𝕜 sl) := by
    intro y yinsk
    have := by apply sk2sl yinsk
    apply subset_convexHull 𝕜 sl
    exact this
    apply Set.mem_range.mpr
    simp
    constructor
    apply subset_convexHull 𝕜 (sl: Set W)
    apply convex_convexHull
  rw [<-fxeq]
  apply Convex.sum_mem hullconv wnng sum1 fyinsl


/- the underlying space of K is mapped to the underlying space of L -/
theorem space2space: MapsTo f K.space L.space := by
  intro x xink
  rcases (mem_space_iff.mp xink) with ⟨sk,⟨skink,xinsk⟩⟩
  rcases (f.hull2hull sk skink) with ⟨sl,⟨slinl,sk2sl⟩⟩
  have fxinsl := sk2sl xinsk
  have hullinsp := convexHull_subset_space slinl
  exact hullinsp fxinsl

def Bcenter (s : Finset V) : V :=
  Finset.centerMass s (fun _ => 1 : V → 𝕜) id

def isSubdiv (K K' : SimplicialComplex 𝕜 V) : Prop :=
  ∀ s ∈ K.faces, Bcenter s ∈ K'.vertices
```

```

[GENNARO PORPORA]

I cant solve a typeclass instance problem in this bit of code (the problem appears in (isPLMap p) in the plmap_iff theorem ). I tried everything
:sob:

-- K' è una suddivisione di K
def isSubdiv (K K' : SimplicialComplex 𝕜 V) : Prop :=
  ∀ s ∈ K.faces, ∃(t: Set (Finset V)),
  (t ⊆ K'.faces) ∧ (s: Set V) = (⋃ s' ∈ t, s')
-- TODO : se K' e' una suddivisione di K allora K'.space = K.space
-- p è una PLMap tra il supporto di K' e il supporto di L' ?
def isPLMap (p:V → W) : Prop :=
  ∃(K' : SimplicialComplex 𝕜 V), ∃(L' : SimplicialComplex 𝕜 W),
  ∃(f: PLMap K' L'), EqOn p f K'.space
-- p è lineare sulle facce di K'
def lin_on_faces (p:V → W) (K' : SimplicialComplex 𝕜 V) : Prop :=
  ∀ s ∈ K'.faces, ∃ (fs: V →ₗ[𝕜] W), EqOn p fs (convexHull 𝕜 s)


theorem plmap_iff (p:V → W) (sp2sp: MapsTo p K.space L.space):

  (isPLMap p) ↔ ∃(K' : SimplicialComplex 𝕜 V),
  (isSubdiv K K') ∧ (lin_on_faces p K') := by

  sorry

end PLMap
```

```

[Ben Eltschig]

Sorry for the late reply - I assume you figured this out by now, but in case you didn't, the error thrown on Bcenter s is lean telling you that Bcenter requives V to be a vector field over some field 𝕜 and can't figure out from the context what that field is. You can fix that by either making 𝕜 an explicit argument of Bcenter and then using it as Bcenter 𝕜 s, or by passing the implicit argument explicitly like in Bcenter (𝕜 := 𝕜) s. Since this issue likely occurs every time you try to use Bcenter s, I would recommend the former.

[Ben Eltschig]

In case you're wondering, the reason that lean can't infer 𝕜 from the Module 𝕜 V instance you have around is that V could very well be a vector space over two different fields; for example, every complex vector space is also a real vector space and so on. It is for this reason that when lean needs an instance like Module ? V and doesn't know yet what ? is, it complains right away instead of looking at the instances you have around and picking the first one it finds.

[Ben Eltschig]

(that was meant in reply to your message from 5 days ago, I didn't see the other one until after I replied)

[GENNARO PORPORA]

OMG you are my SAVIOR !! In truth I completely eliminated Bcenter from my code, but the same problem occured now with isPLMap. With ( k := k) now works !!

[GENNARO PORPORA]

Hi, I have this bit of code

  intro exKp
  rcases exKp with ⟨Kp,eqspace⟩
  have plts := {plt | ∃face ∈ Kp.faces, plt = convexHull 𝕜 (face: Set V)}
  use plts
  constructor
  intro plt hplt

From the hypoteses hplt: plt in plts I want to recover the condition exists face in Kp ... defining the set plts. How I do this ?

[Matteo Cipollina]

is this what you are looking for? Switched from have to let for the set definition, which allowed simp to correctly unpack the hypothesis.

import Mathlib.Analysis.Convex.Hull
import Mathlib.Analysis.Convex.SimplicialComplex.Basic
import Mathlib.Data.Set.Basic

variable {𝕜 : Type*} [Field 𝕜] [LinearOrder 𝕜]
open Set Finset
open Geometry
open SimplicialComplex

variable {V: Type*} [AddCommGroup V] [Module 𝕜 V] [DecidableEq V]

variable (K Kp : SimplicialComplex 𝕜 V)

example : ∃ (plts : Set (Set V)), (∀ plt ∈ plts, ∃ face ∈ Kp.faces, plt = convexHull 𝕜 (face : Set V)) ∧ True := by
  let plts_def : Set (Set V) := {plt_inner | ∃ face ∈ Kp.faces, plt_inner = convexHull 𝕜 (face : Set V)}
  use plts_def
  constructor
  · intro plt hplt
    have property_of_plt : (∃ face ∈ Kp.faces, plt = convexHull 𝕜 (face : Set V)) := by
      revert hplt
      simp [plts_def]
    rcases property_of_plt with ⟨face, ⟨h_face_in_Kp_faces, h_plt_eq_hull⟩⟩
    exact ⟨face, h_face_in_Kp_faces, h_plt_eq_hull⟩
  · trivial

[GENNARO PORPORA]

Thank you so much ! I will try and let you know if it works !

[GENNARO PORPORA]

Ok that worked great, now i'm stuck on this

variable {𝕜 : Type*} [LinearOrderedField 𝕜]
variable {V: Type*} [AddCommGroup V] [Module 𝕜 V] [DecidableEq V]
variable {W : Type*} [AddCommGroup W] [Module 𝕜 W]

structure Polytope where
  vertices : Finset V
  carrier : Set V := (convexHull 𝕜 vertices)

structure isPolytope (s: Set V): Prop where
  exFinset : ∃(t:Finset V), s = convexHull 𝕜 t

structure Polyhedron where
  polytopes : Finset (Set V)
  arePoly : Prop := ∀ s ∈ polytopes, (isPolytope (𝕜:=𝕜) s)
  carrier : Set V := ⋃ s ∈ polytopes, s

structure isPolyhedron (plh: Set V): Prop where
  exPoly : ∃(plts: Finset (Set V)), (∀ s ∈ plts, isPolytope (𝕜:=𝕜) s) ∧
           (plh = ⋃ s ∈ plts, s)

structure Triangulation (P: Polyhedron (𝕜:=𝕜) (V:=V)) where
  complex: SimplicialComplex 𝕜 V
  eqSpace: P.carrier = complex.space

lemma inter_politopes (plt1 plt2: Polytope (𝕜:=𝕜)):
      isPolytope (𝕜:=𝕜) (V:=V) (plt1.carrier ∩ plt2.carrier) := by
  sorry

def baryCenter (P: Polytope (𝕜:=𝕜) (V:=V)) :=
    (∑v ∈ P.vertices, (1:𝕜))⁻¹ • (∑v ∈ P.vertices, v)

def indipSubsets (s: Finset V): Set (Finset V) :=
    {t ⊆ s | AffineIndependent 𝕜 ((↑) : t → V)}

def stellar_div (P: Polytope (𝕜:=𝕜) (V:=V)) : SimplicialComplex 𝕜 V where
    faces := (indipSubsets (P.vertices ∪ {(baryCenter P)}))\{∅}
    not_empty_mem h := h.2 (mem_singleton _)
    indep := by
      intro s hs
      simp at hs
      have := hs.left
      simp [indipSubsets] at this
      exact this.right
    down_closed := by
      intro s t
      intro hs tins tneo
      simp [indipSubsets] at hs
      simp [indipSubsets]
      rcases hs with ⟨⟨hs1,hs2⟩,hs3⟩
      constructor; constructor
      exact fun ⦃a⦄ a_1 ↦ hs1 (tins a_1)

I need to prove that t is an Affine indipendent set of point knowing that s is so and (tins: t subset s)

[GENNARO PORPORA]

I forgot to mention that Im trying to prove that the barycentric (or stellar) subdivision of a n-polytope is Simplicial Complex

[Aaron Liu]

Try docs#AffineIndependent.comp_embedding

[GENNARO PORPORA]

Aaron Liu ha scritto:

Try docs#AffineIndependent.comp_embedding

thank you ! :smile: In the end I solved with
AffineIndependent.mono hs2 tins