coindToInd_of_support_subset_orbit

English

There exists a natural isomorphism between the Ind and Coind functors, linking induction from S to G with coinduction from G to S.

Русский

Существует естественное изоморождение между функторaми Ind и Coind, связывающее индукцию S в G с коиндукцией G в S.

LaTeX

$$$\text{indCoindNatIso } k S .$$

Lean4

theorem coindToInd_of_support_subset_orbit (g : G) (f : coind S.subtype A) (hx : f.1.support ⊆ MulAction.orbit S g) :
    coindToInd A f = IndV.mk S.subtype _ g (f.1 g) :=
  by
  rw [coindToInd_apply, Finset.sum_eq_single ⟦g⟧]
  · simp
  · intro b _ hb
    induction b using Quotient.inductionOn with
    | h
      b =>
      have : f.1 b = 0 := by
        simp_all only [Function.support_subset_iff, ne_eq, Quotient.eq]
        contrapose! hx
        use b, hx, hb
      simp_all
  · simp

Похожие утверждения