internlm/Lean-Github huggingface dataset:
Theorem: quotient_span_eq_top_iff_span_eq_top_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
s : Set S
⊢ Submodule.restrictScalars R (Submodule.span (R ⧸ p) (⇑(Ideal.Quotient.mk (Ideal.map (algebraMap R S) p)) '' s)) =
    Submodule.restrictScalars R
      (Submodule.span (R ⧸ p) (⇑(IsScalarTower.toAlgHom R S (S ⧸ Ideal.map (algebraMap R S) p)) '' s))
Tactic:
rfl
Proof state after:
no goals
Theorem: quotient_span_eq_top_iff_span_eq_top_of_localRing
Proof state before:
case mp
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
s : Set S
H :
  Submodule.restrictScalars R (Submodule.span (R ⧸ p) (⇑(Ideal.Quotient.mk (Ideal.map (algebraMap R S) p)) '' s)) =
    Submodule.map (IsScalarTower.toAlgHom R S (S ⧸ Ideal.map (algebraMap R S) p)) (Submodule.span R s)
⊢ Submodule.span (R ⧸ p) (⇑(Ideal.Quotient.mk (Ideal.map (algebraMap R S) p)) '' s) = ⊤ → Submodule.span R s = ⊤
Tactic:
intro hs
Proof state after:
case mp
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
s : Set S
H :
  Submodule.restrictScalars R (Submodule.span (R ⧸ p) (⇑(Ideal.Quotient.mk (Ideal.map (algebraMap R S) p)) '' s)) =
    Submodule.map (IsScalarTower.toAlgHom R S (S ⧸ Ideal.map (algebraMap R S) p)) (Submodule.span R s)
hs : Submodule.span (R ⧸ p) (⇑(Ideal.Quotient.mk (Ideal.map (algebraMap R S) p)) '' s) = ⊤
⊢ Submodule.span R s = ⊤
Theorem: quotient_span_eq_top_iff_span_eq_top_of_localRing
Proof state before:
case mp
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
s : Set S
H :
  Submodule.restrictScalars R (Submodule.span (R ⧸ p) (⇑(Ideal.Quotient.mk (Ideal.map (algebraMap R S) p)) '' s)) =
    Submodule.map (IsScalarTower.toAlgHom R S (S ⧸ Ideal.map (algebraMap R S) p)) (Submodule.span R s)
hs : Submodule.span (R ⧸ p) (⇑(Ideal.Quotient.mk (Ideal.map (algebraMap R S) p)) '' s) = ⊤
⊢ Submodule.span R s = ⊤
Tactic:
rw [← top_le_iff]
Proof state after:
case mp
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
s : Set S
H :
  Submodule.restrictScalars R (Submodule.span (R ⧸ p) (⇑(Ideal.Quotient.mk (Ideal.map (algebraMap R S) p)) '' s)) =
    Submodule.map (IsScalarTower.toAlgHom R S (S ⧸ Ideal.map (algebraMap R S) p)) (Submodule.span R s)
hs : Submodule.span (R ⧸ p) (⇑(Ideal.Quotient.mk (Ideal.map (algebraMap R S) p)) '' s) = ⊤
⊢ ⊤ ≤ Submodule.span R s
Theorem: quotient_span_eq_top_iff_span_eq_top_of_localRing
Proof state before:
case mp
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
s : Set S
H :
  Submodule.restrictScalars R (Submodule.span (R ⧸ p) (⇑(Ideal.Quotient.mk (Ideal.map (algebraMap R S) p)) '' s)) =
    Submodule.map (IsScalarTower.toAlgHom R S (S ⧸ Ideal.map (algebraMap R S) p)) (Submodule.span R s)
hs : Submodule.span (R ⧸ p) (⇑(Ideal.Quotient.mk (Ideal.map (algebraMap R S) p)) '' s) = ⊤
⊢ ⊤ ≤ Submodule.span R s
Tactic:
apply Submodule.le_of_le_smul_of_le_jacobson_bot
Proof state after:
case mp.hN'
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
s : Set S
H :
  Submodule.restrictScalars R (Submodule.span (R ⧸ p) (⇑(Ideal.Quotient.mk (Ideal.map (algebraMap R S) p)) '' s)) =
    Submodule.map (IsScalarTower.toAlgHom R S (S ⧸ Ideal.map (algebraMap R S) p)) (Submodule.span R s)
