Theorem: DividedPowerAlgebra.isCompl_augIdeal (DividedPowers/DPAlgebra/Graded/GradeZero.lean)

State before:
R : Type u
M : Type v
inst✝⁴ : CommRing R
inst✝³ : AddCommMonoid M
inst✝² : Module R M
inst✝¹ : DecidableEq R
inst✝ : DecidableEq M
⊢ IsAugmentation R (augIdeal R M)
Tactic:
apply IsCompl.mk
State after:
case disjoint
R : Type u
M : Type v
inst✝⁴ : CommRing R
inst✝³ : AddCommMonoid M
inst✝² : Module R M
inst✝¹ : DecidableEq R
inst✝ : DecidableEq M
⊢ Disjoint (Subalgebra.toSubmodule ⊥) (Submodule.restrictScalars R (augIdeal R M))

case codisjoint
R : Type u
M : Type v
inst✝⁴ : CommRing R
inst✝³ : AddCommMonoid M
inst✝² : Module R M
inst✝¹ : DecidableEq R
inst✝ : DecidableEq M
⊢ Codisjoint (Subalgebra.toSubmodule ⊥) (Submodule.restrictScalars R (augIdeal R M))

State before:
case disjoint
R : Type u
M : Type v
inst✝⁴ : CommRing R
inst✝³ : AddCommMonoid M
inst✝² : Module R M
inst✝¹ : DecidableEq R
inst✝ : DecidableEq M
⊢ Disjoint (Subalgebra.toSubmodule ⊥) (Submodule.restrictScalars R (augIdeal R M))
Tactic:
rw [Submodule.disjoint_def]
State after:
case disjoint
R : Type u
M : Type v
inst✝⁴ : CommRing R
inst✝³ : AddCommMonoid M
inst✝² : Module R M
inst✝¹ : DecidableEq R
inst✝ : DecidableEq M
⊢ ∀ x ∈ Subalgebra.toSubmodule ⊥, x ∈ Submodule.restrictScalars R (augIdeal R M) → x = 0

State before:
case disjoint
R : Type u
M : Type v
inst✝⁴ : CommRing R
inst✝³ : AddCommMonoid M
inst✝² : Module R M
inst✝¹ : DecidableEq R
inst✝ : DecidableEq M
⊢ ∀ x ∈ Subalgebra.toSubmodule ⊥, x ∈ Submodule.restrictScalars R (augIdeal R M) → x = 0
Tactic:
intro x
State after:
case disjoint
R : Type u
M : Type v
inst✝⁴ : CommRing R
inst✝³ : AddCommMonoid M
inst✝² : Module R M
inst✝¹ : DecidableEq R
inst✝ : DecidableEq M
x : DividedPowerAlgebra R M
⊢ x ∈ Subalgebra.toSubmodule ⊥ → x ∈ Submodule.restrictScalars R (augIdeal R M) → x = 0

State before:
case disjoint
R : Type u
M : Type v
inst✝⁴ : CommRing R
inst✝³ : AddCommMonoid M
inst✝² : Module R M
inst✝¹ : DecidableEq R
inst✝ : DecidableEq M
x : DividedPowerAlgebra R M
⊢ x ∈ Subalgebra.toSubmodule ⊥ → x ∈ Submodule.restrictScalars R (augIdeal R M) → x = 0
Tactic:
simp only [Subalgebra.mem_toSubmodule, Algebra.mem_bot]
State after:
case disjoint
R : Type u
M : Type v
inst✝⁴ : CommRing R
inst✝³ : AddCommMonoid M
inst✝² : Module R M
inst✝¹ : DecidableEq R
inst✝ : DecidableEq M
x : DividedPowerAlgebra R M
⊢ x ∈ Set.range ⇑(algebraMap R (DividedPowerAlgebra R M)) → x ∈ Submodule.restrictScalars R (augIdeal R M) → x = 0

State before:
case disjoint
R : Type u
M : Type v
inst✝⁴ : CommRing R
inst✝³ : AddCommMonoid M
inst✝² : Module R M
inst✝¹ : DecidableEq R
inst✝ : DecidableEq M
x : DividedPowerAlgebra R M
⊢ x ∈ Set.range ⇑(algebraMap R (DividedPowerAlgebra R M)) → x ∈ Submodule.restrictScalars R (augIdeal R M) → x = 0
Tactic:
rintro ⟨r, rfl⟩
State after:
case disjoint.intro
R : Type u
M : Type v
inst✝⁴ : CommRing R
inst✝³ : AddCommMonoid M
inst✝² : Module R M
inst✝¹ : DecidableEq R
inst✝ : DecidableEq M
r : R
⊢ (algebraMap R (DividedPowerAlgebra R M)) r ∈ Submodule.restrictScalars R (augIdeal R M) →
    (algebraMap R (DividedPowerAlgebra R M)) r = 0

