The automorphism Φ of the cover induced by a weight #
Lemma 4.13 (lem:scalar-object-values, scalar-normalization.tex):
"Every scalar automorphism consequently fixes each V_X̃ up to isomorphism.
Choose such isomorphisms, using the natural ones on projectives, in the
direction for which the following automorphism agrees with the given scalar
automorphism on the lifted projectives. Full faithfulness in Lemma 4.8 turns
them into an object-fixing automorphism Φ of C̃."
For a weight d on L, each lifted object X̃ gets a d-scaled
automorphism of V_X̃ (ScAut): the natural one m ↦ d(z, x̃) m on a lifted
projective x̃ (natAut), and on the other objects the components of an
isomorphism V_X̃^{σ_d} ≅ V_X̃ over a finite covering algebra containing the
support (exists_twistAut, from weight_twist_iso). Conjugating composition
with f : X̃ → Ỹ by these gives a natural family, hence by Lemma 4.8 a morphism
Φ f (Φ). Φ is linear, multiplicative, injective, and multiplies a
morphism z₁ → z₂ of L by d(z₁, z₂) (Φ_proj).
Semilinear maps of V_X̃ #
theorem
MultiplicativeBasisDeformations.CatAlg.MeshData.op_smul_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]
{L : LocalFamily F}
{D : MeshData F L}
{Dg : HomGrading F G}
{T : Finset (D.PV × G)}
{X : ι × G}
(c : k)
(b : ↥(D.covT Dg T))
(y : D.VX Dg T X)
:
MulOpposite.op (c • b) • y = c • MulOpposite.op b • y
theorem
MultiplicativeBasisDeformations.CatAlg.MeshData.scale_unitE
{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]
{L : LocalFamily F}
{D : MeshData F L}
{Dg : HomGrading F G}
{T : Finset (D.PV × G)}
(d : D.PV × G → D.PV × G → k)
(q' q : ↥T)
(u : F ↑(↑q').1 ⟶ F ↑(↑q).1)
(hu : Dg.IsHom ((↑q').2⁻¹ * (↑q).2) u)
:
def
MultiplicativeBasisDeformations.CatAlg.MeshData.semiK
{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]
{L : LocalFamily F}
{D : MeshData F L}
{Dg : HomGrading F G}
{T : Finset (D.PV × G)}
{X : ι × G}
(σ : ↥(D.covT Dg T) ≃ₐ[k] ↥(D.covT Dg T))
(f : D.VX Dg T X →+ D.VX Dg T X)
(hf : ∀ (b : (↥(D.covT Dg T))ᵐᵒᵖ) (y : D.VX Dg T X), f (b • y) = MulOpposite.op (σ (MulOpposite.unop b)) • f y)
:
A map semilinear for an automorphism, as a k-linear map.
Instances For
theorem
MultiplicativeBasisDeformations.CatAlg.MeshData.semiK_isScaled
{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]
{L : LocalFamily F}
{D : MeshData F L}
{Dg : HomGrading F G}
{T : Finset (D.PV × G)}
{X : ι × G}
(σ : ↥(D.covT Dg T) ≃ₐ[k] ↥(D.covT Dg T))
(f : D.VX Dg T X →+ D.VX Dg T X)
(hf : ∀ (b : (↥(D.covT Dg T))ᵐᵒᵖ) (y : D.VX Dg T X), f (b • y) = MulOpposite.op (σ (MulOpposite.unop b)) • f y)
(c : D.PV × G → D.PV × G → k)
(hσ :
∀ (q' q : ↥T) (u : F ↑(↑q').1 ⟶ F ↑(↑q).1) (hu : Dg.IsHom ((↑q').2⁻¹ * (↑q).2) u),
σ (unitE T q' q u hu) = c ↑q' ↑q • unitE T q' q u hu)
:
Scaled automorphisms of V_X̃ #
structure
MultiplicativeBasisDeformations.CatAlg.MeshData.ScAut
{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]
{L : LocalFamily F}
(D : MeshData F L)
(Dg : HomGrading F G)
(d : D.PV × G → D.PV × G → k)
(X : ι × G)
:
Type u
A d-scaled automorphism of V_X̃.
- ψ : ScFam d X X
Instances For
theorem
MultiplicativeBasisDeformations.CatAlg.MeshData.weight_mul_of_ne
{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]
{L : LocalFamily F}
{D : MeshData F L}
{Dg : HomGrading F G}
{d : D.PV × G → D.PV × G → k}
(hd : Thin.IsWeight Set.univ d)
{z' z x : D.PV × G}
{u : F ↑z'.1 ⟶ F ↑z.1}
{m : F ↑z.1 ⟶ F ↑x.1}
(hu : u ∈ Dg.part (z'.2⁻¹ * z.2) ↑z'.1 ↑z.1)
(hm : m ∈ Dg.part (z.2⁻¹ * x.2) ↑z.1 ↑x.1)
(h : CategoryTheory.CategoryStruct.comp u m ≠ 0)
:
d z' x = d z' z * d z x
theorem
MultiplicativeBasisDeformations.CatAlg.MeshData.weight_ne_of_ne
{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]
{L : LocalFamily F}
{D : MeshData F L}
{Dg : HomGrading F G}
{d : D.PV × G → D.PV × G → k}
(hd : Thin.IsWeight Set.univ d)
{z x : D.PV × G}
{m : F ↑z.1 ⟶ F ↑x.1}
(hm : m ∈ Dg.part (z.2⁻¹ * x.2) ↑z.1 ↑x.1)
(h : m ≠ 0)
:
d z x ≠ 0
def
MultiplicativeBasisDeformations.CatAlg.MeshData.natFam
{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]
{L : LocalFamily F}
{D : MeshData F L}
{Dg : HomGrading F G}
(c : D.PV × G → D.PV × G → k)
(x₀ : D.PV × G)
(hc :
∀ (z' z : D.PV × G) (u : F ↑z'.1 ⟶ F ↑z.1) (m : F ↑z.1 ⟶ F ↑x₀.1),
u ∈ Dg.part (z'.2⁻¹ * z.2) ↑z'.1 ↑z.1 →
m ∈ Dg.part (z.2⁻¹ * x₀.2) ↑z.1 ↑x₀.1 → CategoryTheory.CategoryStruct.comp u m ≠ 0 → c z' x₀ = c z' z * c z x₀)
:
ScFam c (↑x₀.1, x₀.2) (↑x₀.1, x₀.2)
The natural scaled family on a lifted projective: m ↦ c(z, x₀) m.
Instances For
def
MultiplicativeBasisDeformations.CatAlg.MeshData.natAut
{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]
{L : LocalFamily F}
{D : MeshData F L}
{Dg : HomGrading F G}
{d : D.PV × G → D.PV × G → k}
(hd : Thin.IsWeight Set.univ d)
(x₀ : D.PV × G)
:
D.ScAut Dg d (↑x₀.1, x₀.2)
The natural automorphism of V_x̃ for a lifted projective x̃.
Instances For
Twisted automorphisms #
noncomputable def
MultiplicativeBasisDeformations.CatAlg.MeshData.suppT
{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]
{L : LocalFamily F}
(D : MeshData F L)
(Dg : HomGrading F G)
[hfd : ∀ (x y : ι), FiniteDimensional k (F x ⟶ F y)]
(X : ι × G)
:
Finset (D.PV × G)
A finite set of lifted projectives containing the support of V_X̃.
Instances For
theorem
MultiplicativeBasisDeformations.CatAlg.MeshData.supp_suppT
{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]
{L : LocalFamily F}
{D : MeshData F L}
{Dg : HomGrading F G}
[hfd : ∀ (x y : ι), FiniteDimensional k (F x ⟶ F y)]
(X : ι × G)
:
theorem
MultiplicativeBasisDeformations.CatAlg.MeshData.id_ne_zero
{k : Type u}
[Field k]
{𝒞 : Type v}
[CategoryTheory.Category.{u, v} 𝒞]
[CategoryTheory.Preadditive 𝒞]
[CategoryTheory.Linear k 𝒞]
{ι : Type}
[Fintype ι]
[DecidableEq ι]
{F : ι → 𝒞}
{L : LocalFamily F}
[hfd : ∀ (x y : ι), FiniteDimensional k (F x ⟶ F y)]
(X : ι)
:
CategoryTheory.CategoryStruct.id (F X) ≠ 0
instance
MultiplicativeBasisDeformations.CatAlg.MeshData.instFiniteDimensionalHomF0
{k : Type u}
[Field k]
{𝒞 : Type v}
[CategoryTheory.Category.{u, v} 𝒞]
[CategoryTheory.Preadditive 𝒞]
[CategoryTheory.Linear k 𝒞]
{ι : Type}
[Fintype ι]
[DecidableEq ι]
{F : ι → 𝒞}
{L : LocalFamily F}
{D : MeshData F L}
[hfd : ∀ (x y : ι), FiniteDimensional k (F x ⟶ F y)]
(x y : D.PV)
:
theorem
MultiplicativeBasisDeformations.CatAlg.MeshData.exists_twistAut
{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]
{L : LocalFamily F}
{D : MeshData F L}
{Dg : HomGrading F G}
{d : D.PV × G → D.PV × G → k}
(hd : Thin.IsWeight Set.univ d)
[hfd : ∀ (x y : ι), FiniteDimensional k (F x ⟶ F y)]
[IsAlgClosed k]
[Infinite k]
(H : HeightData Dg)
(hF : IsRepresentationFinite k (Alg D.F0)ᵐᵒᵖ)
(X : ι × G)
:
Nonempty (D.ScAut Dg d X)
A weight fixes V_X̃ up to isomorphism: a d-scaled automorphism from
an isomorphism V_X̃^{σ_d} ≅ V_X̃ over a finite covering algebra.
def
MultiplicativeBasisDeformations.CatAlg.MeshData.compFam
{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]
{L : LocalFamily F}
{D : MeshData F L}
{Dg : HomGrading F G}
{d : D.PV × G → D.PV × G → k}
(hd : Thin.IsWeight Set.univ d)
{X Y : ι × G}
(A : D.ScAut Dg d X)
(B : D.ScAut Dg d Y)
(f : F X.1 ⟶ F Y.1)
(hf : f ∈ Dg.part (X.2⁻¹ * Y.2) X.1 Y.1)
:
D.NatFam Dg X Y
Conjugating composition with f by scaled automorphisms gives a natural
family.
Instances For
theorem
MultiplicativeBasisDeformations.CatAlg.MeshData.compFam_exists
{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]
{L : LocalFamily F}
{D : MeshData F L}
{Dg : HomGrading F G}
{d : D.PV × G → D.PV × G → k}
(hd : Thin.IsWeight Set.univ d)
[hfd : ∀ (x y : ι), FiniteDimensional k (F x ⟶ F y)]
{X Y : ι × G}
(A : D.ScAut Dg d X)
(B : D.ScAut Dg d Y)
(f : F X.1 ⟶ F Y.1)
(hf : f ∈ Dg.part (X.2⁻¹ * Y.2) X.1 Y.1)
:
noncomputable def
MultiplicativeBasisDeformations.CatAlg.MeshData.aut
{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]
{L : LocalFamily F}
{D : MeshData F L}
{Dg : HomGrading F G}
{d : D.PV × G → D.PV × G → k}
(hd : Thin.IsWeight Set.univ d)
[hfd : ∀ (x y : ι), FiniteDimensional k (F x ⟶ F y)]
[IsAlgClosed k]
[Infinite k]
(H : HeightData Dg)
(hF : IsRepresentationFinite k (Alg D.F0)ᵐᵒᵖ)
(X : ι × G)
:
D.ScAut Dg d X
The chosen automorphisms: natural on the lifted projectives.
Instances For
theorem
MultiplicativeBasisDeformations.CatAlg.MeshData.aut_proj
{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]
{L : LocalFamily F}
{D : MeshData F L}
{Dg : HomGrading F G}
{d : D.PV × G → D.PV × G → k}
(hd : Thin.IsWeight Set.univ d)
[hfd : ∀ (x y : ι), FiniteDimensional k (F x ⟶ F y)]
[IsAlgClosed k]
[Infinite k]
(H : HeightData Dg)
(hF : IsRepresentationFinite k (Alg D.F0)ᵐᵒᵖ)
(x : D.PV × G)
:
noncomputable def
MultiplicativeBasisDeformations.CatAlg.MeshData.Φ
{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]
{L : LocalFamily F}
{D : MeshData F L}
{Dg : HomGrading F G}
{d : D.PV × G → D.PV × G → k}
(hd : Thin.IsWeight Set.univ d)
[hfd : ∀ (x y : ι), FiniteDimensional k (F x ⟶ F y)]
{X Y : ι × G}
[IsAlgClosed k]
[Infinite k]
(H : HeightData Dg)
(hF : IsRepresentationFinite k (Alg D.F0)ᵐᵒᵖ)
(f : F X.1 ⟶ F Y.1)
(hf : f ∈ Dg.part (X.2⁻¹ * Y.2) X.1 Y.1)
:
F X.1 ⟶ F Y.1
The automorphism Φ of C̃ on a morphism f : X̃ → Ỹ.
Instances For
theorem
MultiplicativeBasisDeformations.CatAlg.MeshData.Φ_isHom
{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]
{L : LocalFamily F}
{D : MeshData F L}
{Dg : HomGrading F G}
{d : D.PV × G → D.PV × G → k}
(hd : Thin.IsWeight Set.univ d)
[hfd : ∀ (x y : ι), FiniteDimensional k (F x ⟶ F y)]
{X Y : ι × G}
[IsAlgClosed k]
[Infinite k]
(H : HeightData Dg)
(hF : IsRepresentationFinite k (Alg D.F0)ᵐᵒᵖ)
(f : F X.1 ⟶ F Y.1)
(hf : f ∈ Dg.part (X.2⁻¹ * Y.2) X.1 Y.1)
:
theorem
MultiplicativeBasisDeformations.CatAlg.MeshData.Φ_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]
{L : LocalFamily F}
{D : MeshData F L}
{Dg : HomGrading F G}
{d : D.PV × G → D.PV × G → k}
(hd : Thin.IsWeight Set.univ d)
[hfd : ∀ (x y : ι), FiniteDimensional k (F x ⟶ F y)]
{X Y : ι × G}
[IsAlgClosed k]
[Infinite k]
(H : HeightData Dg)
(hF : IsRepresentationFinite k (Alg D.F0)ᵐᵒᵖ)
(f : F X.1 ⟶ F Y.1)
(hf : f ∈ Dg.part (X.2⁻¹ * Y.2) X.1 Y.1)
:
theorem
MultiplicativeBasisDeformations.CatAlg.MeshData.Φ_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]
{L : LocalFamily F}
{D : MeshData F L}
{Dg : HomGrading F G}
{d : D.PV × G → D.PV × G → k}
(hd : Thin.IsWeight Set.univ d)
[hfd : ∀ (x y : ι), FiniteDimensional k (F x ⟶ F y)]
{X Y : ι × G}
[IsAlgClosed k]
[Infinite k]
(H : HeightData Dg)
(hF : IsRepresentationFinite k (Alg D.F0)ᵐᵒᵖ)
(f : F X.1 ⟶ F Y.1)
(hf : f ∈ Dg.part (X.2⁻¹ * Y.2) X.1 Y.1)
(z : D.PV × G)
(m : F ↑z.1 ⟶ F X.1)
(hm : m ∈ Dg.part (z.2⁻¹ * X.2) (↑z.1) X.1)
:
theorem
MultiplicativeBasisDeformations.CatAlg.MeshData.Φ_unique
{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]
{L : LocalFamily F}
{D : MeshData F L}
{Dg : HomGrading F G}
{d : D.PV × G → D.PV × G → k}
(hd : Thin.IsWeight Set.univ d)
[hfd : ∀ (x y : ι), FiniteDimensional k (F x ⟶ F y)]
{X Y : ι × G}
[IsAlgClosed k]
[Infinite k]
(H : HeightData Dg)
(hF : IsRepresentationFinite k (Alg D.F0)ᵐᵒᵖ)
(f : F X.1 ⟶ F Y.1)
(hf : f ∈ Dg.part (X.2⁻¹ * Y.2) X.1 Y.1)
(g : F X.1 ⟶ F Y.1)
(hg :
∀ (z : D.PV × G),
∀ m ∈ Dg.part (z.2⁻¹ * X.2) (↑z.1) X.1,
((aut hd H hF Y).ψ.φ z) (CategoryTheory.CategoryStruct.comp (((aut hd H hF X).ψ'.φ z) m) f) = CategoryTheory.CategoryStruct.comp m g)
:
Φ hd H hF f hf = g
Uniqueness: Φ f is the only morphism with the defining property.
theorem
MultiplicativeBasisDeformations.CatAlg.MeshData.comp_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]
{Dg : HomGrading F G}
[IsAlgClosed k]
[Infinite k]
{x y z : ι}
{a b c : G}
{f : F x ⟶ F y}
{g : F y ⟶ F z}
(hf : f ∈ Dg.part (a⁻¹ * b) x y)
(hg : g ∈ Dg.part (b⁻¹ * c) y z)
:
CategoryTheory.CategoryStruct.comp f g ∈ Dg.part (a⁻¹ * c) x z
theorem
MultiplicativeBasisDeformations.CatAlg.MeshData.Φ_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]
{L : LocalFamily F}
{D : MeshData F L}
{Dg : HomGrading F G}
{d : D.PV × G → D.PV × G → k}
(hd : Thin.IsWeight Set.univ d)
[hfd : ∀ (x y : ι), FiniteDimensional k (F x ⟶ F y)]
{X Y Z : ι × G}
[IsAlgClosed k]
[Infinite k]
(H : HeightData Dg)
(hF : IsRepresentationFinite k (Alg D.F0)ᵐᵒᵖ)
(f : F X.1 ⟶ F Y.1)
(hf : f ∈ Dg.part (X.2⁻¹ * Y.2) X.1 Y.1)
(g : F Y.1 ⟶ F Z.1)
(hg : g ∈ Dg.part (Y.2⁻¹ * Z.2) Y.1 Z.1)
:
Φ is multiplicative.
theorem
MultiplicativeBasisDeformations.CatAlg.MeshData.Φ_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]
{L : LocalFamily F}
{D : MeshData F L}
{Dg : HomGrading F G}
{d : D.PV × G → D.PV × G → k}
(hd : Thin.IsWeight Set.univ d)
[hfd : ∀ (x y : ι), FiniteDimensional k (F x ⟶ F y)]
{X : ι × G}
[IsAlgClosed k]
[Infinite k]
(H : HeightData Dg)
(hF : IsRepresentationFinite k (Alg D.F0)ᵐᵒᵖ)
(h : CategoryTheory.CategoryStruct.id (F X.1) ∈ Dg.part (X.2⁻¹ * X.2) X.1 X.1)
:
Φ hd H hF (CategoryTheory.CategoryStruct.id (F X.1)) h = CategoryTheory.CategoryStruct.id (F X.1)
theorem
MultiplicativeBasisDeformations.CatAlg.MeshData.Φ_add
{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]
{L : LocalFamily F}
{D : MeshData F L}
{Dg : HomGrading F G}
{d : D.PV × G → D.PV × G → k}
(hd : Thin.IsWeight Set.univ d)
[hfd : ∀ (x y : ι), FiniteDimensional k (F x ⟶ F y)]
{X Y : ι × G}
[IsAlgClosed k]
[Infinite k]
(H : HeightData Dg)
(hF : IsRepresentationFinite k (Alg D.F0)ᵐᵒᵖ)
(f f' : F X.1 ⟶ F Y.1)
(hf : f ∈ Dg.part (X.2⁻¹ * Y.2) X.1 Y.1)
(hf' : f' ∈ Dg.part (X.2⁻¹ * Y.2) X.1 Y.1)
:
theorem
MultiplicativeBasisDeformations.CatAlg.MeshData.Φ_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]
{L : LocalFamily F}
{D : MeshData F L}
{Dg : HomGrading F G}
{d : D.PV × G → D.PV × G → k}
(hd : Thin.IsWeight Set.univ d)
[hfd : ∀ (x y : ι), FiniteDimensional k (F x ⟶ F y)]
{X Y : ι × G}
[IsAlgClosed k]
[Infinite k]
(H : HeightData Dg)
(hF : IsRepresentationFinite k (Alg D.F0)ᵐᵒᵖ)
(c : k)
(f : F X.1 ⟶ F Y.1)
(hf : f ∈ Dg.part (X.2⁻¹ * Y.2) X.1 Y.1)
:
theorem
MultiplicativeBasisDeformations.CatAlg.MeshData.eq_zero_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]
{L : LocalFamily F}
{D : MeshData F L}
{Dg : HomGrading F G}
{d : D.PV × G → D.PV × G → k}
(hd : Thin.IsWeight Set.univ d)
[hfd : ∀ (x y : ι), FiniteDimensional k (F x ⟶ F y)]
{X Y : ι × G}
[IsAlgClosed k]
[Infinite k]
(H : HeightData Dg)
(hF : IsRepresentationFinite k (Alg D.F0)ᵐᵒᵖ)
(f : F X.1 ⟶ F Y.1)
(hf : f ∈ Dg.part (X.2⁻¹ * Y.2) X.1 Y.1)
(h : Φ hd H hF f hf = 0)
:
f = 0
Φ is injective.
theorem
MultiplicativeBasisDeformations.CatAlg.MeshData.Φ_proj
{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]
{L : LocalFamily F}
{D : MeshData F L}
{Dg : HomGrading F G}
{d : D.PV × G → D.PV × G → k}
(hd : Thin.IsWeight Set.univ d)
[hfd : ∀ (x y : ι), FiniteDimensional k (F x ⟶ F y)]
[IsAlgClosed k]
[Infinite k]
(H : HeightData Dg)
(hF : IsRepresentationFinite k (Alg D.F0)ᵐᵒᵖ)
(x₁ x₂ : D.PV × G)
(f : F ↑x₁.1 ⟶ F ↑x₂.1)
(hf : f ∈ Dg.part (x₁.2⁻¹ * x₂.2) ↑x₁.1 ↑x₂.1)
:
Φ hd H hF f hf = d x₁ x₂ • f
Φ agrees with the scalar automorphism on L: it multiplies a morphism
x̃₁ → x̃₂ of lifted projectives by d(x̃₁, x̃₂).