[GOAL]
R : Type u1
inst✝⁴ : CommRing R
M : Type u2
inst✝³ : AddCommGroup M
inst✝² : Module R M
A : Type u_1
inst✝¹ : Semiring A
inst✝ : Algebra R A
g : ExteriorAlgebra R M →ₐ[R] A
m : M
⊢ ↑g (↑(ι R) m) * ↑g (↑(ι R) m) = 0
[PROOFSTEP]
rw [← AlgHom.map_mul, ι_sq_zero, AlgHom.map_zero]
[GOAL]
R : Type u1
inst✝⁴ : CommRing R
M : Type u2
inst✝³ : AddCommGroup M
inst✝² : Module R M
A : Type u_1
inst✝¹ : Semiring A
inst✝ : Algebra R A
⊢ ∀ (a : M →ₗ[R] A),
    (∀ (m : M), ↑a m * ↑a m = 0) ↔
      ∀ (m : M), ↑(↑(Equiv.refl (M →ₗ[R] A)) a) m * ↑(↑(Equiv.refl (M →ₗ[R] A)) a) m = ↑(algebraMap R A) (↑0 m)
[PROOFSTEP]
simp
[GOAL]
R : Type u1
inst✝⁴ : CommRing R
M : Type u2
inst✝³ : AddCommGroup M
inst✝² : Module R M
A : Type u_1
inst✝¹ : Semiring A
inst✝ : Algebra R A
m : M
⊢ ↑0 m * ↑0 m = 0
[PROOFSTEP]
simp
[GOAL]
R : Type u1
inst✝⁴ : CommRing R
M : Type u2
inst✝³ : AddCommGroup M
inst✝² : Module R M
A : Type u_1
inst✝¹ : Semiring A
inst✝ : Algebra R A
x : R
⊢ ↑algebraMapInv (↑(algebraMap R (ExteriorAlgebra R M)) x) = x
[PROOFSTEP]
simp [algebraMapInv]
[GOAL]
R : Type u1
inst✝⁴ : CommRing R
M : Type u2
inst✝³ : AddCommGroup M
inst✝² : Module R M
A : Type u_1
inst✝¹ : Semiring A
inst✝ : Algebra R A
⊢ ExteriorAlgebra R M →ₗ[R] M
[PROOFSTEP]
letI : Module Rᵐᵒᵖ M := Module.compHom _ ((RingHom.id R).fromOpposite mul_comm)
[GOAL]
R : Type u1
inst✝⁴ : CommRing R
M : Type u2
inst✝³ : AddCommGroup M
inst✝² : Module R M
A : Type u_1
inst✝¹ : Semiring A
inst✝ : Algebra R A
this : Module Rᵐᵒᵖ M := Module.compHom M (RingHom.fromOpposite (RingHom.id R) (_ : ∀ (a b : R), a * b = b * a))
⊢ ExteriorAlgebra R M →ₗ[R] M
[PROOFSTEP]
haveI : IsCentralScalar R M := ⟨fun r m => rfl⟩
[GOAL]
R : Type u1
inst✝⁴ : CommRing R
M : Type u2
inst✝³ : AddCommGroup M
inst✝² : Module R M
A : Type u_1
inst✝¹ : Semiring A
inst✝ : Algebra R A
this✝ : Module Rᵐᵒᵖ M := Module.compHom M (RingHom.fromOpposite (RingHom.id R) (_ : ∀ (a b : R), a * b = b * a))
this : IsCentralScalar R M
⊢ ExteriorAlgebra R M →ₗ[R] M
[PROOFSTEP]
exact (TrivSqZeroExt.sndHom R M).comp toTrivSqZeroExt.toLinearMap
[GOAL]
R : Type u1
inst✝⁴ : CommRing R
M : Type u2
inst✝³ : AddCommGroup M
inst✝² : Module R M
A : Type u_1
inst✝¹ : Semiring A
inst✝ : Algebra R A
x : M
⊢ ↑ιInv.toAddHom (↑(ι R) x) = x
[PROOFSTEP]
letI : Module Rᵐᵒᵖ M := Module.compHom _ ((RingHom.id R).fromOpposite mul_comm)
[GOAL]
R : Type u1
inst✝⁴ : CommRing R
M : Type u2
inst✝³ : AddCommGroup M
inst✝² : Module R M
A : Type u_1
inst✝¹ : Semiring A
inst✝ : Algebra R A
x : M
this : Module Rᵐᵒᵖ M := Module.compHom M (RingHom.fromOpposite (RingHom.id R) (_ : ∀ (a b : R), a * b = b * a))
⊢ ↑ιInv.toAddHom (↑(ι R) x) = x
[PROOFSTEP]
haveI : IsCentralScalar R M := ⟨fun r m => rfl⟩
[GOAL]
R : Type u1
inst✝⁴ : CommRing R
M : Type u2
inst✝³ : AddCommGroup M
inst✝² : Module R M
A : Type u_1
inst✝¹ : Semiring A
inst✝ : Algebra R A
x : M
this✝ : Module Rᵐᵒᵖ M := Module.compHom M (RingHom.fromOpposite (RingHom.id R) (_ : ∀ (a b : R), a * b = b * a))
this : IsCentralScalar R M
⊢ ↑ιInv.toAddHom (↑(ι R) x) = x
[PROOFSTEP]
simp [ιInv]
[GOAL]
R : Type u1
inst✝⁴ : CommRing R
M : Type u2
inst✝³ : AddCommGroup M
inst✝² : Module R M
A : Type u_1
inst✝¹ : Semiring A
inst✝ : Algebra R A
x : M
⊢ ↑(ι R) x = 0 ↔ x = 0
[PROOFSTEP]
rw [← ι_inj R x 0, LinearMap.map_zero]
[GOAL]
R : Type u1
inst✝⁴ : CommRing R
M : Type u2
inst✝³ : AddCommGroup M
inst✝² : Module R M
A : Type u_1
inst✝¹ : Semiring A
inst✝ : Algebra R A
x : M
r : R
⊢ ↑(ι R) x = ↑(algebraMap R (ExteriorAlgebra R M)) r ↔ x = 0 ∧ r = 0
[PROOFSTEP]
refine' ⟨fun h => _, _⟩
[GOAL]
case refine'_1
R : Type u1
inst✝⁴ : CommRing R
M : Type u2
inst✝³ : AddCommGroup M
inst✝² : Module R M
A : Type u_1
inst✝¹ : Semiring A
inst✝ : Algebra R A
x : M
r : R
h : ↑(ι R) x = ↑(algebraMap R (ExteriorAlgebra R M)) r
⊢ x = 0 ∧ r = 0
[PROOFSTEP]
letI : Module Rᵐᵒᵖ M := Module.compHom _ ((RingHom.id R).fromOpposite mul_comm)
[GOAL]
case refine'_1
R : Type u1
inst✝⁴ : CommRing R
M : Type u2
inst✝³ : AddCommGroup M
inst✝² : Module R M
A : Type u_1
inst✝¹ : Semiring A
inst✝ : Algebra R A
x : M
r : R
h : ↑(ι R) x = ↑(algebraMap R (ExteriorAlgebra R M)) r
this : Module Rᵐᵒᵖ M := Module.compHom M (RingHom.fromOpposite (RingHom.id R) (_ : ∀ (a b : R), a * b = b * a))
⊢ x = 0 ∧ r = 0
[PROOFSTEP]
haveI : IsCentralScalar R M := ⟨fun r m => rfl⟩
[GOAL]
case refine'_1
R : Type u1
inst✝⁴ : CommRing R
M : Type u2
inst✝³ : AddCommGroup M
inst✝² : Module R M
A : Type u_1
inst✝¹ : Semiring A
inst✝ : Algebra R A
x : M
r : R
h : ↑(ι R) x = ↑(algebraMap R (ExteriorAlgebra R M)) r
this✝ : Module Rᵐᵒᵖ M := Module.compHom M (RingHom.fromOpposite (RingHom.id R) (_ : ∀ (a b : R), a * b = b * a))
this : IsCentralScalar R M
⊢ x = 0 ∧ r = 0
[PROOFSTEP]
have hf0 : toTrivSqZeroExt (ι R x) = (0, x) := toTrivSqZeroExt_ι _
[GOAL]
case refine'_1
R : Type u1
inst✝⁴ : CommRing R
M : Type u2
inst✝³ : AddCommGroup M
inst✝² : Module R M
A : Type u_1
inst✝¹ : Semiring A
inst✝ : Algebra R A
x : M
r : R
h : ↑(ι R) x = ↑(algebraMap R (ExteriorAlgebra R M)) r
this✝ : Module Rᵐᵒᵖ M := Module.compHom M (RingHom.fromOpposite (RingHom.id R) (_ : ∀ (a b : R), a * b = b * a))
this : IsCentralScalar R M
hf0 : ↑toTrivSqZeroExt (↑(ι R) x) = (0, x)
⊢ x = 0 ∧ r = 0
[PROOFSTEP]
rw [h, AlgHom.commutes] at hf0 
[GOAL]
case refine'_1
R : Type u1
inst✝⁴ : CommRing R
M : Type u2
inst✝³ : AddCommGroup M
inst✝² : Module R M
A : Type u_1
inst✝¹ : Semiring A
inst✝ : Algebra R A
x : M
r : R
h : ↑(ι R) x = ↑(algebraMap R (ExteriorAlgebra R M)) r
this✝ : Module Rᵐᵒᵖ M := Module.compHom M (RingHom.fromOpposite (RingHom.id R) (_ : ∀ (a b : R), a * b = b * a))
this : IsCentralScalar R M
hf0 : ↑(algebraMap R (TrivSqZeroExt R M)) r = (0, x)
⊢ x = 0 ∧ r = 0
[PROOFSTEP]
have : r = 0 ∧ 0 = x := Prod.ext_iff.1 hf0
[GOAL]
case refine'_1
R : Type u1
inst✝⁴ : CommRing R
M : Type u2
inst✝³ : AddCommGroup M
inst✝² : Module R M
A : Type u_1
inst✝¹ : Semiring A
inst✝ : Algebra R A
x : M
r : R
h : ↑(ι R) x = ↑(algebraMap R (ExteriorAlgebra R M)) r
this✝¹ : Module Rᵐᵒᵖ M := Module.compHom M (RingHom.fromOpposite (RingHom.id R) (_ : ∀ (a b : R), a * b = b * a))
this✝ : IsCentralScalar R M
hf0 : ↑(algebraMap R (TrivSqZeroExt R M)) r = (0, x)
this : r = 0 ∧ 0 = x
⊢ x = 0 ∧ r = 0
[PROOFSTEP]
exact this.symm.imp_left Eq.symm
[GOAL]
case refine'_2
R : Type u1
inst✝⁴ : CommRing R
M : Type u2
inst✝³ : AddCommGroup M
inst✝² : Module R M
A : Type u_1
inst✝¹ : Semiring A
inst✝ : Algebra R A
x : M
r : R
⊢ x = 0 ∧ r = 0 → ↑(ι R) x = ↑(algebraMap R (ExteriorAlgebra R M)) r
[PROOFSTEP]
rintro ⟨rfl, rfl⟩
[GOAL]
case refine'_2.intro
R : Type u1
inst✝⁴ : CommRing R
M : Type u2
inst✝³ : AddCommGroup M
inst✝² : Module R M
A : Type u_1
inst✝¹ : Semiring A
inst✝ : Algebra R A
⊢ ↑(ι R) 0 = ↑(algebraMap R (ExteriorAlgebra R M)) 0
[PROOFSTEP]
rw [LinearMap.map_zero, RingHom.map_zero]
[GOAL]
R : Type u1
inst✝⁵ : CommRing R
M : Type u2
inst✝⁴ : AddCommGroup M
inst✝³ : Module R M
A : Type u_1
inst✝² : Semiring A
inst✝¹ : Algebra R A
inst✝ : Nontrivial R
x : M
⊢ ↑(ι R) x ≠ 1
[PROOFSTEP]
rw [← (algebraMap R (ExteriorAlgebra R M)).map_one, Ne.def, ι_eq_algebraMap_iff]
[GOAL]
R : Type u1
inst✝⁵ : CommRing R
M : Type u2
inst✝⁴ : AddCommGroup M
inst✝³ : Module R M
A : Type u_1
inst✝² : Semiring A
inst✝¹ : Algebra R A
inst✝ : Nontrivial R
x : M
⊢ ¬(x = 0 ∧ 1 = 0)
[PROOFSTEP]
exact one_ne_zero ∘ And.right
[GOAL]
R : Type u1
inst✝⁴ : CommRing R
M : Type u2
inst✝³ : AddCommGroup M
inst✝² : Module R M
A : Type u_1
inst✝¹ : Semiring A
inst✝ : Algebra R A
⊢ Disjoint (LinearMap.range (ι R)) 1
[PROOFSTEP]
rw [Submodule.disjoint_def]
[GOAL]
R : Type u1
inst✝⁴ : CommRing R
M : Type u2
inst✝³ : AddCommGroup M
inst✝² : Module R M
A : Type u_1
inst✝¹ : Semiring A
inst✝ : Algebra R A
⊢ ∀ (x : ExteriorAlgebra R M), x ∈ LinearMap.range (ι R) → x ∈ 1 → x = 0
[PROOFSTEP]
rintro _ ⟨x, hx⟩ ⟨r, rfl : algebraMap R (ExteriorAlgebra R M) r = _⟩
[GOAL]
case intro.intro
R : Type u1
inst✝⁴ : CommRing R
M : Type u2
inst✝³ : AddCommGroup M
inst✝² : Module R M
A : Type u_1
inst✝¹ : Semiring A
inst✝ : Algebra R A
x : M
r : R
hx : ↑(ι R) x = ↑(algebraMap R (ExteriorAlgebra R M)) r
⊢ ↑(algebraMap R (ExteriorAlgebra R M)) r = 0
[PROOFSTEP]
rw [ι_eq_algebraMap_iff x] at hx 
[GOAL]
case intro.intro
R : Type u1
inst✝⁴ : CommRing R
M : Type u2
inst✝³ : AddCommGroup M
inst✝² : Module R M
A : Type u_1
inst✝¹ : Semiring A
inst✝ : Algebra R A
x : M
r : R
hx : x = 0 ∧ r = 0
⊢ ↑(algebraMap R (ExteriorAlgebra R M)) r = 0
[PROOFSTEP]
rw [hx.2, RingHom.map_zero]
[GOAL]
R : Type u1
inst✝⁴ : CommRing R
M : Type u2
inst✝³ : AddCommGroup M
inst✝² : Module R M
A : Type u_1
inst✝¹ : Semiring A
inst✝ : Algebra R A
x y : M
⊢ ↑(ι R) x * ↑(ι R) y + ↑(ι R) y * ↑(ι R) x = ↑(ι R) (y + x) * ↑(ι R) (y + x)
[PROOFSTEP]
simp [mul_add, add_mul]
[GOAL]
R : Type u1
inst✝⁴ : CommRing R
M : Type u2
inst✝³ : AddCommGroup M
inst✝² : Module R M
A : Type u_1
inst✝¹ : Semiring A
inst✝ : Algebra R A
n : ℕ
f : Fin n → M
i : Fin n
⊢ ↑(ι R) (f i) * List.prod (List.ofFn fun i => ↑(ι R) (f i)) = 0
[PROOFSTEP]
induction' n with n hn
[GOAL]
case zero
R : Type u1
inst✝⁴ : CommRing R
M : Type u2
inst✝³ : AddCommGroup M
inst✝² : Module R M
A : Type u_1
inst✝¹ : Semiring A
inst✝ : Algebra R A
n : ℕ
f✝ : Fin n → M
i✝ : Fin n
f : Fin Nat.zero → M
i : Fin Nat.zero
⊢ ↑(ι R) (f i) * List.prod (List.ofFn fun i => ↑(ι R) (f i)) = 0
[PROOFSTEP]
exact i.elim0
[GOAL]
case succ
R : Type u1
inst✝⁴ : CommRing R
M : Type u2
inst✝³ : AddCommGroup M
inst✝² : Module R M
A : Type u_1
inst✝¹ : Semiring A
inst✝ : Algebra R A
n✝ : ℕ
f✝ : Fin n✝ → M
i✝ : Fin n✝
n : ℕ
hn : ∀ (f : Fin n → M) (i : Fin n), ↑(ι R) (f i) * List.prod (List.ofFn fun i => ↑(ι R) (f i)) = 0
f : Fin (Nat.succ n) → M
i : Fin (Nat.succ n)
⊢ ↑(ι R) (f i) * List.prod (List.ofFn fun i => ↑(ι R) (f i)) = 0
[PROOFSTEP]
rw [List.ofFn_succ, List.prod_cons, ← mul_assoc]
[GOAL]
case succ
R : Type u1
inst✝⁴ : CommRing R
M : Type u2
inst✝³ : AddCommGroup M
inst✝² : Module R M
A : Type u_1
inst✝¹ : Semiring A
inst✝ : Algebra R A
n✝ : ℕ
f✝ : Fin n✝ → M
i✝ : Fin n✝
n : ℕ
hn : ∀ (f : Fin n → M) (i : Fin n), ↑(ι R) (f i) * List.prod (List.ofFn fun i => ↑(ι R) (f i)) = 0
f : Fin (Nat.succ n) → M
i : Fin (Nat.succ n)
⊢ ↑(ι R) (f i) * ↑(ι R) (f 0) * List.prod (List.ofFn fun i => ↑(ι R) (f (Fin.succ i))) = 0
[PROOFSTEP]
by_cases h : i = 0
[GOAL]
case pos
R : Type u1
inst✝⁴ : CommRing R
M : Type u2
inst✝³ : AddCommGroup M
inst✝² : Module R M
A : Type u_1
inst✝¹ : Semiring A
inst✝ : Algebra R A
n✝ : ℕ
f✝ : Fin n✝ → M
i✝ : Fin n✝
n : ℕ
hn : ∀ (f : Fin n → M) (i : Fin n), ↑(ι R) (f i) * List.prod (List.ofFn fun i => ↑(ι R) (f i)) = 0
f : Fin (Nat.succ n) → M
i : Fin (Nat.succ n)
h : i = 0
⊢ ↑(ι R) (f i) * ↑(ι R) (f 0) * List.prod (List.ofFn fun i => ↑(ι R) (f (Fin.succ i))) = 0
[PROOFSTEP]
rw [h, ι_sq_zero, zero_mul]
[GOAL]
case neg
R : Type u1
inst✝⁴ : CommRing R
M : Type u2
inst✝³ : AddCommGroup M
inst✝² : Module R M
A : Type u_1
inst✝¹ : Semiring A
inst✝ : Algebra R A
n✝ : ℕ
f✝ : Fin n✝ → M
i✝ : Fin n✝
n : ℕ
hn : ∀ (f : Fin n → M) (i : Fin n), ↑(ι R) (f i) * List.prod (List.ofFn fun i => ↑(ι R) (f i)) = 0
f : Fin (Nat.succ n) → M
i : Fin (Nat.succ n)
h : ¬i = 0
⊢ ↑(ι R) (f i) * ↑(ι R) (f 0) * List.prod (List.ofFn fun i => ↑(ι R) (f (Fin.succ i))) = 0
[PROOFSTEP]
replace hn := congr_arg ((· * ·) <| ι R <| f 0) (hn (fun i => f <| Fin.succ i) (i.pred h))
[GOAL]
case neg
R : Type u1
inst✝⁴ : CommRing R
M : Type u2
inst✝³ : AddCommGroup M
inst✝² : Module R M
A : Type u_1
inst✝¹ : Semiring A
inst✝ : Algebra R A
n✝ : ℕ
f✝ : Fin n✝ → M
i✝ : Fin n✝
n : ℕ
f : Fin (Nat.succ n) → M
i : Fin (Nat.succ n)
h : ¬i = 0
hn :
  (fun x x_1 => x * x_1) (↑(ι R) (f 0))
      (↑(ι R) (f (Fin.succ (Fin.pred i h))) * List.prod (List.ofFn fun i => ↑(ι R) (f (Fin.succ i)))) =
    (fun x x_1 => x * x_1) (↑(ι R) (f 0)) 0
