Lemma 4.11(2) for a sink

lem:source-basis-extension (scalar-normalization.tex): "Both assertions hold dually for a sink." For a sink t of T = T' ∪ {t}, op t is a source of the opposite category. Weights on S ⊆ O and on the corresponding set of Oᵒᵖ correspond (opScal: a line f : o → o' is the line f.op : op o' → op o), compatibly with restriction (res_opScal), so the split surjection over a source (sourceScalSplit) transports to sinkScalSplit.

def MultiplicativeBasisDeformations.Thin.ScalGroup.lineOp {O : Type v} [CategoryTheory.Category.{w, v} O] [CategoryTheory.Preadditive O] {S : Set O} {S' : Set Oᵒᵖ} (h : ∀ (X : Oᵒᵖ), X ∈ S' ↔ Opposite.unop X ∈ S) (ℓ : NzLine S') : NzLine S

A line of Oᵒᵖ as a line of O.

def MultiplicativeBasisDeformations.Thin.ScalGroup.lineUnop {O : Type v} [CategoryTheory.Category.{w, v} O] [CategoryTheory.Preadditive O] {S : Set O} {S' : Set Oᵒᵖ} (h : ∀ (X : Oᵒᵖ), X ∈ S' ↔ Opposite.unop X ∈ S) (ℓ : NzLine S) : NzLine S'

A line of O as a line of Oᵒᵖ.

theorem MultiplicativeBasisDeformations.Thin.ScalGroup.lineOp_lineUnop {O : Type v} [CategoryTheory.Category.{w, v} O] [CategoryTheory.Preadditive O] {S : Set O} {S' : Set Oᵒᵖ} (h : ∀ (X : Oᵒᵖ), X ∈ S' ↔ Opposite.unop X ∈ S) (ℓ : NzLine S) : lineOp h (lineUnop h ℓ) = ℓ

theorem MultiplicativeBasisDeformations.Thin.ScalGroup.lineUnop_lineOp {O : Type v} [CategoryTheory.Category.{w, v} O] [CategoryTheory.Preadditive O] {S : Set O} {S' : Set Oᵒᵖ} (h : ∀ (X : Oᵒᵖ), X ∈ S' ↔ Opposite.unop X ∈ S) (ℓ : NzLine S') : lineUnop h (lineOp h ℓ) = ℓ

def MultiplicativeBasisDeformations.Thin.ScalGroup.opScalHom (k : Type u) [Field k] {O : Type v} [CategoryTheory.Category.{w, v} O] [CategoryTheory.Preadditive O] [CategoryTheory.Linear k O] {S : Set O} {S' : Set Oᵒᵖ} (h : ∀ (X : Oᵒᵖ), X ∈ S' ↔ Opposite.unop X ∈ S) : ↥(Scal k S) →* ↥(Scal k S')

Weights on S as weights on the opposite set.

def MultiplicativeBasisDeformations.Thin.ScalGroup.unopScalHom (k : Type u) [Field k] {O : Type v} [CategoryTheory.Category.{w, v} O] [CategoryTheory.Preadditive O] [CategoryTheory.Linear k O] {S : Set O} {S' : Set Oᵒᵖ} (h : ∀ (X : Oᵒᵖ), X ∈ S' ↔ Opposite.unop X ∈ S) : ↥(Scal k S') →* ↥(Scal k S)

Weights on the opposite set as weights on S.

def MultiplicativeBasisDeformations.Thin.ScalGroup.opScal (k : Type u) [Field k] {O : Type v} [CategoryTheory.Category.{w, v} O] [CategoryTheory.Preadditive O] [CategoryTheory.Linear k O] {S : Set O} {S' : Set Oᵒᵖ} (h : ∀ (X : Oᵒᵖ), X ∈ S' ↔ Opposite.unop X ∈ S) : ↥(Scal k S) ≃* ↥(Scal k S')

Weights on S are weights on the opposite set.

theorem MultiplicativeBasisDeformations.Thin.ScalGroup.res_opScal {k : Type u} [Field k] {O : Type v} [CategoryTheory.Category.{w, v} O] [CategoryTheory.Preadditive O] [CategoryTheory.Linear k O] {S₁ S₂ : Set O} {S₁' S₂' : Set Oᵒᵖ} (hS : S₁ ⊆ S₂) (hS' : S₁' ⊆ S₂') (h₁ : ∀ (X : Oᵒᵖ), X ∈ S₁' ↔ Opposite.unop X ∈ S₁) (h₂ : ∀ (X : Oᵒᵖ), X ∈ S₂' ↔ Opposite.unop X ∈ S₂) (d : ↥(Scal k S₂)) : (res k hS') ((opScal k h₂) d) = (opScal k h₁) ((res k hS) d)

theorem MultiplicativeBasisDeformations.Thin.ScalGroup.sinkScalSplit {k : Type u} [Field k] {O : Type v} [CategoryTheory.Category.{w, v} O] [CategoryTheory.Preadditive O] [CategoryTheory.Linear k O] [Infinite k] (hT : IsThin k O) (t : O) (S : Finset O) (htS : t ∉ S) (hsnk : ∀ o ∈ S, ∀ (f : t ⟶ o), f = 0) (hrep : SupRepFinite ⋯ ⋯) : (∃ (e : ↥(Scal k ↑S) →* ↥(Scal k (insert t ↑S))), ∀ (d : ↥(Scal k ↑S)), (res k ⋯) (e d) = d) ∧ Function.Surjective ⇑(res k ⋯) ∧ Nonempty (↥(res k ⋯).ker ≃* (Comp (Opposite.op t) (Finset.map opEmb S) → kˣ))

Lemma 4.11(2) for a sink: restriction Scal(T) → Scal(T') is a split surjection, with kernel k* to the power of the components of the support poset of the sink (a source of the opposite category).