Theorem: DividedPowerAlgebra.roby4.isAugmentation_iff_isCompl (DividedPowers/DPAlgebra/Dpow.lean)

State before:
R : Type u
inst✝⁴ : CommRing R
A : Type u
inst✝³ : CommRing A
inst✝² : DecidableEq A
S : Type u
inst✝¹ : CommRing S
inst✝ : Algebra A S
I : Ideal S
hI : DividedPowers I
S₀ : Subalgebra A S
hIS₀ : IsCompl (Subalgebra.toSubmodule S₀) (Submodule.restrictScalars A I)
⊢ IsAugmentation (↥S₀) I ↔ IsCompl (Subalgebra.toSubmodule S₀) (Submodule.restrictScalars A I)
Tactic:
unfold IsAugmentation
State after:
R : Type u
inst✝⁴ : CommRing R
A : Type u
inst✝³ : CommRing A
inst✝² : DecidableEq A
S : Type u
inst✝¹ : CommRing S
inst✝ : Algebra A S
I : Ideal S
hI : DividedPowers I
S₀ : Subalgebra A S
hIS₀ : IsCompl (Subalgebra.toSubmodule S₀) (Submodule.restrictScalars A I)
⊢ IsCompl (Subalgebra.toSubmodule ⊥) (Submodule.restrictScalars (↥S₀) I) ↔
    IsCompl (Subalgebra.toSubmodule S₀) (Submodule.restrictScalars A I)

State before:
R : Type u
inst✝⁴ : CommRing R
A : Type u
inst✝³ : CommRing A
inst✝² : DecidableEq A
S : Type u
inst✝¹ : CommRing S
inst✝ : Algebra A S
I : Ideal S
hI : DividedPowers I
S₀ : Subalgebra A S
hIS₀ : IsCompl (Subalgebra.toSubmodule S₀) (Submodule.restrictScalars A I)
⊢ IsCompl (Subalgebra.toSubmodule ⊥) (Submodule.restrictScalars (↥S₀) I) ↔
    IsCompl (Subalgebra.toSubmodule S₀) (Submodule.restrictScalars A I)
Tactic:
rw [← Submodule.isCompl_restrictScalars_iff A]
State after:
R : Type u
inst✝⁴ : CommRing R
A : Type u
inst✝³ : CommRing A
inst✝² : DecidableEq A
S : Type u
inst✝¹ : CommRing S
inst✝ : Algebra A S
I : Ideal S
hI : DividedPowers I
S₀ : Subalgebra A S
hIS₀ : IsCompl (Subalgebra.toSubmodule S₀) (Submodule.restrictScalars A I)
⊢ IsCompl (Submodule.restrictScalars A (Subalgebra.toSubmodule ⊥))
      (Submodule.restrictScalars A (Submodule.restrictScalars (↥S₀) I)) ↔
    IsCompl (Subalgebra.toSubmodule S₀) (Submodule.restrictScalars A I)

State before:
R : Type u
inst✝⁴ : CommRing R
A : Type u
inst✝³ : CommRing A
inst✝² : DecidableEq A
S : Type u
inst✝¹ : CommRing S
inst✝ : Algebra A S
I : Ideal S
hI : DividedPowers I
S₀ : Subalgebra A S
hIS₀ : IsCompl (Subalgebra.toSubmodule S₀) (Submodule.restrictScalars A I)
⊢ IsCompl (Submodule.restrictScalars A (Subalgebra.toSubmodule ⊥))
      (Submodule.restrictScalars A (Submodule.restrictScalars (↥S₀) I)) ↔
    IsCompl (Subalgebra.toSubmodule S₀) (Submodule.restrictScalars A I)
Tactic:
suffices Submodule.restrictScalars A (Submodule.restrictScalars S₀ I) =
  Submodule.restrictScalars A I by
  rw [this]
  suffices Submodule.restrictScalars A _ = Subalgebra.toSubmodule S₀ by
    rw [this]
  ext x
  simp only [Submodule.restrictScalars_mem, Subalgebra.mem_toSubmodule]
  apply Algebra.mem_bot_of_subalgebra_iff
State after:
R : Type u
inst✝⁴ : CommRing R
A : Type u
inst✝³ : CommRing A
inst✝² : DecidableEq A
S : Type u
inst✝¹ : CommRing S
inst✝ : Algebra A S
I : Ideal S
hI : DividedPowers I
S₀ : Subalgebra A S
hIS₀ : IsCompl (Subalgebra.toSubmodule S₀) (Submodule.restrictScalars A I)
⊢ Submodule.restrictScalars A (Submodule.restrictScalars (↥S₀) I) = Submodule.restrictScalars A I

