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

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.span (R ⧸ p) (⇑(Ideal.Quotient.mk (Ideal.map (algebraMap R S) p)) '' s) = ⊤ ↔ Submodule.span R s = ⊤
Tactic:
have H : (Submodule.span (R ⧸ p) ((Ideal.Quotient.mk (I := pS)) '' s)).restrictScalars R =
    (Submodule.span R s).map (IsScalarTower.toAlgHom R S (S ⧸ pS)) := by
  rw [Submodule.map_span, ← Submodule.restrictScalars_span R (R ⧸ p) Ideal.Quotient.mk_surjective]
  rfl
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
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 = ⊤

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)
⊢ Submodule.span (R ⧸ p) (⇑(Ideal.Quotient.mk (Ideal.map (algebraMap R S) p)) '' s) = ⊤ ↔ Submodule.span R s = ⊤
Tactic:
constructor
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)
⊢ Submodule.span (R ⧸ p) (⇑(Ideal.Quotient.mk (Ideal.map (algebraMap R S) p)) '' s) = ⊤ → Submodule.span R s = ⊤

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) = ⊤

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.map (IsScalarTower.toAlgHom R S (S ⧸ Ideal.map (algebraMap R S) p)) (Submodule.span R s)
Tactic:
rw [Submodule.map_span, ← Submodule.restrictScalars_span R (R ⧸ p) Ideal.Quotient.mk_surjective]
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
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))

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
State after:
no goals

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
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 = ⊤

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]
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

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
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

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 ‹_›
State after:
no goals

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
State after:
no goals

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]
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)

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 -
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)

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]
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)

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]
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 ⊤

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
State after:
no goals

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
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)

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]
State after:
no goals

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
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) = ⊤

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
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) = ⊤

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
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) = ⊤

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
State after:
no goals