Theorem: basisQuotientOfLocalRing_repr (FltRegular/NumberTheory/QuotientTrace.lean)

State before:
R : Type u_3
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
ι : Type u_1
inst✝ : Fintype ι
b : Basis ι R S
x : S
i : ι
⊢ ((basisQuotientOfLocalRing b).repr ((Ideal.Quotient.mk (Ideal.map (algebraMap R S) p)) x)) i =
    (Ideal.Quotient.mk p) ((b.repr x) i)
Tactic:
refine congr_fun (g := Ideal.Quotient.mk p ∘ b.repr x) ?_ i
State after:
R : Type u_3
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
ι : Type u_1
inst✝ : Fintype ι
b : Basis ι R S
x : S
i : ι
⊢ ⇑((basisQuotientOfLocalRing b).repr ((Ideal.Quotient.mk (Ideal.map (algebraMap R S) p)) x)) =
    ⇑(Ideal.Quotient.mk p) ∘ ⇑(b.repr x)

State before:
R : Type u_3
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
ι : Type u_1
inst✝ : Fintype ι
b : Basis ι R S
x : S
i : ι
⊢ ⇑((basisQuotientOfLocalRing b).repr ((Ideal.Quotient.mk (Ideal.map (algebraMap R S) p)) x)) =
    ⇑(Ideal.Quotient.mk p) ∘ ⇑(b.repr x)
Tactic:
apply (Finsupp.linearEquivFunOnFinite (R ⧸ p) _ _).symm.injective
State after:
case a
R : Type u_3
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
ι : Type u_1
inst✝ : Fintype ι
b : Basis ι R S
x : S
i : ι
⊢ (Finsupp.linearEquivFunOnFinite (R ⧸ p) (R ⧸ p) ι).symm
      ⇑((basisQuotientOfLocalRing b).repr ((Ideal.Quotient.mk (Ideal.map (algebraMap R S) p)) x)) =
    (Finsupp.linearEquivFunOnFinite (R ⧸ p) (R ⧸ p) ι).symm (⇑(Ideal.Quotient.mk p) ∘ ⇑(b.repr x))

State before:
case a
R : Type u_3
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
ι : Type u_1
inst✝ : Fintype ι
b : Basis ι R S
x : S
i : ι
⊢ (Finsupp.linearEquivFunOnFinite (R ⧸ p) (R ⧸ p) ι).symm
      ⇑((basisQuotientOfLocalRing b).repr ((Ideal.Quotient.mk (Ideal.map (algebraMap R S) p)) x)) =
    (Finsupp.linearEquivFunOnFinite (R ⧸ p) (R ⧸ p) ι).symm (⇑(Ideal.Quotient.mk p) ∘ ⇑(b.repr x))
Tactic:
apply (basisQuotientOfLocalRing b).repr.symm.injective
State after:
case a.a
R : Type u_3
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
ι : Type u_1
inst✝ : Fintype ι
b : Basis ι R S
x : S
i : ι
⊢ (basisQuotientOfLocalRing b).repr.symm
      ((Finsupp.linearEquivFunOnFinite (R ⧸ p) (R ⧸ p) ι).symm
        ⇑((basisQuotientOfLocalRing b).repr ((Ideal.Quotient.mk (Ideal.map (algebraMap R S) p)) x))) =
    (basisQuotientOfLocalRing b).repr.symm
      ((Finsupp.linearEquivFunOnFinite (R ⧸ p) (R ⧸ p) ι).symm (⇑(Ideal.Quotient.mk p) ∘ ⇑(b.repr x)))

