Symmetric

📁 Source: Mathlib/Combinatorics/Quiver/Symmetric.lean

Statistics

Metric	Count
Definitions MapReverse, symmetrify, HasInvolutiveReverse, toHasReverse, HasReverse, reverse', toNeg, toPos, reverse, instHasInvolutiveReverse, instHasReverse, Symmetrify, of, instHasInvolutiveReverseSymmetrify, instHasReverseSymmetrify, reverse, symmetrifyQuiver	17
Theorems map_reverse', mapReverseComp, mapReverseId, map_reverse, symmetrify_map, symmetrify_mapReverse, symmetrify_obj, inv', reverse_comp, reverse_reverse, reverse_toPath, ofMapReverse, of_reverse, lift_reverse, lift_spec, lift_unique, of_map, of_obj, eq_reverse_iff, reverse_inj, reverse_reverse, symmetrify_reverse	22
Total	39

Prefunctor

Definitions

Name	Category	Theorems
MapReverse 📖	CompData	5 math math: mapReverseId, CategoryTheory.functorMapReverse, symmetrify_mapReverse, mapReverseComp, Quiver.Push.ofMapReverse
symmetrify 📖	CompOp	6 math math: IsCovering.symmetrify, symmetrifyStar, symmetrifyCostar, symmetrify_mapReverse, symmetrify_map, symmetrify_obj

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
mapReverseComp 📖	mathematical	—	MapReverse comp	—	MapReverse.map_reverse'
mapReverseId 📖	mathematical	—	MapReverse id	—	—
map_reverse 📖	mathematical	—	map Quiver.reverse obj	—	MapReverse.map_reverse'
symmetrify_map 📖	mathematical	—	map Quiver.Symmetrify Quiver.symmetrifyQuiver symmetrify Quiver.Hom obj	—	—
symmetrify_mapReverse 📖	mathematical	—	MapReverse Quiver.Symmetrify Quiver.symmetrifyQuiver Quiver.instHasReverseSymmetrify symmetrify	—	—
symmetrify_obj 📖	mathematical	—	obj Quiver.Symmetrify Quiver.symmetrifyQuiver symmetrify	—	—

Prefunctor.MapReverse

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
map_reverse' 📖	mathematical	—	Prefunctor.map Quiver.reverse Prefunctor.obj	—	—

Quiver

Definitions

Name	Category	Theorems
HasInvolutiveReverse 📖	CompData	—
HasReverse 📖	CompData	—
Symmetrify 📖	CompOp	19 math math: IsStronglyConnected.isStronglyConnected_symmetrify, Symmetrify.lift_spec, IsFreeGroupoid.path_nonempty_of_hom, WeaklyConnectedComponent.eq, symmetrify_reverse, Symmetrify.lift_reverse, Symmetrify.of_obj, Symmetrify.of_map, FreeGroupoid.congr_comp_reverse, IsFreeGroupoid.generators_connected, CategoryTheory.FreeGroupoid.eq_mk, Prefunctor.IsCovering.symmetrify, Prefunctor.symmetrifyStar, Prefunctor.symmetrifyCostar, Prefunctor.symmetrify_mapReverse, FreeGroupoid.of_eq, Prefunctor.symmetrify_map, FreeGroupoid.congr_reverse_comp, Prefunctor.symmetrify_obj
instHasInvolutiveReverseSymmetrify 📖	CompOp	—
instHasReverseSymmetrify 📖	CompOp	6 math math: symmetrify_reverse, Symmetrify.lift_reverse, FreeGroupoid.congr_comp_reverse, Prefunctor.symmetrify_mapReverse, FreeGroupoid.congr_reverse, FreeGroupoid.congr_reverse_comp
reverse 📖	CompOp	15 math math: CategoryTheory.Groupoid.reverse_eq_inv, HasInvolutiveReverse.inv', reverse_inj, eq_reverse_iff, symmetrify_reverse, reverse_reverse, Symmetrify.lift_reverse, Prefunctor.map_reverse, Prefunctor.MapReverse.map_reverse', starEquivCostar_apply_snd, starEquivCostar_symm_apply, starEquivCostar_apply, Push.of_reverse, starEquivCostar_symm_apply_snd, Path.reverse_toPath
symmetrifyQuiver 📖	CompOp	19 math math: IsStronglyConnected.isStronglyConnected_symmetrify, Symmetrify.lift_spec, IsFreeGroupoid.path_nonempty_of_hom, WeaklyConnectedComponent.eq, symmetrify_reverse, Symmetrify.lift_reverse, Symmetrify.of_obj, Symmetrify.of_map, FreeGroupoid.congr_comp_reverse, IsFreeGroupoid.generators_connected, CategoryTheory.FreeGroupoid.eq_mk, Prefunctor.IsCovering.symmetrify, Prefunctor.symmetrifyStar, Prefunctor.symmetrifyCostar, Prefunctor.symmetrify_mapReverse, FreeGroupoid.of_eq, Prefunctor.symmetrify_map, FreeGroupoid.congr_reverse_comp, Prefunctor.symmetrify_obj

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
eq_reverse_iff 📖	mathematical	—	reverse HasInvolutiveReverse.toHasReverse	—	reverse_reverse
reverse_inj 📖	mathematical	—	reverse HasInvolutiveReverse.toHasReverse	—	reverse_reverse
reverse_reverse 📖	mathematical	—	reverse HasInvolutiveReverse.toHasReverse	—	HasInvolutiveReverse.inv'
symmetrify_reverse 📖	mathematical	—	reverse Symmetrify symmetrifyQuiver instHasReverseSymmetrify Hom	—	—

