Theorem: Ideal.isAugmentation_baseChange (DividedPowers/ForMathlib/RingTheory/AugmentationIdeal.lean)

State before:
R✝ : Type u_1
inst✝⁶ : CommRing R✝
A : Type u_2
inst✝⁵ : CommRing A
inst✝⁴ : Algebra R✝ A
J : Ideal A
S : Type u_3
inst✝³ : CommRing S
inst✝² : Algebra A S
I : Ideal S
hI : IsCompl (Subalgebra.toSubmodule ⊥) (Submodule.restrictScalars A I)
R : Type u_4
inst✝¹ : CommRing R
inst✝ : Algebra A R
⊢ IsAugmentation R (map Algebra.TensorProduct.includeRight I)
Tactic:
unfold Ideal.IsAugmentation
State after:
R✝ : Type u_1
inst✝⁶ : CommRing R✝
A : Type u_2
inst✝⁵ : CommRing A
inst✝⁴ : Algebra R✝ A
J : Ideal A
S : Type u_3
inst✝³ : CommRing S
inst✝² : Algebra A S
I : Ideal S
hI : IsCompl (Subalgebra.toSubmodule ⊥) (Submodule.restrictScalars A I)
R : Type u_4
inst✝¹ : CommRing R
inst✝ : Algebra A R
⊢ IsCompl (Subalgebra.toSubmodule ⊥) (Submodule.restrictScalars R (map Algebra.TensorProduct.includeRight I))

State before:
R✝ : Type u_1
inst✝⁶ : CommRing R✝
A : Type u_2
inst✝⁵ : CommRing A
inst✝⁴ : Algebra R✝ A
J : Ideal A
S : Type u_3
inst✝³ : CommRing S
inst✝² : Algebra A S
I : Ideal S
hI : IsCompl (Subalgebra.toSubmodule ⊥) (Submodule.restrictScalars A I)
R : Type u_4
inst✝¹ : CommRing R
inst✝ : Algebra A R
⊢ IsCompl (Subalgebra.toSubmodule ⊥) (Submodule.restrictScalars R (map Algebra.TensorProduct.includeRight I))
Tactic:
rw [Algebra.baseChange_bot]
State after:
R✝ : Type u_1
inst✝⁶ : CommRing R✝
A : Type u_2
inst✝⁵ : CommRing A
inst✝⁴ : Algebra R✝ A
J : Ideal A
S : Type u_3
inst✝³ : CommRing S
inst✝² : Algebra A S
I : Ideal S
hI : IsCompl (Subalgebra.toSubmodule ⊥) (Submodule.restrictScalars A I)
R : Type u_4
inst✝¹ : CommRing R
inst✝ : Algebra A R
⊢ IsCompl (LinearMap.range (LinearMap.baseChange R (Subalgebra.toSubmodule ⊥).subtype))
    (Submodule.restrictScalars R (map Algebra.TensorProduct.includeRight I))

State before:
R✝ : Type u_1
inst✝⁶ : CommRing R✝
A : Type u_2
inst✝⁵ : CommRing A
inst✝⁴ : Algebra R✝ A
J : Ideal A
S : Type u_3
inst✝³ : CommRing S
inst✝² : Algebra A S
I : Ideal S
hI : IsCompl (Subalgebra.toSubmodule ⊥) (Submodule.restrictScalars A I)
R : Type u_4
inst✝¹ : CommRing R
inst✝ : Algebra A R
⊢ IsCompl (LinearMap.range (LinearMap.baseChange R (Subalgebra.toSubmodule ⊥).subtype))
    (Submodule.restrictScalars R (map Algebra.TensorProduct.includeRight I))
Tactic:
rw [Algebra.TensorProduct.map_includeRight_eq_range_baseChange]
State after:
R✝ : Type u_1
inst✝⁶ : CommRing R✝
A : Type u_2
inst✝⁵ : CommRing A
inst✝⁴ : Algebra R✝ A
J : Ideal A
S : Type u_3
inst✝³ : CommRing S
inst✝² : Algebra A S
I : Ideal S
hI : IsCompl (Subalgebra.toSubmodule ⊥) (Submodule.restrictScalars A I)
R : Type u_4
inst✝¹ : CommRing R
inst✝ : Algebra A R
⊢ IsCompl (LinearMap.range (LinearMap.baseChange R (Subalgebra.toSubmodule ⊥).subtype))
    (LinearMap.range (LinearMap.baseChange R (Submodule.restrictScalars A I).subtype))

State before:
R✝ : Type u_1
inst✝⁶ : CommRing R✝
A : Type u_2
inst✝⁵ : CommRing A
inst✝⁴ : Algebra R✝ A
J : Ideal A
S : Type u_3
inst✝³ : CommRing S
inst✝² : Algebra A S
I : Ideal S
hI : IsCompl (Subalgebra.toSubmodule ⊥) (Submodule.restrictScalars A I)
R : Type u_4
inst✝¹ : CommRing R
inst✝ : Algebra A R
⊢ IsCompl (LinearMap.range (LinearMap.baseChange R (Subalgebra.toSubmodule ⊥).subtype))
    (LinearMap.range (LinearMap.baseChange R (Submodule.restrictScalars A I).subtype))
Tactic:
exact isCompl_baseChange hI R
State after:
no goals