hs : Submodule.span (R ⧸ p) (⇑(Ideal.Quotient.mk (Ideal.map (algebraMap R S) p)) '' s) = ⊤
⊢ ⊤.FG

case mp.hIJ
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
s : Set S
H :
  Submodule.restrictScalars R (Submodule.span (R ⧸ p) (⇑(Ideal.Quotient.mk (Ideal.map (algebraMap R S) p)) '' s)) =
    Submodule.map (IsScalarTower.toAlgHom R S (S ⧸ Ideal.map (algebraMap R S) p)) (Submodule.span R s)
hs : Submodule.span (R ⧸ p) (⇑(Ideal.Quotient.mk (Ideal.map (algebraMap R S) p)) '' s) = ⊤
⊢ ?mp.I ≤ ⊥.jacobson

case mp.hNN
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
s : Set S
H :
  Submodule.restrictScalars R (Submodule.span (R ⧸ p) (⇑(Ideal.Quotient.mk (Ideal.map (algebraMap R S) p)) '' s)) =
    Submodule.map (IsScalarTower.toAlgHom R S (S ⧸ Ideal.map (algebraMap R S) p)) (Submodule.span R s)
hs : Submodule.span (R ⧸ p) (⇑(Ideal.Quotient.mk (Ideal.map (algebraMap R S) p)) '' s) = ⊤
⊢ ⊤ ≤ Submodule.span R s ⊔ ?mp.I • ⊤

case mp.I
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
s : Set S
H :
  Submodule.restrictScalars R (Submodule.span (R ⧸ p) (⇑(Ideal.Quotient.mk (Ideal.map (algebraMap R S) p)) '' s)) =
    Submodule.map (IsScalarTower.toAlgHom R S (S ⧸ Ideal.map (algebraMap R S) p)) (Submodule.span R s)
hs : Submodule.span (R ⧸ p) (⇑(Ideal.Quotient.mk (Ideal.map (algebraMap R S) p)) '' s) = ⊤
⊢ Ideal R
Theorem: quotient_span_eq_top_iff_span_eq_top_of_localRing
Proof state before:
case mp.hN'
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
s : Set S
H :
  Submodule.restrictScalars R (Submodule.span (R ⧸ p) (⇑(Ideal.Quotient.mk (Ideal.map (algebraMap R S) p)) '' s)) =
    Submodule.map (IsScalarTower.toAlgHom R S (S ⧸ Ideal.map (algebraMap R S) p)) (Submodule.span R s)
hs : Submodule.span (R ⧸ p) (⇑(Ideal.Quotient.mk (Ideal.map (algebraMap R S) p)) '' s) = ⊤
⊢ ⊤.FG
Tactic:
exact Module.finite_def.mp ‹_›
Proof state after:
no goals
Theorem: quotient_span_eq_top_iff_span_eq_top_of_localRing
Proof state before:
case mp.hIJ
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
s : Set S
H :
  Submodule.restrictScalars R (Submodule.span (R ⧸ p) (⇑(Ideal.Quotient.mk (Ideal.map (algebraMap R S) p)) '' s)) =
    Submodule.map (IsScalarTower.toAlgHom R S (S ⧸ Ideal.map (algebraMap R S) p)) (Submodule.span R s)
hs : Submodule.span (R ⧸ p) (⇑(Ideal.Quotient.mk (Ideal.map (algebraMap R S) p)) '' s) = ⊤
⊢ ?mp.I ≤ ⊥.jacobson
Tactic:
exact (jacobson_eq_maximalIdeal ⊥ bot_ne_top).ge
Proof state after:
no goals
Theorem: quotient_span_eq_top_iff_span_eq_top_of_localRing
Proof state before:
case mp.hNN
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
s : Set S
H :
  Submodule.restrictScalars R (Submodule.span (R ⧸ p) (⇑(Ideal.Quotient.mk (Ideal.map (algebraMap R S) p)) '' s)) =
    Submodule.map (IsScalarTower.toAlgHom R S (S ⧸ Ideal.map (algebraMap R S) p)) (Submodule.span R s)
