lean-eval Aristotle (Harmonic) submission for brauer_character_in_cyclotomic

Challenge.lean

import Mathlib

theorem brauer_character_in_cyclotomic (G : Type) [Group G] [Fintype G] :
    ∃ φ : CyclotomicField (Monoid.exponent G) ℚ →+* ℂ,
      ∀ (V : Type) (_ : AddCommGroup V) (_ : Module ℂ V) (_ : FiniteDimensional ℂ V)
        (ρ : Representation ℂ G V) (g : G),
        LinearMap.trace ℂ V (ρ g) ∈ φ.range := by
  sorry

config.json

{
  "challenge_module": "Challenge",
  "solution_module": "Solution",
  "theorem_names": [
    "brauer_character_in_cyclotomic"
  ],
  "permitted_axioms": [
    "propext",
    "Quot.sound",
    "Classical.choice"
  ],
  "enable_nanoda": false
}

Helpers.lean

namespace Submission.Helpers

end Submission.Helpers

lakefile.toml

name = "brauer_character_in_cyclotomic"
testDriver = "workspace_test"
defaultTargets = ["Challenge", "Solution", "Submission"]

[leanOptions]
autoImplicit = false

[[require]]
name = "mathlib"
git = "https://github.com/leanprover-community/mathlib4.git"
rev = "5450b53e5ddc"

[[lean_lib]]
name = "Challenge"

[[lean_lib]]
name = "Solution"

[[lean_lib]]
name = "Submission"

[[lean_exe]]
name = "workspace_test"
root = "WorkspaceTest"

lean-toolchain

leanprover/lean4:v4.30.0-rc2

Solution.lean

import Mathlib
import Submission

theorem brauer_character_in_cyclotomic (G : Type) [Group G] [Fintype G] :
    ∃ φ : CyclotomicField (Monoid.exponent G) ℚ →+* ℂ,
      ∀ (V : Type) (_ : AddCommGroup V) (_ : Module ℂ V) (_ : FiniteDimensional ℂ V)
        (ρ : Representation ℂ G V) (g : G),
        LinearMap.trace ℂ V (ρ g) ∈ φ.range := by
  exact Submission.brauer_character_in_cyclotomic G

Submission.lean

import Mathlib

namespace Submission

open scoped Classical

noncomputable def cyclotomicEmbedding (n : ℕ) :
    CyclotomicField n ℚ →ₐ[ℚ] ℂ := by
  haveI : Algebra.IsAlgebraic ℚ (CyclotomicField n ℚ) := Algebra.IsAlgebraic.of_finite ℚ _
  exact IsAlgClosed.lift

lemma rootOfUnity_mem_range (n : ℕ) (hn : 0 < n)
    (φ : CyclotomicField n ℚ →ₐ[ℚ] ℂ) (ζ : ℂ) (hζ : ζ ^ (n : ℕ) = 1) :
    ζ ∈ φ.toRingHom.range := by
  haveI : NeZero n := ⟨by omega⟩
  obtain ⟨ζ₀, hζ₀⟩ : ∃ ζ₀ : CyclotomicField n ℚ, IsPrimitiveRoot ζ₀ n := by
    have h : IsCyclotomicExtension {n} ℚ (CyclotomicField n ℚ) := inferInstance
    exact h.exists_isPrimitiveRoot (Set.mem_singleton n) (NeZero.ne n)
  have hφζ₀ : IsPrimitiveRoot (φ ζ₀) n := hζ₀.map_of_injective φ.injective
  obtain ⟨k, _, hk⟩ := hφζ₀.eq_pow_of_pow_eq_one hζ
  exact ⟨ζ₀ ^ k, by simp [map_pow, hk]⟩

lemma rep_pow_exponent (G : Type) [Group G] [Fintype G]
    (V : Type) [AddCommGroup V] [Module ℂ V]
    (ρ : Representation ℂ G V) (g : G) :
    (ρ g) ^ (Monoid.exponent G) = 1 := by
  rw [ ← map_pow, Monoid.pow_exponent_eq_one, map_one ]