⊢ ↑(ι R) (f i) * ↑(ι R) (f 0) * List.prod (List.ofFn fun i => ↑(ι R) (f (Fin.succ i))) = 0
[PROOFSTEP]
simp only at hn 
[GOAL]
case neg
R : Type u1
inst✝⁴ : CommRing R
M : Type u2
inst✝³ : AddCommGroup M
inst✝² : Module R M
A : Type u_1
inst✝¹ : Semiring A
inst✝ : Algebra R A
n✝ : ℕ
f✝ : Fin n✝ → M
i✝ : Fin n✝
n : ℕ
f : Fin (Nat.succ n) → M
i : Fin (Nat.succ n)
h : ¬i = 0
hn :
  ↑(ι R) (f 0) * (↑(ι R) (f (Fin.succ (Fin.pred i h))) * List.prod (List.ofFn fun i => ↑(ι R) (f (Fin.succ i)))) =
    ↑(ι R) (f 0) * 0
⊢ ↑(ι R) (f i) * ↑(ι R) (f 0) * List.prod (List.ofFn fun i => ↑(ι R) (f (Fin.succ i))) = 0
[PROOFSTEP]
rw [Fin.succ_pred, ← mul_assoc, mul_zero] at hn 
[GOAL]
case neg
R : Type u1
inst✝⁴ : CommRing R
M : Type u2
inst✝³ : AddCommGroup M
inst✝² : Module R M
A : Type u_1
inst✝¹ : Semiring A
inst✝ : Algebra R A
n✝ : ℕ
f✝ : Fin n✝ → M
i✝ : Fin n✝
n : ℕ
f : Fin (Nat.succ n) → M
i : Fin (Nat.succ n)
h : ¬i = 0
hn : ↑(ι R) (f 0) * ↑(ι R) (f i) * List.prod (List.ofFn fun i => ↑(ι R) (f (Fin.succ i))) = 0
⊢ ↑(ι R) (f i) * ↑(ι R) (f 0) * List.prod (List.ofFn fun i => ↑(ι R) (f (Fin.succ i))) = 0
[PROOFSTEP]
refine' (eq_zero_iff_eq_zero_of_add_eq_zero _).mp hn
[GOAL]
case neg
R : Type u1
inst✝⁴ : CommRing R
M : Type u2
inst✝³ : AddCommGroup M
inst✝² : Module R M
A : Type u_1
inst✝¹ : Semiring A
inst✝ : Algebra R A
n✝ : ℕ
f✝ : Fin n✝ → M
i✝ : Fin n✝
n : ℕ
f : Fin (Nat.succ n) → M
i : Fin (Nat.succ n)
h : ¬i = 0
hn : ↑(ι R) (f 0) * ↑(ι R) (f i) * List.prod (List.ofFn fun i => ↑(ι R) (f (Fin.succ i))) = 0
⊢ ↑(ι R) (f 0) * ↑(ι R) (f i) * List.prod (List.ofFn fun i => ↑(ι R) (f (Fin.succ i))) +
      ↑(ι R) (f i) * ↑(ι R) (f 0) * List.prod (List.ofFn fun i => ↑(ι R) (f (Fin.succ i))) =
    0