State before:
case disjoint.intro
R : Type u
M : Type v
inst✝⁴ : CommRing R
inst✝³ : AddCommMonoid M
inst✝² : Module R M
inst✝¹ : DecidableEq R
inst✝ : DecidableEq M
r : R
⊢ (algebraMap R (DividedPowerAlgebra R M)) r ∈ Submodule.restrictScalars R (augIdeal R M) →
    (algebraMap R (DividedPowerAlgebra R M)) r = 0
Tactic:
simp only [Submodule.restrictScalars_mem, mem_augIdeal_iff, AlgHom.commutes,
  Algebra.id.map_eq_id, RingHom.id_apply]
State after:
case disjoint.intro
R : Type u
M : Type v
inst✝⁴ : CommRing R
inst✝³ : AddCommMonoid M
inst✝² : Module R M
inst✝¹ : DecidableEq R
inst✝ : DecidableEq M
r : R
⊢ r = 0 → (algebraMap R (DividedPowerAlgebra R M)) r = 0

State before:
case disjoint.intro
R : Type u
M : Type v
inst✝⁴ : CommRing R
inst✝³ : AddCommMonoid M
inst✝² : Module R M
inst✝¹ : DecidableEq R
inst✝ : DecidableEq M
r : R
⊢ r = 0 → (algebraMap R (DividedPowerAlgebra R M)) r = 0
Tactic:
intro hr
State after:
case disjoint.intro
R : Type u
M : Type v
inst✝⁴ : CommRing R
inst✝³ : AddCommMonoid M
inst✝² : Module R M
inst✝¹ : DecidableEq R
inst✝ : DecidableEq M
r : R
hr : r = 0
⊢ (algebraMap R (DividedPowerAlgebra R M)) r = 0

State before:
case disjoint.intro
R : Type u
M : Type v
inst✝⁴ : CommRing R
inst✝³ : AddCommMonoid M
inst✝² : Module R M
inst✝¹ : DecidableEq R
inst✝ : DecidableEq M
r : R
hr : r = 0
⊢ (algebraMap R (DividedPowerAlgebra R M)) r = 0
Tactic:
rw [hr, map_zero]
State after:
no goals

State before:
case codisjoint
R : Type u
M : Type v
inst✝⁴ : CommRing R
inst✝³ : AddCommMonoid M
inst✝² : Module R M
inst✝¹ : DecidableEq R
inst✝ : DecidableEq M
⊢ Codisjoint (Subalgebra.toSubmodule ⊥) (Submodule.restrictScalars R (augIdeal R M))
Tactic:
rw [codisjoint_iff, eq_top_iff]
State after:
case codisjoint
R : Type u
M : Type v
inst✝⁴ : CommRing R
inst✝³ : AddCommMonoid M
inst✝² : Module R M
inst✝¹ : DecidableEq R
inst✝ : DecidableEq M
⊢ ⊤ ≤ Subalgebra.toSubmodule ⊥ ⊔ Submodule.restrictScalars R (augIdeal R M)

State before:
case codisjoint
R : Type u
M : Type v
inst✝⁴ : CommRing R
inst✝³ : AddCommMonoid M
inst✝² : Module R M
inst✝¹ : DecidableEq R
inst✝ : DecidableEq M
⊢ ⊤ ≤ Subalgebra.toSubmodule ⊥ ⊔ Submodule.restrictScalars R (augIdeal R M)
Tactic:
intro p _
State after:
case codisjoint
R : Type u
M : Type v
inst✝⁴ : CommRing R
inst✝³ : AddCommMonoid M
inst✝² : Module R M
inst✝¹ : DecidableEq R
inst✝ : DecidableEq M
p : DividedPowerAlgebra R M
a✝ : p ∈ ⊤
⊢ p ∈ Subalgebra.toSubmodule ⊥ ⊔ Submodule.restrictScalars R (augIdeal R M)

