Theorem: DividedPowerAlgebra.toModule_free (DividedPowers/DPAlgebra/PolynomialMap.lean)

State before:
R : Type u
inst✝³ : CommRing R
M : Type u_1
inst✝² : AddCommGroup M
inst✝¹ : Module R M
inst✝ : Module.Free R M
⊢ Module.Free R (DividedPowerAlgebra R M)
Tactic:
classical
haveI : ∀ i, Module.Free R (grade R M i) := fun i ↦ grade_free R M i
haveI : Module.Free R (DirectSum ℕ fun i ↦ ↥(grade R M i)) := by
  apply Module.Free.directSum
apply Module.Free.of_equiv (DirectSum.decomposeLinearEquiv (grade R M)).symm
State after:
no goals

State before:
R : Type u
inst✝³ : CommRing R
M : Type u_1
inst✝² : AddCommGroup M
inst✝¹ : Module R M
inst✝ : Module.Free R M
⊢ Module.Free R (DividedPowerAlgebra R M)
Tactic:
haveI : ∀ i, Module.Free R (grade R M i) := fun i ↦ grade_free R M i
State after:
R : Type u
inst✝³ : CommRing R
M : Type u_1
inst✝² : AddCommGroup M
inst✝¹ : Module R M
inst✝ : Module.Free R M
this : ∀ (i : ℕ), Module.Free R ↥(grade R M i)
⊢ Module.Free R (DividedPowerAlgebra R M)

State before:
R : Type u
inst✝³ : CommRing R
M : Type u_1
inst✝² : AddCommGroup M
inst✝¹ : Module R M
inst✝ : Module.Free R M
this : ∀ (i : ℕ), Module.Free R ↥(grade R M i)
⊢ Module.Free R (DividedPowerAlgebra R M)
Tactic:
haveI : Module.Free R (DirectSum ℕ fun i ↦ ↥(grade R M i)) := by
  apply Module.Free.directSum
State after:
R : Type u
inst✝³ : CommRing R
M : Type u_1
inst✝² : AddCommGroup M
inst✝¹ : Module R M
inst✝ : Module.Free R M
this✝ : ∀ (i : ℕ), Module.Free R ↥(grade R M i)
this : Module.Free R (DirectSum ℕ fun i => ↥(grade R M i))
⊢ Module.Free R (DividedPowerAlgebra R M)

State before:
R : Type u
inst✝³ : CommRing R
M : Type u_1
inst✝² : AddCommGroup M
inst✝¹ : Module R M
inst✝ : Module.Free R M
this✝ : ∀ (i : ℕ), Module.Free R ↥(grade R M i)
this : Module.Free R (DirectSum ℕ fun i => ↥(grade R M i))
⊢ Module.Free R (DividedPowerAlgebra R M)
Tactic:
apply Module.Free.of_equiv (DirectSum.decomposeLinearEquiv (grade R M)).symm
State after:
no goals

State before:
R : Type u
inst✝³ : CommRing R
M : Type u_1
inst✝² : AddCommGroup M
inst✝¹ : Module R M
inst✝ : Module.Free R M
this : ∀ (i : ℕ), Module.Free R ↥(grade R M i)
⊢ Module.Free R (DirectSum ℕ fun i => ↥(grade R M i))
Tactic:
apply Module.Free.directSum
State after:
no goals