Theorem: Algebra.trace_quotient_mk (FltRegular/NumberTheory/QuotientTrace.lean)

State before:
R : Type u_1
S : Type u_2
inst✝⁷ : CommRing R
inst✝⁶ : CommRing S
inst✝⁵ : Algebra R S
inst✝⁴ : LocalRing R
inst✝³ : Module.Free R S
inst✝² : Module.Finite R S
p : Ideal R
inst✝¹ : p.IsMaximal
inst✝ : LocalRing R
x : S
⊢ (trace (R ⧸ p) (S ⧸ Ideal.map (algebraMap R S) p)) ((Ideal.Quotient.mk (Ideal.map (algebraMap R S) p)) x) =
    (Ideal.Quotient.mk p) ((trace R S) x)
Tactic:
classical
let ι := Module.Free.ChooseBasisIndex R S
let b : Basis ι R S := Module.Free.chooseBasis R S
rw [trace_eq_matrix_trace b, trace_eq_matrix_trace (basisQuotientOfLocalRing b)]
show _ = (Ideal.Quotient.mk p).toAddMonoidHom _
rw [AddMonoidHom.map_trace]
congr 1
ext i j
simp only [leftMulMatrix_apply, coe_lmul_eq_mul, LinearMap.toMatrix_apply,
  basisQuotientOfLocalRing_apply, LinearMap.mul_apply', RingHom.toAddMonoidHom_eq_coe,
  AddMonoidHom.mapMatrix_apply, AddMonoidHom.coe_coe, Matrix.map_apply, ← map_mul,
  basisQuotientOfLocalRing_repr]
State after:
no goals

State before:
R : Type u_1
S : Type u_2
inst✝⁷ : CommRing R
inst✝⁶ : CommRing S
inst✝⁵ : Algebra R S
inst✝⁴ : LocalRing R
inst✝³ : Module.Free R S
inst✝² : Module.Finite R S
p : Ideal R
inst✝¹ : p.IsMaximal
inst✝ : LocalRing R
x : S
⊢ (trace (R ⧸ p) (S ⧸ Ideal.map (algebraMap R S) p)) ((Ideal.Quotient.mk (Ideal.map (algebraMap R S) p)) x) =
    (Ideal.Quotient.mk p) ((trace R S) x)
Tactic:
let ι := Module.Free.ChooseBasisIndex R S
State after:
R : Type u_1
S : Type u_2
inst✝⁷ : CommRing R
inst✝⁶ : CommRing S
inst✝⁵ : Algebra R S
inst✝⁴ : LocalRing R
inst✝³ : Module.Free R S
inst✝² : Module.Finite R S
p : Ideal R
inst✝¹ : p.IsMaximal
inst✝ : LocalRing R
x : S
ι : Type u_2 := Module.Free.ChooseBasisIndex R S
⊢ (trace (R ⧸ p) (S ⧸ Ideal.map (algebraMap R S) p)) ((Ideal.Quotient.mk (Ideal.map (algebraMap R S) p)) x) =
    (Ideal.Quotient.mk p) ((trace R S) x)

State before:
R : Type u_1
S : Type u_2
inst✝⁷ : CommRing R
inst✝⁶ : CommRing S
inst✝⁵ : Algebra R S
inst✝⁴ : LocalRing R
inst✝³ : Module.Free R S
inst✝² : Module.Finite R S
p : Ideal R
inst✝¹ : p.IsMaximal
inst✝ : LocalRing R
x : S
ι : Type u_2 := Module.Free.ChooseBasisIndex R S
⊢ (trace (R ⧸ p) (S ⧸ Ideal.map (algebraMap R S) p)) ((Ideal.Quotient.mk (Ideal.map (algebraMap R S) p)) x) =
    (Ideal.Quotient.mk p) ((trace R S) x)
Tactic:
let b : Basis ι R S := Module.Free.chooseBasis R S
State after:
R : Type u_1
S : Type u_2
inst✝⁷ : CommRing R
inst✝⁶ : CommRing S
inst✝⁵ : Algebra R S
inst✝⁴ : LocalRing R
inst✝³ : Module.Free R S
inst✝² : Module.Finite R S
p : Ideal R
inst✝¹ : p.IsMaximal
inst✝ : LocalRing R
x : S
ι : Type u_2 := Module.Free.ChooseBasisIndex R S
b : Basis ι R S := Module.Free.chooseBasis R S
⊢ (trace (R ⧸ p) (S ⧸ Ideal.map (algebraMap R S) p)) ((Ideal.Quotient.mk (Ideal.map (algebraMap R S) p)) x) =
    (Ideal.Quotient.mk p) ((trace R S) x)

