UniversalNormDescent.lean

theorem restricted_norm_action
    {R : IntegralRepGroupType} [Group R] (H : Subgroup R) [H.Normal] [Fintype H]
    (B : Rep ℤ R) (r : R) (x : B.V) :
    (∑ h : H, B.ρ h.1 (B.ρ r x)) =
      B.ρ r (∑ h : H, B.ρ h.1 x)

theorem restricted_rep_norm_action
    {R : IntegralRepGroupType} [Group R] (H : Subgroup R) [H.Normal] [Fintype H]
    (B : Rep ℤ R) (r : R) (x : B.V) :
    let U : Rep ℤ H := Rep.res H.subtype B
    U.norm.hom (B.ρ r x) = B.ρ r (U.norm.hom x) := by
  let U : Rep ℤ H := Rep.res H.subtype B
  simpa [Rep.norm, Representation.norm] using
    restricted_norm_action H B r x

def conjugateStableAction
    {R : IntegralRepGroupType} [Group R] [TopologicalSpace R] [ContinuousMul R]
    (B : Rep ℤ R) (F : ClosedSubgroup R) (s : R)
    (hF : conjugateClosedSubgroup F s = F)
    (a : ambientFixedAddSubgroup B F) : ambientFixedAddSubgroup B F

theorem transport_fixed_coe
    {R : IntegralRepGroupType} [Group R] [TopologicalSpace R]
    (B : Rep ℤ R) (F' F : ClosedSubgroup R) (h : F' = F)
    (a : ambientFixedAddSubgroup B F') :
    (((h ▸ a : ambientFixedAddSubgroup B F) : B.V)) = a.1

theorem relativeNorm_transport_coe
    {R : IntegralRepGroupType} [Group R] [TopologicalSpace R]
    (B : Rep ℤ R)
    (F' E' F E : ClosedSubgroup R)
    (hF : F' = F) (hE : E' = E)
    (hE'F' : E'.toSubgroup ≤ F'.toSubgroup)
    (hEF : E.toSubgroup ≤ F.toSubgroup)
    [Finite (F'.toSubgroup ⧸ extensionSubgroup F' E' hE'F')]
    [Finite (F.toSubgroup ⧸ extensionSubgroup F E hEF)]
    (a : ambientFixedAddSubgroup B E') :
    ((relativeNorm B F E hEF (hE ▸ a) : ambientFixedAddSubgroup B F) : B.V) =
      ((relativeNorm B F' E' hE'F' a : ambientFixedAddSubgroup B F') : B.V)

theorem conjugateStableAction_coe
    {R : IntegralRepGroupType} [Group R] [TopologicalSpace R] [ContinuousMul R]
    (B : Rep ℤ R) (F : ClosedSubgroup R) (s : R)
    (hF : conjugateClosedSubgroup F s = F)
    (a : ambientFixedAddSubgroup B F) :
    ((conjugateStableAction B F s hF a : ambientFixedAddSubgroup B F) : B.V) =
      B.ρ s⁻¹ a.1

theorem relativeNorm_conjugateStableAction
    {R : IntegralRepGroupType} [Group R] [TopologicalSpace R] [ContinuousMul R]
    (B : Rep ℤ R) (F E : ClosedSubgroup R)
    (hEF : E.toSubgroup ≤ F.toSubgroup) (s : R)
    [Finite (F.toSubgroup ⧸ extensionSubgroup F E hEF)]
    (hF : conjugateClosedSubgroup F s = F)
    (hE : conjugateClosedSubgroup E s = E)
    (a : ambientFixedAddSubgroup B E) :
    relativeNorm B F E hEF (conjugateStableAction B E s hE a) =
      conjugateStableAction B F s hF (relativeNorm B F E hEF a)

theorem universalNormDescent_cyclic_lift_and_correction
    {R : IntegralRepGroupType} [Group R] (H : Subgroup R) [H.Normal] [Fintype H]
    (B : Rep ℤ R) (g : H) (hg : ∀ q, q ∈ Subgroup.zpowers g)
    (hzero0 :
      let U : Rep ℤ H := Rep.res H.subtype B
      Limits.IsZero (tateCohomology U 0))
    (hzeroMinusOne :
      let U : Rep ℤ H := Rep.res H.subtype B
      Limits.IsZero (tateCohomology U (-1)))
    {ι : Type v} (s : Finset ι) (φ : R) (τ : ι → R)
    (u : B.V) (uᵢ : ι → B.V)
    (huFixed : ∀ q : H, B.ρ q.1 u = u)
    (huᵢFixed : ∀ (i : ι) (q : H), B.ρ q.1 (uᵢ i) = uᵢ i)
    (hstar : B.ρ φ u - u =
      ∑ i ∈ s, (B.ρ (τ i) (uᵢ i) - uᵢ i)) :
    ∃ (uBar : B.V) (uBarᵢ : ι → B.V) (y : B.V),
      (∑ q : H, B.ρ q.1 uBar) = u ∧
      (∀ i, (∑ q : H, B.ρ q.1 (uBarᵢ i)) = uᵢ i) ∧
      B.ρ g.1 y - y =
        B.ρ φ uBar - uBar -
          ∑ i ∈ s, (B.ρ (τ i) (uBarᵢ i) - uBarᵢ i) := by
  let U : Rep ℤ H := Rep.res H.subtype B
  have huGenerator : U.ρ g u = u := huFixed g
  have huLift : ∃ z : B.V, U.norm.hom z = u :=
    exists_norm_eq_of_tateHZero_isZero U g hg hzero0 u huGenerator
  obtain ⟨uBar, huBar⟩ := huLift
  have huᵢGenerator (i : ι) : U.ρ g (uᵢ i) = uᵢ i := huᵢFixed i g
  have huᵢLift (i : ι) : ∃ z : B.V, U.norm.hom z = uᵢ i :=
    exists_norm_eq_of_tateHZero_isZero U g hg hzero0
      (uᵢ i) (huᵢGenerator i)
  choose uBarᵢ huBarᵢ using huᵢLift
  let delta : B.V :=
    B.ρ φ uBar - uBar -
      ∑ i ∈ s, (B.ρ (τ i) (uBarᵢ i) - uBarᵢ i)
  have hdeltaNorm : U.norm.hom delta = 0 := by
    calc
      U.norm.hom delta =
          U.norm.hom (B.ρ φ uBar) - U.norm.hom uBar -
            ∑ i ∈ s,
              (U.norm.hom (B.ρ (τ i) (uBarᵢ i)) -
                U.norm.hom (uBarᵢ i)) := by
        dsimp [delta]
        rw [map_sub, map_sub, map_sum]
        simp_rw [map_sub]
      _ = B.ρ φ u - u -
          ∑ i ∈ s, (B.ρ (τ i) (uᵢ i) - uᵢ i) := by
        rw [restricted_rep_norm_action H B φ uBar, huBar]
        congr 1
        apply Finset.sum_congr rfl
        intro i _
        rw [restricted_rep_norm_action H B (τ i) (uBarᵢ i), huBarᵢ i]
      _ = 0 := by rw [hstar, sub_self]
  obtain ⟨y, hy⟩ :=
    CyclicCohomology.normKernel_le_sigmaMinusOneRange_of_tateHMinusOne_isZero
      U g hg hzeroMinusOne delta hdeltaNorm
  refine ⟨uBar, uBarᵢ, y, ?_, ?_, ?_⟩
  · simpa [U, Rep.norm, Representation.norm] using huBar
  · intro i
    simpa [U, Rep.norm, Representation.norm] using huBarᵢ i
  · simpa [U, delta] using hy

theorem rep_norm_eq_generatorPowerSum
    {Q : IntegralRepGroupType} [Group Q] [Fintype Q]
    (B : Rep ℤ Q) (g : Q) (hg : ∀ q, q ∈ Subgroup.zpowers g)
    (n : ℕ) (hcard : Fintype.card Q = n) (x : B.V) :
    B.norm.hom x = ∑ i : Fin n, B.ρ (g ^ i.1) x

theorem rep_action_pow_eq_iterate {R : IntegralRepGroupType} [Group R]
    (B : Rep ℤ R) (g : R) (n : ℕ) (x : B.V) :
    B.ρ (g ^ n) x = ((B.ρ g)^[n]) x

theorem rep_norm_eq_generatorIterateSum
    {Q : IntegralRepGroupType} [Group Q] [Fintype Q]
    (B : Rep ℤ Q) (g : Q) (hg : ∀ q, q ∈ Subgroup.zpowers g)
    (n : ℕ) (hcard : Fintype.card Q = n)
    (f : B.V → B.V) (hf : ∀ z, B.ρ g z = f z) (x : B.V) :
    B.norm.hom x = ∑ i : Fin n, (f^[i.1]) x

theorem rep_action_pow_fixed {R : IntegralRepGroupType} [Group R]
    (B : Rep ℤ R) (g : R) (x : B.V) (hx : B.ρ g x = x) (n : ℕ) :
    B.ρ (g ^ n) x = x