[PROOFSTEP]
rw [← add_mul, ι_add_mul_swap, zero_mul]
[GOAL]
R : Type u1
inst✝⁴ : CommRing R
M : Type u2
inst✝³ : AddCommGroup M
inst✝² : Module R M
A : Type u_1
inst✝¹ : Semiring A
inst✝ : Algebra R A
n : ℕ
F : MultilinearMap R (fun x => M) (ExteriorAlgebra R M) :=
  MultilinearMap.compLinearMap (MultilinearMap.mkPiAlgebraFin R n (ExteriorAlgebra R M)) fun x => ι R
f : Fin n → M
x y : Fin n
hfxy : f x = f y
hxy : x ≠ y
⊢ MultilinearMap.toFun
      { toFun := ↑F,
        map_add' :=
          (_ :
            ∀ [inst : DecidableEq (Fin n)] (m : Fin n → M) (i : Fin n) (x y : M),
              MultilinearMap.toFun F (Function.update m i (x + y)) =
                MultilinearMap.toFun F (Function.update m i x) + MultilinearMap.toFun F (Function.update m i y)),
        map_smul' :=
          (_ :
            ∀ [inst : DecidableEq (Fin n)] (m : Fin n → M) (i : Fin n) (c : R) (x : M),
              MultilinearMap.toFun F (Function.update m i (c • x)) =
                c • MultilinearMap.toFun F (Function.update m i x)) }
      f =
    0