State before:
R : Type u_1
S : Type u_2
inst✝⁷ : CommRing R
inst✝⁶ : CommRing S
inst✝⁵ : Algebra R S
inst✝⁴ : LocalRing R
inst✝³ : Module.Free R S
inst✝² : Module.Finite R S
p : Ideal R
inst✝¹ : p.IsMaximal
inst✝ : LocalRing R
x : S
ι : Type u_2 := Module.Free.ChooseBasisIndex R S
b : Basis ι R S := Module.Free.chooseBasis R S
⊢ (trace (R ⧸ p) (S ⧸ Ideal.map (algebraMap R S) p)) ((Ideal.Quotient.mk (Ideal.map (algebraMap R S) p)) x) =
    (Ideal.Quotient.mk p) ((trace R S) x)
Tactic:
rw [trace_eq_matrix_trace b, trace_eq_matrix_trace (basisQuotientOfLocalRing b)]
State after:
R : Type u_1
S : Type u_2
inst✝⁷ : CommRing R
inst✝⁶ : CommRing S
inst✝⁵ : Algebra R S
inst✝⁴ : LocalRing R
inst✝³ : Module.Free R S
inst✝² : Module.Finite R S
p : Ideal R
inst✝¹ : p.IsMaximal
inst✝ : LocalRing R
x : S
ι : Type u_2 := Module.Free.ChooseBasisIndex R S
b : Basis ι R S := Module.Free.chooseBasis R S
⊢ ((leftMulMatrix (basisQuotientOfLocalRing b)) ((Ideal.Quotient.mk (Ideal.map (algebraMap R S) p)) x)).trace =
    (Ideal.Quotient.mk p) ((leftMulMatrix b) x).trace

State before:
R : Type u_1
S : Type u_2
inst✝⁷ : CommRing R
inst✝⁶ : CommRing S
inst✝⁵ : Algebra R S
inst✝⁴ : LocalRing R
inst✝³ : Module.Free R S
inst✝² : Module.Finite R S
p : Ideal R
inst✝¹ : p.IsMaximal
inst✝ : LocalRing R
x : S
ι : Type u_2 := Module.Free.ChooseBasisIndex R S
b : Basis ι R S := Module.Free.chooseBasis R S
⊢ ((leftMulMatrix (basisQuotientOfLocalRing b)) ((Ideal.Quotient.mk (Ideal.map (algebraMap R S) p)) x)).trace =
    (Ideal.Quotient.mk p) ((leftMulMatrix b) x).trace
Tactic:
show _ = (Ideal.Quotient.mk p).toAddMonoidHom _
State after:
R : Type u_1
S : Type u_2
inst✝⁷ : CommRing R
inst✝⁶ : CommRing S
inst✝⁵ : Algebra R S
inst✝⁴ : LocalRing R
inst✝³ : Module.Free R S
inst✝² : Module.Finite R S
p : Ideal R
inst✝¹ : p.IsMaximal
inst✝ : LocalRing R
x : S
ι : Type u_2 := Module.Free.ChooseBasisIndex R S
b : Basis ι R S := Module.Free.chooseBasis R S
⊢ ((leftMulMatrix (basisQuotientOfLocalRing b)) ((Ideal.Quotient.mk (Ideal.map (algebraMap R S) p)) x)).trace =
    (Ideal.Quotient.mk p).toAddMonoidHom ((leftMulMatrix b) x).trace

State before:
R : Type u_1
S : Type u_2
inst✝⁷ : CommRing R
inst✝⁶ : CommRing S
inst✝⁵ : Algebra R S
inst✝⁴ : LocalRing R
inst✝³ : Module.Free R S
inst✝² : Module.Finite R S
p : Ideal R
inst✝¹ : p.IsMaximal
inst✝ : LocalRing R
x : S
ι : Type u_2 := Module.Free.ChooseBasisIndex R S
b : Basis ι R S := Module.Free.chooseBasis R S
⊢ ((leftMulMatrix (basisQuotientOfLocalRing b)) ((Ideal.Quotient.mk (Ideal.map (algebraMap R S) p)) x)).trace =
    (Ideal.Quotient.mk p).toAddMonoidHom ((leftMulMatrix b) x).trace
Tactic:
rw [AddMonoidHom.map_trace]
State after:
R : Type u_1
S : Type u_2
inst✝⁷ : CommRing R
inst✝⁶ : CommRing S
inst✝⁵ : Algebra R S
inst✝⁴ : LocalRing R
inst✝³ : Module.Free R S
inst✝² : Module.Finite R S
p : Ideal R
inst✝¹ : p.IsMaximal
inst✝ : LocalRing R
x : S
ι : Type u_2 := Module.Free.ChooseBasisIndex R S
b : Basis ι R S := Module.Free.chooseBasis R S
⊢ ((leftMulMatrix (basisQuotientOfLocalRing b)) ((Ideal.Quotient.mk (Ideal.map (algebraMap R S) p)) x)).trace =
    ((Ideal.Quotient.mk p).toAddMonoidHom.mapMatrix ((leftMulMatrix b) x)).trace

