internlm/Lean-Github huggingface dataset:
Theorem: finrank_quotient_map_of_localRing
Proof state before:
R : Type u_2
S : Type u_1
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
this✝ : Module.Finite R (S ⧸ Ideal.map (algebraMap R S) p)
this : Module.Finite (R ⧸ p) (S ⧸ Ideal.map (algebraMap R S) p)
⊢ finrank (R ⧸ p) (S ⧸ Ideal.map (algebraMap R S) p) = finrank R S
Tactic:
apply le_antisymm
Proof state after:
case a
R : Type u_2
S : Type u_1
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
this✝ : Module.Finite R (S ⧸ Ideal.map (algebraMap R S) p)
this : Module.Finite (R ⧸ p) (S ⧸ Ideal.map (algebraMap R S) p)
⊢ finrank (R ⧸ p) (S ⧸ Ideal.map (algebraMap R S) p) ≤ finrank R S

case a
R : Type u_2
S : Type u_1
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
this✝ : Module.Finite R (S ⧸ Ideal.map (algebraMap R S) p)
this : Module.Finite (R ⧸ p) (S ⧸ Ideal.map (algebraMap R S) p)
⊢ finrank R S ≤ finrank (R ⧸ p) (S ⧸ Ideal.map (algebraMap R S) p)
Theorem: finrank_quotient_map_of_localRing
Proof state before:
case a
R : Type u_2
S : Type u_1
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
this✝ : Module.Finite R (S ⧸ Ideal.map (algebraMap R S) p)
this : Module.Finite (R ⧸ p) (S ⧸ Ideal.map (algebraMap R S) p)
⊢ finrank (R ⧸ p) (S ⧸ Ideal.map (algebraMap R S) p) ≤ finrank R S
Tactic:
let b := Module.Free.chooseBasis R S
Proof state after:
case a
R : Type u_2
S : Type u_1
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
this✝ : Module.Finite R (S ⧸ Ideal.map (algebraMap R S) p)
this : Module.Finite (R ⧸ p) (S ⧸ Ideal.map (algebraMap R S) p)
b : Basis (Module.Free.ChooseBasisIndex R S) R S := Module.Free.chooseBasis R S
⊢ finrank (R ⧸ p) (S ⧸ Ideal.map (algebraMap R S) p) ≤ finrank R S
Theorem: finrank_quotient_map_of_localRing
Proof state before:
case a
R : Type u_2
S : Type u_1
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
this✝ : Module.Finite R (S ⧸ Ideal.map (algebraMap R S) p)
this : Module.Finite (R ⧸ p) (S ⧸ Ideal.map (algebraMap R S) p)
b : Basis (Module.Free.ChooseBasisIndex R S) R S := Module.Free.chooseBasis R S
⊢ finrank (R ⧸ p) (S ⧸ Ideal.map (algebraMap R S) p) ≤ finrank R S
Tactic:
conv_rhs => rw [finrank_eq_card_chooseBasisIndex]
Proof state after:
case a
R : Type u_2
S : Type u_1
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
this✝ : Module.Finite R (S ⧸ Ideal.map (algebraMap R S) p)
this : Module.Finite (R ⧸ p) (S ⧸ Ideal.map (algebraMap R S) p)
b : Basis (Module.Free.ChooseBasisIndex R S) R S := Module.Free.chooseBasis R S
⊢ finrank (R ⧸ p) (S ⧸ Ideal.map (algebraMap R S) p) ≤ Fintype.card (Module.Free.ChooseBasisIndex R S)
Theorem: finrank_quotient_map_of_localRing
Proof state before:
case a
R : Type u_2
S : Type u_1
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
this✝ : Module.Finite R (S ⧸ Ideal.map (algebraMap R S) p)
this : Module.Finite (R ⧸ p) (S ⧸ Ideal.map (algebraMap R S) p)
b : Basis (Module.Free.ChooseBasisIndex R S) R S := Module.Free.chooseBasis R S
⊢ finrank (R ⧸ p) (S ⧸ Ideal.map (algebraMap R S) p) ≤ Fintype.card (Module.Free.ChooseBasisIndex R S)
Tactic:
apply finrank_le_of_span_eq_top (IsScalarTower.toAlgHom R S (S ⧸ pS) ∘ b)
Proof state after:
case a
R : Type u_2
S : Type u_1
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
this✝ : Module.Finite R (S ⧸ Ideal.map (algebraMap R S) p)
this : Module.Finite (R ⧸ p) (S ⧸ Ideal.map (algebraMap R S) p)
b : Basis (Module.Free.ChooseBasisIndex R S) R S := Module.Free.chooseBasis R S
⊢ Submodule.span (R ⧸ p) (Set.range (⇑(IsScalarTower.toAlgHom R S (S ⧸ Ideal.map (algebraMap R S) p)) ∘ ⇑b)) = ⊤
Theorem: finrank_quotient_map_of_localRing
Proof state before:
case a
R : Type u_2
S : Type u_1
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
this✝ : Module.Finite R (S ⧸ Ideal.map (algebraMap R S) p)
this : Module.Finite (R ⧸ p) (S ⧸ Ideal.map (algebraMap R S) p)
b : Basis (Module.Free.ChooseBasisIndex R S) R S := Module.Free.chooseBasis R S
⊢ Submodule.span (R ⧸ p) (Set.range (⇑(IsScalarTower.toAlgHom R S (S ⧸ Ideal.map (algebraMap R S) p)) ∘ ⇑b)) = ⊤
Tactic:
rw [Set.range_comp]
Proof state after:
case a
R : Type u_2
S : Type u_1
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
this✝ : Module.Finite R (S ⧸ Ideal.map (algebraMap R S) p)
this : Module.Finite (R ⧸ p) (S ⧸ Ideal.map (algebraMap R S) p)
b : Basis (Module.Free.ChooseBasisIndex R S) R S := Module.Free.chooseBasis R S
⊢ Submodule.span (R ⧸ p) (⇑(IsScalarTower.toAlgHom R S (S ⧸ Ideal.map (algebraMap R S) p)) '' Set.range ⇑b) = ⊤
Theorem: finrank_quotient_map_of_localRing
Proof state before:
case a
R : Type u_2
S : Type u_1
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
this✝ : Module.Finite R (S ⧸ Ideal.map (algebraMap R S) p)
this : Module.Finite (R ⧸ p) (S ⧸ Ideal.map (algebraMap R S) p)
b : Basis (Module.Free.ChooseBasisIndex R S) R S := Module.Free.chooseBasis R S
⊢ Submodule.span (R ⧸ p) (⇑(IsScalarTower.toAlgHom R S (S ⧸ Ideal.map (algebraMap R S) p)) '' Set.range ⇑b) = ⊤
Tactic:
apply (quotient_span_eq_top_iff_span_eq_top_of_localRing _).mpr b.span_eq
Proof state after:
no goals
Theorem: finrank_quotient_map_of_localRing
Proof state before:
case a
R : Type u_2
S : Type u_1
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
this✝ : Module.Finite R (S ⧸ Ideal.map (algebraMap R S) p)
this : Module.Finite (R ⧸ p) (S ⧸ Ideal.map (algebraMap R S) p)
⊢ finrank R S ≤ finrank (R ⧸ p) (S ⧸ Ideal.map (algebraMap R S) p)
Tactic:
let b := Module.Free.chooseBasis (R ⧸ p) (S ⧸ pS)
Proof state after:
case a
R : Type u_2
S : Type u_1
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
this✝ : Module.Finite R (S ⧸ Ideal.map (algebraMap R S) p)
this : Module.Finite (R ⧸ p) (S ⧸ Ideal.map (algebraMap R S) p)
b : Basis (Module.Free.ChooseBasisIndex (R ⧸ p) (S ⧸ Ideal.map (algebraMap R S) p)) (R ⧸ p)
  (S ⧸ Ideal.map (algebraMap R S) p) :=
  Module.Free.chooseBasis (R ⧸ p) (S ⧸ Ideal.map (algebraMap R S) p)