State before:
case codisjoint
R : Type u
M : Type v
inst✝⁴ : CommRing R
inst✝³ : AddCommMonoid M
inst✝² : Module R M
inst✝¹ : DecidableEq R
inst✝ : DecidableEq M
p : DividedPowerAlgebra R M
a✝ : p ∈ ⊤
⊢ p ∈ Subalgebra.toSubmodule ⊥ ⊔ Submodule.restrictScalars R (augIdeal R M)
Tactic:
simp only [Submodule.mem_sup, Subalgebra.mem_toSubmodule, Submodule.restrictScalars_mem]
State after:
case codisjoint
R : Type u
M : Type v
inst✝⁴ : CommRing R
inst✝³ : AddCommMonoid M
inst✝² : Module R M
inst✝¹ : DecidableEq R
inst✝ : DecidableEq M
p : DividedPowerAlgebra R M
a✝ : p ∈ ⊤
⊢ ∃ y ∈ ⊥, ∃ z ∈ augIdeal R M, y + z = p

State before:
case codisjoint
R : Type u
M : Type v
inst✝⁴ : CommRing R
inst✝³ : AddCommMonoid M
inst✝² : Module R M
inst✝¹ : DecidableEq R
inst✝ : DecidableEq M
p : DividedPowerAlgebra R M
a✝ : p ∈ ⊤
⊢ ∃ y ∈ ⊥, ∃ z ∈ augIdeal R M, y + z = p
Tactic:
refine ⟨algebraMap R _ (algebraMapInv R M p), ?_, _, ?_, add_sub_cancel _ p⟩
State after:
case codisjoint.refine_1
R : Type u
M : Type v
inst✝⁴ : CommRing R
inst✝³ : AddCommMonoid M
inst✝² : Module R M
inst✝¹ : DecidableEq R
inst✝ : DecidableEq M
p : DividedPowerAlgebra R M
a✝ : p ∈ ⊤
⊢ (algebraMap R (DividedPowerAlgebra R M)) ((algebraMapInv R M) p) ∈ ⊥

case codisjoint.refine_2
R : Type u
M : Type v
inst✝⁴ : CommRing R
inst✝³ : AddCommMonoid M
inst✝² : Module R M
inst✝¹ : DecidableEq R
inst✝ : DecidableEq M
p : DividedPowerAlgebra R M
a✝ : p ∈ ⊤
⊢ p - (algebraMap R (DividedPowerAlgebra R M)) ((algebraMapInv R M) p) ∈ augIdeal R M

State before:
case codisjoint.refine_1
R : Type u
M : Type v
inst✝⁴ : CommRing R
inst✝³ : AddCommMonoid M
inst✝² : Module R M
inst✝¹ : DecidableEq R
inst✝ : DecidableEq M
p : DividedPowerAlgebra R M
a✝ : p ∈ ⊤
⊢ (algebraMap R (DividedPowerAlgebra R M)) ((algebraMapInv R M) p) ∈ ⊥
Tactic:
rw [Algebra.mem_bot]
State after:
case codisjoint.refine_1
R : Type u
M : Type v
inst✝⁴ : CommRing R
inst✝³ : AddCommMonoid M
inst✝² : Module R M
inst✝¹ : DecidableEq R
inst✝ : DecidableEq M
p : DividedPowerAlgebra R M
a✝ : p ∈ ⊤
⊢ (algebraMap R (DividedPowerAlgebra R M)) ((algebraMapInv R M) p) ∈ Set.range ⇑(algebraMap R (DividedPowerAlgebra R M))

State before:
case codisjoint.refine_1
R : Type u
M : Type v
inst✝⁴ : CommRing R
inst✝³ : AddCommMonoid M
inst✝² : Module R M
inst✝¹ : DecidableEq R
inst✝ : DecidableEq M
p : DividedPowerAlgebra R M
a✝ : p ∈ ⊤
⊢ (algebraMap R (DividedPowerAlgebra R M)) ((algebraMapInv R M) p) ∈ Set.range ⇑(algebraMap R (DividedPowerAlgebra R M))
Tactic:
exact Set.mem_range_self ((algebraMapInv R M) p)
State after:
no goals

State before:
case codisjoint.refine_2
R : Type u
M : Type v
inst✝⁴ : CommRing R
inst✝³ : AddCommMonoid M
inst✝² : Module R M
inst✝¹ : DecidableEq R
inst✝ : DecidableEq M
p : DividedPowerAlgebra R M
a✝ : p ∈ ⊤
⊢ p - (algebraMap R (DividedPowerAlgebra R M)) ((algebraMapInv R M) p) ∈ augIdeal R M
Tactic:
simp only [mem_augIdeal_iff, map_sub, AlgHom.commutes, Algebra.id.map_eq_id,
RingHom.id_apply, sub_self]
State after:
no goals