Theorem: relativeUnitsModule_zeta_smul (FltRegular/NumberTheory/Hilbert92.lean)

State before:
p : ℕ+
K : Type u_1
inst✝¹³ : Field K
inst✝¹² : NumberField K
k : Type u_2
inst✝¹¹ : Field k
inst✝¹⁰ : NumberField k
hp : (↑p).Prime
G : Type u_3
H : Type u_4
inst✝⁹ : AddCommGroup G
inst✝⁸ : CommGroup H
inst✝⁷ : Fintype H
hCard : Fintype.card H = ↑p
σ✝ : H
hσ✝ : Subgroup.zpowers σ✝ = ⊤
r : ℕ
inst✝⁶ : DistribMulAction H G
inst✝⁵ : Module.Free ℤ G
inst✝⁴ : Module.Finite ℤ G
hf : finrank ℤ G = r * (↑p - 1)
inst✝³ : Algebra k K
inst✝² : IsGalois k K
inst✝¹ : FiniteDimensional k K
inst✝ : IsUnramifiedAtInfinitePlaces k K
hKL : finrank k K = ↑p
σ : K ≃ₐ[k] K
hσ : ∀ (x : K ≃ₐ[k] K), x ∈ Subgroup.zpowers σ
x : (𝓞 K)ˣ
⊢ zeta ↑p • mkG x = mkG ((Units.map ↑((galRestrictHom (𝓞 k) k K (𝓞 K)) ↑σ)) x)
Tactic:
let φ := (addMonoidEndRingEquivInt _
    (Monoid.EndAdditive <| relativeUnitsMap <| ((AlgEquiv.algHomUnitsEquiv _ _).symm σ).val))
State after:
p : ℕ+
K : Type u_1
inst✝¹³ : Field K
inst✝¹² : NumberField K
k : Type u_2
inst✝¹¹ : Field k
inst✝¹⁰ : NumberField k
hp : (↑p).Prime
G : Type u_3
H : Type u_4
inst✝⁹ : AddCommGroup G
inst✝⁸ : CommGroup H
inst✝⁷ : Fintype H
hCard : Fintype.card H = ↑p
σ✝ : H
hσ✝ : Subgroup.zpowers σ✝ = ⊤
r : ℕ
inst✝⁶ : DistribMulAction H G
inst✝⁵ : Module.Free ℤ G
inst✝⁴ : Module.Finite ℤ G
hf : finrank ℤ G = r * (↑p - 1)
inst✝³ : Algebra k K
inst✝² : IsGalois k K
inst✝¹ : FiniteDimensional k K
inst✝ : IsUnramifiedAtInfinitePlaces k K
hKL : finrank k K = ↑p
σ : K ≃ₐ[k] K
hσ : ∀ (x : K ≃ₐ[k] K), x ∈ Subgroup.zpowers σ
x : (𝓞 K)ˣ
φ : Module.End ℤ (Additive (RelativeUnits k K)) :=
  (addMonoidEndRingEquivInt (Additive (RelativeUnits k K)))
    (Monoid.EndAdditive (relativeUnitsMap ↑((AlgEquiv.algHomUnitsEquiv k K).symm σ)))
⊢ zeta ↑p • mkG x = mkG ((Units.map ↑((galRestrictHom (𝓞 k) k K (𝓞 K)) ↑σ)) x)

State before:
p : ℕ+
K : Type u_1
inst✝¹³ : Field K
inst✝¹² : NumberField K
k : Type u_2
inst✝¹¹ : Field k
inst✝¹⁰ : NumberField k
hp : (↑p).Prime
G : Type u_3
H : Type u_4
inst✝⁹ : AddCommGroup G
inst✝⁸ : CommGroup H
inst✝⁷ : Fintype H
hCard : Fintype.card H = ↑p
σ✝ : H
hσ✝ : Subgroup.zpowers σ✝ = ⊤
r : ℕ
inst✝⁶ : DistribMulAction H G
inst✝⁵ : Module.Free ℤ G
inst✝⁴ : Module.Finite ℤ G
hf : finrank ℤ G = r * (↑p - 1)
inst✝³ : Algebra k K
inst✝² : IsGalois k K
inst✝¹ : FiniteDimensional k K
inst✝ : IsUnramifiedAtInfinitePlaces k K
hKL : finrank k K = ↑p
σ : K ≃ₐ[k] K
hσ : ∀ (x : K ≃ₐ[k] K), x ∈ Subgroup.zpowers σ
x : (𝓞 K)ˣ
φ : Module.End ℤ (Additive (RelativeUnits k K)) :=
  (addMonoidEndRingEquivInt (Additive (RelativeUnits k K)))
    (Monoid.EndAdditive (relativeUnitsMap ↑((AlgEquiv.algHomUnitsEquiv k K).symm σ)))