lemma charpoly_root_pow_eq_one {V : Type} [AddCommGroup V] [Module ℂ V]
    [FiniteDimensional ℂ V] (f : V →ₗ[ℂ] V) (n : ℕ) (_hn : 0 < n) (hf : f ^ n = 1)
    (ζ : ℂ) (hζ : ζ ∈ f.charpoly.roots) :
    ζ ^ n = 1 := by
  -- Since ζ is an eigenvalue of f, there exists a nonzero vector v such that f(v) = ζv.
  obtain ⟨v, hv⟩ : ∃ v : V, v ≠ 0 ∧ f v = ζ • v := by
    have := ( Module.End.hasEigenvalue_iff_isRoot_charpoly f ζ ).mpr ( by aesop );
    obtain ⟨ v, hv ⟩ := this.exists_hasEigenvector; obtain ⟨ hv₁, hv₂ ⟩ := hv; use v; aesop;
  -- Applying $f^n$ to $v$, we get $f^n(v) = ζ^n • v$.
  have hfnv : (f ^ n) v = ζ ^ n • v := by
    refine' Nat.recOn n _ _ <;> simp_all +decide [ pow_succ ];
    exact fun n hn => by rw [ smul_smul, mul_comm ] ;
  exact smul_left_injective _ hv.1 <| by simpa [ hf ] using hfnv.symm;

lemma trace_eq_charpoly_roots_sum {V : Type} [AddCommGroup V] [Module ℂ V]
    [FiniteDimensional ℂ V] (f : V →ₗ[ℂ] V) :
    LinearMap.trace ℂ V f = f.charpoly.roots.sum := by
  convert LinearMap.trace_eq_matrix_trace ℂ (Module.finBasis ℂ V) f using 1;
  rw [ Matrix.trace_eq_sum_roots_charpoly ];
  rw [ LinearMap.charpoly_toMatrix ]

lemma trace_mem_range (G : Type) [Group G] [Fintype G]
    (φ : CyclotomicField (Monoid.exponent G) ℚ →ₐ[ℚ] ℂ)
    (V : Type) [AddCommGroup V] [Module ℂ V] [FiniteDimensional ℂ V]
    (ρ : Representation ℂ G V) (g : G) :
    LinearMap.trace ℂ V (ρ g) ∈ φ.toRingHom.range := by
  have hn : 0 < Monoid.exponent G := by
    rw [Monoid.exponent_pos]; exact Monoid.ExponentExists.of_finite
  rw [trace_eq_charpoly_roots_sum]
  have hpow := rep_pow_exponent G V ρ g
  apply Multiset.sum_induction _ _
  · intro a b ha hb; exact Subsemiring.add_mem _ ha hb
  · exact ⟨0, map_zero _⟩
  · intro ζ hζ
    exact rootOfUnity_mem_range _ hn φ ζ (charpoly_root_pow_eq_one _ _ hn hpow ζ hζ)

theorem brauer_character_in_cyclotomic (G : Type) [Group G] [Fintype G] :
    ∃ φ : CyclotomicField (Monoid.exponent G) ℚ →+* ℂ,
      ∀ (V : Type) (_ : AddCommGroup V) (_ : Module ℂ V) (_ : FiniteDimensional ℂ V)
        (ρ : Representation ℂ G V) (g : G),
        LinearMap.trace ℂ V (ρ g) ∈ φ.range := by
  exact ⟨(cyclotomicEmbedding _).toRingHom,
    fun V _ _ _ ρ g => trace_mem_range G _ V ρ g⟩

end Submission

WorkspaceTest.lean

import Lean

open Lean

def comparatorExists (comparatorBin : String) : IO Bool := do
  if comparatorBin.contains '/' then
    return (← System.FilePath.pathExists comparatorBin)
  try
    let child ← IO.Process.spawn {
      cmd := "sh"
      args := #["-c", "command -v \"$1\" >/dev/null 2>&1", "sh", comparatorBin]
    }
    let exitCode ← child.wait
    return exitCode == 0
  catch _ =>
    return false

def main : IO UInt32 := do
  let comparatorBin := (← IO.getEnv "COMPARATOR_BIN").getD "comparator"
  if !(← comparatorExists comparatorBin) then
    IO.eprintln s!"Failed to run comparator via `{comparatorBin}`."
    IO.eprintln "Make sure `comparator` is installed and on your `PATH`, or set `COMPARATOR_BIN=/path/to/comparator`."
    IO.eprintln "See the root repository README for comparator setup details, including landrun and lean4export."
    pure 1
  else
    try
      let child ← IO.Process.spawn {
        cmd := "lake"
        args := #["env", comparatorBin, "config.json"]
      }
      let exitCode ← child.wait
      pure exitCode
    catch err =>
      IO.eprintln s!"Failed to run comparator via `{comparatorBin}`."
      IO.eprintln "Make sure `comparator` is installed and on your `PATH`, or set `COMPARATOR_BIN=/path/to/comparator`."
      IO.eprintln "See the root repository README for comparator setup details, including landrun and lean4export."
      IO.eprintln s!"Original error: {err}"
      pure 1