internlm/Lean-Github huggingface dataset:
Theorem: DividedPowerAlgebra.ext_iff
Proof state before:
R : Type u_2
M : Type u_3
inst✝⁴ : CommRing R
inst✝³ : AddCommMonoid M
inst✝² : Module R M
A : Type u_1
inst✝¹ : CommRing A
inst✝ : Algebra R A
f g : DividedPowerAlgebra R M →ₐ[R] A
⊢ f = g ↔ ∀ (n : ℕ) (m : M), f (dp R n m) = g (dp R n m)
Tactic:
constructor
Proof state after:
case mp
R : Type u_2
M : Type u_3
inst✝⁴ : CommRing R
inst✝³ : AddCommMonoid M
inst✝² : Module R M
A : Type u_1
inst✝¹ : CommRing A
inst✝ : Algebra R A
f g : DividedPowerAlgebra R M →ₐ[R] A
⊢ f = g → ∀ (n : ℕ) (m : M), f (dp R n m) = g (dp R n m)

case mpr
R : Type u_2
M : Type u_3
inst✝⁴ : CommRing R
inst✝³ : AddCommMonoid M
inst✝² : Module R M
A : Type u_1
inst✝¹ : CommRing A
inst✝ : Algebra R A
f g : DividedPowerAlgebra R M →ₐ[R] A
⊢ (∀ (n : ℕ) (m : M), f (dp R n m) = g (dp R n m)) → f = g
Theorem: DividedPowerAlgebra.ext_iff
Proof state before:
case mp
R : Type u_2
M : Type u_3
inst✝⁴ : CommRing R
inst✝³ : AddCommMonoid M
inst✝² : Module R M
A : Type u_1
inst✝¹ : CommRing A
inst✝ : Algebra R A
f g : DividedPowerAlgebra R M →ₐ[R] A
⊢ f = g → ∀ (n : ℕ) (m : M), f (dp R n m) = g (dp R n m)

case mpr
R : Type u_2
M : Type u_3
inst✝⁴ : CommRing R
inst✝³ : AddCommMonoid M
inst✝² : Module R M
A : Type u_1
inst✝¹ : CommRing A
inst✝ : Algebra R A
f g : DividedPowerAlgebra R M →ₐ[R] A
⊢ (∀ (n : ℕ) (m : M), f (dp R n m) = g (dp R n m)) → f = g
Tactic:
. intro h n m
  rw [h]