⊢ zeta ↑p • mkG x = mkG ((Units.map ↑((galRestrictHom (𝓞 k) k K (𝓞 K)) ↑σ)) x)
Tactic:
show QuotientAddGroup.mk ((Module.AEval'.of φ).symm <|
  Polynomial.X (R := ℤ) • Module.AEval'.of φ (Additive.ofMul (QuotientGroup.mk x))) = _
State after:
p : ℕ+
K : Type u_1
inst✝¹³ : Field K
inst✝¹² : NumberField K
k : Type u_2
inst✝¹¹ : Field k
inst✝¹⁰ : NumberField k
hp : (↑p).Prime
G : Type u_3
H : Type u_4
inst✝⁹ : AddCommGroup G
inst✝⁸ : CommGroup H
inst✝⁷ : Fintype H
hCard : Fintype.card H = ↑p
σ✝ : H
hσ✝ : Subgroup.zpowers σ✝ = ⊤
r : ℕ
inst✝⁶ : DistribMulAction H G
inst✝⁵ : Module.Free ℤ G
inst✝⁴ : Module.Finite ℤ G
hf : finrank ℤ G = r * (↑p - 1)
inst✝³ : Algebra k K
inst✝² : IsGalois k K
inst✝¹ : FiniteDimensional k K
inst✝ : IsUnramifiedAtInfinitePlaces k K
hKL : finrank k K = ↑p
σ : K ≃ₐ[k] K
hσ : ∀ (x : K ≃ₐ[k] K), x ∈ Subgroup.zpowers σ
x : (𝓞 K)ˣ
φ : Module.End ℤ (Additive (RelativeUnits k K)) :=
  (addMonoidEndRingEquivInt (Additive (RelativeUnits k K)))
    (Monoid.EndAdditive (relativeUnitsMap ↑((AlgEquiv.algHomUnitsEquiv k K).symm σ)))
⊢ ↑((Module.AEval'.of φ).symm (Polynomial.X • (Module.AEval'.of φ) (Additive.ofMul ↑x))) =
    mkG ((Units.map ↑((galRestrictHom (𝓞 k) k K (𝓞 K)) ↑σ)) x)

State before:
p : ℕ+
K : Type u_1
inst✝¹³ : Field K
inst✝¹² : NumberField K
k : Type u_2
inst✝¹¹ : Field k
inst✝¹⁰ : NumberField k
hp : (↑p).Prime
G : Type u_3
H : Type u_4
inst✝⁹ : AddCommGroup G
inst✝⁸ : CommGroup H
inst✝⁷ : Fintype H
hCard : Fintype.card H = ↑p
σ✝ : H
hσ✝ : Subgroup.zpowers σ✝ = ⊤
r : ℕ
inst✝⁶ : DistribMulAction H G
inst✝⁵ : Module.Free ℤ G
inst✝⁴ : Module.Finite ℤ G
hf : finrank ℤ G = r * (↑p - 1)
inst✝³ : Algebra k K
inst✝² : IsGalois k K
inst✝¹ : FiniteDimensional k K
inst✝ : IsUnramifiedAtInfinitePlaces k K
hKL : finrank k K = ↑p
σ : K ≃ₐ[k] K
hσ : ∀ (x : K ≃ₐ[k] K), x ∈ Subgroup.zpowers σ
x : (𝓞 K)ˣ
φ : Module.End ℤ (Additive (RelativeUnits k K)) :=
  (addMonoidEndRingEquivInt (Additive (RelativeUnits k K)))
    (Monoid.EndAdditive (relativeUnitsMap ↑((AlgEquiv.algHomUnitsEquiv k K).symm σ)))
⊢ ↑((Module.AEval'.of φ).symm (Polynomial.X • (Module.AEval'.of φ) (Additive.ofMul ↑x))) =
    mkG ((Units.map ↑((galRestrictHom (𝓞 k) k K (𝓞 K)) ↑σ)) x)