[PROOFSTEP]
dsimp
[GOAL]
R : Type u1
inst✝⁴ : CommRing R
M : Type u2
inst✝³ : AddCommGroup M
inst✝² : Module R M
A : Type u_1
inst✝¹ : Semiring A
inst✝ : Algebra R A
n : ℕ
F : MultilinearMap R (fun x => M) (ExteriorAlgebra R M) :=
  MultilinearMap.compLinearMap (MultilinearMap.mkPiAlgebraFin R n (ExteriorAlgebra R M)) fun x => ι R
f : Fin n → M
x y : Fin n
hfxy : f x = f y
hxy : x ≠ y
⊢ List.prod (List.ofFn fun i => ↑(ι R) (f i)) = 0
[PROOFSTEP]
clear F
[GOAL]
R : Type u1
inst✝⁴ : CommRing R
M : Type u2
inst✝³ : AddCommGroup M
inst✝² : Module R M
A : Type u_1
inst✝¹ : Semiring A
inst✝ : Algebra R A
n : ℕ
f : Fin n → M
x y : Fin n
hfxy : f x = f y
hxy : x ≠ y
⊢ List.prod (List.ofFn fun i => ↑(ι R) (f i)) = 0
[PROOFSTEP]
wlog h : x < y
[GOAL]
case inr
R : Type u1
inst✝⁴ : CommRing R
M : Type u2
inst✝³ : AddCommGroup M
inst✝² : Module R M
A : Type u_1
inst✝¹ : Semiring A
inst✝ : Algebra R A
n : ℕ
f : Fin n → M
x y : Fin n
hfxy : f x = f y
hxy : x ≠ y
this :
  ∀ (R : Type u1) [inst : CommRing R] {M : Type u2} [inst_1 : AddCommGroup M] [inst_2 : Module R M] {A : Type u_1}
    [inst_3 : Semiring A] [inst_4 : Algebra R A] (n : ℕ) (f : Fin n → M) (x y : Fin n),
    f x = f y → x ≠ y → x < y → List.prod (List.ofFn fun i => ↑(ι R) (f i)) = 0
