Documentation

TauCeti.RepresentationTheory.Quiver.Acyclic.Basic

Acyclic quivers #

This file defines an acyclic quiver to be one whose closed paths are all trivial. It develops the elementary path API for excluding directed cycles, including the fact that paths cannot run in both directions between distinct vertices.

This is the orientation-sensitive notion of acyclicity used for path algebras and quiver representations. It is distinct from acyclicity of the underlying undirected graph.

References #

This file implements the Layer 0 “Acyclicity, as a predicate” target of TauCetiRoadmap/RepresentationTheory/QuiverRepresentations/Suggested.lean and its README.md.

source
def TauCeti.Quiver.IsAcyclic (V : Type u) [Quiver V] :
Prop

A quiver is acyclic if every closed path is trivial.

Equations
Instances For
    source
    theorem TauCeti.Quiver.isAcyclic_def {V : Type u} [Quiver V] :
    IsAcyclic V ↔ ∀ ⦃a : V⦄ (p : Quiver.Path a a), p = Quiver.Path.nil

    The defining closed-path condition for an acyclic quiver.

    source
    theorem TauCeti.Quiver.IsAcyclic.eq_nil {V : Type u} [Quiver V] (h : IsAcyclic V) {a : V} (p : Quiver.Path a a) :
    p = Quiver.Path.nil

    Every closed path in an acyclic quiver is trivial.

    source
    theorem TauCeti.Quiver.IsAcyclic.iff_forall_length_eq_zero {V : Type u} [Quiver V] :
    IsAcyclic V ↔ ∀ ⦃a : V⦄ (p : Quiver.Path a a), p.length = 0

    A quiver is acyclic exactly when every closed path has length zero.

    source
    @[simp]
    theorem TauCeti.Quiver.IsAcyclic.length_eq_zero {V : Type u} [Quiver V] (h : IsAcyclic V) {a : V} (p : Quiver.Path a a) :
    p.length = 0

    In an acyclic quiver, every closed path has length zero.

    source
    theorem TauCeti.Quiver.IsAcyclic.not_length_pos {V : Type u} [Quiver V] (h : IsAcyclic V) {a : V} (p : Quiver.Path a a) :
    ¬0 < p.length

    An acyclic quiver has no closed path of positive length.

    source
    theorem TauCeti.Quiver.IsAcyclic.iff_forall_not_length_pos {V : Type u} [Quiver V] :
    IsAcyclic V ↔ ∀ ⦃a : V⦄ (p : Quiver.Path a a), ¬0 < p.length

    A quiver is acyclic exactly when it has no closed path of positive length.

    source
    theorem TauCeti.Quiver.IsAcyclic.iff_not_exists_ne_nil {V : Type u} [Quiver V] :
    IsAcyclic V ↔ ¬∃ (a : V) (p : Quiver.Path a a), p ≠ Quiver.Path.nil

    A quiver is acyclic exactly when it has no nontrivial closed path.

    source
    @[simp]
    theorem TauCeti.Quiver.IsAcyclic.comp_eq_nil {V : Type u} [Quiver V] (h : IsAcyclic V) {a b : V} (p : Quiver.Path a b) (q : Quiver.Path b a) :
    p.comp q = Quiver.Path.nil

    The composition of paths in opposite directions is trivial in an acyclic quiver.

    source
    theorem TauCeti.Quiver.IsAcyclic.length_eq_zero_of_paths_left {V : Type u} [Quiver V] (h : IsAcyclic V) {a b : V} (p : Quiver.Path a b) (q : Quiver.Path b a) :
    p.length = 0

    If paths run in both directions in an acyclic quiver, the forward path has length zero.

    source
    theorem TauCeti.Quiver.IsAcyclic.length_eq_zero_of_paths_right {V : Type u} [Quiver V] (h : IsAcyclic V) {a b : V} (p : Quiver.Path a b) (q : Quiver.Path b a) :
    q.length = 0

    If paths run in both directions in an acyclic quiver, the reverse path has length zero.

    source
    theorem TauCeti.Quiver.IsAcyclic.eq_of_paths {V : Type u} [Quiver V] (h : IsAcyclic V) {a b : V} (p : Quiver.Path a b) (q : Quiver.Path b a) :
    a = b

    Vertices joined by paths in both directions in an acyclic quiver are equal.

    source
    theorem TauCeti.Quiver.IsAcyclic.vertices_nodup {V : Type u} [Quiver V] (h : IsAcyclic V) {a b : V} (p : Quiver.Path a b) :
    p.vertices.Nodup

    The vertices encountered by a path in an acyclic quiver are pairwise distinct.

    source
    theorem TauCeti.Quiver.IsAcyclic.not_nonempty_path_and_nonempty_path {V : Type u} [Quiver V] (h : IsAcyclic V) {a b : V} (hab : a ≠ b) :
    ¬(Nonempty (Quiver.Path a b) ∧ Nonempty (Quiver.Path b a))

    Between distinct vertices of an acyclic quiver, paths cannot exist in both directions.

    source
    theorem TauCeti.Quiver.IsAcyclic.isEmpty_path_of_path {V : Type u} [Quiver V] (h : IsAcyclic V) {a b : V} (hab : a ≠ b) (p : Quiver.Path a b) :
    IsEmpty (Quiver.Path b a)

    A path between distinct vertices of an acyclic quiver excludes every reverse path.

    source
    theorem TauCeti.Quiver.IsAcyclic.isEmpty_hom_self {V : Type u} [Quiver V] (h : IsAcyclic V) (a : V) :
    IsEmpty (a ⟶ a)

    An acyclic quiver has no loops.

    source
    theorem TauCeti.Quiver.IsAcyclic.isEmpty_hom_of_hom {V : Type u} [Quiver V] (h : IsAcyclic V) {a b : V} (e : a ⟶ b) :
    IsEmpty (b ⟶ a)

    In an acyclic quiver, an arrow excludes every reverse arrow.

    source
    theorem TauCeti.Quiver.IsAcyclic.subsingleton_path_self {V : Type u} [Quiver V] (h : IsAcyclic V) (a : V) :
    Subsingleton (Quiver.Path a a)

    Closed paths in an acyclic quiver form a subsingleton.

    source
    theorem TauCeti.Quiver.IsAcyclic.card_path_self {V : Type u} [Quiver V] (h : IsAcyclic V) (a : V) :
    Nat.card (Quiver.Path a a) = 1

    An acyclic quiver has exactly one closed path at each vertex, the trivial one.

    source
    theorem TauCeti.Quiver.IsAcyclic.of_isEmpty_hom {V : Type u} [Quiver V] [∀ (a b : V), IsEmpty (a ⟶ b)] :
    IsAcyclic V

    A quiver with no arrows is acyclic.

    source
    theorem TauCeti.Quiver.IsAcyclic.of_mapPath_self_injective {V : Type u} [Quiver V] {W : Type u_1} [Quiver W] (F : V ⥤q W) (hW : IsAcyclic W) (hinj : ∀ ⦃a : V⦄, Function.Injective F.mapPath) :
    IsAcyclic V

    A quiver mapping to an acyclic quiver is acyclic if the induced map on each closed-path type is injective.

    source
    theorem TauCeti.Quiver.IsAcyclic.of_mapPath_injective {V : Type u} [Quiver V] {W : Type u_1} [Quiver W] (F : V ⥤q W) (hW : IsAcyclic W) (hinj : ∀ ⦃a b : V⦄, Function.Injective F.mapPath) :
    IsAcyclic V

    A quiver is acyclic if its induced maps on all path types are injective and its target is acyclic.