hs : Submodule.span (R ⧸ p) (⇑(Ideal.Quotient.mk (Ideal.map (algebraMap R S) p)) '' s) = ⊤
⊢ ⊤ ≤ Submodule.span R s ⊔ p • ⊤
Tactic:
rw [Ideal.smul_top_eq_map]
Proof state after:
case mp.hNN
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
s : Set S
H :
  Submodule.restrictScalars R (Submodule.span (R ⧸ p) (⇑(Ideal.Quotient.mk (Ideal.map (algebraMap R S) p)) '' s)) =
    Submodule.map (IsScalarTower.toAlgHom R S (S ⧸ Ideal.map (algebraMap R S) p)) (Submodule.span R s)
hs : Submodule.span (R ⧸ p) (⇑(Ideal.Quotient.mk (Ideal.map (algebraMap R S) p)) '' s) = ⊤
⊢ ⊤ ≤ Submodule.span R s ⊔ Submodule.restrictScalars R (Ideal.map (algebraMap R S) p)
Theorem: quotient_span_eq_top_iff_span_eq_top_of_localRing
Proof state before:
case mp.hNN
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
s : Set S
H :
  Submodule.restrictScalars R (Submodule.span (R ⧸ p) (⇑(Ideal.Quotient.mk (Ideal.map (algebraMap R S) p)) '' s)) =
    Submodule.map (IsScalarTower.toAlgHom R S (S ⧸ Ideal.map (algebraMap R S) p)) (Submodule.span R s)
hs : Submodule.span (R ⧸ p) (⇑(Ideal.Quotient.mk (Ideal.map (algebraMap R S) p)) '' s) = ⊤
⊢ ⊤ ≤ Submodule.span R s ⊔ Submodule.restrictScalars R (Ideal.map (algebraMap R S) p)
Tactic:
rintro x -
Proof state after:
case mp.hNN
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
s : Set S
H :
  Submodule.restrictScalars R (Submodule.span (R ⧸ p) (⇑(Ideal.Quotient.mk (Ideal.map (algebraMap R S) p)) '' s)) =
    Submodule.map (IsScalarTower.toAlgHom R S (S ⧸ Ideal.map (algebraMap R S) p)) (Submodule.span R s)
hs : Submodule.span (R ⧸ p) (⇑(Ideal.Quotient.mk (Ideal.map (algebraMap R S) p)) '' s) = ⊤
x : S
⊢ x ∈ Submodule.span R s ⊔ Submodule.restrictScalars R (Ideal.map (algebraMap R S) p)
Theorem: quotient_span_eq_top_iff_span_eq_top_of_localRing
Proof state before:
case mp.hNN
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
s : Set S
H :
  Submodule.restrictScalars R (Submodule.span (R ⧸ p) (⇑(Ideal.Quotient.mk (Ideal.map (algebraMap R S) p)) '' s)) =
    Submodule.map (IsScalarTower.toAlgHom R S (S ⧸ Ideal.map (algebraMap R S) p)) (Submodule.span R s)
hs : Submodule.span (R ⧸ p) (⇑(Ideal.Quotient.mk (Ideal.map (algebraMap R S) p)) '' s) = ⊤
x : S
⊢ x ∈ Submodule.span R s ⊔ Submodule.restrictScalars R (Ideal.map (algebraMap R S) p)
Tactic:
have : LinearMap.ker (IsScalarTower.toAlgHom R S (S ⧸ pS)) =
    Submodule.restrictScalars R pS := by
  ext; simp [Ideal.Quotient.eq_zero_iff_mem]
