Lattice.lean

def coordinatePermutation (σ : Equiv.Perm ι) :
    (ι → ℝ) ≃ₗ[ℝ] (ι → ℝ) where
  toFun x i := x (σ.symm i)
  invFun x i := x (σ i)
  left_inv x := by
    funext i
    simp
  right_inv x := by
    funext i
    simp
  map_add' _ _ := rfl
  map_smul' _ _ := rfl

theorem coordinatePermutation_apply
    (σ : Equiv.Perm ι) (x : ι → ℝ) (i : ι) :
    coordinatePermutation σ x i = x (σ.symm i)

theorem coordinatePermutation_refl :
    coordinatePermutation (Equiv.refl ι) =
      LinearEquiv.refl ℝ (ι → ℝ)

theorem coordinatePermutation_mul
    (σ τ : Equiv.Perm ι) :
    coordinatePermutation (σ * τ) =
      (coordinatePermutation τ).trans
        (coordinatePermutation σ)

theorem coordinatePermutation_inv
    (σ : Equiv.Perm ι) :
    coordinatePermutation σ⁻¹ =
      (coordinatePermutation σ).symm

theorem coordinatePermutation_single
    [DecidableEq ι] (σ : Equiv.Perm ι) (i : ι) :
    coordinatePermutation σ (Pi.single i (1 : ℝ)) =
      Pi.single (σ i) 1

def latticeApproximation
    (L : Submodule ℤ (ι → ℝ)) [DiscreteTopology L]
    [IsZLattice ℝ L] (x : ι → ℝ) : L

def latticeApproximationRadius
    (L : Submodule ℤ (ι → ℝ)) [DiscreteTopology L]
    [IsZLattice ℝ L] : ℝ

theorem latticeApproximationRadius_nonneg
    (L : Submodule ℤ (ι → ℝ)) [DiscreteTopology L]
    [IsZLattice ℝ L] :
    0 ≤ latticeApproximationRadius L

theorem norm_sub_latticeApproximation_le
    (L : Submodule ℤ (ι → ℝ)) [DiscreteTopology L]
    [IsZLattice ℝ L] (x : ι → ℝ) :
    ‖x - (latticeApproximation L x : ι → ℝ)‖ ≤
      latticeApproximationRadius L

theorem abs_latticeApproximation_sub_apply_le
    (L : Submodule ℤ (ι → ℝ)) [DiscreteTopology L]
    [IsZLattice ℝ L] (x : ι → ℝ) (i : ι) :
    |(latticeApproximation L x : ι → ℝ) i - x i| ≤
      latticeApproximationRadius L := by
  have hcoord :
      ‖(x - (latticeApproximation L x : ι → ℝ)) i‖ ≤
        ‖x - (latticeApproximation L x : ι → ℝ)‖ :=
    norm_le_pi_norm (x - (latticeApproximation L x : ι → ℝ)) i
  rw [Pi.sub_apply, Real.norm_eq_abs, abs_sub_comm] at hcoord
  exact hcoord.trans (norm_sub_latticeApproximation_le L x)

def permutationRepresentation
    (ρ : G →* Equiv.Perm ι) (g : G) :
    (ι → ℝ) ≃ₗ[ℝ] (ι → ℝ)

theorem permutationRepresentation_one
    (ρ : G →* Equiv.Perm ι) :
    permutationRepresentation ρ 1 =
      LinearEquiv.refl ℝ (ι → ℝ)

theorem permutationRepresentation_mul
    (ρ : G →* Equiv.Perm ι) (g h : G) :
    permutationRepresentation ρ (g * h) =
      (permutationRepresentation ρ h).trans
        (permutationRepresentation ρ g)