State before:
R : Type u_1
S : Type u_2
inst✝⁷ : CommRing R
inst✝⁶ : CommRing S
inst✝⁵ : Algebra R S
inst✝⁴ : LocalRing R
inst✝³ : Module.Free R S
inst✝² : Module.Finite R S
p : Ideal R
inst✝¹ : p.IsMaximal
inst✝ : LocalRing R
x : S
ι : Type u_2 := Module.Free.ChooseBasisIndex R S
b : Basis ι R S := Module.Free.chooseBasis R S
⊢ ((leftMulMatrix (basisQuotientOfLocalRing b)) ((Ideal.Quotient.mk (Ideal.map (algebraMap R S) p)) x)).trace =
    ((Ideal.Quotient.mk p).toAddMonoidHom.mapMatrix ((leftMulMatrix b) x)).trace
Tactic:
congr 1
State after:
case e_A
R : Type u_1
S : Type u_2
inst✝⁷ : CommRing R
inst✝⁶ : CommRing S
inst✝⁵ : Algebra R S
inst✝⁴ : LocalRing R
inst✝³ : Module.Free R S
inst✝² : Module.Finite R S
p : Ideal R
inst✝¹ : p.IsMaximal
inst✝ : LocalRing R
x : S
ι : Type u_2 := Module.Free.ChooseBasisIndex R S
b : Basis ι R S := Module.Free.chooseBasis R S
⊢ (leftMulMatrix (basisQuotientOfLocalRing b)) ((Ideal.Quotient.mk (Ideal.map (algebraMap R S) p)) x) =
    (Ideal.Quotient.mk p).toAddMonoidHom.mapMatrix ((leftMulMatrix b) x)

State before:
case e_A
R : Type u_1
S : Type u_2
inst✝⁷ : CommRing R
inst✝⁶ : CommRing S
inst✝⁵ : Algebra R S
inst✝⁴ : LocalRing R
inst✝³ : Module.Free R S
inst✝² : Module.Finite R S
p : Ideal R
inst✝¹ : p.IsMaximal
inst✝ : LocalRing R
x : S
ι : Type u_2 := Module.Free.ChooseBasisIndex R S
b : Basis ι R S := Module.Free.chooseBasis R S
⊢ (leftMulMatrix (basisQuotientOfLocalRing b)) ((Ideal.Quotient.mk (Ideal.map (algebraMap R S) p)) x) =
    (Ideal.Quotient.mk p).toAddMonoidHom.mapMatrix ((leftMulMatrix b) x)
Tactic:
ext i j
State after:
case e_A.a
R : Type u_1
S : Type u_2
inst✝⁷ : CommRing R
inst✝⁶ : CommRing S
inst✝⁵ : Algebra R S
inst✝⁴ : LocalRing R
inst✝³ : Module.Free R S
inst✝² : Module.Finite R S
p : Ideal R
inst✝¹ : p.IsMaximal
inst✝ : LocalRing R
x : S
ι : Type u_2 := Module.Free.ChooseBasisIndex R S
b : Basis ι R S := Module.Free.chooseBasis R S
i j : ι
⊢ (leftMulMatrix (basisQuotientOfLocalRing b)) ((Ideal.Quotient.mk (Ideal.map (algebraMap R S) p)) x) i j =
    (Ideal.Quotient.mk p).toAddMonoidHom.mapMatrix ((leftMulMatrix b) x) i j

State before:
case e_A.a
R : Type u_1
S : Type u_2
inst✝⁷ : CommRing R
inst✝⁶ : CommRing S
inst✝⁵ : Algebra R S
inst✝⁴ : LocalRing R
inst✝³ : Module.Free R S
inst✝² : Module.Finite R S
p : Ideal R
inst✝¹ : p.IsMaximal
inst✝ : LocalRing R
x : S
ι : Type u_2 := Module.Free.ChooseBasisIndex R S
b : Basis ι R S := Module.Free.chooseBasis R S
i j : ι
⊢ (leftMulMatrix (basisQuotientOfLocalRing b)) ((Ideal.Quotient.mk (Ideal.map (algebraMap R S) p)) x) i j =
    (Ideal.Quotient.mk p).toAddMonoidHom.mapMatrix ((leftMulMatrix b) x) i j
Tactic:
simp only [leftMulMatrix_apply, coe_lmul_eq_mul, LinearMap.toMatrix_apply,
  basisQuotientOfLocalRing_apply, LinearMap.mul_apply', RingHom.toAddMonoidHom_eq_coe,
  AddMonoidHom.mapMatrix_apply, AddMonoidHom.coe_coe, Matrix.map_apply, ← map_mul,
  basisQuotientOfLocalRing_repr]
State after:
no goals