Theorem: Algebra.isNilpotent_trace_of_isNilpotent (FltRegular/NumberTheory/AuxLemmas.lean)

State before:
R : Type u
S : Type v
inst✝² : CommRing R
inst✝¹ : CommRing S
inst✝ : Algebra R S
x : S
hx : IsNilpotent x
⊢ IsNilpotent ((trace R S) x)
Tactic:
by_cases hS : ∃ s : Finset S, Nonempty (Basis s R S)
State after:
case pos
R : Type u
S : Type v
inst✝² : CommRing R
inst✝¹ : CommRing S
inst✝ : Algebra R S
x : S
hx : IsNilpotent x
hS : ∃ s, Nonempty (Basis { x // x ∈ s } R S)
⊢ IsNilpotent ((trace R S) x)

case neg
R : Type u
S : Type v
inst✝² : CommRing R
inst✝¹ : CommRing S
inst✝ : Algebra R S
x : S
hx : IsNilpotent x
hS : ¬∃ s, Nonempty (Basis { x // x ∈ s } R S)
⊢ IsNilpotent ((trace R S) x)

State before:
case pos
R : Type u
S : Type v
inst✝² : CommRing R
inst✝¹ : CommRing S
inst✝ : Algebra R S
x : S
hx : IsNilpotent x
hS : ∃ s, Nonempty (Basis { x // x ∈ s } R S)
⊢ IsNilpotent ((trace R S) x)
Tactic:
obtain ⟨s, ⟨b⟩⟩ := hS
State after:
case pos.intro.intro
R : Type u
S : Type v
inst✝² : CommRing R
inst✝¹ : CommRing S
inst✝ : Algebra R S
x : S
hx : IsNilpotent x
s : Finset S
b : Basis { x // x ∈ s } R S
⊢ IsNilpotent ((trace R S) x)

State before:
case pos.intro.intro
R : Type u
S : Type v
inst✝² : CommRing R
inst✝¹ : CommRing S
inst✝ : Algebra R S
x : S
hx : IsNilpotent x
s : Finset S
b : Basis { x // x ∈ s } R S
⊢ IsNilpotent ((trace R S) x)
Tactic:
have := Module.Finite.of_basis b
State after:
case pos.intro.intro
R : Type u
S : Type v
inst✝² : CommRing R
inst✝¹ : CommRing S
inst✝ : Algebra R S
x : S
hx : IsNilpotent x
s : Finset S
b : Basis { x // x ∈ s } R S
this : Module.Finite R S
⊢ IsNilpotent ((trace R S) x)

State before:
case pos.intro.intro
R : Type u
S : Type v
inst✝² : CommRing R
inst✝¹ : CommRing S
inst✝ : Algebra R S
x : S
hx : IsNilpotent x
s : Finset S
b : Basis { x // x ∈ s } R S
this : Module.Finite R S
⊢ IsNilpotent ((trace R S) x)
Tactic:
have := (Module.free_def.{u, v, v} R S).mpr ⟨s, ⟨b⟩⟩
State after:
case pos.intro.intro
R : Type u
S : Type v
inst✝² : CommRing R
inst✝¹ : CommRing S
inst✝ : Algebra R S
x : S
hx : IsNilpotent x
s : Finset S
b : Basis { x // x ∈ s } R S
this✝ : Module.Finite R S
this : Module.Free R S
⊢ IsNilpotent ((trace R S) x)

State before:
case pos.intro.intro
R : Type u
S : Type v
inst✝² : CommRing R
inst✝¹ : CommRing S
inst✝ : Algebra R S
x : S
hx : IsNilpotent x
s : Finset S
b : Basis { x // x ∈ s } R S
this✝ : Module.Finite R S
this : Module.Free R S
⊢ IsNilpotent ((trace R S) x)
Tactic:
apply LinearMap.isNilpotent_trace_of_isNilpotent (hx.map (lmul R S))
State after:
no goals

State before:
case neg
R : Type u
S : Type v
inst✝² : CommRing R
inst✝¹ : CommRing S
inst✝ : Algebra R S
x : S
hx : IsNilpotent x
hS : ¬∃ s, Nonempty (Basis { x // x ∈ s } R S)
⊢ IsNilpotent ((trace R S) x)
Tactic:
rw [trace_eq_zero_of_not_exists_basis _ hS, LinearMap.zero_apply]
State after:
case neg
R : Type u
S : Type v
inst✝² : CommRing R
inst✝¹ : CommRing S
inst✝ : Algebra R S
x : S
hx : IsNilpotent x
hS : ¬∃ s, Nonempty (Basis { x // x ∈ s } R S)
⊢ IsNilpotent 0

State before:
case neg
R : Type u
S : Type v
inst✝² : CommRing R
inst✝¹ : CommRing S
inst✝ : Algebra R S
x : S
hx : IsNilpotent x
hS : ¬∃ s, Nonempty (Basis { x // x ∈ s } R S)
⊢ IsNilpotent 0
Tactic:
exact IsNilpotent.zero
State after:
no goals