def permutationLatticeEquiv
    (ρ : G →* Equiv.Perm ι)
    (L : Submodule ℤ (ι → ℝ))
    (hL : ∀ (g : G) (x : ι → ℝ), x ∈ L →
      permutationRepresentation ρ g x ∈ L)
    (g : G) : L ≃ₗ[ℤ] L where
  toFun x :=
    ⟨permutationRepresentation ρ g x.1, hL g x.1 x.2⟩
  invFun x :=
    ⟨permutationRepresentation ρ g⁻¹ x.1,
      hL g⁻¹ x.1 x.2⟩
  left_inv x := by
    apply Subtype.ext
    change coordinatePermutation (ρ g⁻¹)
      (coordinatePermutation (ρ g) x.1) = x.1
    rw [map_inv,
      coordinatePermutation_inv]
    exact (coordinatePermutation (ρ g)).symm_apply_apply x.1
  right_inv x := by
    apply Subtype.ext
    change coordinatePermutation (ρ g)
      (coordinatePermutation (ρ g⁻¹) x.1) = x.1
    rw [map_inv,
      coordinatePermutation_inv]
    exact (coordinatePermutation (ρ g)).apply_symm_apply x.1
  map_add' x y := by
    apply Subtype.ext
    exact map_add _ _ _
  map_smul' n x := by
    apply Subtype.ext
    exact map_zsmul _ _ _

theorem coe_permutationLatticeEquiv
    (ρ : G →* Equiv.Perm ι)
    (L : Submodule ℤ (ι → ℝ))
    (hL : ∀ (g : G) (x : ι → ℝ), x ∈ L →
      permutationRepresentation ρ g x ∈ L)
    (g : G) (x : L) :
    ((permutationLatticeEquiv ρ L hL g x : L) : ι → ℝ) =
      permutationRepresentation ρ g x

def averagedLatticeVector
    (ρ : G →* Equiv.Perm ι)
    (L : Submodule ℤ (ι → ℝ)) [DiscreteTopology L]
    [IsZLattice ℝ L]
    (hL : ∀ (g : G) (x : ι → ℝ), x ∈ L →
      permutationRepresentation ρ g x ∈ L)
    (t : ℝ) (i : ι) : L

def permutationLatticeScale
    (L : Submodule ℤ (ι → ℝ)) [DiscreteTopology L]
    [IsZLattice ℝ L] : ℝ

theorem permutationLatticeScale_pos
    (L : Submodule ℤ (ι → ℝ)) [DiscreteTopology L]
    [IsZLattice ℝ L] :
    0 < permutationLatticeScale L

theorem averagedLatticeVector_apply
    (ρ : G →* Equiv.Perm ι)
    (L : Submodule ℤ (ι → ℝ)) [DiscreteTopology L]
    [IsZLattice ℝ L]
    (hL : ∀ (g : G) (x : ι → ℝ), x ∈ L →
      permutationRepresentation ρ g x ∈ L)
    (t : ℝ) (i j : ι) :
    (averagedLatticeVector ρ L hL t i : ι → ℝ) j =
      ∑ g : G,
        (latticeApproximation L
          (t • Pi.single ((ρ g).symm i) (1 : ℝ)) :
            ι → ℝ) ((ρ g).symm j)

theorem averagingSummand_diagonal_bound
    (ρ : G →* Equiv.Perm ι)
    (L : Submodule ℤ (ι → ℝ)) [DiscreteTopology L]
    [IsZLattice ℝ L] (t : ℝ) (g : G) (i : ι) :
    |(latticeApproximation L
          (t • Pi.single ((ρ g).symm i) (1 : ℝ)) :
        ι → ℝ) ((ρ g).symm i) - t| ≤
      latticeApproximationRadius L := by
  have h :=
    abs_latticeApproximation_sub_apply_le L
      (t • Pi.single ((ρ g).symm i) (1 : ℝ))
      ((ρ g).symm i)
  simpa using h

theorem averagingSummand_offDiagonal_bound
    (ρ : G →* Equiv.Perm ι)
    (L : Submodule ℤ (ι → ℝ)) [DiscreteTopology L]
    [IsZLattice ℝ L] (t : ℝ) (g : G) {i j : ι}
    (hji : j ≠ i) :
    |(latticeApproximation L
          (t • Pi.single ((ρ g).symm i) (1 : ℝ)) :
        ι → ℝ) ((ρ g).symm j)| ≤
      latticeApproximationRadius L := by
  have h :=
    abs_latticeApproximation_sub_apply_le L
      (t • Pi.single ((ρ g).symm i) (1 : ℝ))
      ((ρ g).symm j)
  have hne : (ρ g).symm j ≠ (ρ g).symm i :=
    (ρ g).symm.injective.ne hji
  simpa [hne] using h