h : ¬x < y
⊢ List.prod (List.ofFn fun i => ↑(ι R) (f i)) = 0
[PROOFSTEP]
exact this R (A := A) n f y x hfxy.symm hxy.symm (hxy.lt_or_lt.resolve_left h)
[GOAL]
R✝ : Type u1
inst✝⁷ : CommRing R✝
M✝ : Type u2
inst✝⁶ : AddCommGroup M✝
inst✝⁵ : Module R✝ M✝
R : Type u1
inst✝⁴ : CommRing R
M : Type u2
inst✝³ : AddCommGroup M
inst✝² : Module R M
A : Type u_1
inst✝¹ : Semiring A
inst✝ : Algebra R A
n : ℕ
f : Fin n → M
x y : Fin n
hfxy : f x = f y
hxy : x ≠ y
h : x < y
⊢ List.prod (List.ofFn fun i => ↑(ι R) (f i)) = 0
[PROOFSTEP]
clear hxy
[GOAL]
R✝ : Type u1
inst✝⁷ : CommRing R✝
M✝ : Type u2
inst✝⁶ : AddCommGroup M✝
inst✝⁵ : Module R✝ M✝
R : Type u1
inst✝⁴ : CommRing R
M : Type u2
inst✝³ : AddCommGroup M
inst✝² : Module R M
A : Type u_1
inst✝¹ : Semiring A
inst✝ : Algebra R A
n : ℕ
f : Fin n → M
x y : Fin n
hfxy : f x = f y
h : x < y
⊢ List.prod (List.ofFn fun i => ↑(ι R) (f i)) = 0
[PROOFSTEP]
induction' n with n hn
[GOAL]
case zero
R✝ : Type u1
inst✝⁷ : CommRing R✝
M✝ : Type u2
inst✝⁶ : AddCommGroup M✝
inst✝⁵ : Module R✝ M✝
R : Type u1
inst✝⁴ : CommRing R
M : Type u2
inst✝³ : AddCommGroup M
inst✝² : Module R M
A : Type u_1
inst✝¹ : Semiring A
inst✝ : Algebra R A
n : ℕ
f✝ : Fin n → M
x✝ y✝ : Fin n
hfxy✝ : f✝ x✝ = f✝ y✝
h✝ : x✝ < y✝
f : Fin Nat.zero → M
x y : Fin Nat.zero
hfxy : f x = f y
h : x < y
⊢ List.prod (List.ofFn fun i => ↑(ι R) (f i)) = 0
[PROOFSTEP]
exact x.elim0
[GOAL]
case succ
R✝ : Type u1
inst✝⁷ : CommRing R✝
M✝ : Type u2
inst✝⁶ : AddCommGroup M✝
inst✝⁵ : Module R✝ M✝
R : Type u1
inst✝⁴ : CommRing R
M : Type u2
inst✝³ : AddCommGroup M
inst✝² : Module R M
A : Type u_1
inst✝¹ : Semiring A
inst✝ : Algebra R A
n✝ : ℕ
f✝ : Fin n✝ → M
x✝ y✝ : Fin n✝
hfxy✝ : f✝ x✝ = f✝ y✝
h✝ : x✝ < y✝
n : ℕ
hn : ∀ (f : Fin n → M) (x y : Fin n), f x = f y → x < y → List.prod (List.ofFn fun i => ↑(ι R) (f i)) = 0
f : Fin (Nat.succ n) → M
x y : Fin (Nat.succ n)
hfxy : f x = f y
h : x < y
⊢ List.prod (List.ofFn fun i => ↑(ι R) (f i)) = 0
[PROOFSTEP]
rw [List.ofFn_succ, List.prod_cons]
[GOAL]
case succ
R✝ : Type u1
inst✝⁷ : CommRing R✝
M✝ : Type u2
inst✝⁶ : AddCommGroup M✝
inst✝⁵ : Module R✝ M✝
R : Type u1
inst✝⁴ : CommRing R
M : Type u2
inst✝³ : AddCommGroup M
inst✝² : Module R M
A : Type u_1
inst✝¹ : Semiring A
inst✝ : Algebra R A
n✝ : ℕ
f✝ : Fin n✝ → M
x✝ y✝ : Fin n✝
hfxy✝ : f✝ x✝ = f✝ y✝
h✝ : x✝ < y✝
n : ℕ
hn : ∀ (f : Fin n → M) (x y : Fin n), f x = f y → x < y → List.prod (List.ofFn fun i => ↑(ι R) (f i)) = 0
f : Fin (Nat.succ n) → M
x y : Fin (Nat.succ n)
hfxy : f x = f y
h : x < y
⊢ ↑(ι R) (f 0) * List.prod (List.ofFn fun i => ↑(ι R) (f (Fin.succ i))) = 0
[PROOFSTEP]
by_cases hx :
  x =
    0
      -- one of the repeated terms is on the left