Proof state after:
case mpr
R : Type u_2
M : Type u_3
inst✝⁴ : CommRing R
inst✝³ : AddCommMonoid M
inst✝² : Module R M
A : Type u_1
inst✝¹ : CommRing A
inst✝ : Algebra R A
f g : DividedPowerAlgebra R M →ₐ[R] A
⊢ (∀ (n : ℕ) (m : M), f (dp R n m) = g (dp R n m)) → f = g
Theorem: DividedPowerAlgebra.ext_iff
Proof state before:
case mpr
R : Type u_2
M : Type u_3
inst✝⁴ : CommRing R
inst✝³ : AddCommMonoid M
inst✝² : Module R M
A : Type u_1
inst✝¹ : CommRing A
inst✝ : Algebra R A
f g : DividedPowerAlgebra R M →ₐ[R] A
⊢ (∀ (n : ℕ) (m : M), f (dp R n m) = g (dp R n m)) → f = g
Tactic:
. intro h
  rw [FunLike.ext'_iff]
  apply Function.Surjective.injective_comp_right (mkAlgHom_surjective R (Rel R M))
  simp only [← AlgHom.coe_comp, ← FunLike.ext'_iff]
  exact MvPolynomial.algHom_ext fun ⟨n, m⟩ => h n m
Proof state after:
no goals
Theorem: DividedPowerAlgebra.ext_iff
Proof state before:
case mp
R : Type u_2
M : Type u_3
inst✝⁴ : CommRing R
inst✝³ : AddCommMonoid M
inst✝² : Module R M
A : Type u_1
inst✝¹ : CommRing A
inst✝ : Algebra R A
f g : DividedPowerAlgebra R M →ₐ[R] A
⊢ f = g → ∀ (n : ℕ) (m : M), f (dp R n m) = g (dp R n m)
Tactic:
intro h n m
Proof state after:
case mp
R : Type u_2
M : Type u_3
inst✝⁴ : CommRing R
inst✝³ : AddCommMonoid M
inst✝² : Module R M
A : Type u_1
inst✝¹ : CommRing A
inst✝ : Algebra R A
f g : DividedPowerAlgebra R M →ₐ[R] A
h : f = g
n : ℕ
m : M
⊢ f (dp R n m) = g (dp R n m)
Theorem: DividedPowerAlgebra.ext_iff
Proof state before:
case mp
R : Type u_2
M : Type u_3
inst✝⁴ : CommRing R
inst✝³ : AddCommMonoid M
inst✝² : Module R M
A : Type u_1
inst✝¹ : CommRing A
inst✝ : Algebra R A
f g : DividedPowerAlgebra R M →ₐ[R] A
h : f = g
n : ℕ
m : M
⊢ f (dp R n m) = g (dp R n m)
Tactic:
rw [h]
Proof state after:
no goals
Theorem: DividedPowerAlgebra.ext_iff
Proof state before:
case mpr
R : Type u_2
M : Type u_3
inst✝⁴ : CommRing R
inst✝³ : AddCommMonoid M
inst✝² : Module R M
A : Type u_1
inst✝¹ : CommRing A
inst✝ : Algebra R A
f g : DividedPowerAlgebra R M →ₐ[R] A
⊢ (∀ (n : ℕ) (m : M), f (dp R n m) = g (dp R n m)) → f = g
Tactic:
intro h
Proof state after:
case mpr
R : Type u_2
M : Type u_3
inst✝⁴ : CommRing R
inst✝³ : AddCommMonoid M
inst✝² : Module R M
A : Type u_1
inst✝¹ : CommRing A
inst✝ : Algebra R A
f g : DividedPowerAlgebra R M →ₐ[R] A
h : ∀ (n : ℕ) (m : M), f (dp R n m) = g (dp R n m)
⊢ f = g
Theorem: DividedPowerAlgebra.lift'_imp
Proof state before:
R : Type u_3
M : Type u_1
inst✝⁴ : CommRing R
inst✝³ : AddCommMonoid M
inst✝² : Module R M
A : Type u_2
inst✝¹ : CommRing A
inst✝ : Algebra R A
f : ℕ × M → A
hf_zero : ∀ (m : M), f (0, m) = 1
hf_smul : ∀ (n : ℕ) (r : R) (m : M), f (n, r • m) = r ^ n • f (n, m)
hf_mul : ∀ (n p : ℕ) (m : M), f (n, m) * f (p, m) = (n + p).choose n • f (n + p, m)
hf_add : ∀ (n : ℕ) (u v : M), f (n, u + v) = ∑ x ∈ range (n + 1), f (x, u) * f (n - x, v)
p q : MvPolynomial (ℕ × M) R
h : Rel R M p q
⊢ (eval₂AlgHom R f) p = (eval₂AlgHom R f) q
Tactic:
cases' h with a r n a m n a n a b <;> 
  simp only [eval₂AlgHom_X', map_one, map_zero, map_smul, AlgHom.map_mul, map_nsmul, AlgHom.map_sum]
Proof state after:
no goals
Theorem: DividedPowerAlgebra.lift'AlgHom_apply
Proof state before:
R : Type u_3
M : Type u_1
inst✝⁴ : CommRing R
inst✝³ : AddCommMonoid M
inst✝² : Module R M
A : Type u_2
inst✝¹ : CommRing A
inst✝ : Algebra R A
f : ℕ × M → A
hf_zero : ∀ (m : M), f (0, m) = 1
hf_smul : ∀ (n : ℕ) (r : R) (m : M), f (n, r • m) = r ^ n • f (n, m)
hf_mul : ∀ (n p : ℕ) (m : M), f (n, m) * f (p, m) = (n + p).choose n • f (n + p, m)
hf_add : ∀ (n : ℕ) (u v : M), f (n, u + v) = ∑ x ∈ range (n + 1), f (x, u) * f (n - x, v)
p : MvPolynomial (ℕ × M) R
⊢ (lift' f hf_zero hf_smul hf_mul hf_add) (mk p) = (aeval f) p
Tactic:
rw [mk, lift', RingQuot.liftAlgHom_mkAlgHom_apply, coe_eval₂AlgHom]
Proof state after:
R : Type u_3
M : Type u_1
inst✝⁴ : CommRing R
inst✝³ : AddCommMonoid M
inst✝² : Module R M
A : Type u_2
inst✝¹ : CommRing A
inst✝ : Algebra R A
f : ℕ × M → A
hf_zero : ∀ (m : M), f (0, m) = 1
hf_smul : ∀ (n : ℕ) (r : R) (m : M), f (n, r • m) = r ^ n • f (n, m)
hf_mul : ∀ (n p : ℕ) (m : M), f (n, m) * f (p, m) = (n + p).choose n • f (n + p, m)
hf_add : ∀ (n : ℕ) (u v : M), f (n, u + v) = ∑ x ∈ range (n + 1), f (x, u) * f (n - x, v)
p : MvPolynomial (ℕ × M) R
⊢ (sorryAx (DividedPowerAlgebra R M →ₐ[R] A) true)
      ((sorryAx (MvPolynomial (ℕ × M) R →ₐ[R] DividedPowerAlgebra R M) true) p) =
    (aeval f) p
Theorem: DividedPowerAlgebra.lift'AlgHom_apply_dp
Proof state before:
R : Type u_3
M : Type u_1
inst✝⁴ : CommRing R
inst✝³ : AddCommMonoid M
inst✝² : Module R M
A : Type u_2
inst✝¹ : CommRing A
inst✝ : Algebra R A
f : ℕ × M → A
hf_zero : ∀ (m : M), f (0, m) = 1
hf_smul : ∀ (n : ℕ) (r : R) (m : M), f (n, r • m) = r ^ n • f (n, m)
hf_mul : ∀ (n p : ℕ) (m : M), f (n, m) * f (p, m) = (n + p).choose n • f (n + p, m)
hf_add : ∀ (n : ℕ) (u v : M), f (n, u + v) = ∑ x ∈ range (n + 1), f (x, u) * f (n - x, v)
n : ℕ
m : M
⊢ (lift' f hf_zero hf_smul hf_mul hf_add) (dp R n m) = f (n, m)
Tactic:
rw [dp_def, ← mk, lift'AlgHom_apply f hf_zero hf_smul hf_mul hf_add, aeval_X]
Proof state after:
R : Type u_3
M : Type u_1
inst✝⁴ : CommRing R
inst✝³ : AddCommMonoid M
inst✝² : Module R M
A : Type u_2
inst✝¹ : CommRing A
inst✝ : Algebra R A
f : ℕ × M → A
hf_zero : ∀ (m : M), f (0, m) = 1
hf_smul : ∀ (n : ℕ) (r : R) (m : M), f (n, r • m) = r ^ n • f (n, m)
hf_mul : ∀ (n p : ℕ) (m : M), f (n, m) * f (p, m) = (n + p).choose n • f (n + p, m)
hf_add : ∀ (n : ℕ) (u v : M), f (n, u + v) = ∑ x ∈ range (n + 1), f (x, u) * f (n - x, v)
n : ℕ
m : M
⊢ (lift' f hf_zero hf_smul hf_mul hf_add) ((mkAlgHom R (Rel R M)) (X (n, m))) = f (n, m)
Theorem: DividedPowerAlgebra.liftAlgHom_apply
Proof state before:
R : Type u_1
M : Type u_2
inst✝⁴ : CommRing R
inst✝³ : AddCommMonoid M
inst✝² : Module R M
A : Type u_3
inst✝¹ : CommRing A
inst✝ : Algebra R A
I : Ideal A
hI : DividedPowers I
φ : M →ₗ[R] A
hφ : ∀ (m : M), φ m ∈ I
p : MvPolynomial (ℕ × M) R
⊢ (lift hI φ hφ) (mk p) = (aeval fun nm => hI.dpow nm.1 (φ nm.2)) p
Tactic:
rw [lift, lift'AlgHom_apply]
Proof state after:
no goals
Theorem: DividedPowerAlgebra.liftAlgHom_apply_dp
Proof state before:
R : Type u_2
M : Type u_3
inst✝⁴ : CommRing R
inst✝³ : AddCommMonoid M
inst✝² : Module R M
A : Type u_1
inst✝¹ : CommRing A
inst✝ : Algebra R A
I : Ideal A
hI : DividedPowers I
φ : M →ₗ[R] A
hφ : ∀ (m : M), φ m ∈ I
n : ℕ
m : M
⊢ (lift hI φ hφ) (dp R n m) = hI.dpow n (φ m)
Tactic:
rw [lift, lift'AlgHom_apply_dp]
Proof state after:
no goals
Theorem: DividedPowerAlgebra.LinearMap.dp_smul
Proof state before:
R : Type u_4
M : Type u_3
inst✝¹⁰ : CommRing R
inst✝⁹ : AddCommMonoid M
inst✝⁸ : Module R M
S : Type u_1
inst✝⁷ : CommRing S
inst✝⁶ : Algebra R S
N : Type u_2
inst✝⁵ : AddCommMonoid N
inst✝⁴ : Module R N
inst✝³ : Module S N
inst✝² : IsScalarTower R S N
inst✝¹ : Algebra R (DividedPowerAlgebra S N)
inst✝ : IsScalarTower R S (DividedPowerAlgebra S N)
f : M →ₗ[R] N
r : R
n : ℕ
a : M
⊢ dp S n (f (r • a)) = r ^ n • dp S n (f a)
Tactic:
rw [f.map_smul, algebra_compatible_smul S r (f a)]
Proof state after:
R : Type u_4
M : Type u_3
inst✝¹⁰ : CommRing R
inst✝⁹ : AddCommMonoid M
inst✝⁸ : Module R M
S : Type u_1
inst✝⁷ : CommRing S
inst✝⁶ : Algebra R S
N : Type u_2
inst✝⁵ : AddCommMonoid N
inst✝⁴ : Module R N
inst✝³ : Module S N
inst✝² : IsScalarTower R S N
inst✝¹ : Algebra R (DividedPowerAlgebra S N)
inst✝ : IsScalarTower R S (DividedPowerAlgebra S N)
f : M →ₗ[R] N
r : R
n : ℕ
a : M
⊢ dp S n ((algebraMap R S) r • f a) = r ^ n • dp S n (f a)
Theorem: DividedPowerAlgebra.LinearMap.dp_smul
Proof state before:
R : Type u_4
M : Type u_3
inst✝¹⁰ : CommRing R
inst✝⁹ : AddCommMonoid M
inst✝⁸ : Module R M
S : Type u_1
inst✝⁷ : CommRing S
inst✝⁶ : Algebra R S
N : Type u_2
inst✝⁵ : AddCommMonoid N
inst✝⁴ : Module R N
inst✝³ : Module S N
inst✝² : IsScalarTower R S N
inst✝¹ : Algebra R (DividedPowerAlgebra S N)
inst✝ : IsScalarTower R S (DividedPowerAlgebra S N)
f : M →ₗ[R] N
r : R
n : ℕ
a : M
⊢ dp S n ((algebraMap R S) r • f a) = r ^ n • dp S n (f a)
Tactic:
rw [DividedPowerAlgebra.dp_smul S ((algebraMap R S) r) n (f a)]
Proof state after:
R : Type u_4
M : Type u_3
inst✝¹⁰ : CommRing R
inst✝⁹ : AddCommMonoid M
inst✝⁸ : Module R M
S : Type u_1
inst✝⁷ : CommRing S
inst✝⁶ : Algebra R S
N : Type u_2
inst✝⁵ : AddCommMonoid N
inst✝⁴ : Module R N
inst✝³ : Module S N
inst✝² : IsScalarTower R S N
inst✝¹ : Algebra R (DividedPowerAlgebra S N)
inst✝ : IsScalarTower R S (DividedPowerAlgebra S N)
f : M →ₗ[R] N
r : R
n : ℕ
a : M
⊢ (algebraMap R S) r ^ n • dp S n (f a) = r ^ n • dp S n (f a)
Theorem: DividedPowerAlgebra.LinearMap.dp_smul
Proof state before:
R : Type u_4
M : Type u_3
inst✝¹⁰ : CommRing R
inst✝⁹ : AddCommMonoid M
inst✝⁸ : Module R M
S : Type u_1
inst✝⁷ : CommRing S
inst✝⁶ : Algebra R S
N : Type u_2
inst✝⁵ : AddCommMonoid N
inst✝⁴ : Module R N
inst✝³ : Module S N
inst✝² : IsScalarTower R S N
inst✝¹ : Algebra R (DividedPowerAlgebra S N)
inst✝ : IsScalarTower R S (DividedPowerAlgebra S N)
f : M →ₗ[R] N
r : R
n : ℕ
a : M
⊢ (algebraMap R S) r ^ n • dp S n (f a) = r ^ n • dp S n (f a)
Tactic:
rw [← map_pow, ← algebra_compatible_smul]
Proof state after:
R : Type u_4
M : Type u_3
inst✝¹⁰ : CommRing R
inst✝⁹ : AddCommMonoid M
inst✝⁸ : Module R M
S : Type u_1
inst✝⁷ : CommRing S
inst✝⁶ : Algebra R S
N : Type u_2
inst✝⁵ : AddCommMonoid N
inst✝⁴ : Module R N
inst✝³ : Module S N
inst✝² : IsScalarTower R S N
inst✝¹ : Algebra R (DividedPowerAlgebra S N)
inst✝ : IsScalarTower R S (DividedPowerAlgebra S N)
f : M →ₗ[R] N
r : R
n : ℕ
a : M
⊢ (algebraMap R S) (r ^ n) • dp S n (f a) = r ^ n • dp S n (f a)
Theorem: DividedPowerAlgebra.LinearMap.dp_add
Proof state before:
R : Type u_4
M : Type u_3
inst✝¹⁰ : CommRing R
inst✝⁹ : AddCommMonoid M
inst✝⁸ : Module R M
S : Type u_1
inst✝⁷ : CommRing S
inst✝⁶ : Algebra R S
N : Type u_2
inst✝⁵ : AddCommMonoid N
inst✝⁴ : Module R N
inst✝³ : Module S N
inst✝² : IsScalarTower R S N
inst✝¹ : Algebra R (DividedPowerAlgebra S N)
inst✝ : IsScalarTower R S (DividedPowerAlgebra S N)
f : M →ₗ[R] N
n : ℕ
a b : M
⊢ dp S n (f (a + b)) = ∑ k ∈ range (n + 1), dp S k (f a) * dp S (n - k) (f b)
Tactic:
rw [map_add, DividedPowerAlgebra.dp_add]
Proof state after:
no goals
Theorem: Submodule.sup_restrictScalars
Proof state before:
R✝ : Type u_1
inst✝⁹ : CommRing R✝
A✝ : Type u_2
inst✝⁸ : CommRing A✝
inst✝⁷ : Algebra R✝ A✝
J : Ideal A✝
A : Type u_3
inst✝⁶ : CommSemiring A
R : Type u_4
inst✝⁵ : Ring R
inst✝⁴ : Algebra A R
M : Type u_5
inst✝³ : AddCommGroup M
inst✝² : Module A M
inst✝¹ : Module R M
inst✝ : IsScalarTower A R M
M₁ M₂ : Submodule R M
⊢ restrictScalars A (M₁ ⊔ M₂) = restrictScalars A M₁ ⊔ restrictScalars A M₂
Tactic:
apply Submodule.toAddSubmonoid_injective
Proof state after:
case a
R✝ : Type u_1
inst✝⁹ : CommRing R✝
A✝ : Type u_2
inst✝⁸ : CommRing A✝
inst✝⁷ : Algebra R✝ A✝
J : Ideal A✝
A : Type u_3
inst✝⁶ : CommSemiring A
R : Type u_4
inst✝⁵ : Ring R
inst✝⁴ : Algebra A R
M : Type u_5
inst✝³ : AddCommGroup M
inst✝² : Module A M
inst✝¹ : Module R M
inst✝ : IsScalarTower A R M
M₁ M₂ : Submodule R M
⊢ (restrictScalars A (M₁ ⊔ M₂)).toAddSubmonoid = (restrictScalars A M₁ ⊔ restrictScalars A M₂).toAddSubmonoid
Theorem: Submodule.sup_restrictScalars
Proof state before:
case a
R✝ : Type u_1
inst✝⁹ : CommRing R✝
A✝ : Type u_2
inst✝⁸ : CommRing A✝
inst✝⁷ : Algebra R✝ A✝
J : Ideal A✝
A : Type u_3
inst✝⁶ : CommSemiring A
R : Type u_4
inst✝⁵ : Ring R
inst✝⁴ : Algebra A R
M : Type u_5
inst✝³ : AddCommGroup M
inst✝² : Module A M
inst✝¹ : Module R M
inst✝ : IsScalarTower A R M
M₁ M₂ : Submodule R M
⊢ (restrictScalars A (M₁ ⊔ M₂)).toAddSubmonoid = (restrictScalars A M₁ ⊔ restrictScalars A M₂).toAddSubmonoid
Tactic:
simp only [Submodule.toAddSubmonoid_restrictScalars, Submodule.sup_toAddSubmonoid]
Proof state after:
no goals
Theorem: Submodule.codisjoint_restrictScalars_iff
Proof state before:
R✝ : Type u_1
inst✝⁹ : CommRing R✝
A✝ : Type u_2
inst✝⁸ : CommRing A✝
inst✝⁷ : Algebra R✝ A✝
J : Ideal A✝
A : Type u_3
inst✝⁶ : CommSemiring A
R : Type u_4
inst✝⁵ : Ring R
inst✝⁴ : Algebra A R
M : Type u_5
inst✝³ : AddCommGroup M
inst✝² : Module A M
inst✝¹ : Module R M
inst✝ : IsScalarTower A R M
M₁ M₂ : Submodule R M
⊢ Codisjoint (restrictScalars A M₁) (restrictScalars A M₂) ↔ Codisjoint M₁ M₂
Tactic:
simp only [codisjoint_iff, ← Submodule.sup_restrictScalars, Submodule.restrictScalars_eq_top_iff]
Proof state after:
no goals
Theorem: Submodule.disjoint_restrictScalars_iff
Proof state before:
R✝ : Type u_1
inst✝⁹ : CommRing R✝
A✝ : Type u_2
inst✝⁸ : CommRing A✝
inst✝⁷ : Algebra R✝ A✝
J : Ideal A✝
A : Type u_3
inst✝⁶ : CommSemiring A
R : Type u_4
inst✝⁵ : Ring R
inst✝⁴ : Algebra A R
M : Type u_5
inst✝³ : AddCommGroup M
inst✝² : Module A M
inst✝¹ : Module R M
inst✝ : IsScalarTower A R M
M₁ M₂ : Submodule R M
⊢ Disjoint (restrictScalars A M₁) (restrictScalars A M₂) ↔ Disjoint M₁ M₂
Tactic:
simp only [Submodule.disjoint_def, Submodule.restrictScalars_mem]
Proof state after:
no goals
Theorem: Submodule.isCompl_restrictScalars_iff
Proof state before:
R✝ : Type u_1
inst✝⁹ : CommRing R✝
A✝ : Type u_2
inst✝⁸ : CommRing A✝
inst✝⁷ : Algebra R✝ A✝
J : Ideal A✝
A : Type u_3
inst✝⁶ : CommSemiring A
R : Type u_4
inst✝⁵ : Ring R
inst✝⁴ : Algebra A R
M : Type u_5
inst✝³ : AddCommGroup M
inst✝² : Module A M
inst✝¹ : Module R M
inst✝ : IsScalarTower A R M
M₁ M₂ : Submodule R M
⊢ IsCompl (restrictScalars A M₁) (restrictScalars A M₂) ↔ IsCompl M₁ M₂
Tactic:
simp only [isCompl_iff, Submodule.disjoint_restrictScalars_iff, Submodule.codisjoint_restrictScalars_iff]
Proof state after:
no goals
Theorem: LinearMap.ker_lTensor_of_linearProjOfIsCompl
Proof state before:
R : Type u_1
inst✝⁶ : CommRing R
A : Type u_2
inst✝⁵ : CommRing A
inst✝⁴ : Algebra R A
J : Ideal A
M : Type u_3
inst✝³ : AddCommGroup M
inst✝² : Module A M
M₁ M₂ : Submodule A M
hM : IsCompl M₁ M₂
Q : Type u_4
inst✝¹ : AddCommGroup Q
inst✝ : Module A Q
⊢ ker (lTensor Q (M₁.linearProjOfIsCompl M₂ hM)) = range (lTensor Q M₂.subtype)
Tactic:
rw [← exact_iff]
Proof state after:
R : Type u_1
inst✝⁶ : CommRing R
A : Type u_2
inst✝⁵ : CommRing A
inst✝⁴ : Algebra R A
J : Ideal A
M : Type u_3
inst✝³ : AddCommGroup M
inst✝² : Module A M
M₁ M₂ : Submodule A M
hM : IsCompl M₁ M₂
Q : Type u_4
inst✝¹ : AddCommGroup Q
inst✝ : Module A Q
⊢ Function.Exact ⇑(lTensor Q M₂.subtype) ⇑(lTensor Q (M₁.linearProjOfIsCompl M₂ hM))
Theorem: LinearMap.ker_lTensor_of_linearProjOfIsCompl
Proof state before:
R : Type u_1
inst✝⁶ : CommRing R
A : Type u_2
inst✝⁵ : CommRing A
inst✝⁴ : Algebra R A
J : Ideal A
M : Type u_3
inst✝³ : AddCommGroup M
inst✝² : Module A M
M₁ M₂ : Submodule A M
hM : IsCompl M₁ M₂
Q : Type u_4
inst✝¹ : AddCommGroup Q
inst✝ : Module A Q
⊢ Function.Exact ⇑(lTensor Q M₂.subtype) ⇑(lTensor Q (M₁.linearProjOfIsCompl M₂ hM))
Tactic:
apply lTensor_exact
Proof state after:
case hfg
R : Type u_1
inst✝⁶ : CommRing R
A : Type u_2
inst✝⁵ : CommRing A
inst✝⁴ : Algebra R A
J : Ideal A
M : Type u_3
inst✝³ : AddCommGroup M
inst✝² : Module A M
M₁ M₂ : Submodule A M
hM : IsCompl M₁ M₂
Q : Type u_4
inst✝¹ : AddCommGroup Q
inst✝ : Module A Q
⊢ Function.Exact ⇑M₂.subtype ⇑(M₁.linearProjOfIsCompl M₂ hM)

case hg
R : Type u_1
inst✝⁶ : CommRing R
A : Type u_2
inst✝⁵ : CommRing A
inst✝⁴ : Algebra R A
J : Ideal A
M : Type u_3
inst✝³ : AddCommGroup M
inst✝² : Module A M
M₁ M₂ : Submodule A M
hM : IsCompl M₁ M₂
Q : Type u_4
inst✝¹ : AddCommGroup Q
inst✝ : Module A Q
⊢ Function.Surjective ⇑(M₁.linearProjOfIsCompl M₂ hM)
Theorem: LinearMap.ker_lTensor_of_linearProjOfIsCompl
Proof state before:
case hfg
R : Type u_1
inst✝⁶ : CommRing R
A : Type u_2
inst✝⁵ : CommRing A
inst✝⁴ : Algebra R A
J : Ideal A
M : Type u_3
inst✝³ : AddCommGroup M
inst✝² : Module A M
M₁ M₂ : Submodule A M
hM : IsCompl M₁ M₂
Q : Type u_4
inst✝¹ : AddCommGroup Q
inst✝ : Module A Q
⊢ Function.Exact ⇑M₂.subtype ⇑(M₁.linearProjOfIsCompl M₂ hM)

case hg
R : Type u_1
inst✝⁶ : CommRing R
A : Type u_2
inst✝⁵ : CommRing A
inst✝⁴ : Algebra R A
J : Ideal A
M : Type u_3
inst✝³ : AddCommGroup M
inst✝² : Module A M
M₁ M₂ : Submodule A M
hM : IsCompl M₁ M₂
Q : Type u_4
inst✝¹ : AddCommGroup Q
inst✝ : Module A Q
⊢ Function.Surjective ⇑(M₁.linearProjOfIsCompl M₂ hM)
Tactic:
simp only [exact_iff, range_subtype, linearProjOfIsCompl_ker]
Proof state after:
case hg
R : Type u_1
inst✝⁶ : CommRing R
A : Type u_2
inst✝⁵ : CommRing A
inst✝⁴ : Algebra R A
J : Ideal A
M : Type u_3
inst✝³ : AddCommGroup M
inst✝² : Module A M
M₁ M₂ : Submodule A M
hM : IsCompl M₁ M₂
Q : Type u_4
inst✝¹ : AddCommGroup Q
inst✝ : Module A Q
⊢ Function.Surjective ⇑(M₁.linearProjOfIsCompl M₂ hM)
Theorem: LinearMap.ker_lTensor_of_linearProjOfIsCompl
Proof state before:
case hg
R : Type u_1
inst✝⁶ : CommRing R
A : Type u_2
inst✝⁵ : CommRing A
inst✝⁴ : Algebra R A
J : Ideal A
M : Type u_3
inst✝³ : AddCommGroup M
inst✝² : Module A M
M₁ M₂ : Submodule A M
hM : IsCompl M₁ M₂
Q : Type u_4
inst✝¹ : AddCommGroup Q
inst✝ : Module A Q
⊢ Function.Surjective ⇑(M₁.linearProjOfIsCompl M₂ hM)
Tactic:
simp only [← range_eq_top, linearProjOfIsCompl_range]
Proof state after:
no goals
Theorem: LinearMap.ker_baseChange_of_linearProjOfIsCompl
Proof state before:
R✝ : Type u_1
inst✝⁶ : CommRing R✝
A : Type u_2
inst✝⁵ : CommRing A
inst✝⁴ : Algebra R✝ A
J : Ideal A
M : Type u_3
inst✝³ : AddCommGroup M
inst✝² : Module A M
M₁ M₂ : Submodule A M
hM : IsCompl M₁ M₂
R : Type u_4
inst✝¹ : CommRing R
inst✝ : Algebra A R
⊢ ker (baseChange R (M₁.linearProjOfIsCompl M₂ hM)) = range (baseChange R M₂.subtype)
Tactic:
simpa only [← exact_iff] using ker_lTensor_of_linearProjOfIsCompl hM R
Proof state after:
no goals
Theorem: LinearMap.isCompl_lTensor
Proof state before:
R : Type u_1
inst✝⁶ : CommRing R
A : Type u_2
inst✝⁵ : CommRing A
inst✝⁴ : Algebra R A
J : Ideal A
M : Type u_3
inst✝³ : AddCommGroup M
inst✝² : Module A M
M₁ M₂ : Submodule A M
hM : IsCompl M₁ M₂
Q : Type u_4
inst✝¹ : AddCommGroup Q
inst✝ : Module A Q
⊢ IsCompl (range (lTensor Q M₁.subtype)) (range (lTensor Q M₂.subtype))
Tactic:
have hq :
  M₁.subtype.comp (linearProjOfIsCompl _ _ hM)
    + M₂.subtype.comp (linearProjOfIsCompl _ _ hM.symm) = id := by
  ext x
  simp only [add_apply, coe_comp, coeSubtype, Function.comp_apply,
    id_coe, id_eq]
  rw [linear_proj_add_linearProjOfIsCompl_eq_self]
Proof state after:
R : Type u_1
inst✝⁶ : CommRing R
A : Type u_2
inst✝⁵ : CommRing A
inst✝⁴ : Algebra R A
J : Ideal A
M : Type u_3
inst✝³ : AddCommGroup M
inst✝² : Module A M
M₁ M₂ : Submodule A M
hM : IsCompl M₁ M₂
Q : Type u_4
inst✝¹ : AddCommGroup Q
inst✝ : Module A Q
hq : M₁.subtype ∘ₗ M₁.linearProjOfIsCompl M₂ hM + M₂.subtype ∘ₗ M₂.linearProjOfIsCompl M₁ ⋯ = id
⊢ IsCompl (range (lTensor Q M₁.subtype)) (range (lTensor Q M₂.subtype))
Theorem: LinearMap.isCompl_lTensor
Proof state before:
R : Type u_1
inst✝⁶ : CommRing R
A : Type u_2
inst✝⁵ : CommRing A
inst✝⁴ : Algebra R A
J : Ideal A
M : Type u_3
inst✝³ : AddCommGroup M
inst✝² : Module A M
M₁ M₂ : Submodule A M
hM : IsCompl M₁ M₂
Q : Type u_4
inst✝¹ : AddCommGroup Q
inst✝ : Module A Q
hq : M₁.subtype ∘ₗ M₁.linearProjOfIsCompl M₂ hM + M₂.subtype ∘ₗ M₂.linearProjOfIsCompl M₁ ⋯ = id
⊢ IsCompl (range (lTensor Q M₁.subtype)) (range (lTensor Q M₂.subtype))
Tactic:
apply IsCompl.mk
Proof state after:
case disjoint
R : Type u_1
inst✝⁶ : CommRing R
A : Type u_2
inst✝⁵ : CommRing A
inst✝⁴ : Algebra R A
J : Ideal A
M : Type u_3
inst✝³ : AddCommGroup M
inst✝² : Module A M
M₁ M₂ : Submodule A M
hM : IsCompl M₁ M₂
Q : Type u_4
inst✝¹ : AddCommGroup Q
inst✝ : Module A Q
hq : M₁.subtype ∘ₗ M₁.linearProjOfIsCompl M₂ hM + M₂.subtype ∘ₗ M₂.linearProjOfIsCompl M₁ ⋯ = id
⊢ Disjoint (range (lTensor Q M₁.subtype)) (range (lTensor Q M₂.subtype))

case codisjoint
R : Type u_1
inst✝⁶ : CommRing R
A : Type u_2
inst✝⁵ : CommRing A
inst✝⁴ : Algebra R A
J : Ideal A
M : Type u_3
inst✝³ : AddCommGroup M
inst✝² : Module A M
M₁ M₂ : Submodule A M
hM : IsCompl M₁ M₂
Q : Type u_4
inst✝¹ : AddCommGroup Q
inst✝ : Module A Q
hq : M₁.subtype ∘ₗ M₁.linearProjOfIsCompl M₂ hM + M₂.subtype ∘ₗ M₂.linearProjOfIsCompl M₁ ⋯ = id
⊢ Codisjoint (range (lTensor Q M₁.subtype)) (range (lTensor Q M₂.subtype))
Theorem: LinearMap.isCompl_lTensor
Proof state before:
R : Type u_1
inst✝⁶ : CommRing R
A : Type u_2
inst✝⁵ : CommRing A
inst✝⁴ : Algebra R A
J : Ideal A
M : Type u_3
inst✝³ : AddCommGroup M
inst✝² : Module A M
M₁ M₂ : Submodule A M
hM : IsCompl M₁ M₂
Q : Type u_4
inst✝¹ : AddCommGroup Q
inst✝ : Module A Q
⊢ M₁.subtype ∘ₗ M₁.linearProjOfIsCompl M₂ hM + M₂.subtype ∘ₗ M₂.linearProjOfIsCompl M₁ ⋯ = id
Tactic:
ext x
Proof state after:
case h
R : Type u_1
inst✝⁶ : CommRing R
A : Type u_2
inst✝⁵ : CommRing A
inst✝⁴ : Algebra R A
J : Ideal A
M : Type u_3
inst✝³ : AddCommGroup M
inst✝² : Module A M
M₁ M₂ : Submodule A M
hM : IsCompl M₁ M₂
Q : Type u_4
inst✝¹ : AddCommGroup Q
inst✝ : Module A Q
x : M
⊢ (M₁.subtype ∘ₗ M₁.linearProjOfIsCompl M₂ hM + M₂.subtype ∘ₗ M₂.linearProjOfIsCompl M₁ ⋯) x = id x
Theorem: LinearMap.isCompl_lTensor
Proof state before:
case h
R : Type u_1
inst✝⁶ : CommRing R
A : Type u_2
inst✝⁵ : CommRing A
inst✝⁴ : Algebra R A
J : Ideal A
M : Type u_3
inst✝³ : AddCommGroup M
inst✝² : Module A M
M₁ M₂ : Submodule A M
hM : IsCompl M₁ M₂
Q : Type u_4
inst✝¹ : AddCommGroup Q
inst✝ : Module A Q
x : M
⊢ (M₁.subtype ∘ₗ M₁.linearProjOfIsCompl M₂ hM + M₂.subtype ∘ₗ M₂.linearProjOfIsCompl M₁ ⋯) x = id x
Tactic:
simp only [add_apply, coe_comp, coeSubtype, Function.comp_apply,
  id_coe, id_eq]
Proof state after:
case h
R : Type u_1
inst✝⁶ : CommRing R
A : Type u_2
inst✝⁵ : CommRing A
inst✝⁴ : Algebra R A
J : Ideal A
M : Type u_3
inst✝³ : AddCommGroup M
inst✝² : Module A M
M₁ M₂ : Submodule A M
hM : IsCompl M₁ M₂
Q : Type u_4
inst✝¹ : AddCommGroup Q
inst✝ : Module A Q
x : M
⊢ ↑((M₁.linearProjOfIsCompl M₂ hM) x) + ↑((M₂.linearProjOfIsCompl M₁ ⋯) x) = x
Theorem: LinearMap.isCompl_lTensor
Proof state before:
case h
R : Type u_1
inst✝⁶ : CommRing R
A : Type u_2
inst✝⁵ : CommRing A
inst✝⁴ : Algebra R A
J : Ideal A
M : Type u_3
inst✝³ : AddCommGroup M
inst✝² : Module A M
M₁ M₂ : Submodule A M
hM : IsCompl M₁ M₂
Q : Type u_4
inst✝¹ : AddCommGroup Q
inst✝ : Module A Q
x : M
⊢ ↑((M₁.linearProjOfIsCompl M₂ hM) x) + ↑((M₂.linearProjOfIsCompl M₁ ⋯) x) = x
Tactic:
rw [linear_proj_add_linearProjOfIsCompl_eq_self]
Proof state after:
no goals