theorem averagedLatticeVector_diagonal_bound
    (ρ : G →* Equiv.Perm ι)
    (L : Submodule ℤ (ι → ℝ)) [DiscreteTopology L]
    [IsZLattice ℝ L]
    (hL : ∀ (g : G) (x : ι → ℝ), x ∈ L →
      permutationRepresentation ρ g x ∈ L)
    (t : ℝ) (i : ι) :
    |(averagedLatticeVector ρ L hL t i : ι → ℝ) i -
        (Fintype.card G : ℝ) * t| ≤
      (Fintype.card G : ℝ) *
        latticeApproximationRadius L := by
  rw [averagedLatticeVector_apply]
  let a : G → ℝ := fun g ↦
    (latticeApproximation L
      (t • Pi.single ((ρ g).symm i) (1 : ℝ)) :
        ι → ℝ) ((ρ g).symm i)
  change |(∑ g : G, a g) -
    (Fintype.card G : ℝ) * t| ≤
      (Fintype.card G : ℝ) *
        latticeApproximationRadius L
  have ha (g : G) :
      |a g - t| ≤ latticeApproximationRadius L := by
    simpa only [a] using
      averagingSummand_diagonal_bound ρ L t g i
  have heq :
      (∑ g : G, a g) -
          (Fintype.card G : ℝ) * t =
        ∑ g : G, (a g - t) := by
    rw [Finset.sum_sub_distrib]
    simp
  rw [heq]
  calc
    |∑ g : G, (a g - t)| ≤
        ∑ g : G, |a g - t| :=
      Finset.abs_sum_le_sum_abs _ _
    _ ≤ ∑ _g : G, latticeApproximationRadius L :=
      Finset.sum_le_sum fun g _ ↦ ha g
    _ = (Fintype.card G : ℝ) *
        latticeApproximationRadius L := by simp

theorem averagedLatticeVector_offDiagonal_bound
    (ρ : G →* Equiv.Perm ι)
    (L : Submodule ℤ (ι → ℝ)) [DiscreteTopology L]
    [IsZLattice ℝ L]
    (hL : ∀ (g : G) (x : ι → ℝ), x ∈ L →
      permutationRepresentation ρ g x ∈ L)
    (t : ℝ) {i j : ι} (hji : j ≠ i) :
    |(averagedLatticeVector ρ L hL t i : ι → ℝ) j| ≤
      (Fintype.card G : ℝ) *
        latticeApproximationRadius L := by
  rw [averagedLatticeVector_apply]
  let a : G → ℝ := fun g ↦
    (latticeApproximation L
      (t • Pi.single ((ρ g).symm i) (1 : ℝ)) :
        ι → ℝ) ((ρ g).symm j)
  change |∑ g : G, a g| ≤
    (Fintype.card G : ℝ) *
      latticeApproximationRadius L
  have ha (g : G) :
      |a g| ≤ latticeApproximationRadius L := by
    simpa only [a] using
      averagingSummand_offDiagonal_bound
        ρ L t g hji
  calc
    |∑ g : G, a g| ≤ ∑ g : G, |a g| :=
      Finset.abs_sum_le_sum_abs _ _
    _ ≤ ∑ _g : G, latticeApproximationRadius L :=
      Finset.sum_le_sum fun g _ ↦ ha g
    _ = (Fintype.card G : ℝ) *
        latticeApproximationRadius L := by simp

def averagedLatticeMatrix
    (ρ : G →* Equiv.Perm ι)
    (L : Submodule ℤ (ι → ℝ)) [DiscreteTopology L]
    [IsZLattice ℝ L]
    (hL : ∀ (g : G) (x : ι → ℝ), x ∈ L →
      permutationRepresentation ρ g x ∈ L)
    (t : ℝ) : Matrix ι ι ℝ

theorem averagedLatticeMatrix_sum_col_lt_diag
    (ρ : G →* Equiv.Perm ι)
    (L : Submodule ℤ (ι → ℝ)) [DiscreteTopology L]
    [IsZLattice ℝ L]
    (hL : ∀ (g : G) (x : ι → ℝ), x ∈ L →
      permutationRepresentation ρ g x ∈ L) :
    ∀ k : ι,
      ∑ j ∈ Finset.univ.erase k,
          ‖averagedLatticeMatrix ρ L hL
            (permutationLatticeScale L) j k‖ <
        ‖averagedLatticeMatrix ρ L hL
            (permutationLatticeScale L) k k‖