Proof state after:
case mp.hNN
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
s : Set S
H :
  Submodule.restrictScalars R (Submodule.span (R ⧸ p) (⇑(Ideal.Quotient.mk (Ideal.map (algebraMap R S) p)) '' s)) =
    Submodule.map (IsScalarTower.toAlgHom R S (S ⧸ Ideal.map (algebraMap R S) p)) (Submodule.span R s)
hs : Submodule.span (R ⧸ p) (⇑(Ideal.Quotient.mk (Ideal.map (algebraMap R S) p)) '' s) = ⊤
x : S
this :
  LinearMap.ker (IsScalarTower.toAlgHom R S (S ⧸ Ideal.map (algebraMap R S) p)) =
    Submodule.restrictScalars R (Ideal.map (algebraMap R S) p)
⊢ x ∈ Submodule.span R s ⊔ Submodule.restrictScalars R (Ideal.map (algebraMap R S) p)
Theorem: quotient_span_eq_top_iff_span_eq_top_of_localRing
Proof state before:
case mp.hNN
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
s : Set S
H :
  Submodule.restrictScalars R (Submodule.span (R ⧸ p) (⇑(Ideal.Quotient.mk (Ideal.map (algebraMap R S) p)) '' s)) =
    Submodule.map (IsScalarTower.toAlgHom R S (S ⧸ Ideal.map (algebraMap R S) p)) (Submodule.span R s)
hs : Submodule.span (R ⧸ p) (⇑(Ideal.Quotient.mk (Ideal.map (algebraMap R S) p)) '' s) = ⊤
x : S
this :
  LinearMap.ker (IsScalarTower.toAlgHom R S (S ⧸ Ideal.map (algebraMap R S) p)) =
    Submodule.restrictScalars R (Ideal.map (algebraMap R S) p)
⊢ x ∈ Submodule.span R s ⊔ Submodule.restrictScalars R (Ideal.map (algebraMap R S) p)
Tactic:
rw [← this, ← Submodule.comap_map_eq, Submodule.mem_comap, ← H, hs]
Proof state after:
case mp.hNN
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
s : Set S
H :
  Submodule.restrictScalars R (Submodule.span (R ⧸ p) (⇑(Ideal.Quotient.mk (Ideal.map (algebraMap R S) p)) '' s)) =
    Submodule.map (IsScalarTower.toAlgHom R S (S ⧸ Ideal.map (algebraMap R S) p)) (Submodule.span R s)
hs : Submodule.span (R ⧸ p) (⇑(Ideal.Quotient.mk (Ideal.map (algebraMap R S) p)) '' s) = ⊤
x : S
this :
  LinearMap.ker (IsScalarTower.toAlgHom R S (S ⧸ Ideal.map (algebraMap R S) p)) =
    Submodule.restrictScalars R (Ideal.map (algebraMap R S) p)
⊢ (IsScalarTower.toAlgHom R S (S ⧸ Ideal.map (algebraMap R S) p)) x ∈ Submodule.restrictScalars R ⊤
Theorem: quotient_span_eq_top_iff_span_eq_top_of_localRing
Proof state before:
case mp.hNN
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
s : Set S
H :
  Submodule.restrictScalars R (Submodule.span (R ⧸ p) (⇑(Ideal.Quotient.mk (Ideal.map (algebraMap R S) p)) '' s)) =
    Submodule.map (IsScalarTower.toAlgHom R S (S ⧸ Ideal.map (algebraMap R S) p)) (Submodule.span R s)
hs : Submodule.span (R ⧸ p) (⇑(Ideal.Quotient.mk (Ideal.map (algebraMap R S) p)) '' s) = ⊤
x : S
this :
  LinearMap.ker (IsScalarTower.toAlgHom R S (S ⧸ Ideal.map (algebraMap R S) p)) =
    Submodule.restrictScalars R (Ideal.map (algebraMap R S) p)
⊢ (IsScalarTower.toAlgHom R S (S ⧸ Ideal.map (algebraMap R S) p)) x ∈ Submodule.restrictScalars R ⊤
Tactic:
trivial
Proof state after:
no goals
Theorem: quotient_span_eq_top_iff_span_eq_top_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
s : Set S
H :
  Submodule.restrictScalars R (Submodule.span (R ⧸ p) (⇑(Ideal.Quotient.mk (Ideal.map (algebraMap R S) p)) '' s)) =
    Submodule.map (IsScalarTower.toAlgHom R S (S ⧸ Ideal.map (algebraMap R S) p)) (Submodule.span R s)