State before:
case a.a
R : Type u_3
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
ι : Type u_1
inst✝ : Fintype ι
b : Basis ι R S
x : S
i : ι
⊢ (basisQuotientOfLocalRing b).repr.symm
      ((Finsupp.linearEquivFunOnFinite (R ⧸ p) (R ⧸ p) ι).symm
        ⇑((basisQuotientOfLocalRing b).repr ((Ideal.Quotient.mk (Ideal.map (algebraMap R S) p)) x))) =
    (basisQuotientOfLocalRing b).repr.symm
      ((Finsupp.linearEquivFunOnFinite (R ⧸ p) (R ⧸ p) ι).symm (⇑(Ideal.Quotient.mk p) ∘ ⇑(b.repr x)))
Tactic:
simp only [Finsupp.linearEquivFunOnFinite_symm_coe, LinearEquiv.symm_apply_apply,
  Basis.repr_symm_apply]
State after:
case a.a
R : Type u_3
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
ι : Type u_1
inst✝ : Fintype ι
b : Basis ι R S
x : S
i : ι
⊢ (Ideal.Quotient.mk (Ideal.map (algebraMap R S) p)) x =
    (Finsupp.total ι (S ⧸ Ideal.map (algebraMap R S) p) (R ⧸ p) ⇑(basisQuotientOfLocalRing b))
      ((Finsupp.linearEquivFunOnFinite (R ⧸ p) (R ⧸ p) ι).symm (⇑(Ideal.Quotient.mk p) ∘ ⇑(b.repr x)))

State before:
case a.a
R : Type u_3
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
ι : Type u_1
inst✝ : Fintype ι
b : Basis ι R S
x : S
i : ι
⊢ (Ideal.Quotient.mk (Ideal.map (algebraMap R S) p)) x =
    (Finsupp.total ι (S ⧸ Ideal.map (algebraMap R S) p) (R ⧸ p) ⇑(basisQuotientOfLocalRing b))
      ((Finsupp.linearEquivFunOnFinite (R ⧸ p) (R ⧸ p) ι).symm (⇑(Ideal.Quotient.mk p) ∘ ⇑(b.repr x)))
Tactic:
rw [Finsupp.total_eq_fintype_total_apply _ (R ⧸ p), Fintype.total_apply]
State after:
case a.a
R : Type u_3
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
ι : Type u_1
inst✝ : Fintype ι
b : Basis ι R S
x : S
i : ι
⊢ (Ideal.Quotient.mk (Ideal.map (algebraMap R S) p)) x =
    ∑ i : ι, (⇑(Ideal.Quotient.mk p) ∘ ⇑(b.repr x)) i • (basisQuotientOfLocalRing b) i

State before:
case a.a
R : Type u_3
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
ι : Type u_1
inst✝ : Fintype ι
b : Basis ι R S
x : S
i : ι
⊢ (Ideal.Quotient.mk (Ideal.map (algebraMap R S) p)) x =
    ∑ i : ι, (⇑(Ideal.Quotient.mk p) ∘ ⇑(b.repr x)) i • (basisQuotientOfLocalRing b) i
Tactic:
simp only [Function.comp_apply, basisQuotientOfLocalRing_apply,
  Ideal.Quotient.mk_smul_mk_quotient_map_quotient, ← Algebra.smul_def]
State after:
case a.a
R : Type u_3
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
ι : Type u_1
inst✝ : Fintype ι
b : Basis ι R S
x : S
i : ι
⊢ (Ideal.Quotient.mk (Ideal.map (algebraMap R S) p)) x =
    ∑ x_1 : ι, (Ideal.Quotient.mk (Ideal.map (algebraMap R S) p)) ((b.repr x) x_1 • b x_1)

State before:
case a.a
R : Type u_3
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
ι : Type u_1
inst✝ : Fintype ι
b : Basis ι R S
x : S
i : ι
⊢ (Ideal.Quotient.mk (Ideal.map (algebraMap R S) p)) x =
    ∑ x_1 : ι, (Ideal.Quotient.mk (Ideal.map (algebraMap R S) p)) ((b.repr x) x_1 • b x_1)
Tactic:
rw [← map_sum, Basis.sum_repr b x]
State after:
no goals