Orbit Hom formulas under translate orthogonality #
Gabriel's orbit Hom formula expresses a downstairs Hom space as the direct sum of the Hom spaces from one lift to all translates of the other. If every nonidentity translated Hom vanishes, the direct sum has only its identity component. This file proves that the canonical map from the original Hom space is then a linear equivalence. It is the linear-algebraic mechanism by which separated covering windows make push-down fully faithful locally.
noncomputable def
MagnitudeConjecture.CoveringHom.identityLof
{k : Type u}
[Semiring k]
{G : Type v}
[Group G]
{H : G → Type w}
[(g : G) → AddCommMonoid (H g)]
[(g : G) → Module k (H g)]
:
H 1 →ₗ[k] DirectSum G fun (g : G) => H g
The inclusion of the identity-indexed summand, without exposing a
DecidableEq G parameter in later covering data.
Instances For
noncomputable def
MagnitudeConjecture.CoveringHom.uniqueComponentLinearEquiv
{k : Type u}
[Semiring k]
{I : Type v}
(M : I → Type w)
[(i : I) → AddCommMonoid (M i)]
[(i : I) → Module k (M i)]
(i₀ : I)
(orthogonal : ∀ (i : I), i ≠ i₀ → Subsingleton (M i))
:
M i₀ ≃ₗ[k] DirectSum I fun (i : I) => M i
A direct sum whose components away from i₀ are subsingletons is
linearly equivalent to its i₀-component.
Instances For
structure
MagnitudeConjecture.CoveringHom.OrbitHomDecomposition
{k : Type u}
[Semiring k]
{G : Type v}
[Group G]
{H : G → Type w}
[(g : G) → AddCommMonoid (H g)]
[(g : G) → Module k (H g)]
(Downstairs : Type w')
[AddCommMonoid Downstairs]
[Module k Downstairs]
:
Type (max (max v w) w')
The data of an orbit Hom formula together with its compatibility with the canonical map from the identity translate.
- homEquiv : Downstairs ≃ₗ[k] DirectSum G fun (g : G) => H g
- lift : H 1 →ₗ[k] Downstairs
- homEquiv_lift (f : H 1) : self.homEquiv (self.lift f) = identityLof f
Instances For
theorem
MagnitudeConjecture.CoveringHom.OrbitHomDecomposition.lift_injective
{k : Type u}
[Semiring k]
{G : Type v}
[Group G]
{H : G → Type w}
[(g : G) → AddCommMonoid (H g)]
[(g : G) → Module k (H g)]
{Downstairs : Type w'}
[AddCommMonoid Downstairs]
[Module k Downstairs]
(D : OrbitHomDecomposition Downstairs)
:
Function.Injective ⇑D.lift
Translate orthogonality makes the canonical identity-component map injective.
theorem
MagnitudeConjecture.CoveringHom.OrbitHomDecomposition.lift_surjective_of_orthogonal
{k : Type u}
[Semiring k]
{G : Type v}
[Group G]
{H : G → Type w}
[(g : G) → AddCommMonoid (H g)]
[(g : G) → Module k (H g)]
{Downstairs : Type w'}
[AddCommMonoid Downstairs]
[Module k Downstairs]
(D : OrbitHomDecomposition Downstairs)
(orthogonal : ∀ (g : G), g ≠ 1 → Subsingleton (H g))
:
Function.Surjective ⇑D.lift
If all nonidentity translated Hom spaces vanish, the canonical identity-component map is surjective.
noncomputable def
MagnitudeConjecture.CoveringHom.OrbitHomDecomposition.liftLinearEquivOfOrthogonal
{k : Type u}
[Semiring k]
{G : Type v}
[Group G]
{H : G → Type w}
[(g : G) → AddCommMonoid (H g)]
[(g : G) → Module k (H g)]
{Downstairs : Type w'}
[AddCommMonoid Downstairs]
[Module k Downstairs]
(D : OrbitHomDecomposition Downstairs)
(orthogonal : ∀ (g : G), g ≠ 1 → Subsingleton (H g))
:
H 1 ≃ₗ[k] Downstairs
Under translate orthogonality, the canonical map appearing in the orbit Hom formula is a linear equivalence.
Instances For
@[simp]
theorem
MagnitudeConjecture.CoveringHom.OrbitHomDecomposition.liftLinearEquivOfOrthogonal_apply
{k : Type u}
[Semiring k]
{G : Type v}
[Group G]
{H : G → Type w}
[(g : G) → AddCommMonoid (H g)]
[(g : G) → Module k (H g)]
{Downstairs : Type w'}
[AddCommMonoid Downstairs]
[Module k Downstairs]
(D : OrbitHomDecomposition Downstairs)
(orthogonal : ∀ (g : G), g ≠ 1 → Subsingleton (H g))
(f : H 1)
:
(D.liftLinearEquivOfOrthogonal orthogonal) f = D.lift f
theorem
MagnitudeConjecture.CoveringHom.OrbitHomDecomposition.lift_bijective_of_orthogonal
{k : Type u}
[Semiring k]
{G : Type v}
[Group G]
{H : G → Type w}
[(g : G) → AddCommMonoid (H g)]
[(g : G) → Module k (H g)]
{Downstairs : Type w'}
[AddCommMonoid Downstairs]
[Module k Downstairs]
(D : OrbitHomDecomposition Downstairs)
(orthogonal : ∀ (g : G), g ≠ 1 → Subsingleton (H g))
:
Function.Bijective ⇑D.lift
Bijective form used to install local fullness and faithfulness of a push-down functor on a separated window.
structure
MagnitudeConjecture.CoveringHom.FunctorOrbitHomDecomposition
{k : Type u}
[Semiring k]
{G : Type v}
[Group G]
{C : Type uC}
[CategoryTheory.Category.{vC, uC} C]
[CategoryTheory.Preadditive C]
{D : Type uD}
[CategoryTheory.Category.{vD, uD} D]
[CategoryTheory.Preadditive D]
[CategoryTheory.Linear k C]
[CategoryTheory.Linear k D]
(F : CategoryTheory.Functor C D)
(K : C → C → G → Type w)
[(X Y : C) → (g : G) → AddCommMonoid (K X Y g)]
[(X Y : C) → (g : G) → Module k (K X Y g)]
:
Type (max (max (max (max uC v) vC) vD) w)
A Gabriel-shaped orbit Hom formula for every pair of objects of a source
category. sourceEquiv identifies the identity summand with the original
Hom space, and map_compat says that inclusion of that summand is the functor's
map on morphisms.
- sourceEquiv (X Y : C) : (X ⟶ Y) ≃ₗ[k] K X Y 1
- homDecomposition (X Y : C) : OrbitHomDecomposition (F.obj X ⟶ F.obj Y)
- map_compat (X Y : C) (f : X ⟶ Y) : (self.homDecomposition X Y).lift ((self.sourceEquiv X Y) f) = F.map f
Instances For
def
MagnitudeConjecture.CoveringHom.TranslateHomOrthogonal
{G : Type v}
[Group G]
{C : Type uC}
(K : C → C → G → Type w)
:
Every nonidentity translate Hom summand vanishes. When C is the full
subcategory on a covering window, this is the pairwise separation condition
needed for local full faithfulness.
Instances For
noncomputable def
MagnitudeConjecture.CoveringHom.FunctorOrbitHomDecomposition.endRingEquivOfEndOrthogonal
{k : Type u}
[Semiring k]
{G : Type v}
[Group G]
{C : Type uC}
[CategoryTheory.Category.{vC, uC} C]
[CategoryTheory.Preadditive C]
{D : Type uD}
[CategoryTheory.Category.{vD, uD} D]
[CategoryTheory.Preadditive D]
[CategoryTheory.Linear k C]
[CategoryTheory.Linear k D]
{F : CategoryTheory.Functor C D}
{K : C → C → G → Type w}
[(X Y : C) → (g : G) → AddCommMonoid (K X Y g)]
[(X Y : C) → (g : G) → Module k (K X Y g)]
(E : FunctorOrbitHomDecomposition F K)
(X : C)
(orthogonal : ∀ (g : G), g ≠ 1 → Subsingleton (K X X g))
:
CategoryTheory.End X ≃+* CategoryTheory.End (F.obj X)
If the nonidentity summands in the orbit formula for End(X) vanish,
then the functor identifies the endomorphism rings of X and F.obj X.
Unlike global local full faithfulness, this needs orthogonality only for the
single pair (X, X).
Instances For
@[simp]
theorem
MagnitudeConjecture.CoveringHom.FunctorOrbitHomDecomposition.endRingEquivOfEndOrthogonal_apply
{k : Type u}
[Semiring k]
{G : Type v}
[Group G]
{C : Type uC}
[CategoryTheory.Category.{vC, uC} C]
[CategoryTheory.Preadditive C]
{D : Type uD}
[CategoryTheory.Category.{vD, uD} D]
[CategoryTheory.Preadditive D]
[CategoryTheory.Linear k C]
[CategoryTheory.Linear k D]
{F : CategoryTheory.Functor C D}
{K : C → C → G → Type w}
[(X Y : C) → (g : G) → AddCommMonoid (K X Y g)]
[(X Y : C) → (g : G) → Module k (K X Y g)]
(E : FunctorOrbitHomDecomposition F K)
(X : C)
(orthogonal : ∀ (g : G), g ≠ 1 → Subsingleton (K X X g))
(f : CategoryTheory.End X)
:
(E.endRingEquivOfEndOrthogonal X orthogonal) f = F.map f
theorem
MagnitudeConjecture.CoveringHom.FunctorOrbitHomDecomposition.indecomposable_map_of_end_orthogonal
{k : Type u}
[Semiring k]
{G : Type v}
[Group G]
{C : Type uC}
[CategoryTheory.Category.{vC, uC} C]
[CategoryTheory.Preadditive C]
{D : Type uD}
[CategoryTheory.Category.{vD, uD} D]
[CategoryTheory.Preadditive D]
[CategoryTheory.Linear k C]
[CategoryTheory.Linear k D]
{F : CategoryTheory.Functor C D}
{K : C → C → G → Type w}
[(X Y : C) → (g : G) → AddCommMonoid (K X Y g)]
[(X Y : C) → (g : G) → Module k (K X Y g)]
(E : FunctorOrbitHomDecomposition F K)
(X : C)
(orthogonal : ∀ (g : G), g ≠ 1 → Subsingleton (K X X g))
[IsLocalRing (CategoryTheory.End X)]
[CategoryTheory.Limits.HasBinaryBiproducts D]
:
CategoryTheory.Indecomposable (F.obj X)
Self-translate orthogonality preserves an object with local endomorphism ring as an indecomposable object downstairs.
noncomputable def
MagnitudeConjecture.CoveringHom.FunctorOrbitHomDecomposition.mapLinearEquivOfOrthogonal
{k : Type u}
[Semiring k]
{G : Type v}
[Group G]
{C : Type uC}
[CategoryTheory.Category.{vC, uC} C]
[CategoryTheory.Preadditive C]
{D : Type uD}
[CategoryTheory.Category.{vD, uD} D]
[CategoryTheory.Preadditive D]
[CategoryTheory.Linear k C]
[CategoryTheory.Linear k D]
{F : CategoryTheory.Functor C D}
{K : C → C → G → Type w}
[(X Y : C) → (g : G) → AddCommMonoid (K X Y g)]
[(X Y : C) → (g : G) → Module k (K X Y g)]
(E : FunctorOrbitHomDecomposition F K)
(orthogonal : TranslateHomOrthogonal K)
(X Y : C)
:
(X ⟶ Y) ≃ₗ[k] F.obj X ⟶ F.obj Y
Pairwise translate orthogonality turns the orbit Hom formula into a linear equivalence between each source and image Hom space.
Instances For
@[simp]
theorem
MagnitudeConjecture.CoveringHom.FunctorOrbitHomDecomposition.mapLinearEquivOfOrthogonal_apply
{k : Type u}
[Semiring k]
{G : Type v}
[Group G]
{C : Type uC}
[CategoryTheory.Category.{vC, uC} C]
[CategoryTheory.Preadditive C]
{D : Type uD}
[CategoryTheory.Category.{vD, uD} D]
[CategoryTheory.Preadditive D]
[CategoryTheory.Linear k C]
[CategoryTheory.Linear k D]
{F : CategoryTheory.Functor C D}
{K : C → C → G → Type w}
[(X Y : C) → (g : G) → AddCommMonoid (K X Y g)]
[(X Y : C) → (g : G) → Module k (K X Y g)]
(E : FunctorOrbitHomDecomposition F K)
(orthogonal : TranslateHomOrthogonal K)
{X Y : C}
(f : X ⟶ Y)
:
(E.mapLinearEquivOfOrthogonal orthogonal X Y) f = F.map f
theorem
MagnitudeConjecture.CoveringHom.FunctorOrbitHomDecomposition.map_bijective_of_orthogonal
{k : Type u}
[Semiring k]
{G : Type v}
[Group G]
{C : Type uC}
[CategoryTheory.Category.{vC, uC} C]
[CategoryTheory.Preadditive C]
{D : Type uD}
[CategoryTheory.Category.{vD, uD} D]
[CategoryTheory.Preadditive D]
[CategoryTheory.Linear k C]
[CategoryTheory.Linear k D]
{F : CategoryTheory.Functor C D}
{K : C → C → G → Type w}
[(X Y : C) → (g : G) → AddCommMonoid (K X Y g)]
[(X Y : C) → (g : G) → Module k (K X Y g)]
(E : FunctorOrbitHomDecomposition F K)
(orthogonal : TranslateHomOrthogonal K)
(X Y : C)
:
Function.Bijective F.map
On every pair of source objects, the functor map is bijective.
theorem
MagnitudeConjecture.CoveringHom.FunctorOrbitHomDecomposition.fullOfOrthogonal
{k : Type u}
[Semiring k]
{G : Type v}
[Group G]
{C : Type uC}
[CategoryTheory.Category.{vC, uC} C]
[CategoryTheory.Preadditive C]
{D : Type uD}
[CategoryTheory.Category.{vD, uD} D]
[CategoryTheory.Preadditive D]
[CategoryTheory.Linear k C]
[CategoryTheory.Linear k D]
{F : CategoryTheory.Functor C D}
{K : C → C → G → Type w}
[(X Y : C) → (g : G) → AddCommMonoid (K X Y g)]
[(X Y : C) → (g : G) → Module k (K X Y g)]
(E : FunctorOrbitHomDecomposition F K)
(orthogonal : TranslateHomOrthogonal K)
:
F.Full
The actual Mathlib fullness instance supplied by an orthogonal orbit Hom decomposition.
theorem
MagnitudeConjecture.CoveringHom.FunctorOrbitHomDecomposition.map_injective
{k : Type u}
[Semiring k]
{G : Type v}
[Group G]
{C : Type uC}
[CategoryTheory.Category.{vC, uC} C]
[CategoryTheory.Preadditive C]
{D : Type uD}
[CategoryTheory.Category.{vD, uD} D]
[CategoryTheory.Preadditive D]
[CategoryTheory.Linear k C]
[CategoryTheory.Linear k D]
{F : CategoryTheory.Functor C D}
{K : C → C → G → Type w}
[(X Y : C) → (g : G) → AddCommMonoid (K X Y g)]
[(X Y : C) → (g : G) → Module k (K X Y g)]
(E : FunctorOrbitHomDecomposition F K)
(X Y : C)
:
Function.Injective F.map
Inclusion of the identity translate is injective before any orthogonality hypothesis is imposed.
theorem
MagnitudeConjecture.CoveringHom.FunctorOrbitHomDecomposition.faithful
{k : Type u}
[Semiring k]
{G : Type v}
[Group G]
{C : Type uC}
[CategoryTheory.Category.{vC, uC} C]
[CategoryTheory.Preadditive C]
{D : Type uD}
[CategoryTheory.Category.{vD, uD} D]
[CategoryTheory.Preadditive D]
[CategoryTheory.Linear k C]
[CategoryTheory.Linear k D]
{F : CategoryTheory.Functor C D}
{K : C → C → G → Type w}
[(X Y : C) → (g : G) → AddCommMonoid (K X Y g)]
[(X Y : C) → (g : G) → Module k (K X Y g)]
(E : FunctorOrbitHomDecomposition F K)
:
F.Faithful
Every functor carrying a Gabriel-shaped orbit Hom decomposition is faithful; translate orthogonality is needed only for fullness.
theorem
MagnitudeConjecture.CoveringHom.FunctorOrbitHomDecomposition.isIrreducibleMorphism_map_iff_of_orthogonal
{k : Type u}
[Semiring k]
{G : Type v}
[Group G]
{C : Type uC}
[CategoryTheory.Category.{vC, uC} C]
[CategoryTheory.Preadditive C]
{D : Type uD}
[CategoryTheory.Category.{vD, uD} D]
[CategoryTheory.Preadditive D]
[CategoryTheory.Linear k C]
[CategoryTheory.Linear k D]
{F : CategoryTheory.Functor C D}
{K : C → C → G → Type w}
[(X Y : C) → (g : G) → AddCommMonoid (K X Y g)]
[(X Y : C) → (g : G) → Module k (K X Y g)]
(E : FunctorOrbitHomDecomposition F K)
(orthogonal : TranslateHomOrthogonal K)
{X Y : C}
{f : X ⟶ Y}
(hclosed : IsLocallyFactorizationClosedAt F f)
:
The orbit Hom formula and translate orthogonality feed directly into the local irreducibility-transport theorem.
theorem
MagnitudeConjecture.CoveringHom.FunctorOrbitHomDecomposition.rightAlmostSplit_map_of_orthogonal
{k : Type u}
[Semiring k]
{G : Type v}
[Group G]
{C : Type uC}
[CategoryTheory.Category.{vC, uC} C]
[CategoryTheory.Preadditive C]
{D : Type uD}
[CategoryTheory.Category.{vD, uD} D]
[CategoryTheory.Preadditive D]
[CategoryTheory.Linear k C]
[CategoryTheory.Linear k D]
{F : CategoryTheory.Functor C D}
{K : C → C → G → Type w}
[(X Y : C) → (g : G) → AddCommMonoid (K X Y g)]
[(X Y : C) → (g : G) → Module k (K X Y g)]
(E : FunctorOrbitHomDecomposition F K)
(orthogonal : TranslateHomOrthogonal K)
{X Y : C}
{f : X ⟶ Y}
(hf : QuotientSubmoduleEquidistribution.IsRightAlmostSplit f)
(hclosed : IsLocallyRightObjectClosedAt F Y)
:
The same local full-faithfulness mechanism preserves a right almost-split map once the relevant incoming objects lie in the controlled image.
theorem
MagnitudeConjecture.CoveringHom.FunctorOrbitHomDecomposition.leftAlmostSplit_map_of_orthogonal
{k : Type u}
[Semiring k]
{G : Type v}
[Group G]
{C : Type uC}
[CategoryTheory.Category.{vC, uC} C]
[CategoryTheory.Preadditive C]
{D : Type uD}
[CategoryTheory.Category.{vD, uD} D]
[CategoryTheory.Preadditive D]
[CategoryTheory.Linear k C]
[CategoryTheory.Linear k D]
{F : CategoryTheory.Functor C D}
{K : C → C → G → Type w}
[(X Y : C) → (g : G) → AddCommMonoid (K X Y g)]
[(X Y : C) → (g : G) → Module k (K X Y g)]
(E : FunctorOrbitHomDecomposition F K)
(orthogonal : TranslateHomOrthogonal K)
{X Y : C}
{f : X ⟶ Y}
(hf : QuotientSubmoduleEquidistribution.IsLeftAlmostSplit f)
(hclosed : IsLocallyLeftObjectClosedAt F X)
:
Dual local almost-split transport from the orthogonal orbit Hom formula.