[GOAL]
case pos
R✝ : Type u1
inst✝⁷ : CommRing R✝
M✝ : Type u2
inst✝⁶ : AddCommGroup M✝
inst✝⁵ : Module R✝ M✝
R : Type u1
inst✝⁴ : CommRing R
M : Type u2
inst✝³ : AddCommGroup M
inst✝² : Module R M
A : Type u_1
inst✝¹ : Semiring A
inst✝ : Algebra R A
n✝ : ℕ
f✝ : Fin n✝ → M
x✝ y✝ : Fin n✝
hfxy✝ : f✝ x✝ = f✝ y✝
h✝ : x✝ < y✝
n : ℕ
hn : ∀ (f : Fin n → M) (x y : Fin n), f x = f y → x < y → List.prod (List.ofFn fun i => ↑(ι R) (f i)) = 0
f : Fin (Nat.succ n) → M
x y : Fin (Nat.succ n)
hfxy : f x = f y
h : x < y
hx : x = 0
⊢ ↑(ι R) (f 0) * List.prod (List.ofFn fun i => ↑(ι R) (f (Fin.succ i))) = 0
[PROOFSTEP]
rw [hx] at hfxy h 
[GOAL]
case pos
R✝ : Type u1
inst✝⁷ : CommRing R✝
M✝ : Type u2
inst✝⁶ : AddCommGroup M✝
inst✝⁵ : Module R✝ M✝
R : Type u1
inst✝⁴ : CommRing R
M : Type u2
inst✝³ : AddCommGroup M
inst✝² : Module R M
A : Type u_1
inst✝¹ : Semiring A
inst✝ : Algebra R A
n✝ : ℕ
f✝ : Fin n✝ → M
x✝ y✝ : Fin n✝
hfxy✝ : f✝ x✝ = f✝ y✝
h✝ : x✝ < y✝
n : ℕ
hn : ∀ (f : Fin n → M) (x y : Fin n), f x = f y → x < y → List.prod (List.ofFn fun i => ↑(ι R) (f i)) = 0
f : Fin (Nat.succ n) → M
x y : Fin (Nat.succ n)
hfxy : f 0 = f y
h : 0 < y
hx : x = 0
⊢ ↑(ι R) (f 0) * List.prod (List.ofFn fun i => ↑(ι R) (f (Fin.succ i))) = 0
[PROOFSTEP]
rw [hfxy, ← Fin.succ_pred y (ne_of_lt h).symm]
[GOAL]
case pos
R✝ : Type u1
inst✝⁷ : CommRing R✝
M✝ : Type u2
inst✝⁶ : AddCommGroup M✝
inst✝⁵ : Module R✝ M✝
R : Type u1
inst✝⁴ : CommRing R
M : Type u2
inst✝³ : AddCommGroup M
inst✝² : Module R M
A : Type u_1
inst✝¹ : Semiring A
inst✝ : Algebra R A
n✝ : ℕ
f✝ : Fin n✝ → M
x✝ y✝ : Fin n✝
hfxy✝ : f✝ x✝ = f✝ y✝
h✝ : x✝ < y✝
n : ℕ
hn : ∀ (f : Fin n → M) (x y : Fin n), f x = f y → x < y → List.prod (List.ofFn fun i => ↑(ι R) (f i)) = 0
f : Fin (Nat.succ n) → M
x y : Fin (Nat.succ n)
hfxy : f 0 = f y
h : 0 < y
hx : x = 0
⊢ ↑(ι R) (f (Fin.succ (Fin.pred y (_ : y ≠ 0)))) * List.prod (List.ofFn fun i => ↑(ι R) (f (Fin.succ i))) = 0
[PROOFSTEP]
exact
  ι_mul_prod_list (f ∘ Fin.succ)
    _
      -- ignore the left-most term and induct on the remaining ones, decrementing indices