⊢ finrank R S ≤ finrank (R ⧸ p) (S ⧸ Ideal.map (algebraMap R S) p)
Theorem: finrank_quotient_map_of_localRing
Proof state before:
case a
R : Type u_2
S : Type u_1
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
this✝ : Module.Finite R (S ⧸ Ideal.map (algebraMap R S) p)
this : Module.Finite (R ⧸ p) (S ⧸ Ideal.map (algebraMap R S) p)
b : Basis (Module.Free.ChooseBasisIndex (R ⧸ p) (S ⧸ Ideal.map (algebraMap R S) p)) (R ⧸ p)
  (S ⧸ Ideal.map (algebraMap R S) p) :=
  Module.Free.chooseBasis (R ⧸ p) (S ⧸ Ideal.map (algebraMap R S) p)
⊢ finrank R S ≤ finrank (R ⧸ p) (S ⧸ Ideal.map (algebraMap R S) p)
Tactic:
choose b' hb' using fun i ↦ Ideal.Quotient.mk_surjective (b i)
Proof state after:
case a
R : Type u_2
S : Type u_1
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
this✝ : Module.Finite R (S ⧸ Ideal.map (algebraMap R S) p)
this : Module.Finite (R ⧸ p) (S ⧸ Ideal.map (algebraMap R S) p)
b : Basis (Module.Free.ChooseBasisIndex (R ⧸ p) (S ⧸ Ideal.map (algebraMap R S) p)) (R ⧸ p)
  (S ⧸ Ideal.map (algebraMap R S) p) :=
  Module.Free.chooseBasis (R ⧸ p) (S ⧸ Ideal.map (algebraMap R S) p)