theorem averagedLatticeMatrix_det_ne_zero
    (ρ : G →* Equiv.Perm ι)
    (L : Submodule ℤ (ι → ℝ)) [DiscreteTopology L]
    [IsZLattice ℝ L]
    (hL : ∀ (g : G) (x : ι → ℝ), x ∈ L →
      permutationRepresentation ρ g x ∈ L) :
    (averagedLatticeMatrix ρ L hL
      (permutationLatticeScale L)).det ≠ 0

theorem averagedLatticeVector_linearIndependent
    (ρ : G →* Equiv.Perm ι)
    (L : Submodule ℤ (ι → ℝ)) [DiscreteTopology L]
    [IsZLattice ℝ L]
    (hL : ∀ (g : G) (x : ι → ℝ), x ∈ L →
      permutationRepresentation ρ g x ∈ L) :
    LinearIndependent ℝ
      (fun i ↦
        (averagedLatticeVector ρ L hL
          (permutationLatticeScale L) i :
            ι → ℝ)) := by
  have hcols :=
    Matrix.linearIndependent_cols_of_det_ne_zero
      (averagedLatticeMatrix_det_ne_zero ρ L hL)
  change LinearIndependent ℝ
    (fun i j ↦
      averagedLatticeMatrix ρ L hL
        (permutationLatticeScale L) j i) at hcols
  simpa only [averagedLatticeMatrix] using hcols

theorem averagedLatticeVector_equivariant
    (ρ : G →* Equiv.Perm ι)
    (L : Submodule ℤ (ι → ℝ)) [DiscreteTopology L]
    [IsZLattice ℝ L]
    (hL : ∀ (g : G) (x : ι → ℝ), x ∈ L →
      permutationRepresentation ρ g x ∈ L)
    (t : ℝ) (g : G) (i : ι) :
    permutationLatticeEquiv ρ L hL g
        (averagedLatticeVector ρ L hL t i) =
      averagedLatticeVector ρ L hL t (ρ g i)

def permutationSublattice
    (ρ : G →* Equiv.Perm ι)
    (L : Submodule ℤ (ι → ℝ)) [DiscreteTopology L]
    [IsZLattice ℝ L]
    (hL : ∀ (g : G) (x : ι → ℝ), x ∈ L →
      permutationRepresentation ρ g x ∈ L) :
    Submodule ℤ (ι → ℝ)

theorem permutationSublattice_le
    (ρ : G →* Equiv.Perm ι)
    (L : Submodule ℤ (ι → ℝ)) [DiscreteTopology L]
    [IsZLattice ℝ L]
    (hL : ∀ (g : G) (x : ι → ℝ), x ∈ L →
      permutationRepresentation ρ g x ∈ L) :
    permutationSublattice ρ L hL ≤ L

instance permutationSublattice_discreteTopology
    (ρ : G →* Equiv.Perm ι)
    (L : Submodule ℤ (ι → ℝ)) [DiscreteTopology L]
    [IsZLattice ℝ L]
    (hL : ∀ (g : G) (x : ι → ℝ), x ∈ L →
      permutationRepresentation ρ g x ∈ L) :
    DiscreteTopology (permutationSublattice ρ L hL)

theorem permutationSublattice_span_eq_top
    (ρ : G →* Equiv.Perm ι)
    (L : Submodule ℤ (ι → ℝ)) [DiscreteTopology L]
    [IsZLattice ℝ L]
    (hL : ∀ (g : G) (x : ι → ℝ), x ∈ L →
      permutationRepresentation ρ g x ∈ L) :
    Submodule.span ℝ
        (permutationSublattice ρ L hL :
          Set (ι → ℝ)) = ⊤

instance permutationSublattice_isZLattice
    (ρ : G →* Equiv.Perm ι)
    (L : Submodule ℤ (ι → ℝ)) [DiscreteTopology L]
    [IsZLattice ℝ L]
    (hL : ∀ (g : G) (x : ι → ℝ), x ∈ L →
      permutationRepresentation ρ g x ∈ L) :
    IsZLattice ℝ (permutationSublattice ρ L hL) where
  span_top := permutationSublattice_span_eq_top ρ L hL

def permutationSublatticeBasis
    (ρ : G →* Equiv.Perm ι)
    (L : Submodule ℤ (ι → ℝ)) [DiscreteTopology L]
    [IsZLattice ℝ L]
    (hL : ∀ (g : G) (x : ι → ℝ), x ∈ L →
      permutationRepresentation ρ g x ∈ L) :
    Basis ι ℤ (permutationSublattice ρ L hL)

