Built with
doc-gen4 , running Lean4.
Bubbles (
) indicate interactive fragments: hover for details, tap to reveal contents.
Use
Ctrl+↑ Ctrl+↓ to navigate,
Ctrl+🖱️ to focus.
On Mac, use
Cmd instead of
Ctrl .
/-
Copyright (c) 2020 Scott Morrison. All rights reserved.
Released under Apache 2.0 license as described in the file LICENSE.
Authors: Scott Morrison
! This file was ported from Lean 3 source module data.finsupp.pointwise
! leanprover-community/mathlib commit f7fc89d5d5ff1db2d1242c7bb0e9062ce47ef47c
! Please do not edit these lines, except to modify the commit id
! if you have ported upstream changes.
-/
import Mathlib.Data.Finsupp.Defs
import Mathlib.Algebra.Ring.Pi
/-!
# The pointwise product on `Finsupp`.
For the convolution product on `Finsupp` when the domain has a binary operation,
see the type synonyms `AddMonoidAlgebra`
(which is in turn used to define `Polynomial` and `MvPolynomial`)
and `MonoidAlgebra`.
-/
noncomputable section
open Finset
universe u₁ u₂ u₃ u₄ u₅
variable { α : Type u₁ } { β : Type u₂ } { γ : Type u₃ } { δ : Type u₄ } { ι : Type u₅ }
namespace Finsupp
/-! ### Declarations about the pointwise product on `Finsupp`s -/
section
variable [ MulZeroClass : Type ?u.3444 → Type ?u.3444 β ]
/-- The product of `f g : α →₀ β` is the finitely supported function
whose value at `a` is `f a * g a`. -/
instance : Mul ( α →₀ β ) :=
⟨ zipWith : {α : Type ?u.401} →
{M : Type ?u.400} →
{N : Type ?u.399} →
{P : Type ?u.398} →
[inst : Zero M [inst_1 : Zero N [inst_2 : Zero P (f : M → N → P f 0 0 = 0 (α →₀ M (α →₀ N α →₀ P (· * ·) ( mul_zero 0 )⟩
theorem coe_mul : ∀ (g₁ g₂ : α →₀ β ↑(g₁ * g₂ = ↑g₁ * ↑g₂ coe_mul ( g₁ g₂ : α →₀ β ) : ⇑( g₁ * g₂ ) = g₁ * g₂ :=
rfl : ∀ {α : Sort ?u.3412} {a : α }, a = a
#align finsupp.coe_mul Finsupp.coe_mul
@[ simp ]
theorem mul_apply : ∀ {g₁ g₂ : α →₀ β a : α }, ↑(g₁ * g₂ a = ↑g₁ a * ↑g₂ a mul_apply { g₁ g₂ : α →₀ β } { a : α } : ( g₁ * g₂ ) a = g₁ a * g₂ a :=
rfl : ∀ {α : Sort ?u.4439} {a : α }, a = a
#align finsupp.mul_apply Finsupp.mul_apply : ∀ {α : Type u₁} {β : Type u₂} [inst : MulZeroClass β g₁ g₂ : α →₀ β a : α }, ↑(g₁ * g₂ a = ↑g₁ a * ↑g₂ a
theorem support_mul : ∀ [inst : DecidableEq α g₁ g₂ : α →₀ β (g₁ * g₂ ⊆ g₁ .support∩ g₂ .support support_mul [ DecidableEq : Sort ?u.4500 → Sort (max1?u.4500) α ] { g₁ g₂ : α →₀ β } :
( g₁ * g₂ ). support ⊆ g₁ . support ∩ g₂ . support := by
(g₁ * g₂ ⊆ g₁ .support∩ g₂ .supportintro a h a ∈ g₁ .support∩ g₂ .support
(g₁ * g₂ ⊆ g₁ .support∩ g₂ .supportsimp only [ mul_apply : ∀ {α : Type ?u.5045} {β : Type ?u.5044} [inst : MulZeroClass β g₁ g₂ : α →₀ β a : α }, ↑(g₁ * g₂ a = ↑g₁ a * ↑g₂ a , mem_support_iff : ∀ {α : Type ?u.5076} {M : Type ?u.5077} [inst : Zero M f : α →₀ M a : α }, a ∈ f .support↔ ↑f a ≠ 0 ] at h a ∈ g₁ .support∩ g₂ .support
(g₁ * g₂ ⊆ g₁ .support∩ g₂ .supportsimp only [ mem_support_iff : ∀ {α : Type ?u.5679} {M : Type ?u.5680} [inst : Zero M f : α →₀ M a : α }, a ∈ f .support↔ ↑f a ≠ 0 , mem_inter , Ne.def : ∀ {α : Sort ?u.5732} (a b : α ), (a ≠ b = ¬ a = b ]
(g₁ * g₂ ⊆ g₁ .support∩ g₂ .supportrw [ ← not_or ]
(g₁ * g₂ ⊆ g₁ .support∩ g₂ .supportintro w
(g₁ * g₂ ⊆ g₁ .support∩ g₂ .supportapply h
(g₁ * g₂ ⊆ g₁ .support∩ g₂ .supportcases' w with w w <;> ( rw [ w ] ; simp )
#align finsupp.support_mul Finsupp.support_mul
instance : MulZeroClass : Type ?u.6625 → Type ?u.6625 ( α →₀ β ) :=
FunLike.coe_injective . mulZeroClass _ coe_zero : ∀ {α : Type ?u.7164} {M : Type ?u.7165} [inst : Zero M ↑0 = 0 coe_mul
end
instance [ SemigroupWithZero : Type ?u.7575 → Type ?u.7575 β ] : SemigroupWithZero : Type ?u.7578 → Type ?u.7578 ( α →₀ β ) :=
FunLike.coe_injective . semigroupWithZero _ coe_zero : ∀ {α : Type ?u.8073} {M : Type ?u.8074} [inst : Zero M ↑0 = 0 coe_mul
instance [ NonUnitalNonAssocSemiring : Type ?u.8991 → Type ?u.8991 β ] : NonUnitalNonAssocSemiring : Type ?u.8994 → Type ?u.8994 ( α →₀ β ) :=
FunLike.coe_injective . nonUnitalNonAssocSemiring _ coe_zero : ∀ {α : Type ?u.9597} {M : Type ?u.9598} [inst : Zero M ↑0 = 0 coe_add coe_mul fun _ _ ↦ rfl : ∀ {α : Sort ?u.10523} {a : α }, a = a
instance [ NonUnitalSemiring : Type ?u.11139 → Type ?u.11139 β ] : NonUnitalSemiring : Type ?u.11142 → Type ?u.11142 ( α →₀ β ) :=
FunLike.coe_injective . nonUnitalSemiring _ coe_zero : ∀ {α : Type ?u.11702} {M : Type ?u.11703} [inst : Zero M ↑0 = 0 coe_add coe_mul fun _ _ ↦ rfl : ∀ {α : Sort ?u.12788} {a : α }, a = a
instance [ NonUnitalCommSemiring : Type ?u.13409 → Type ?u.13409 β ] : NonUnitalCommSemiring : Type ?u.13412 → Type ?u.13412 ( α →₀ β ) :=
FunLike.coe_injective . nonUnitalCommSemiring _ coe_zero : ∀ {α : Type ?u.13976} {M : Type ?u.13977} [inst : Zero M ↑0 = 0 coe_add coe_mul fun _ _ ↦ rfl : ∀ {α : Sort ?u.15072} {a : α }, a = a
instance [ NonUnitalNonAssocRing : Type ?u.15699 → Type ?u.15699 β ] : NonUnitalNonAssocRing : Type ?u.15702 → Type ?u.15702 ( α →₀ β ) :=
FunLike.coe_injective . nonUnitalNonAssocRing _ coe_zero : ∀ {α : Type ?u.16390} {M : Type ?u.16391} [inst : Zero M ↑0 = 0 coe_add coe_mul coe_neg coe_sub
( fun _ _ ↦ rfl : ∀ {α : Sort ?u.17435} {a : α }, a = a ) fun _ _ ↦ rfl : ∀ {α : Sort ?u.17709} {a : α }, a = a
instance [ NonUnitalRing : Type ?u.18052 → Type ?u.18052 β ] : NonUnitalRing : Type ?u.18055 → Type ?u.18055 ( α →₀ β ) :=
FunLike.coe_injective . nonUnitalRing : {α : Type ?u.18461} →
{β : Type ?u.18460} →
[inst : NonUnitalRing α [inst_1 : Zero β [inst_2 : Add β [inst_3 : Mul β [inst_4 : Neg β [inst_5 : Sub β [inst_6 : SMul ℕ β [inst_7 : SMul ℤ β (f : β → α Function.Injective f f 0 = 0 (∀ (x y : β ), f (x + y = f x + f y ) →
(∀ (x y : β ), f (x * y = f x * f y ) →
(∀ (x : β ), f (- x = - f x ) →
(∀ (x y : β ), f (x - y = f x - f y ) →
(∀ (x : β ) (n : ℕ ), f (n • x = n • f x ) →
(∀ (x : β ) (n : ℤ ), f (n • x = n • f x ) → NonUnitalRing β _ coe_zero : ∀ {α : Type ?u.18717} {M : Type ?u.18718} [inst : Zero M ↑0 = 0 coe_add coe_mul coe_neg coe_sub ( fun _ _ ↦ rfl : ∀ {α : Sort ?u.19831} {a : α }, a = a )
fun _ _ ↦ rfl : ∀ {α : Sort ?u.20112} {a : α }, a = a
instance [ NonUnitalCommRing : Type ?u.20427 → Type ?u.20427 β ] : NonUnitalCommRing : Type ?u.20430 → Type ?u.20430 ( α →₀ β ) :=
FunLike.coe_injective . nonUnitalCommRing _ coe_zero : ∀ {α : Type ?u.21078} {M : Type ?u.21079} [inst : Zero M ↑0 = 0 coe_add coe_mul coe_neg coe_sub
( fun _ _ ↦ rfl : ∀ {α : Sort ?u.22194} {a : α }, a = a ) fun _ _ ↦ rfl : ∀ {α : Sort ?u.22479} {a : α }, a = a
-- TODO can this be generalized in the direction of `Pi.smul'`
-- (i.e. dependent functions and finsupps)
-- TODO in theory this could be generalised, we only really need `smul_zero` for the definition
instance pointwiseScalar [ Semiring β ] : SMul : Type ?u.22800 → Type ?u.22799 → Type (max?u.22800?u.22799) ( α → β ) ( α →₀ β ) where
smul f g :=
Finsupp.ofSupportFinite ( fun a ↦ f a • g a ) ( by
apply Set.Finite.subset g . finite_support
simp only [ Function.support_subset_iff , Finsupp.mem_support_iff : ∀ {α : Type ?u.23706} {M : Type ?u.23707} [inst : Zero M f : α →₀ M a : α }, a ∈ f .support↔ ↑f a ≠ 0 , Ne.def : ∀ {α : Sort ?u.23734} (a b : α ), (a ≠ b = ¬ a = b ,
Finsupp.fun_support_eq , Finset.mem_coe : ∀ {α : Type ?u.23767} {a : α } {s : Finset α a ∈ ↑s ↔ a ∈ s ] ∀ (x : α ), ¬ f x • ↑g x = 0 ¬ ↑g x = 0
intro x hx h
apply hx
rw [ h , smul_zero ] )
#align finsupp.pointwise_scalar Finsupp.pointwiseScalar
@[ simp ]
theorem coe_pointwise_smul : ∀ {α : Type u₁} {β : Type u₂} [inst : Semiring β f : α → β g : α →₀ β ↑(f • g = ↑(f • g coe_pointwise_smul [ Semiring β ] ( f : α → β ) ( g : α →₀ β ) : FunLike.coe ( f • g ) = f • g :=
rfl : ∀ {α : Sort ?u.25621} {a : α }, a = a
#align finsupp.coe_pointwise_smul Finsupp.coe_pointwise_smul : ∀ {α : Type u₁} {β : Type u₂} [inst : Semiring β f : α → β g : α →₀ β ↑(f • g = ↑(f • g
/-- The pointwise multiplicative action of functions on finitely supported functions -/
instance pointwiseModule [ Semiring β ] : Module ( α → β ) ( α →₀ β ) :=
Function.Injective.module _ coeFnAddHom FunLike.coe_injective coe_pointwise_smul : ∀ {α : Type ?u.26944} {β : Type ?u.26943} [inst : Semiring β f : α → β g : α →₀ β ↑(f • g = ↑(f • g
#align finsupp.pointwise_module Finsupp.pointwiseModule
end Finsupp