b' : Module.Free.ChooseBasisIndex (R ⧸ p) (S ⧸ Ideal.map (algebraMap R S) p) → S
hb' :
  ∀ (i : Module.Free.ChooseBasisIndex (R ⧸ p) (S ⧸ Ideal.map (algebraMap R S) p)),
    (Ideal.Quotient.mk (Ideal.map (algebraMap R S) p)) (b' i) = b i
⊢ finrank R S ≤ finrank (R ⧸ p) (S ⧸ Ideal.map (algebraMap R S) p)
Theorem: finrank_quotient_map_of_localRing
Proof state before:
case a
R : Type u_2
S : Type u_1
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
this✝ : Module.Finite R (S ⧸ Ideal.map (algebraMap R S) p)
this : Module.Finite (R ⧸ p) (S ⧸ Ideal.map (algebraMap R S) p)
b : Basis (Module.Free.ChooseBasisIndex (R ⧸ p) (S ⧸ Ideal.map (algebraMap R S) p)) (R ⧸ p)
  (S ⧸ Ideal.map (algebraMap R S) p) :=
  Module.Free.chooseBasis (R ⧸ p) (S ⧸ Ideal.map (algebraMap R S) p)
b' : Module.Free.ChooseBasisIndex (R ⧸ p) (S ⧸ Ideal.map (algebraMap R S) p) → S
hb' :
  ∀ (i : Module.Free.ChooseBasisIndex (R ⧸ p) (S ⧸ Ideal.map (algebraMap R S) p)),
    (Ideal.Quotient.mk (Ideal.map (algebraMap R S) p)) (b' i) = b i
⊢ finrank R S ≤ finrank (R ⧸ p) (S ⧸ Ideal.map (algebraMap R S) p)
Tactic:
conv_rhs => rw [finrank_eq_card_chooseBasisIndex]
Proof state after:
case a
R : Type u_2
S : Type u_1
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
this✝ : Module.Finite R (S ⧸ Ideal.map (algebraMap R S) p)
this : Module.Finite (R ⧸ p) (S ⧸ Ideal.map (algebraMap R S) p)
b : Basis (Module.Free.ChooseBasisIndex (R ⧸ p) (S ⧸ Ideal.map (algebraMap R S) p)) (R ⧸ p)
  (S ⧸ Ideal.map (algebraMap R S) p) :=
  Module.Free.chooseBasis (R ⧸ p) (S ⧸ Ideal.map (algebraMap R S) p)
b' : Module.Free.ChooseBasisIndex (R ⧸ p) (S ⧸ Ideal.map (algebraMap R S) p) → S
hb' :
  ∀ (i : Module.Free.ChooseBasisIndex (R ⧸ p) (S ⧸ Ideal.map (algebraMap R S) p)),
    (Ideal.Quotient.mk (Ideal.map (algebraMap R S) p)) (b' i) = b i
⊢ finrank R S ≤ Fintype.card (Module.Free.ChooseBasisIndex (R ⧸ p) (S ⧸ Ideal.map (algebraMap R S) p))
Theorem: finrank_quotient_map_of_localRing
Proof state before:
case a
R : Type u_2
S : Type u_1
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
this✝ : Module.Finite R (S ⧸ Ideal.map (algebraMap R S) p)
this : Module.Finite (R ⧸ p) (S ⧸ Ideal.map (algebraMap R S) p)
b : Basis (Module.Free.ChooseBasisIndex (R ⧸ p) (S ⧸ Ideal.map (algebraMap R S) p)) (R ⧸ p)
  (S ⧸ Ideal.map (algebraMap R S) p) :=
  Module.Free.chooseBasis (R ⧸ p) (S ⧸ Ideal.map (algebraMap R S) p)
b' : Module.Free.ChooseBasisIndex (R ⧸ p) (S ⧸ Ideal.map (algebraMap R S) p) → S
hb' :
  ∀ (i : Module.Free.ChooseBasisIndex (R ⧸ p) (S ⧸ Ideal.map (algebraMap R S) p)),
    (Ideal.Quotient.mk (Ideal.map (algebraMap R S) p)) (b' i) = b i
⊢ finrank R S ≤ Fintype.card (Module.Free.ChooseBasisIndex (R ⧸ p) (S ⧸ Ideal.map (algebraMap R S) p))
Tactic:
apply finrank_le_of_span_eq_top b'
Proof state after:
case a
R : Type u_2
S : Type u_1
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
this✝ : Module.Finite R (S ⧸ Ideal.map (algebraMap R S) p)
this : Module.Finite (R ⧸ p) (S ⧸ Ideal.map (algebraMap R S) p)
b : Basis (Module.Free.ChooseBasisIndex (R ⧸ p) (S ⧸ Ideal.map (algebraMap R S) p)) (R ⧸ p)
  (S ⧸ Ideal.map (algebraMap R S) p) :=
  Module.Free.chooseBasis (R ⧸ p) (S ⧸ Ideal.map (algebraMap R S) p)
b' : Module.Free.ChooseBasisIndex (R ⧸ p) (S ⧸ Ideal.map (algebraMap R S) p) → S
hb' :
  ∀ (i : Module.Free.ChooseBasisIndex (R ⧸ p) (S ⧸ Ideal.map (algebraMap R S) p)),
    (Ideal.Quotient.mk (Ideal.map (algebraMap R S) p)) (b' i) = b i
⊢ Submodule.span R (Set.range b') = ⊤
Theorem: finrank_quotient_map_of_localRing
Proof state before:
case a
R : Type u_2
S : Type u_1
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
this✝ : Module.Finite R (S ⧸ Ideal.map (algebraMap R S) p)
this : Module.Finite (R ⧸ p) (S ⧸ Ideal.map (algebraMap R S) p)
b : Basis (Module.Free.ChooseBasisIndex (R ⧸ p) (S ⧸ Ideal.map (algebraMap R S) p)) (R ⧸ p)
  (S ⧸ Ideal.map (algebraMap R S) p) :=
  Module.Free.chooseBasis (R ⧸ p) (S ⧸ Ideal.map (algebraMap R S) p)
b' : Module.Free.ChooseBasisIndex (R ⧸ p) (S ⧸ Ideal.map (algebraMap R S) p) → S
hb' :
  ∀ (i : Module.Free.ChooseBasisIndex (R ⧸ p) (S ⧸ Ideal.map (algebraMap R S) p)),
    (Ideal.Quotient.mk (Ideal.map (algebraMap R S) p)) (b' i) = b i
⊢ Submodule.span R (Set.range b') = ⊤
Tactic:
apply (quotient_span_eq_top_iff_span_eq_top_of_localRing _).mp
Proof state after:
case a
R : Type u_2
S : Type u_1
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
this✝ : Module.Finite R (S ⧸ Ideal.map (algebraMap R S) p)
this : Module.Finite (R ⧸ p) (S ⧸ Ideal.map (algebraMap R S) p)
b : Basis (Module.Free.ChooseBasisIndex (R ⧸ p) (S ⧸ Ideal.map (algebraMap R S) p)) (R ⧸ p)
  (S ⧸ Ideal.map (algebraMap R S) p) :=
  Module.Free.chooseBasis (R ⧸ p) (S ⧸ Ideal.map (algebraMap R S) p)
b' : Module.Free.ChooseBasisIndex (R ⧸ p) (S ⧸ Ideal.map (algebraMap R S) p) → S
hb' :
  ∀ (i : Module.Free.ChooseBasisIndex (R ⧸ p) (S ⧸ Ideal.map (algebraMap R S) p)),
    (Ideal.Quotient.mk (Ideal.map (algebraMap R S) p)) (b' i) = b i
⊢ Submodule.span (R ⧸ p) (⇑(Ideal.Quotient.mk (Ideal.map (algebraMap R S) p)) '' Set.range b') = ⊤
Theorem: finrank_quotient_map_of_localRing
Proof state before:
case a
R : Type u_2
S : Type u_1
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
this✝ : Module.Finite R (S ⧸ Ideal.map (algebraMap R S) p)
this : Module.Finite (R ⧸ p) (S ⧸ Ideal.map (algebraMap R S) p)
b : Basis (Module.Free.ChooseBasisIndex (R ⧸ p) (S ⧸ Ideal.map (algebraMap R S) p)) (R ⧸ p)
  (S ⧸ Ideal.map (algebraMap R S) p) :=
  Module.Free.chooseBasis (R ⧸ p) (S ⧸ Ideal.map (algebraMap R S) p)
b' : Module.Free.ChooseBasisIndex (R ⧸ p) (S ⧸ Ideal.map (algebraMap R S) p) → S
hb' :
  ∀ (i : Module.Free.ChooseBasisIndex (R ⧸ p) (S ⧸ Ideal.map (algebraMap R S) p)),
    (Ideal.Quotient.mk (Ideal.map (algebraMap R S) p)) (b' i) = b i
⊢ Submodule.span (R ⧸ p) (⇑(Ideal.Quotient.mk (Ideal.map (algebraMap R S) p)) '' Set.range b') = ⊤
Tactic:
rw [← Set.range_comp, show Ideal.Quotient.mk pS ∘ b' = ⇑b from funext hb']
Proof state after:
case a
R : Type u_2
S : Type u_1
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
this✝ : Module.Finite R (S ⧸ Ideal.map (algebraMap R S) p)
this : Module.Finite (R ⧸ p) (S ⧸ Ideal.map (algebraMap R S) p)
b : Basis (Module.Free.ChooseBasisIndex (R ⧸ p) (S ⧸ Ideal.map (algebraMap R S) p)) (R ⧸ p)
  (S ⧸ Ideal.map (algebraMap R S) p) :=
  Module.Free.chooseBasis (R ⧸ p) (S ⧸ Ideal.map (algebraMap R S) p)
b' : Module.Free.ChooseBasisIndex (R ⧸ p) (S ⧸ Ideal.map (algebraMap R S) p) → S
hb' :
  ∀ (i : Module.Free.ChooseBasisIndex (R ⧸ p) (S ⧸ Ideal.map (algebraMap R S) p)),
    (Ideal.Quotient.mk (Ideal.map (algebraMap R S) p)) (b' i) = b i
⊢ Submodule.span (R ⧸ p) (Set.range ⇑b) = ⊤
Theorem: finrank_quotient_map_of_localRing
Proof state before:
case a
R : Type u_2
S : Type u_1
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
this✝ : Module.Finite R (S ⧸ Ideal.map (algebraMap R S) p)
this : Module.Finite (R ⧸ p) (S ⧸ Ideal.map (algebraMap R S) p)
b : Basis (Module.Free.ChooseBasisIndex (R ⧸ p) (S ⧸ Ideal.map (algebraMap R S) p)) (R ⧸ p)
  (S ⧸ Ideal.map (algebraMap R S) p) :=
  Module.Free.chooseBasis (R ⧸ p) (S ⧸ Ideal.map (algebraMap R S) p)
b' : Module.Free.ChooseBasisIndex (R ⧸ p) (S ⧸ Ideal.map (algebraMap R S) p) → S
hb' :
  ∀ (i : Module.Free.ChooseBasisIndex (R ⧸ p) (S ⧸ Ideal.map (algebraMap R S) p)),
    (Ideal.Quotient.mk (Ideal.map (algebraMap R S) p)) (b' i) = b i
⊢ Submodule.span (R ⧸ p) (Set.range ⇑b) = ⊤
Tactic:
exact b.span_eq
Proof state after:
no goals
Theorem: basisQuotientOfLocalRing_apply
Proof 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
i : ι
⊢ (basisQuotientOfLocalRing b) i = (Ideal.Quotient.mk (Ideal.map (algebraMap R S) p)) (b i)
Tactic:
delta basisQuotientOfLocalRing
Proof 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
i : ι
⊢ (basisOfTopLeSpanOfCardEqFinrank (⇑(Ideal.Quotient.mk (Ideal.map (algebraMap R S) p)) ∘ ⇑b) ⋯ ⋯) i =
    (Ideal.Quotient.mk (Ideal.map (algebraMap R S) p)) (b i)
Theorem: basisQuotientOfLocalRing_apply
Proof 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
i : ι
⊢ (basisOfTopLeSpanOfCardEqFinrank (⇑(Ideal.Quotient.mk (Ideal.map (algebraMap R S) p)) ∘ ⇑b) ⋯ ⋯) i =
    (Ideal.Quotient.mk (Ideal.map (algebraMap R S) p)) (b i)
Tactic:
rw [coe_basisOfTopLeSpanOfCardEqFinrank, Function.comp_apply]
Proof state after:
no goals
Theorem: basisQuotientOfLocalRing_repr
Proof 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
Proof 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)
Theorem: basisQuotientOfLocalRing_repr
Proof 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
Proof 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))
Theorem: basisQuotientOfLocalRing_repr
Proof 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
Proof 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)))
Theorem: basisQuotientOfLocalRing_repr
Proof 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]
Proof 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)))