[GOAL]
case neg
R✝ : Type u1
inst✝⁷ : CommRing R✝
M✝ : Type u2
inst✝⁶ : AddCommGroup M✝
inst✝⁵ : Module R✝ M✝
R : Type u1
inst✝⁴ : CommRing R
M : Type u2
inst✝³ : AddCommGroup M
inst✝² : Module R M
A : Type u_1
inst✝¹ : Semiring A
inst✝ : Algebra R A
n✝ : ℕ
f✝ : Fin n✝ → M
x✝ y✝ : Fin n✝
hfxy✝ : f✝ x✝ = f✝ y✝
h✝ : x✝ < y✝
n : ℕ
hn : ∀ (f : Fin n → M) (x y : Fin n), f x = f y → x < y → List.prod (List.ofFn fun i => ↑(ι R) (f i)) = 0
f : Fin (Nat.succ n) → M
x y : Fin (Nat.succ n)
hfxy : f x = f y
h : x < y
hx : ¬x = 0
⊢ ↑(ι R) (f 0) * List.prod (List.ofFn fun i => ↑(ι R) (f (Fin.succ i))) = 0
[PROOFSTEP]
convert mul_zero (ι R (f 0))
[GOAL]
case h.e'_2.h.e'_6
R✝ : Type u1
inst✝⁷ : CommRing R✝
M✝ : Type u2
inst✝⁶ : AddCommGroup M✝
inst✝⁵ : Module R✝ M✝
R : Type u1
inst✝⁴ : CommRing R
M : Type u2
inst✝³ : AddCommGroup M
inst✝² : Module R M
A : Type u_1
inst✝¹ : Semiring A
inst✝ : Algebra R A
n✝ : ℕ
f✝ : Fin n✝ → M
x✝ y✝ : Fin n✝
hfxy✝ : f✝ x✝ = f✝ y✝
h✝ : x✝ < y✝
n : ℕ
hn : ∀ (f : Fin n → M) (x y : Fin n), f x = f y → x < y → List.prod (List.ofFn fun i => ↑(ι R) (f i)) = 0
f : Fin (Nat.succ n) → M
x y : Fin (Nat.succ n)
hfxy : f x = f y
h : x < y
hx : ¬x = 0
⊢ List.prod (List.ofFn fun i => ↑(ι R) (f (Fin.succ i))) = 0
[PROOFSTEP]
refine'
  hn (fun i => f <| Fin.succ i) (x.pred hx) (y.pred (ne_of_lt <| lt_of_le_of_lt x.zero_le h).symm) _
    (Fin.pred_lt_pred_iff.mpr h)