State before:
R : Type u
inst✝⁴ : CommRing R
A : Type u
inst✝³ : CommRing A
inst✝² : DecidableEq A
S : Type u
inst✝¹ : CommRing S
inst✝ : Algebra A S
I : Ideal S
hI : DividedPowers I
S₀ : Subalgebra A S
hIS₀ : IsCompl (Subalgebra.toSubmodule S₀) (Submodule.restrictScalars A I)
⊢ Submodule.restrictScalars A (Submodule.restrictScalars (↥S₀) I) = Submodule.restrictScalars A I
Tactic:
ext x
State after:
case h
R : Type u
inst✝⁴ : CommRing R
A : Type u
inst✝³ : CommRing A
inst✝² : DecidableEq A
S : Type u
inst✝¹ : CommRing S
inst✝ : Algebra A S
I : Ideal S
hI : DividedPowers I
S₀ : Subalgebra A S
hIS₀ : IsCompl (Subalgebra.toSubmodule S₀) (Submodule.restrictScalars A I)
x : S
⊢ x ∈ Submodule.restrictScalars A (Submodule.restrictScalars (↥S₀) I) ↔ x ∈ Submodule.restrictScalars A I

State before:
case h
R : Type u
inst✝⁴ : CommRing R
A : Type u
inst✝³ : CommRing A
inst✝² : DecidableEq A
S : Type u
inst✝¹ : CommRing S
inst✝ : Algebra A S
I : Ideal S
hI : DividedPowers I
S₀ : Subalgebra A S
hIS₀ : IsCompl (Subalgebra.toSubmodule S₀) (Submodule.restrictScalars A I)
x : S
⊢ x ∈ Submodule.restrictScalars A (Submodule.restrictScalars (↥S₀) I) ↔ x ∈ Submodule.restrictScalars A I
Tactic:
simp only [Submodule.restrictScalars_mem]
State after:
no goals

State before:
R : Type u
inst✝⁴ : CommRing R
A : Type u
inst✝³ : CommRing A
inst✝² : DecidableEq A
S : Type u
inst✝¹ : CommRing S
inst✝ : Algebra A S
I : Ideal S
hI : DividedPowers I
S₀ : Subalgebra A S
hIS₀ : IsCompl (Subalgebra.toSubmodule S₀) (Submodule.restrictScalars A I)
this : Submodule.restrictScalars A (Submodule.restrictScalars (↥S₀) I) = Submodule.restrictScalars A I
⊢ IsCompl (Submodule.restrictScalars A (Subalgebra.toSubmodule ⊥))
      (Submodule.restrictScalars A (Submodule.restrictScalars (↥S₀) I)) ↔
    IsCompl (Subalgebra.toSubmodule S₀) (Submodule.restrictScalars A I)
Tactic:
rw [this]
State after:
R : Type u
inst✝⁴ : CommRing R
A : Type u
inst✝³ : CommRing A
inst✝² : DecidableEq A
S : Type u
inst✝¹ : CommRing S
inst✝ : Algebra A S
I : Ideal S
hI : DividedPowers I
S₀ : Subalgebra A S
hIS₀ : IsCompl (Subalgebra.toSubmodule S₀) (Submodule.restrictScalars A I)
this : Submodule.restrictScalars A (Submodule.restrictScalars (↥S₀) I) = Submodule.restrictScalars A I
⊢ IsCompl (Submodule.restrictScalars A (Subalgebra.toSubmodule ⊥)) (Submodule.restrictScalars A I) ↔
    IsCompl (Subalgebra.toSubmodule S₀) (Submodule.restrictScalars A I)

State before:
R : Type u
inst✝⁴ : CommRing R
A : Type u
inst✝³ : CommRing A
inst✝² : DecidableEq A
S : Type u
inst✝¹ : CommRing S
inst✝ : Algebra A S
I : Ideal S
hI : DividedPowers I
S₀ : Subalgebra A S
hIS₀ : IsCompl (Subalgebra.toSubmodule S₀) (Submodule.restrictScalars A I)
this : Submodule.restrictScalars A (Submodule.restrictScalars (↥S₀) I) = Submodule.restrictScalars A I
⊢ IsCompl (Submodule.restrictScalars A (Subalgebra.toSubmodule ⊥)) (Submodule.restrictScalars A I) ↔
    IsCompl (Subalgebra.toSubmodule S₀) (Submodule.restrictScalars A I)
Tactic:
suffices Submodule.restrictScalars A _ = Subalgebra.toSubmodule S₀ by
  rw [this]
State after:
R : Type u
inst✝⁴ : CommRing R
A : Type u
inst✝³ : CommRing A
inst✝² : DecidableEq A
S : Type u
inst✝¹ : CommRing S
inst✝ : Algebra A S
I : Ideal S
hI : DividedPowers I
S₀ : Subalgebra A S
hIS₀ : IsCompl (Subalgebra.toSubmodule S₀) (Submodule.restrictScalars A I)
this : Submodule.restrictScalars A (Submodule.restrictScalars (↥S₀) I) = Submodule.restrictScalars A I
⊢ Submodule.restrictScalars A (Subalgebra.toSubmodule ⊥) = Subalgebra.toSubmodule S₀