Quiver.HasInvolutiveReverse

Definitions

Name	Category	Theorems
toHasReverse 📖	CompOp	14 math math: CategoryTheory.Groupoid.reverse_eq_inv, inv', Quiver.reverse_inj, Quiver.eq_reverse_iff, Quiver.reverse_reverse, Quiver.Symmetrify.lift_reverse, Quiver.Path.reverse_reverse, Quiver.starEquivCostar_apply_snd, Quiver.starEquivCostar_symm_apply, CategoryTheory.functorMapReverse, Quiver.starEquivCostar_apply, Quiver.Push.of_reverse, Quiver.starEquivCostar_symm_apply_snd, Quiver.Push.ofMapReverse

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
inv' 📖	mathematical	—	Quiver.reverse toHasReverse	—	—

Quiver.HasReverse

Definitions

Name	Category	Theorems
reverse' 📖	CompOp	—

Quiver.Hom

Definitions

Name	Category	Theorems
toNeg 📖	CompOp	—
toPos 📖	CompOp	—

Quiver.Path

Definitions

Name	Category	Theorems
reverse 📖	CompOp	6 math math: reverse_comp, Quiver.FreeGroupoid.congr_comp_reverse, reverse_reverse, Quiver.FreeGroupoid.congr_reverse, Quiver.FreeGroupoid.congr_reverse_comp, reverse_toPath

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
reverse_comp 📖	mathematical	—	reverse comp	—	nil_comp comp_assoc
reverse_reverse 📖	mathematical	—	reverse Quiver.HasInvolutiveReverse.toHasReverse	—	reverse.eq_2 reverse_comp reverse_toPath Quiver.reverse_reverse
reverse_toPath 📖	mathematical	—	reverse Quiver.Hom.toPath Quiver.reverse	—	—

Quiver.Push

Definitions

Name	Category	Theorems
instHasInvolutiveReverse 📖	CompOp	—
instHasReverse 📖	CompOp	2 math math: of_reverse, ofMapReverse

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
ofMapReverse 📖	mathematical	—	Prefunctor.MapReverse Quiver.Push Quiver.instPush Quiver.HasInvolutiveReverse.toHasReverse instHasReverse of	—	—
of_reverse 📖	mathematical	—	Quiver.reverse Quiver.Push Quiver.instPush instHasReverse Quiver.HasInvolutiveReverse.toHasReverse Prefunctor.obj of Prefunctor.map	—	—

Quiver.Symmetrify

Definitions

Name	Category	Theorems
of 📖	CompOp	6 math math: lift_spec, of_obj, of_map, Prefunctor.symmetrifyStar, Prefunctor.symmetrifyCostar, Quiver.FreeGroupoid.of_eq

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
lift_reverse 📖	mathematical	—	Prefunctor.map Quiver.Symmetrify Quiver.symmetrifyQuiver lift Quiver.HasInvolutiveReverse.toHasReverse Quiver.reverse Quiver.instHasReverseSymmetrify Prefunctor.obj	—	Quiver.reverse_reverse
lift_spec 📖	mathematical	—	Prefunctor.comp Quiver.Symmetrify Quiver.symmetrifyQuiver of lift	—	Prefunctor.ext
lift_unique 📖	mathematical	Prefunctor.comp Quiver.Symmetrify Quiver.symmetrifyQuiver of Prefunctor.map Quiver.reverse Quiver.instHasReverseSymmetrify Prefunctor.obj	lift	—	Prefunctor.ext
of_map 📖	mathematical	—	Prefunctor.map Quiver.Symmetrify Quiver.symmetrifyQuiver of Quiver.Hom	—	—
of_obj 📖	mathematical	—	Prefunctor.obj Quiver.Symmetrify Quiver.symmetrifyQuiver of	—	—

---

← Back to Index