Proposition 4.14: descent of a multiplicative basis along a free deck group #
prop:scalar-normalization (scalar-normalization.tex): "Let b_{xy}
be the multiplicative basis constructed on L. For a free deck generator g,
write g(b_{xy}) = d_g(x, y) b_{gx,gy}. The coefficients form a multiplicative
weight. By Lemma 4.13, write d_g(x, y) = a_g(y)/a_g(x). On each orbit of
objects solve f(gx) = a_g(x) f(x) for all free generators. The orbit graph is a
Cayley tree, so a value at one root determines consistent values everywhere.
Then b'_{xy} = (f(y)/f(x)) b_{xy} is still multiplicative and is deck
invariant."
For a graded family with a thin cover, a multiplicative basis β on the cover,
a free grading group, and Lemma 4.13 as a hypothesis (hratio), we build the
deck-invariant multiplicative basis b' (invBasis). The deck group acts on
the cover by translating sheets (tr), with the same morphisms (trHom). The
values f are the transport of (root, 1) under the homomorphism from the free
group to permutations of objects × kˣ lifting the generators (Ψ): this is
"a value at one root determines consistent values everywhere".
Deck translations of the cover #
def
MultiplicativeBasisDeformations.CatAlg.tr
{k : Type u}
[Field k]
{𝒞 : Type v}
[CategoryTheory.Category.{u, v} 𝒞]
[CategoryTheory.Preadditive 𝒞]
[CategoryTheory.Linear k 𝒞]
{ι : Type}
{F : ι → 𝒞}
{G : Type}
[Group G]
[DecidableEq G]
{D : HomGrading F G}
(g : G)
(o : CovObj D)
:
CovObj D
Translation of the sheet by g.
Instances For
@[simp]
theorem
MultiplicativeBasisDeformations.CatAlg.tr_fst
{k : Type u}
[Field k]
{𝒞 : Type v}
[CategoryTheory.Category.{u, v} 𝒞]
[CategoryTheory.Preadditive 𝒞]
[CategoryTheory.Linear k 𝒞]
{ι : Type}
[Fintype ι]
[DecidableEq ι]
{F : ι → 𝒞}
{G : Type}
[Group G]
[DecidableEq G]
{D : HomGrading F G}
(g : G)
(o : CovObj D)
:
(tr g o).1 = o.1
@[simp]
theorem
MultiplicativeBasisDeformations.CatAlg.tr_snd
{k : Type u}
[Field k]
{𝒞 : Type v}
[CategoryTheory.Category.{u, v} 𝒞]
[CategoryTheory.Preadditive 𝒞]
[CategoryTheory.Linear k 𝒞]
{ι : Type}
[Fintype ι]
[DecidableEq ι]
{F : ι → 𝒞}
{G : Type}
[Group G]
[DecidableEq G]
{D : HomGrading F G}
(g : G)
(o : CovObj D)
:
(tr g o).2 = g * o.2
theorem
MultiplicativeBasisDeformations.CatAlg.tr_mul
{k : Type u}
[Field k]
{𝒞 : Type v}
[CategoryTheory.Category.{u, v} 𝒞]
[CategoryTheory.Preadditive 𝒞]
[CategoryTheory.Linear k 𝒞]
{ι : Type}
[Fintype ι]
[DecidableEq ι]
{F : ι → 𝒞}
{G : Type}
[Group G]
[DecidableEq G]
{D : HomGrading F G}
(g h : G)
(o : CovObj D)
:
theorem
MultiplicativeBasisDeformations.CatAlg.tr_one
{k : Type u}
[Field k]
{𝒞 : Type v}
[CategoryTheory.Category.{u, v} 𝒞]
[CategoryTheory.Preadditive 𝒞]
[CategoryTheory.Linear k 𝒞]
{ι : Type}
[Fintype ι]
[DecidableEq ι]
{F : ι → 𝒞}
{G : Type}
[Group G]
[DecidableEq G]
{D : HomGrading F G}
(o : CovObj D)
:
tr 1 o = o
theorem
MultiplicativeBasisDeformations.CatAlg.tr_inv_tr
{k : Type u}
[Field k]
{𝒞 : Type v}
[CategoryTheory.Category.{u, v} 𝒞]
[CategoryTheory.Preadditive 𝒞]
[CategoryTheory.Linear k 𝒞]
{ι : Type}
[Fintype ι]
[DecidableEq ι]
{F : ι → 𝒞}
{G : Type}
[Group G]
[DecidableEq G]
{D : HomGrading F G}
(g : G)
(o : CovObj D)
:
theorem
MultiplicativeBasisDeformations.CatAlg.tr_tr_inv
{k : Type u}
[Field k]
{𝒞 : Type v}
[CategoryTheory.Category.{u, v} 𝒞]
[CategoryTheory.Preadditive 𝒞]
[CategoryTheory.Linear k 𝒞]
{ι : Type}
[Fintype ι]
[DecidableEq ι]
{F : ι → 𝒞}
{G : Type}
[Group G]
[DecidableEq G]
{D : HomGrading F G}
(g : G)
(o : CovObj D)
:
theorem
MultiplicativeBasisDeformations.CatAlg.tr_part
{k : Type u}
[Field k]
{𝒞 : Type v}
[CategoryTheory.Category.{u, v} 𝒞]
[CategoryTheory.Preadditive 𝒞]
[CategoryTheory.Linear k 𝒞]
{ι : Type}
[Fintype ι]
[DecidableEq ι]
{F : ι → 𝒞}
{G : Type}
[Group G]
[DecidableEq G]
{D : HomGrading F G}
(g : G)
(o o' : CovObj D)
:
def
MultiplicativeBasisDeformations.CatAlg.trHom
{k : Type u}
[Field k]
{𝒞 : Type v}
[CategoryTheory.Category.{u, v} 𝒞]
[CategoryTheory.Preadditive 𝒞]
[CategoryTheory.Linear k 𝒞]
{ι : Type}
[Fintype ι]
[DecidableEq ι]
{F : ι → 𝒞}
{G : Type}
[Group G]
[DecidableEq G]
{D : HomGrading F G}
(g : G)
{o o' : CovObj D}
(f : o ⟶ o')
:
The translated morphism (the same morphism of the family).
Instances For
@[simp]
theorem
MultiplicativeBasisDeformations.CatAlg.trHom_val
{k : Type u}
[Field k]
{𝒞 : Type v}
[CategoryTheory.Category.{u, v} 𝒞]
[CategoryTheory.Preadditive 𝒞]
[CategoryTheory.Linear k 𝒞]
{ι : Type}
[Fintype ι]
[DecidableEq ι]
{F : ι → 𝒞}
{G : Type}
[Group G]
[DecidableEq G]
{D : HomGrading F G}
(g : G)
{o o' : CovObj D}
(f : o ⟶ o')
:
↑(trHom g f) = ↑f
theorem
MultiplicativeBasisDeformations.CatAlg.trHom_comp
{k : Type u}
[Field k]
{𝒞 : Type v}
[CategoryTheory.Category.{u, v} 𝒞]
[CategoryTheory.Preadditive 𝒞]
[CategoryTheory.Linear k 𝒞]
{ι : Type}
[Fintype ι]
[DecidableEq ι]
{F : ι → 𝒞}
{G : Type}
[Group G]
[DecidableEq G]
{D : HomGrading F G}
(g : G)
{o o' o'' : CovObj D}
(f : o ⟶ o')
(f' : o' ⟶ o'')
:
theorem
MultiplicativeBasisDeformations.CatAlg.trHom_smul
{k : Type u}
[Field k]
{𝒞 : Type v}
[CategoryTheory.Category.{u, v} 𝒞]
[CategoryTheory.Preadditive 𝒞]
[CategoryTheory.Linear k 𝒞]
{ι : Type}
[Fintype ι]
[DecidableEq ι]
{F : ι → 𝒞}
{G : Type}
[Group G]
[DecidableEq G]
{D : HomGrading F G}
(g : G)
{o o' : CovObj D}
(c : k)
(f : o ⟶ o')
:
theorem
MultiplicativeBasisDeformations.CatAlg.trHom_ne_zero
{k : Type u}
[Field k]
{𝒞 : Type v}
[CategoryTheory.Category.{u, v} 𝒞]
[CategoryTheory.Preadditive 𝒞]
[CategoryTheory.Linear k 𝒞]
{ι : Type}
[Fintype ι]
[DecidableEq ι]
{F : ι → 𝒞}
{G : Type}
[Group G]
[DecidableEq G]
{D : HomGrading F G}
(g : G)
{o o' : CovObj D}
{f : o ⟶ o'}
(hf : f ≠ 0)
:
trHom g f ≠ 0
def
MultiplicativeBasisDeformations.CatAlg.untrHom
{k : Type u}
[Field k]
{𝒞 : Type v}
[CategoryTheory.Category.{u, v} 𝒞]
[CategoryTheory.Preadditive 𝒞]
[CategoryTheory.Linear k 𝒞]
{ι : Type}
[Fintype ι]
[DecidableEq ι]
{F : ι → 𝒞}
{G : Type}
[Group G]
[DecidableEq G]
{D : HomGrading F G}
(g : G)
{o o' : CovObj D}
(f : tr g o ⟶ tr g o')
:
o ⟶ o'
Morphisms back from the translated objects.
Instances For
The weights d_g #
theorem
MultiplicativeBasisDeformations.CatAlg.β_ne_zero_iff
{k : Type u}
[Field k]
{𝒞 : Type v}
[CategoryTheory.Category.{u, v} 𝒞]
[CategoryTheory.Preadditive 𝒞]
[CategoryTheory.Linear k 𝒞]
{ι : Type}
[Fintype ι]
[DecidableEq ι]
{F : ι → 𝒞}
{G : Type}
[Group G]
[DecidableEq G]
{D : HomGrading F G}
{β : (o o' : CovObj D) → o ⟶ o'}
(hβ : Thin.MultBasis Set.univ β)
{o o' : CovObj D}
:
β o o' ≠ 0 ↔ ∃ (f : o ⟶ o'), f ≠ 0
noncomputable def
MultiplicativeBasisDeformations.CatAlg.dg
{k : Type u}
[Field k]
{𝒞 : Type v}
[CategoryTheory.Category.{u, v} 𝒞]
[CategoryTheory.Preadditive 𝒞]
[CategoryTheory.Linear k 𝒞]
{ι : Type}
[Fintype ι]
[DecidableEq ι]
{F : ι → 𝒞}
{G : Type}
[Group G]
[DecidableEq G]
{D : HomGrading F G}
(hT : Thin.IsThin k (CovObj D))
(β : (o o' : CovObj D) → o ⟶ o')
(g : G)
(o o' : CovObj D)
:
k
The coefficients of a deck translation: g(b_{xy}) = d_g(x, y) b_{gx,gy}.
Instances For
theorem
MultiplicativeBasisDeformations.CatAlg.dg_spec
{k : Type u}
[Field k]
{𝒞 : Type v}
[CategoryTheory.Category.{u, v} 𝒞]
[CategoryTheory.Preadditive 𝒞]
[CategoryTheory.Linear k 𝒞]
{ι : Type}
[Fintype ι]
[DecidableEq ι]
{F : ι → 𝒞}
{G : Type}
[Group G]
[DecidableEq G]
{D : HomGrading F G}
(hT : Thin.IsThin k (CovObj D))
{β : (o o' : CovObj D) → o ⟶ o'}
(hβ : Thin.MultBasis Set.univ β)
(g : G)
{o o' : CovObj D}
(h : β o o' ≠ 0)
:
theorem
MultiplicativeBasisDeformations.CatAlg.dg_isWeight
{k : Type u}
[Field k]
{𝒞 : Type v}
[CategoryTheory.Category.{u, v} 𝒞]
[CategoryTheory.Preadditive 𝒞]
[CategoryTheory.Linear k 𝒞]
{ι : Type}
[Fintype ι]
[DecidableEq ι]
{F : ι → 𝒞}
{G : Type}
[Group G]
[DecidableEq G]
{D : HomGrading F G}
(hT : Thin.IsThin k (CovObj D))
{β : (o o' : CovObj D) → o ⟶ o'}
(hβ : Thin.MultBasis Set.univ β)
(g : G)
:
Thin.IsWeight Set.univ (dg hT β g)
The coefficients form a multiplicative weight.
Object values on the orbits #
theorem
MultiplicativeBasisDeformations.CatAlg.exists_aG
{k : Type u}
[Field k]
{𝒞 : Type v}
[CategoryTheory.Category.{u, v} 𝒞]
[CategoryTheory.Preadditive 𝒞]
[CategoryTheory.Linear k 𝒞]
{ι : Type}
[Fintype ι]
[DecidableEq ι]
{F : ι → 𝒞}
{G : Type}
[Group G]
[DecidableEq G]
{D : HomGrading F G}
(hT : Thin.IsThin k (CovObj D))
{β : (o o' : CovObj D) → o ⟶ o'}
(hβ : Thin.MultBasis Set.univ β)
[IsFreeGroup G]
(hratio :
∀ (d : CovObj D → CovObj D → k),
Thin.IsWeight Set.univ d →
∃ (ζ : CovObj D → k), (∀ (o : CovObj D), ζ o ≠ 0) ∧ ∀ (o o' : CovObj D) (f : o ⟶ o'), f ≠ 0 → d o o' = ζ o' / ζ o)
(g : G)
:
Lemma 4.13 applied to d_g: d_g(x, y) = a_g(y)/a_g(x).
noncomputable def
MultiplicativeBasisDeformations.CatAlg.aG
{k : Type u}
[Field k]
{𝒞 : Type v}
[CategoryTheory.Category.{u, v} 𝒞]
[CategoryTheory.Preadditive 𝒞]
[CategoryTheory.Linear k 𝒞]
{ι : Type}
[Fintype ι]
[DecidableEq ι]
{F : ι → 𝒞}
{G : Type}
[Group G]
[DecidableEq G]
{D : HomGrading F G}
(hT : Thin.IsThin k (CovObj D))
{β : (o o' : CovObj D) → o ⟶ o'}
(hβ : Thin.MultBasis Set.univ β)
[IsFreeGroup G]
(hratio :
∀ (d : CovObj D → CovObj D → k),
Thin.IsWeight Set.univ d →
∃ (ζ : CovObj D → k), (∀ (o : CovObj D), ζ o ≠ 0) ∧ ∀ (o o' : CovObj D) (f : o ⟶ o'), f ≠ 0 → d o o' = ζ o' / ζ o)
(g : G)
(o : CovObj D)
:
kˣ
The values a_g.
Instances For
theorem
MultiplicativeBasisDeformations.CatAlg.aG_spec
{k : Type u}
[Field k]
{𝒞 : Type v}
[CategoryTheory.Category.{u, v} 𝒞]
[CategoryTheory.Preadditive 𝒞]
[CategoryTheory.Linear k 𝒞]
{ι : Type}
[Fintype ι]
[DecidableEq ι]
{F : ι → 𝒞}
{G : Type}
[Group G]
[DecidableEq G]
{D : HomGrading F G}
(hT : Thin.IsThin k (CovObj D))
{β : (o o' : CovObj D) → o ⟶ o'}
(hβ : Thin.MultBasis Set.univ β)
[IsFreeGroup G]
(hratio :
∀ (d : CovObj D → CovObj D → k),
Thin.IsWeight Set.univ d →
∃ (ζ : CovObj D → k), (∀ (o : CovObj D), ζ o ≠ 0) ∧ ∀ (o o' : CovObj D) (f : o ⟶ o'), f ≠ 0 → d o o' = ζ o' / ζ o)
(g : G)
{o o' : CovObj D}
(h : β o o' ≠ 0)
:
noncomputable def
MultiplicativeBasisDeformations.CatAlg.πs
{k : Type u}
[Field k]
{𝒞 : Type v}
[CategoryTheory.Category.{u, v} 𝒞]
[CategoryTheory.Preadditive 𝒞]
[CategoryTheory.Linear k 𝒞]
{ι : Type}
[Fintype ι]
[DecidableEq ι]
{F : ι → 𝒞}
{G : Type}
[Group G]
[DecidableEq G]
{D : HomGrading F G}
(hT : Thin.IsThin k (CovObj D))
{β : (o o' : CovObj D) → o ⟶ o'}
(hβ : Thin.MultBasis Set.univ β)
[IsFreeGroup G]
(hratio :
∀ (d : CovObj D → CovObj D → k),
Thin.IsWeight Set.univ d →
∃ (ζ : CovObj D → k), (∀ (o : CovObj D), ζ o ≠ 0) ∧ ∀ (o o' : CovObj D) (f : o ⟶ o'), f ≠ 0 → d o o' = ζ o' / ζ o)
(a : IsFreeGroup.Generators G)
:
Equiv.Perm (CovObj D × kˣ)
The permutation of objects × kˣ lifting a free generator:
(o, λ) ↦ (g o, a_g(o) λ).
Instances For
noncomputable def
MultiplicativeBasisDeformations.CatAlg.Ψd
{k : Type u}
[Field k]
{𝒞 : Type v}
[CategoryTheory.Category.{u, v} 𝒞]
[CategoryTheory.Preadditive 𝒞]
[CategoryTheory.Linear k 𝒞]
{ι : Type}
[Fintype ι]
[DecidableEq ι]
{F : ι → 𝒞}
{G : Type}
[Group G]
[DecidableEq G]
{D : HomGrading F G}
(hT : Thin.IsThin k (CovObj D))
{β : (o o' : CovObj D) → o ⟶ o'}
(hβ : Thin.MultBasis Set.univ β)
[IsFreeGroup G]
(hratio :
∀ (d : CovObj D → CovObj D → k),
Thin.IsWeight Set.univ d →
∃ (ζ : CovObj D → k), (∀ (o : CovObj D), ζ o ≠ 0) ∧ ∀ (o o' : CovObj D) (f : o ⟶ o'), f ≠ 0 → d o o' = ζ o' / ζ o)
:
G →* Equiv.Perm (CovObj D × kˣ)
The lift to the free group.
Instances For
def
MultiplicativeBasisDeformations.CatAlg.HasForm
{k : Type u}
[Field k]
{𝒞 : Type v}
[CategoryTheory.Category.{u, v} 𝒞]
[CategoryTheory.Preadditive 𝒞]
[CategoryTheory.Linear k 𝒞]
{ι : Type}
{F : ι → 𝒞}
{G : Type}
[Group G]
[DecidableEq G]
{D : HomGrading F G}
(σ : Equiv.Perm (CovObj D × kˣ))
(g : G)
:
The transports have the form (o, λ) ↦ (g o, c(o) λ).
Instances For
theorem
MultiplicativeBasisDeformations.CatAlg.hasForm_mul
{k : Type u}
[Field k]
{𝒞 : Type v}
[CategoryTheory.Category.{u, v} 𝒞]
[CategoryTheory.Preadditive 𝒞]
[CategoryTheory.Linear k 𝒞]
{ι : Type}
[Fintype ι]
[DecidableEq ι]
{F : ι → 𝒞}
{G : Type}
[Group G]
[DecidableEq G]
{D : HomGrading F G}
[IsFreeGroup G]
{σ τ : Equiv.Perm (CovObj D × kˣ)}
{g h : G}
(hσ : HasForm σ g)
(hτ : HasForm τ h)
:
HasForm (σ * τ) (g * h)
theorem
MultiplicativeBasisDeformations.CatAlg.hasForm_inv
{k : Type u}
[Field k]
{𝒞 : Type v}
[CategoryTheory.Category.{u, v} 𝒞]
[CategoryTheory.Preadditive 𝒞]
[CategoryTheory.Linear k 𝒞]
{ι : Type}
[Fintype ι]
[DecidableEq ι]
{F : ι → 𝒞}
{G : Type}
[Group G]
[DecidableEq G]
{D : HomGrading F G}
[IsFreeGroup G]
{σ : Equiv.Perm (CovObj D × kˣ)}
{g : G}
(hσ : HasForm σ g)
:
HasForm σ⁻¹ g⁻¹
theorem
MultiplicativeBasisDeformations.CatAlg.free_induction
{G : Type}
[Group G]
[DecidableEq G]
[IsFreeGroup G]
{P : G → Prop}
(h1 : P 1)
(hof : ∀ (a : IsFreeGroup.Generators G), P (IsFreeGroup.of a))
(hmul : ∀ (g h : G), P g → P h → P (g * h))
(hinv : ∀ (g : G), P g → P g⁻¹)
(g : G)
:
P g
Induction over a free group.
theorem
MultiplicativeBasisDeformations.CatAlg.Ψd_form
{k : Type u}
[Field k]
{𝒞 : Type v}
[CategoryTheory.Category.{u, v} 𝒞]
[CategoryTheory.Preadditive 𝒞]
[CategoryTheory.Linear k 𝒞]
{ι : Type}
[Fintype ι]
[DecidableEq ι]
{F : ι → 𝒞}
{G : Type}
[Group G]
[DecidableEq G]
{D : HomGrading F G}
(hT : Thin.IsThin k (CovObj D))
{β : (o o' : CovObj D) → o ⟶ o'}
(hβ : Thin.MultBasis Set.univ β)
[IsFreeGroup G]
(hratio :
∀ (d : CovObj D → CovObj D → k),
Thin.IsWeight Set.univ d →
∃ (ζ : CovObj D → k), (∀ (o : CovObj D), ζ o ≠ 0) ∧ ∀ (o o' : CovObj D) (f : o ⟶ o'), f ≠ 0 → d o o' = ζ o' / ζ o)
(g : G)
:
def
MultiplicativeBasisDeformations.CatAlg.root
{k : Type u}
[Field k]
{𝒞 : Type v}
[CategoryTheory.Category.{u, v} 𝒞]
[CategoryTheory.Preadditive 𝒞]
[CategoryTheory.Linear k 𝒞]
{ι : Type}
{F : ι → 𝒞}
{G : Type}
[Group G]
[DecidableEq G]
{D : HomGrading F G}
(o : CovObj D)
:
CovObj D
The root of the orbit of o.
Instances For
theorem
MultiplicativeBasisDeformations.CatAlg.tr_root
{k : Type u}
[Field k]
{𝒞 : Type v}
[CategoryTheory.Category.{u, v} 𝒞]
[CategoryTheory.Preadditive 𝒞]
[CategoryTheory.Linear k 𝒞]
{ι : Type}
[Fintype ι]
[DecidableEq ι]
{F : ι → 𝒞}
{G : Type}
[Group G]
[DecidableEq G]
{D : HomGrading F G}
[IsFreeGroup G]
(o : CovObj D)
:
noncomputable def
MultiplicativeBasisDeformations.CatAlg.fv
{k : Type u}
[Field k]
{𝒞 : Type v}
[CategoryTheory.Category.{u, v} 𝒞]
[CategoryTheory.Preadditive 𝒞]
[CategoryTheory.Linear k 𝒞]
{ι : Type}
[Fintype ι]
[DecidableEq ι]
{F : ι → 𝒞}
{G : Type}
[Group G]
[DecidableEq G]
{D : HomGrading F G}
(hT : Thin.IsThin k (CovObj D))
{β : (o o' : CovObj D) → o ⟶ o'}
(hβ : Thin.MultBasis Set.univ β)
[IsFreeGroup G]
(hratio :
∀ (d : CovObj D → CovObj D → k),
Thin.IsWeight Set.univ d →
∃ (ζ : CovObj D → k), (∀ (o : CovObj D), ζ o ≠ 0) ∧ ∀ (o o' : CovObj D) (f : o ⟶ o'), f ≠ 0 → d o o' = ζ o' / ζ o)
(o : CovObj D)
:
kˣ
The object values f: the transport of (root, 1).
Instances For
theorem
MultiplicativeBasisDeformations.CatAlg.Ψd_root
{k : Type u}
[Field k]
{𝒞 : Type v}
[CategoryTheory.Category.{u, v} 𝒞]
[CategoryTheory.Preadditive 𝒞]
[CategoryTheory.Linear k 𝒞]
{ι : Type}
[Fintype ι]
[DecidableEq ι]
{F : ι → 𝒞}
{G : Type}
[Group G]
[DecidableEq G]
{D : HomGrading F G}
(hT : Thin.IsThin k (CovObj D))
{β : (o o' : CovObj D) → o ⟶ o'}
(hβ : Thin.MultBasis Set.univ β)
[IsFreeGroup G]
(hratio :
∀ (d : CovObj D → CovObj D → k),
Thin.IsWeight Set.univ d →
∃ (ζ : CovObj D → k), (∀ (o : CovObj D), ζ o ≠ 0) ∧ ∀ (o o' : CovObj D) (f : o ⟶ o'), f ≠ 0 → d o o' = ζ o' / ζ o)
(o : CovObj D)
:
theorem
MultiplicativeBasisDeformations.CatAlg.fv_tr
{k : Type u}
[Field k]
{𝒞 : Type v}
[CategoryTheory.Category.{u, v} 𝒞]
[CategoryTheory.Preadditive 𝒞]
[CategoryTheory.Linear k 𝒞]
{ι : Type}
[Fintype ι]
[DecidableEq ι]
{F : ι → 𝒞}
{G : Type}
[Group G]
[DecidableEq G]
{D : HomGrading F G}
(hT : Thin.IsThin k (CovObj D))
{β : (o o' : CovObj D) → o ⟶ o'}
(hβ : Thin.MultBasis Set.univ β)
[IsFreeGroup G]
(hratio :
∀ (d : CovObj D → CovObj D → k),
Thin.IsWeight Set.univ d →
∃ (ζ : CovObj D → k), (∀ (o : CovObj D), ζ o ≠ 0) ∧ ∀ (o o' : CovObj D) (f : o ⟶ o'), f ≠ 0 → d o o' = ζ o' / ζ o)
(a : IsFreeGroup.Generators G)
(o : CovObj D)
:
f(g x) = a_g(x) f(x) for the free generators.
The invariant basis #
noncomputable def
MultiplicativeBasisDeformations.CatAlg.bInv
{k : Type u}
[Field k]
{𝒞 : Type v}
[CategoryTheory.Category.{u, v} 𝒞]
[CategoryTheory.Preadditive 𝒞]
[CategoryTheory.Linear k 𝒞]
{ι : Type}
[Fintype ι]
[DecidableEq ι]
{F : ι → 𝒞}
{G : Type}
[Group G]
[DecidableEq G]
{D : HomGrading F G}
(hT : Thin.IsThin k (CovObj D))
{β : (o o' : CovObj D) → o ⟶ o'}
(hβ : Thin.MultBasis Set.univ β)
[IsFreeGroup G]
(hratio :
∀ (d : CovObj D → CovObj D → k),
Thin.IsWeight Set.univ d →
∃ (ζ : CovObj D → k), (∀ (o : CovObj D), ζ o ≠ 0) ∧ ∀ (o o' : CovObj D) (f : o ⟶ o'), f ≠ 0 → d o o' = ζ o' / ζ o)
(o o' : CovObj D)
:
o ⟶ o'
b'_{xy} = (f(y)/f(x)) b_{xy}.
Instances For
def
MultiplicativeBasisDeformations.CatAlg.pt
{k : Type u}
[Field k]
{𝒞 : Type v}
[CategoryTheory.Category.{u, v} 𝒞]
[CategoryTheory.Preadditive 𝒞]
[CategoryTheory.Linear k 𝒞]
{ι : Type}
{F : ι → 𝒞}
{G : Type}
[Group G]
[DecidableEq G]
{D : HomGrading F G}
(x : ι)
(g : G)
:
CovObj D
The object (x, g) of the cover.
Instances For
@[simp]
theorem
MultiplicativeBasisDeformations.CatAlg.pt_fst
{k : Type u}
[Field k]
{𝒞 : Type v}
[CategoryTheory.Category.{u, v} 𝒞]
[CategoryTheory.Preadditive 𝒞]
[CategoryTheory.Linear k 𝒞]
{ι : Type}
[Fintype ι]
[DecidableEq ι]
{F : ι → 𝒞}
{G : Type}
[Group G]
[DecidableEq G]
{D : HomGrading F G}
[IsFreeGroup G]
(x : ι)
(g : G)
:
(pt x g).1 = x
@[simp]
theorem
MultiplicativeBasisDeformations.CatAlg.pt_snd
{k : Type u}
[Field k]
{𝒞 : Type v}
[CategoryTheory.Category.{u, v} 𝒞]
[CategoryTheory.Preadditive 𝒞]
[CategoryTheory.Linear k 𝒞]
{ι : Type}
[Fintype ι]
[DecidableEq ι]
{F : ι → 𝒞}
{G : Type}
[Group G]
[DecidableEq G]
{D : HomGrading F G}
[IsFreeGroup G]
(x : ι)
(g : G)
:
(pt x g).2 = g
theorem
MultiplicativeBasisDeformations.CatAlg.bInv_sheet
{k : Type u}
[Field k]
{𝒞 : Type v}
[CategoryTheory.Category.{u, v} 𝒞]
[CategoryTheory.Preadditive 𝒞]
[CategoryTheory.Linear k 𝒞]
{ι : Type}
[Fintype ι]
[DecidableEq ι]
{F : ι → 𝒞}
{G : Type}
[Group G]
[DecidableEq G]
{D : HomGrading F G}
(hT : Thin.IsThin k (CovObj D))
{β : (o o' : CovObj D) → o ⟶ o'}
(hβ : Thin.MultBasis Set.univ β)
[IsFreeGroup G]
(hratio :
∀ (d : CovObj D → CovObj D → k),
Thin.IsWeight Set.univ d →
∃ (ζ : CovObj D → k), (∀ (o : CovObj D), ζ o ≠ 0) ∧ ∀ (o o' : CovObj D) (f : o ⟶ o'), f ≠ 0 → d o o' = ζ o' / ζ o)
{x y : ι}
{g g' h h' : G}
(hg : g = g')
(hh : h = h')
:
theorem
MultiplicativeBasisDeformations.CatAlg.bInv_mul
{k : Type u}
[Field k]
{𝒞 : Type v}
[CategoryTheory.Category.{u, v} 𝒞]
[CategoryTheory.Preadditive 𝒞]
[CategoryTheory.Linear k 𝒞]
{ι : Type}
[Fintype ι]
[DecidableEq ι]
{F : ι → 𝒞}
{G : Type}
[Group G]
[DecidableEq G]
{D : HomGrading F G}
(hT : Thin.IsThin k (CovObj D))
{β : (o o' : CovObj D) → o ⟶ o'}
(hβ : Thin.MultBasis Set.univ β)
[IsFreeGroup G]
(hratio :
∀ (d : CovObj D → CovObj D → k),
Thin.IsWeight Set.univ d →
∃ (ζ : CovObj D → k), (∀ (o : CovObj D), ζ o ≠ 0) ∧ ∀ (o o' : CovObj D) (f : o ⟶ o'), f ≠ 0 → d o o' = ζ o' / ζ o)
(o o' o'' : CovObj D)
:
b' is still multiplicative.
theorem
MultiplicativeBasisDeformations.CatAlg.bInv_id
{k : Type u}
[Field k]
{𝒞 : Type v}
[CategoryTheory.Category.{u, v} 𝒞]
[CategoryTheory.Preadditive 𝒞]
[CategoryTheory.Linear k 𝒞]
{ι : Type}
[Fintype ι]
[DecidableEq ι]
{F : ι → 𝒞}
{G : Type}
[Group G]
[DecidableEq G]
{D : HomGrading F G}
(hT : Thin.IsThin k (CovObj D))
{β : (o o' : CovObj D) → o ⟶ o'}
(hβ : Thin.MultBasis Set.univ β)
[IsFreeGroup G]
(hratio :
∀ (d : CovObj D → CovObj D → k),
Thin.IsWeight Set.univ d →
∃ (ζ : CovObj D → k), (∀ (o : CovObj D), ζ o ≠ 0) ∧ ∀ (o o' : CovObj D) (f : o ⟶ o'), f ≠ 0 → d o o' = ζ o' / ζ o)
(o : CovObj D)
:
bInv hT hβ hratio o o = CategoryTheory.CategoryStruct.id o
theorem
MultiplicativeBasisDeformations.CatAlg.bInv_ne_zero
{k : Type u}
[Field k]
{𝒞 : Type v}
[CategoryTheory.Category.{u, v} 𝒞]
[CategoryTheory.Preadditive 𝒞]
[CategoryTheory.Linear k 𝒞]
{ι : Type}
[Fintype ι]
[DecidableEq ι]
{F : ι → 𝒞}
{G : Type}
[Group G]
[DecidableEq G]
{D : HomGrading F G}
(hT : Thin.IsThin k (CovObj D))
{β : (o o' : CovObj D) → o ⟶ o'}
(hβ : Thin.MultBasis Set.univ β)
[IsFreeGroup G]
(hratio :
∀ (d : CovObj D → CovObj D → k),
Thin.IsWeight Set.univ d →
∃ (ζ : CovObj D → k), (∀ (o : CovObj D), ζ o ≠ 0) ∧ ∀ (o o' : CovObj D) (f : o ⟶ o'), f ≠ 0 → d o o' = ζ o' / ζ o)
{o o' : CovObj D}
(h : β o o' ≠ 0)
:
bInv hT hβ hratio o o' ≠ 0
theorem
MultiplicativeBasisDeformations.CatAlg.bInv_tr_of
{k : Type u}
[Field k]
{𝒞 : Type v}
[CategoryTheory.Category.{u, v} 𝒞]
[CategoryTheory.Preadditive 𝒞]
[CategoryTheory.Linear k 𝒞]
{ι : Type}
[Fintype ι]
[DecidableEq ι]
{F : ι → 𝒞}
{G : Type}
[Group G]
[DecidableEq G]
{D : HomGrading F G}
(hT : Thin.IsThin k (CovObj D))
{β : (o o' : CovObj D) → o ⟶ o'}
(hβ : Thin.MultBasis Set.univ β)
[IsFreeGroup G]
(hratio :
∀ (d : CovObj D → CovObj D → k),
Thin.IsWeight Set.univ d →
∃ (ζ : CovObj D → k), (∀ (o : CovObj D), ζ o ≠ 0) ∧ ∀ (o o' : CovObj D) (f : o ⟶ o'), f ≠ 0 → d o o' = ζ o' / ζ o)
(a : IsFreeGroup.Generators G)
(o o' : CovObj D)
:
b' is invariant under the free generators.
theorem
MultiplicativeBasisDeformations.CatAlg.bInv_tr
{k : Type u}
[Field k]
{𝒞 : Type v}
[CategoryTheory.Category.{u, v} 𝒞]
[CategoryTheory.Preadditive 𝒞]
[CategoryTheory.Linear k 𝒞]
{ι : Type}
[Fintype ι]
[DecidableEq ι]
{F : ι → 𝒞}
{G : Type}
[Group G]
[DecidableEq G]
{D : HomGrading F G}
(hT : Thin.IsThin k (CovObj D))
{β : (o o' : CovObj D) → o ⟶ o'}
(hβ : Thin.MultBasis Set.univ β)
[IsFreeGroup G]
(hratio :
∀ (d : CovObj D → CovObj D → k),
Thin.IsWeight Set.univ d →
∃ (ζ : CovObj D → k), (∀ (o : CovObj D), ζ o ≠ 0) ∧ ∀ (o o' : CovObj D) (f : o ⟶ o'), f ≠ 0 → d o o' = ζ o' / ζ o)
(g : G)
(o o' : CovObj D)
:
b' is deck invariant.
Descent #
noncomputable def
MultiplicativeBasisDeformations.CatAlg.bD
{k : Type u}
[Field k]
{𝒞 : Type v}
[CategoryTheory.Category.{u, v} 𝒞]
[CategoryTheory.Preadditive 𝒞]
[CategoryTheory.Linear k 𝒞]
{ι : Type}
[Fintype ι]
[DecidableEq ι]
{F : ι → 𝒞}
{G : Type}
[Group G]
[DecidableEq G]
{D : HomGrading F G}
(hT : Thin.IsThin k (CovObj D))
{β : (o o' : CovObj D) → o ⟶ o'}
(hβ : Thin.MultBasis Set.univ β)
[IsFreeGroup G]
(hratio :
∀ (d : CovObj D → CovObj D → k),
Thin.IsWeight Set.univ d →
∃ (ζ : CovObj D → k), (∀ (o : CovObj D), ζ o ≠ 0) ∧ ∀ (o o' : CovObj D) (f : o ⟶ o'), f ≠ 0 → d o o' = ζ o' / ζ o)
(x y : ι)
(g : G)
:
F x ⟶ F y
The descended vectors: b(x, y, g) = b'_{(x,1),(y,g)}.
Instances For
theorem
MultiplicativeBasisDeformations.CatAlg.bD_mem
{k : Type u}
[Field k]
{𝒞 : Type v}
[CategoryTheory.Category.{u, v} 𝒞]
[CategoryTheory.Preadditive 𝒞]
[CategoryTheory.Linear k 𝒞]
{ι : Type}
[Fintype ι]
[DecidableEq ι]
{F : ι → 𝒞}
{G : Type}
[Group G]
[DecidableEq G]
{D : HomGrading F G}
(hT : Thin.IsThin k (CovObj D))
{β : (o o' : CovObj D) → o ⟶ o'}
(hβ : Thin.MultBasis Set.univ β)
[IsFreeGroup G]
(hratio :
∀ (d : CovObj D → CovObj D → k),
Thin.IsWeight Set.univ d →
∃ (ζ : CovObj D → k), (∀ (o : CovObj D), ζ o ≠ 0) ∧ ∀ (o o' : CovObj D) (f : o ⟶ o'), f ≠ 0 → d o o' = ζ o' / ζ o)
(x y : ι)
(g : G)
:
theorem
MultiplicativeBasisDeformations.CatAlg.bD_ne_zero
{k : Type u}
[Field k]
{𝒞 : Type v}
[CategoryTheory.Category.{u, v} 𝒞]
[CategoryTheory.Preadditive 𝒞]
[CategoryTheory.Linear k 𝒞]
{ι : Type}
[Fintype ι]
[DecidableEq ι]
{F : ι → 𝒞}
{G : Type}
[Group G]
[DecidableEq G]
{D : HomGrading F G}
(hT : Thin.IsThin k (CovObj D))
{β : (o o' : CovObj D) → o ⟶ o'}
(hβ : Thin.MultBasis Set.univ β)
[IsFreeGroup G]
(hratio :
∀ (d : CovObj D → CovObj D → k),
Thin.IsWeight Set.univ d →
∃ (ζ : CovObj D → k), (∀ (o : CovObj D), ζ o ≠ 0) ∧ ∀ (o o' : CovObj D) (f : o ⟶ o'), f ≠ 0 → d o o' = ζ o' / ζ o)
{x y : ι}
{g : G}
(h : D.part g x y ≠ ⊥)
:
bD hT hβ hratio x y g ≠ 0
theorem
MultiplicativeBasisDeformations.CatAlg.bD_span
{k : Type u}
[Field k]
{𝒞 : Type v}
[CategoryTheory.Category.{u, v} 𝒞]
[CategoryTheory.Preadditive 𝒞]
[CategoryTheory.Linear k 𝒞]
{ι : Type}
[Fintype ι]
[DecidableEq ι]
{F : ι → 𝒞}
{G : Type}
[Group G]
[DecidableEq G]
{D : HomGrading F G}
(hT : Thin.IsThin k (CovObj D))
{β : (o o' : CovObj D) → o ⟶ o'}
(hβ : Thin.MultBasis Set.univ β)
[IsFreeGroup G]
(hratio :
∀ (d : CovObj D → CovObj D → k),
Thin.IsWeight Set.univ d →
∃ (ζ : CovObj D → k), (∀ (o : CovObj D), ζ o ≠ 0) ∧ ∀ (o o' : CovObj D) (f : o ⟶ o'), f ≠ 0 → d o o' = ζ o' / ζ o)
{x y : ι}
{g : G}
{f : F x ⟶ F y}
(hf : f ∈ D.part g x y)
:
∃ (c : k), f = c • bD hT hβ hratio x y g
theorem
MultiplicativeBasisDeformations.CatAlg.bD_id
{k : Type u}
[Field k]
{𝒞 : Type v}
[CategoryTheory.Category.{u, v} 𝒞]
[CategoryTheory.Preadditive 𝒞]
[CategoryTheory.Linear k 𝒞]
{ι : Type}
[Fintype ι]
[DecidableEq ι]
{F : ι → 𝒞}
{G : Type}
[Group G]
[DecidableEq G]
{D : HomGrading F G}
(hT : Thin.IsThin k (CovObj D))
{β : (o o' : CovObj D) → o ⟶ o'}
(hβ : Thin.MultBasis Set.univ β)
[IsFreeGroup G]
(hratio :
∀ (d : CovObj D → CovObj D → k),
Thin.IsWeight Set.univ d →
∃ (ζ : CovObj D → k), (∀ (o : CovObj D), ζ o ≠ 0) ∧ ∀ (o o' : CovObj D) (f : o ⟶ o'), f ≠ 0 → d o o' = ζ o' / ζ o)
(x : ι)
:
bD hT hβ hratio x x 1 = CategoryTheory.CategoryStruct.id (F x)
theorem
MultiplicativeBasisDeformations.CatAlg.bD_mul
{k : Type u}
[Field k]
{𝒞 : Type v}
[CategoryTheory.Category.{u, v} 𝒞]
[CategoryTheory.Preadditive 𝒞]
[CategoryTheory.Linear k 𝒞]
{ι : Type}
[Fintype ι]
[DecidableEq ι]
{F : ι → 𝒞}
{G : Type}
[Group G]
[DecidableEq G]
{D : HomGrading F G}
(hT : Thin.IsThin k (CovObj D))
{β : (o o' : CovObj D) → o ⟶ o'}
(hβ : Thin.MultBasis Set.univ β)
[IsFreeGroup G]
(hratio :
∀ (d : CovObj D → CovObj D → k),
Thin.IsWeight Set.univ d →
∃ (ζ : CovObj D → k), (∀ (o : CovObj D), ζ o ≠ 0) ∧ ∀ (o o' : CovObj D) (f : o ⟶ o'), f ≠ 0 → d o o' = ζ o' / ζ o)
(x y z : ι)
(g h : G)
:
The descended vectors are multiplicative.