State before:
R : Type u
inst✝⁴ : CommRing R
A : Type u
inst✝³ : CommRing A
inst✝² : DecidableEq A
S : Type u
inst✝¹ : CommRing S
inst✝ : Algebra A S
I : Ideal S
hI : DividedPowers I
S₀ : Subalgebra A S
hIS₀ : IsCompl (Subalgebra.toSubmodule S₀) (Submodule.restrictScalars A I)
this : Submodule.restrictScalars A (Submodule.restrictScalars (↥S₀) I) = Submodule.restrictScalars A I
⊢ Submodule.restrictScalars A (Subalgebra.toSubmodule ⊥) = Subalgebra.toSubmodule S₀
Tactic:
ext x
State after:
case h
R : Type u
inst✝⁴ : CommRing R
A : Type u
inst✝³ : CommRing A
inst✝² : DecidableEq A
S : Type u
inst✝¹ : CommRing S
inst✝ : Algebra A S
I : Ideal S
hI : DividedPowers I
S₀ : Subalgebra A S
hIS₀ : IsCompl (Subalgebra.toSubmodule S₀) (Submodule.restrictScalars A I)
this : Submodule.restrictScalars A (Submodule.restrictScalars (↥S₀) I) = Submodule.restrictScalars A I
x : S
⊢ x ∈ Submodule.restrictScalars A (Subalgebra.toSubmodule ⊥) ↔ x ∈ Subalgebra.toSubmodule S₀

State before:
case h
R : Type u
inst✝⁴ : CommRing R
A : Type u
inst✝³ : CommRing A
inst✝² : DecidableEq A
S : Type u
inst✝¹ : CommRing S
inst✝ : Algebra A S
I : Ideal S
hI : DividedPowers I
S₀ : Subalgebra A S
hIS₀ : IsCompl (Subalgebra.toSubmodule S₀) (Submodule.restrictScalars A I)
this : Submodule.restrictScalars A (Submodule.restrictScalars (↥S₀) I) = Submodule.restrictScalars A I
x : S
⊢ x ∈ Submodule.restrictScalars A (Subalgebra.toSubmodule ⊥) ↔ x ∈ Subalgebra.toSubmodule S₀
Tactic:
simp only [Submodule.restrictScalars_mem, Subalgebra.mem_toSubmodule]
State after:
case h
R : Type u
inst✝⁴ : CommRing R
A : Type u
inst✝³ : CommRing A
inst✝² : DecidableEq A
S : Type u
inst✝¹ : CommRing S
inst✝ : Algebra A S
I : Ideal S
hI : DividedPowers I
S₀ : Subalgebra A S
hIS₀ : IsCompl (Subalgebra.toSubmodule S₀) (Submodule.restrictScalars A I)
this : Submodule.restrictScalars A (Submodule.restrictScalars (↥S₀) I) = Submodule.restrictScalars A I
x : S
⊢ x ∈ ⊥ ↔ x ∈ S₀

State before:
case h
R : Type u
inst✝⁴ : CommRing R
A : Type u
inst✝³ : CommRing A
inst✝² : DecidableEq A
S : Type u
inst✝¹ : CommRing S
inst✝ : Algebra A S
I : Ideal S
hI : DividedPowers I
S₀ : Subalgebra A S
hIS₀ : IsCompl (Subalgebra.toSubmodule S₀) (Submodule.restrictScalars A I)
this : Submodule.restrictScalars A (Submodule.restrictScalars (↥S₀) I) = Submodule.restrictScalars A I
x : S
⊢ x ∈ ⊥ ↔ x ∈ S₀
Tactic:
apply Algebra.mem_bot_of_subalgebra_iff
State after:
no goals

State before:
R : Type u
inst✝⁴ : CommRing R
A : Type u
inst✝³ : CommRing A
inst✝² : DecidableEq A
S : Type u
inst✝¹ : CommRing S
inst✝ : Algebra A S
I : Ideal S
hI : DividedPowers I
S₀ : Subalgebra A S
hIS₀ : IsCompl (Subalgebra.toSubmodule S₀) (Submodule.restrictScalars A I)
this✝ : Submodule.restrictScalars A (Submodule.restrictScalars (↥S₀) I) = Submodule.restrictScalars A I
this : Submodule.restrictScalars A ?m.89183 = Subalgebra.toSubmodule S₀
⊢ IsCompl (Submodule.restrictScalars A (Subalgebra.toSubmodule ⊥)) (Submodule.restrictScalars A I) ↔
    IsCompl (Subalgebra.toSubmodule S₀) (Submodule.restrictScalars A I)
Tactic:
rw [this]
State after:
no goals