Lifts a Finsupp from an underlying type to a Finsupp on a quotient

noncomputable def Quot.liftFinsupp {α : Type u_1} {β : Type u_2} {r : α → α → Prop} [Zero β] (f : α →₀ β) (h : ∀ (a b : α), r a b → f a = f b) : Quot r →₀ β

Lift a function α →₀ β to Quot r →₀ β.

Equations

• Quot.liftFinsupp f h = { support := Finset.image (Quot.mk r) f.support, toFun := Quot.lift (⇑f) h, mem_support_toFun := ⋯ }

@[simp]

theorem Quot.liftFinsupp_mk {α : Type u_1} {β : Type u_2} {r : α → α → Prop} [Zero β] (f : α →₀ β) (h : ∀ (a b : α), r a b → f a = f b) (a : α) : (Quot.liftFinsupp f h) (mk r a) = f a

noncomputable def Quotient.liftFinsupp {α : Type u_1} {β : Type u_2} {s : Setoid α} [Zero β] (f : α →₀ β) (h : ∀ (a b : α), s a b → f a = f b) : Quotient s →₀ β

Lift a function α →₀ β to Quot r →₀ β.

Equations

• Quotient.liftFinsupp f h = Quot.liftFinsupp f h

@[simp]

theorem Quotient.liftFinsupp_mk {α : Type u_1} {β : Type u_2} {s : Setoid α} [Zero β] (f : α →₀ β) (h : ∀ (a b : α), s a b → f a = f b) (a : α) : (Quotient.liftFinsupp f h) ⟦a⟧ = f a

noncomputable def Setoid.liftFinsuppEquiv {α : Type u_1} {β : Type u_2} (s : Setoid α) [Zero β] (hs : ∀ (a : α), {b : α | s b a}.Finite) : { f : α →₀ β // ∀ (a b : α), s a b → f a = f b } ≃ (Quotient s →₀ β)

Finitely supported functions on α that are constant on the classes of s correspond to finitely supported functions on Quotient s, provided the classes are finite.

Equations

• One or more equations did not get rendered due to their size.

@[simp]

theorem Setoid.liftFinsuppEquiv_apply_mk {α : Type u_1} {β : Type u_2} {s : Setoid α} [Zero β] (hs : ∀ (a : α), {b : α | s b a}.Finite) (f : { f : α →₀ β // ∀ (a b : α), s a b → f a = f b }) (a : α) : ((s.liftFinsuppEquiv hs) f) ⟦a⟧ = ↑f a

@[simp]

theorem Setoid.liftFinsuppEquiv_symm_apply {α : Type u_1} {β : Type u_2} {s : Setoid α} [Zero β] (hs : ∀ (a : α), {b : α | s b a}.Finite) (f : Quotient s →₀ β) (a : α) : ↑((s.liftFinsuppEquiv hs).symm f) a = f ⟦a⟧