theorem permutationSublatticeBasis_apply_coe
    (ρ : G →* Equiv.Perm ι)
    (L : Submodule ℤ (ι → ℝ)) [DiscreteTopology L]
    [IsZLattice ℝ L]
    (hL : ∀ (g : G) (x : ι → ℝ), x ∈ L →
      permutationRepresentation ρ g x ∈ L)
    (i : ι) :
    ((permutationSublatticeBasis ρ L hL i :
        permutationSublattice ρ L hL) : ι → ℝ) =
      averagedLatticeVector ρ L hL
        (permutationLatticeScale L) i

theorem permutationSublatticeBasis_permuted
    (ρ : G →* Equiv.Perm ι)
    (L : Submodule ℤ (ι → ℝ)) [DiscreteTopology L]
    [IsZLattice ℝ L]
    (hL : ∀ (g : G) (x : ι → ℝ), x ∈ L →
      permutationRepresentation ρ g x ∈ L)
    (g : G) (i : ι) :
    permutationRepresentation ρ g
        (permutationSublatticeBasis ρ L hL i :
          ι → ℝ) =
      (permutationSublatticeBasis ρ L hL (ρ g i) :
        ι → ℝ)

theorem exists_complete_permutationSublattice
    [Finite G]
    (ρ : G →* Equiv.Perm ι)
    (L : Submodule ℤ (ι → ℝ)) [DiscreteTopology L]
    [IsZLattice ℝ L]
    (hL : ∀ (g : G) (x : ι → ℝ), x ∈ L →
      permutationRepresentation ρ g x ∈ L) :
    ∃ L' : Submodule ℤ (ι → ℝ),
      L' ≤ L ∧
      DiscreteTopology L' ∧
      Submodule.span ℝ (L' : Set (ι → ℝ)) = ⊤ ∧
      ∃ b : Basis ι ℤ L',
        ∀ (g : G) (i : ι),
          permutationRepresentation ρ g
              (b i : ι → ℝ) =
            (b (ρ g i) : ι → ℝ)

theorem basisEquivFunL_symm_coordinatePermutation
    [Finite ι]
    (b : Basis ι ℝ E)
    (ρ : G →* Equiv.Perm ι)
    (α : G →* (E ≃ₗ[ℝ] E))
    (hb : ∀ (g : G) (i : ι),
      α g (b i) = b (ρ g i))
    (g : G) (x : ι → ℝ) :
    b.equivFunL.symm
        (coordinatePermutation (ρ g) x) =
      α g (b.equivFunL.symm x)

theorem exists_complete_permutationSublattice_of_basis
    [Finite G] [Finite ι]
    (b : Basis ι ℝ E)
    (ρ : G →* Equiv.Perm ι)
    (α : G →* (E ≃ₗ[ℝ] E))
    (hb : ∀ (g : G) (i : ι),
      α g (b i) = b (ρ g i))
    (L : Submodule ℤ E) [DiscreteTopology L]
    [IsZLattice ℝ L]
    (hL : ∀ (g : G) (x : E), x ∈ L →
      α g x ∈ L) :
    ∃ L' : Submodule ℤ E,
      L' ≤ L ∧
      DiscreteTopology L' ∧
      Submodule.span ℝ (L' : Set E) = ⊤ ∧
      ∃ b' : Basis ι ℤ L',
        ∀ (g : G) (i : ι),
          α g (b' i : E) =
            (b' (ρ g i) : E)

theorem finite_quotient_of_complete_sublattice
    (L L' : Submodule ℤ E)
    [DiscreteTopology L] [IsZLattice ℝ L]
    [DiscreteTopology L'] [IsZLattice ℝ L']
    (hL' : L' ≤ L) :
    Finite (L ⧸ L'.comap L.subtype)

theorem permutationSublattice_finite_quotient
    (ρ : G →* Equiv.Perm ι)
    (L : Submodule ℤ (ι → ℝ)) [DiscreteTopology L]
    [IsZLattice ℝ L]
    (hL : ∀ (g : G) (x : ι → ℝ), x ∈ L →
      permutationRepresentation ρ g x ∈ L) :
    Finite
      (L ⧸
        (permutationSublattice ρ L hL).comap
          L.subtype)