[GOAL]
case h.e'_2.h.e'_6
R✝ : Type u1
inst✝⁷ : CommRing R✝
M✝ : Type u2
inst✝⁶ : AddCommGroup M✝
inst✝⁵ : Module R✝ M✝
R : Type u1
inst✝⁴ : CommRing R
M : Type u2
inst✝³ : AddCommGroup M
inst✝² : Module R M
A : Type u_1
inst✝¹ : Semiring A
inst✝ : Algebra R A
n✝ : ℕ
f✝ : Fin n✝ → M
x✝ y✝ : Fin n✝
hfxy✝ : f✝ x✝ = f✝ y✝
h✝ : x✝ < y✝
n : ℕ
hn : ∀ (f : Fin n → M) (x y : Fin n), f x = f y → x < y → List.prod (List.ofFn fun i => ↑(ι R) (f i)) = 0
f : Fin (Nat.succ n) → M
x y : Fin (Nat.succ n)
hfxy : f x = f y
h : x < y
hx : ¬x = 0
⊢ (fun i => f (Fin.succ i)) (Fin.pred x hx) = (fun i => f (Fin.succ i)) (Fin.pred y (_ : y ≠ 0))
[PROOFSTEP]
simp only [Fin.succ_pred]
[GOAL]
case h.e'_2.h.e'_6
R✝ : Type u1
inst✝⁷ : CommRing R✝
M✝ : Type u2
inst✝⁶ : AddCommGroup M✝
inst✝⁵ : Module R✝ M✝
R : Type u1
inst✝⁴ : CommRing R
M : Type u2
inst✝³ : AddCommGroup M
inst✝² : Module R M
A : Type u_1
inst✝¹ : Semiring A
inst✝ : Algebra R A
n✝ : ℕ
f✝ : Fin n✝ → M
x✝ y✝ : Fin n✝
hfxy✝ : f✝ x✝ = f✝ y✝
h✝ : x✝ < y✝
n : ℕ
hn : ∀ (f : Fin n → M) (x y : Fin n), f x = f y → x < y → List.prod (List.ofFn fun i => ↑(ι R) (f i)) = 0
f : Fin (Nat.succ n) → M
x y : Fin (Nat.succ n)
hfxy : f x = f y
h : x < y
hx : ¬x = 0
⊢ f x = f y
[PROOFSTEP]
exact hfxy
[GOAL]
R : Type u1
inst✝⁴ : CommRing R
M : Type u2
inst✝³ : AddCommGroup M
inst✝² : Module R M
A : Type u_1
inst✝¹ : Semiring A
inst✝ : Algebra R A
n : ℕ
m : M
v : Fin n → M
⊢ ↑(ι R) (Matrix.vecCons m v 0) * ↑(ιMulti R n) (Matrix.vecTail (Matrix.vecCons m v)) =
    ↑(↑(LinearMap.compAlternatingMap (LinearMap.mulLeft R (↑(ι R) m))) (ιMulti R n)) v
[PROOFSTEP]
simp_rw [Matrix.tail_cons]
[GOAL]
R : Type u1
inst✝⁴ : CommRing R
M : Type u2
inst✝³ : AddCommGroup M
inst✝² : Module R M
A : Type u_1
inst✝¹ : Semiring A
inst✝ : Algebra R A
n : ℕ
m : M
v : Fin n → M
⊢ ↑(ι R) (Matrix.vecCons m v 0) * ↑(ιMulti R n) v =
    ↑(↑(LinearMap.compAlternatingMap (LinearMap.mulLeft R (↑(ι R) m))) (ιMulti R n)) v
[PROOFSTEP]
rfl
[GOAL]
R : Type u1
inst✝² : CommRing R
M : Type u2
inst✝¹ : AddCommGroup M
inst✝ : Module R M
m : M
⊢ ↑toExterior (↑(ι R) m) = ↑(ExteriorAlgebra.ι R) m
[PROOFSTEP]
simp [toExterior]