Tactic:
simp only [AlgEquiv.val_algHomUnitsEquiv_symm_apply, Monoid.EndAdditive_apply, Equiv.toFun_as_coe,
  addMonoidEndRingEquivInt_apply, AddHom.toFun_eq_coe, LinearMap.coe_toAddHom,
  LinearEquiv.coe_coe, addMonoidHomLequivInt_apply, Module.AEval.of_symm_smul, Polynomial.aeval_X,
  LinearEquiv.symm_apply_apply, LinearMap.smul_def, AddMonoidHom.coe_toIntLinearMap,
  MonoidHom.toAdditive_apply_apply, toMul_ofMul, relativeUnitsMap_mk, unit_to_U]
State after:
p : ℕ+
K : Type u_1
inst✝¹³ : Field K
inst✝¹² : NumberField K
k : Type u_2
inst✝¹¹ : Field k
inst✝¹⁰ : NumberField k
hp : (↑p).Prime
G : Type u_3
H : Type u_4
inst✝⁹ : AddCommGroup G
inst✝⁸ : CommGroup H
inst✝⁷ : Fintype H
hCard : Fintype.card H = ↑p
σ✝ : H
hσ✝ : Subgroup.zpowers σ✝ = ⊤
r : ℕ
inst✝⁶ : DistribMulAction H G
inst✝⁵ : Module.Free ℤ G
inst✝⁴ : Module.Finite ℤ G
hf : finrank ℤ G = r * (↑p - 1)
inst✝³ : Algebra k K
inst✝² : IsGalois k K
inst✝¹ : FiniteDimensional k K
inst✝ : IsUnramifiedAtInfinitePlaces k K
hKL : finrank k K = ↑p
σ : K ≃ₐ[k] K
hσ : ∀ (x : K ≃ₐ[k] K), x ∈ Subgroup.zpowers σ
x : (𝓞 K)ˣ
φ : Module.End ℤ (Additive (RelativeUnits k K)) :=
  (addMonoidEndRingEquivInt (Additive (RelativeUnits k K)))
    (Monoid.EndAdditive (relativeUnitsMap ↑((AlgEquiv.algHomUnitsEquiv k K).symm σ)))
⊢ ↑(φ (Additive.ofMul ↑x)) = ↑(Additive.ofMul ↑((Units.map ↑((galRestrictHom (𝓞 k) k K (𝓞 K)) ↑σ)) x))

State before:
p : ℕ+
K : Type u_1
inst✝¹³ : Field K
inst✝¹² : NumberField K
k : Type u_2
inst✝¹¹ : Field k
inst✝¹⁰ : NumberField k
hp : (↑p).Prime
G : Type u_3
H : Type u_4
inst✝⁹ : AddCommGroup G
inst✝⁸ : CommGroup H
inst✝⁷ : Fintype H
hCard : Fintype.card H = ↑p
σ✝ : H
hσ✝ : Subgroup.zpowers σ✝ = ⊤
r : ℕ
inst✝⁶ : DistribMulAction H G
inst✝⁵ : Module.Free ℤ G
inst✝⁴ : Module.Finite ℤ G
hf : finrank ℤ G = r * (↑p - 1)
inst✝³ : Algebra k K
inst✝² : IsGalois k K
inst✝¹ : FiniteDimensional k K
inst✝ : IsUnramifiedAtInfinitePlaces k K
hKL : finrank k K = ↑p
σ : K ≃ₐ[k] K
hσ : ∀ (x : K ≃ₐ[k] K), x ∈ Subgroup.zpowers σ
x : (𝓞 K)ˣ
φ : Module.End ℤ (Additive (RelativeUnits k K)) :=
  (addMonoidEndRingEquivInt (Additive (RelativeUnits k K)))
    (Monoid.EndAdditive (relativeUnitsMap ↑((AlgEquiv.algHomUnitsEquiv k K).symm σ)))
⊢ ↑(φ (Additive.ofMul ↑x)) = ↑(Additive.ofMul ↑((Units.map ↑((galRestrictHom (𝓞 k) k K (𝓞 K)) ↑σ)) x))
Tactic:
rfl
State after:
no goals