Physlib.QFT.QED.AnomalyCancellation.LowDim.Two

Imports

/-
Copyright (c) 2024 Joseph Tooby-Smith. All rights reserved.
Released under Apache 2.0 license as described in the file LICENSE.
Authors: Joseph Tooby-Smith
-/
module

public import Physlib.QFT.QED.AnomalyCancellation.Basic

The Pure U(1) case with 2 fermions

We define an equivalence between LinSols and Sols.

@[expose] public section

An equivalence between LinSols and Sols.


def equiv : (PureU1 2).LinSols ≃ (PureU1 2).Sols where
  toFun S := ⟨⟨S, fun i => Fin.elim0 i⟩, byn:ℕS:(PureU1 2).LinSols⊢ (PureU1 2).cubicACC { toLinSols := S, quadSol := ⋯ }.val = 0
    have hLin := pureU1_linear Sn:ℕS:(PureU1 2).LinSolshLin:∑ i, S.val i = 0⊢ (PureU1 2).cubicACC { toLinSols := S, quadSol := ⋯ }.val = 0
    simp only [Fin.sum_univ_two, Fin.isValue] at hLinn:ℕS:(PureU1 2).LinSolshLin:S.val 0 + S.val 1 = 0⊢ (PureU1 2).cubicACC { toLinSols := S, quadSol := ⋯ }.val = 0
    erw [accCube_explicitn:ℕS:(PureU1 2).LinSolshLin:S.val 0 + S.val 1 = 0⊢ ∑ i, { toLinSols := S, quadSol := ⋯ }.val i ^ 3 = 0]n:ℕS:(PureU1 2).LinSolshLin:S.val 0 + S.val 1 = 0⊢ ∑ i, { toLinSols := S, quadSol := ⋯ }.val i ^ 3 = 0
    simp only [Fin.sum_univ_two, Fin.isValue]n:ℕS:(PureU1 2).LinSolshLin:S.val 0 + S.val 1 = 0⊢ S.val 0 ^ 3 + S.val 1 ^ 3 = 0
    rw [show S.val (0 : Fin 2) = - S.val (1 : Fin 2) from eq_neg_of_add_eq_zero_left hLinn:ℕS:(PureU1 2).LinSolshLin:S.val 0 + S.val 1 = 0⊢ (-S.val 1) ^ 3 + S.val 1 ^ 3 = 0n:ℕS:(PureU1 2).LinSolshLin:S.val 0 + S.val 1 = 0⊢ (-S.val 1) ^ 3 + S.val 1 ^ 3 = 0]n:ℕS:(PureU1 2).LinSolshLin:S.val 0 + S.val 1 = 0⊢ (-S.val 1) ^ 3 + S.val 1 ^ 3 = 0
    ringAll goals completed! 🐙⟩
  invFun S := S.1.1
  left_inv S := rfl
  right_inv S := rfl