English
An induction principle for PiTensorProduct expressing motive by induction on tprodCoeff and addition.
Русский
Принцип индукции для PiTensorProduct, выражающий свойство через индукцию по tprodCoeff и сложение.
LaTeX
$$motive z if base and additivity hold$$
Lean4
/-- Construct an `AddMonoidHom` from `(⨂[R] i, s i)` to some space `F` from a function
`φ : (R × Π i, s i) → F` with the appropriate properties. -/
def liftAddHom (φ : (R × Π i, s i) → F) (C0 : ∀ (r : R) (f : Π i, s i) (i : ι) (_ : f i = 0), φ (r, f) = 0)
(C0' : ∀ f : Π i, s i, φ (0, f) = 0)
(C_add :
∀ [DecidableEq ι] (r : R) (f : Π i, s i) (i : ι) (m₁ m₂ : s i),
φ (r, update f i m₁) + φ (r, update f i m₂) = φ (r, update f i (m₁ + m₂)))
(C_add_scalar : ∀ (r r' : R) (f : Π i, s i), φ (r, f) + φ (r', f) = φ (r + r', f))
(C_smul : ∀ [DecidableEq ι] (r : R) (f : Π i, s i) (i : ι) (r' : R), φ (r, update f i (r' • f i)) = φ (r' * r, f)) :
(⨂[R] i, s i) →+ F :=
(addConGen (PiTensorProduct.Eqv R s)).lift (FreeAddMonoid.lift φ) <|
AddCon.addConGen_le fun x y hxy ↦
match hxy with
| Eqv.of_zero r' f i hf => (AddCon.ker_rel _).2 <| by simp [FreeAddMonoid.lift_eval_of, C0 r' f i hf]
| Eqv.of_zero_scalar f => (AddCon.ker_rel _).2 <| by simp [FreeAddMonoid.lift_eval_of, C0']
| Eqv.of_add inst z f i m₁ m₂ => (AddCon.ker_rel _).2 <| by simp [FreeAddMonoid.lift_eval_of, @C_add inst]
| Eqv.of_add_scalar z₁ z₂ f => (AddCon.ker_rel _).2 <| by simp [FreeAddMonoid.lift_eval_of, C_add_scalar]
| Eqv.of_smul inst z f i r' => (AddCon.ker_rel _).2 <| by simp [FreeAddMonoid.lift_eval_of, @C_smul inst]
| Eqv.add_comm x y => (AddCon.ker_rel _).2 <| by simp_rw [AddMonoidHom.map_add, add_comm]