hs : Submodule.span (R ⧸ p) (⇑(Ideal.Quotient.mk (Ideal.map (algebraMap R S) p)) '' s) = ⊤
x : S
⊢ LinearMap.ker (IsScalarTower.toAlgHom R S (S ⧸ Ideal.map (algebraMap R S) p)) =
    Submodule.restrictScalars R (Ideal.map (algebraMap R S) p)
Tactic:
ext
Proof state after:
case h
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
s : Set S
H :
  Submodule.restrictScalars R (Submodule.span (R ⧸ p) (⇑(Ideal.Quotient.mk (Ideal.map (algebraMap R S) p)) '' s)) =
    Submodule.map (IsScalarTower.toAlgHom R S (S ⧸ Ideal.map (algebraMap R S) p)) (Submodule.span R s)
hs : Submodule.span (R ⧸ p) (⇑(Ideal.Quotient.mk (Ideal.map (algebraMap R S) p)) '' s) = ⊤
x x✝ : S
⊢ x✝ ∈ LinearMap.ker (IsScalarTower.toAlgHom R S (S ⧸ Ideal.map (algebraMap R S) p)) ↔
    x✝ ∈ Submodule.restrictScalars R (Ideal.map (algebraMap R S) p)
Theorem: quotient_span_eq_top_iff_span_eq_top_of_localRing
Proof state before:
case h
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
s : Set S
H :
  Submodule.restrictScalars R (Submodule.span (R ⧸ p) (⇑(Ideal.Quotient.mk (Ideal.map (algebraMap R S) p)) '' s)) =
    Submodule.map (IsScalarTower.toAlgHom R S (S ⧸ Ideal.map (algebraMap R S) p)) (Submodule.span R s)
hs : Submodule.span (R ⧸ p) (⇑(Ideal.Quotient.mk (Ideal.map (algebraMap R S) p)) '' s) = ⊤
x x✝ : S
⊢ x✝ ∈ LinearMap.ker (IsScalarTower.toAlgHom R S (S ⧸ Ideal.map (algebraMap R S) p)) ↔
    x✝ ∈ Submodule.restrictScalars R (Ideal.map (algebraMap R S) p)
Tactic:
simp [Ideal.Quotient.eq_zero_iff_mem]
Proof state after:
no goals
Theorem: quotient_span_eq_top_iff_span_eq_top_of_localRing
Proof state before:
case mpr
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
s : Set S
H :
  Submodule.restrictScalars R (Submodule.span (R ⧸ p) (⇑(Ideal.Quotient.mk (Ideal.map (algebraMap R S) p)) '' s)) =
    Submodule.map (IsScalarTower.toAlgHom R S (S ⧸ Ideal.map (algebraMap R S) p)) (Submodule.span R s)
⊢ Submodule.span R s = ⊤ → Submodule.span (R ⧸ p) (⇑(Ideal.Quotient.mk (Ideal.map (algebraMap R S) p)) '' s) = ⊤
Tactic:
intro hs
Proof state after:
case mpr
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
s : Set S
H :
  Submodule.restrictScalars R (Submodule.span (R ⧸ p) (⇑(Ideal.Quotient.mk (Ideal.map (algebraMap R S) p)) '' s)) =
    Submodule.map (IsScalarTower.toAlgHom R S (S ⧸ Ideal.map (algebraMap R S) p)) (Submodule.span R s)
hs : Submodule.span R s = ⊤
⊢ Submodule.span (R ⧸ p) (⇑(Ideal.Quotient.mk (Ideal.map (algebraMap R S) p)) '' s) = ⊤
Theorem: quotient_span_eq_top_iff_span_eq_top_of_localRing
Proof state before:
case mpr
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
s : Set S
H :
  Submodule.restrictScalars R (Submodule.span (R ⧸ p) (⇑(Ideal.Quotient.mk (Ideal.map (algebraMap R S) p)) '' s)) =
    Submodule.map (IsScalarTower.toAlgHom R S (S ⧸ Ideal.map (algebraMap R S) p)) (Submodule.span R s)
hs : Submodule.span R s = ⊤
⊢ Submodule.span (R ⧸ p) (⇑(Ideal.Quotient.mk (Ideal.map (algebraMap R S) p)) '' s) = ⊤
Tactic:
rw [hs, Submodule.map_top] at H
Proof state after:
case mpr
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
s : Set S
H :
  Submodule.restrictScalars R (Submodule.span (R ⧸ p) (⇑(Ideal.Quotient.mk (Ideal.map (algebraMap R S) p)) '' s)) =
    LinearMap.range (IsScalarTower.toAlgHom R S (S ⧸ Ideal.map (algebraMap R S) p))
hs : Submodule.span R s = ⊤
⊢ Submodule.span (R ⧸ p) (⇑(Ideal.Quotient.mk (Ideal.map (algebraMap R S) p)) '' s) = ⊤
Theorem: quotient_span_eq_top_iff_span_eq_top_of_localRing
Proof state before:
case mpr
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
s : Set S
H :
  Submodule.restrictScalars R (Submodule.span (R ⧸ p) (⇑(Ideal.Quotient.mk (Ideal.map (algebraMap R S) p)) '' s)) =
    LinearMap.range (IsScalarTower.toAlgHom R S (S ⧸ Ideal.map (algebraMap R S) p))
hs : Submodule.span R s = ⊤
⊢ Submodule.span (R ⧸ p) (⇑(Ideal.Quotient.mk (Ideal.map (algebraMap R S) p)) '' s) = ⊤
Tactic:
change _ = LinearMap.range (Ideal.Quotient.mkₐ _ _) at H
Proof state after:
case mpr
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
s : Set S
hs : Submodule.span R s = ⊤
H :
  Submodule.restrictScalars R (Submodule.span (R ⧸ p) (⇑(Ideal.Quotient.mk (Ideal.map (algebraMap R S) p)) '' s)) =
    LinearMap.range (Ideal.Quotient.mkₐ R (Ideal.map (algebraMap R S) p))
⊢ Submodule.span (R ⧸ p) (⇑(Ideal.Quotient.mk (Ideal.map (algebraMap R S) p)) '' s) = ⊤
Theorem: quotient_span_eq_top_iff_span_eq_top_of_localRing
Proof state before:
case mpr
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
s : Set S
hs : Submodule.span R s = ⊤
H :
  Submodule.restrictScalars R (Submodule.span (R ⧸ p) (⇑(Ideal.Quotient.mk (Ideal.map (algebraMap R S) p)) '' s)) =
    LinearMap.range (Ideal.Quotient.mkₐ R (Ideal.map (algebraMap R S) p))
⊢ Submodule.span (R ⧸ p) (⇑(Ideal.Quotient.mk (Ideal.map (algebraMap R S) p)) '' s) = ⊤
Tactic:
rwa [LinearMap.range_eq_top.mpr (Ideal.Quotient.mkₐ_surjective _ _),
  Submodule.restrictScalars_eq_top_iff] at H
Proof state after:
no goals
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
⊢ finrank (R ⧸ p) (S ⧸ Ideal.map (algebraMap R S) p) = finrank R S
Tactic:
have : Module.Finite R (S ⧸ pS) := Module.Finite.of_surjective
  (IsScalarTower.toAlgHom R S (S ⧸ pS)).toLinearMap (Ideal.Quotient.mk_surjective (I := pS))
Proof state after:
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)
⊢ finrank (R ⧸ p) (S ⧸ Ideal.map (algebraMap R S) p) = finrank R S
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)
⊢ finrank (R ⧸ p) (S ⧸ Ideal.map (algebraMap R S) p) = finrank R S
Tactic:
have : Module.Finite (R ⧸ p) (S ⧸ pS) := Module.Finite.of_restrictScalars_finite R _ _
Proof state after:
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