docs: Add doc strings for all defs
This commit is contained in:
jstoobysmith
parent
fc2065b744
commit
a5c1b88f05
2 changed files with 40 additions and 5 deletions
|
|
@ -93,7 +93,8 @@ def preimageType' {𝓥 : Type} (v : 𝓥) : Over 𝓥 ⥤ Type where
|
|||
Set.mem_singleton_iff]⟩
|
||||
|
||||
/-- The functor from `Over (P.HalfEdgeLabel × 𝓔 × 𝓥)` to
|
||||
`Over P.HalfEdgeLabel` induced by pull-back along insertion of `v : P.VertexLabel`. -/
|
||||
`Over P.HalfEdgeLabel` induced by pull-back along insertion of `v : P.VertexLabel`.
|
||||
For a given vertex, it returns all half edges corresponding to that vertex. -/
|
||||
def preimageVertex {𝓔 𝓥 : Type} (v : 𝓥) :
|
||||
Over (P.HalfEdgeLabel × 𝓔 × 𝓥) ⥤ Over P.HalfEdgeLabel where
|
||||
obj f := Over.mk (fun x => Prod.fst (f.hom x.1) :
|
||||
|
|
@ -102,7 +103,8 @@ def preimageVertex {𝓔 𝓥 : Type} (v : 𝓥) :
|
|||
(funext <| fun x => congrArg Prod.fst <| congrFun F.w x.1)
|
||||
|
||||
/-- The functor from `Over (P.HalfEdgeLabel × P.EdgeLabel × P.VertexLabel)` to
|
||||
`Over P.HalfEdgeLabel` induced by pull-back along insertion of `v : P.EdgeLabel`. -/
|
||||
`Over P.HalfEdgeLabel` induced by pull-back along insertion of `v : P.EdgeLabel`.
|
||||
For a given edge, it returns all half edges corresponding to that edge. -/
|
||||
def preimageEdge {𝓔 𝓥 : Type} (v : 𝓔) :
|
||||
Over (P.HalfEdgeLabel × 𝓔 × 𝓥) ⥤ Over P.HalfEdgeLabel where
|
||||
obj f := Over.mk (fun x => Prod.fst (f.hom x.1) :
|
||||
|
|
@ -174,6 +176,8 @@ instance [IsFinitePreFeynmanRule P] (v : P.EdgeLabel) : Fintype (P.edgeLabelMap
|
|||
instance [IsFinitePreFeynmanRule P] (v : P.EdgeLabel) : DecidableEq (P.edgeLabelMap v).left :=
|
||||
IsFinitePreFeynmanRule.edgeMapDecidable v
|
||||
|
||||
/-- It is decidable to check whether a half edge of a diagram (an object in
|
||||
`Over (P.HalfEdgeLabel × 𝓔 × 𝓥)`) corresponds to a given vertex. -/
|
||||
instance preimageVertexDecidablePred {𝓔 𝓥 : Type} [DecidableEq 𝓥] (v : 𝓥)
|
||||
(F : Over (P.HalfEdgeLabel × 𝓔 × 𝓥)) :
|
||||
DecidablePred fun x => x ∈ (P.toVertex.obj F).hom ⁻¹' {v} := fun y =>
|
||||
|
|
@ -181,6 +185,8 @@ instance preimageVertexDecidablePred {𝓔 𝓥 : Type} [DecidableEq 𝓥] (v :
|
|||
| isTrue h => isTrue h
|
||||
| isFalse h => isFalse h
|
||||
|
||||
/-- It is decidable to check whether a half edge of a diagram (an object in
|
||||
`Over (P.HalfEdgeLabel × 𝓔 × 𝓥)`) corresponds to a given edge. -/
|
||||
instance preimageEdgeDecidablePred {𝓔 𝓥 : Type} [DecidableEq 𝓔] (v : 𝓔)
|
||||
(F : Over (P.HalfEdgeLabel × 𝓔 × 𝓥)) :
|
||||
DecidablePred fun x => x ∈ (P.toEdge.obj F).hom ⁻¹' {v} := fun y =>
|
||||
|
|
@ -195,24 +201,31 @@ instance preimageVertexDecidable {𝓔 𝓥 : Type} (v : 𝓥)
|
|||
(F : Over (P.HalfEdgeLabel × 𝓔 × 𝓥)) [DecidableEq F.left] :
|
||||
DecidableEq ((P.preimageVertex v).obj F).left := Subtype.instDecidableEq
|
||||
|
||||
/-- The half edges corresponding to a given edge has an indexing set which is decidable. -/
|
||||
instance preimageEdgeDecidable {𝓔 𝓥 : Type} (v : 𝓔)
|
||||
(F : Over (P.HalfEdgeLabel × 𝓔 × 𝓥)) [DecidableEq F.left] :
|
||||
DecidableEq ((P.preimageEdge v).obj F).left := Subtype.instDecidableEq
|
||||
|
||||
/-- The half edges corresponding to a given vertex has an indexing set which is decidable. -/
|
||||
instance preimageVertexFintype {𝓔 𝓥 : Type} [DecidableEq 𝓥]
|
||||
(v : 𝓥) (F : Over (P.HalfEdgeLabel × 𝓔 × 𝓥)) [h : Fintype F.left] :
|
||||
Fintype ((P.preimageVertex v).obj F).left := @Subtype.fintype _ _ _ h
|
||||
|
||||
/-- The half edges corresponding to a given edge has an indexing set which is finite. -/
|
||||
instance preimageEdgeFintype {𝓔 𝓥 : Type} [DecidableEq 𝓔]
|
||||
(v : 𝓔) (F : Over (P.HalfEdgeLabel × 𝓔 × 𝓥)) [h : Fintype F.left] :
|
||||
Fintype ((P.preimageEdge v).obj F).left := @Subtype.fintype _ _ _ h
|
||||
|
||||
/-- The half edges corresponding to a given vertex has an indexing set which is finite. -/
|
||||
instance preimageVertexMapFintype [IsFinitePreFeynmanRule P] {𝓔 𝓥 : Type}
|
||||
[DecidableEq 𝓥] (v : 𝓥) (f : 𝓥 ⟶ P.VertexLabel) (F : Over (P.HalfEdgeLabel × 𝓔 × 𝓥))
|
||||
[Fintype F.left] :
|
||||
Fintype ((P.vertexLabelMap (f v)).left → ((P.preimageVertex v).obj F).left) :=
|
||||
Pi.fintype
|
||||
|
||||
/-- Given an edge, there is a finite number of maps between the indexing set of the
|
||||
expected half-edges corresponding to that edges label, and the actual indexing
|
||||
set of half-edges corresponding to that edge. Given various finiteness conditions. -/
|
||||
instance preimageEdgeMapFintype [IsFinitePreFeynmanRule P] {𝓔 𝓥 : Type}
|
||||
[DecidableEq 𝓔] (v : 𝓔) (f : 𝓔 ⟶ P.EdgeLabel) (F : Over (P.HalfEdgeLabel × 𝓔 × 𝓥))
|
||||
[Fintype F.left] :
|
||||
|
|
@ -245,6 +258,7 @@ lemma external_iff_exists_bijection {P : PreFeynmanRule} (v : P.VertexLabel) :
|
|||
obtain ⟨fm, hf1, hf2⟩ := ft
|
||||
exact ⟨f, fm, hf1, hf2⟩
|
||||
|
||||
/-- Whether or not a vertex is external is decidable. -/
|
||||
instance externalDecidable [IsFinitePreFeynmanRule P] (v : P.VertexLabel) :
|
||||
Decidable (External v) :=
|
||||
decidable_of_decidable_of_iff (external_iff_exists_bijection v).symm
|
||||
|
|
@ -301,6 +315,8 @@ lemma diagramEdgeProp_iff {𝓔 𝓥 : Type} (F : Over (P.HalfEdgeLabel × 𝓔
|
|||
obtain ⟨fm, hf1, hf2⟩ := (isIso_of_reflects_iso _ (Over.forget P.HalfEdgeLabel) : IsIso f)
|
||||
exact ⟨f, fm, hf1, hf2⟩
|
||||
|
||||
/-- The proposition `DiagramVertexProp` is decidable given various decidablity and finite
|
||||
conditions. -/
|
||||
instance diagramVertexPropDecidable
|
||||
[IsFinitePreFeynmanRule P] {𝓔 𝓥 : Type} [Fintype 𝓥] [DecidableEq 𝓥]
|
||||
(F : Over (P.HalfEdgeLabel × 𝓔 × 𝓥)) [DecidableEq F.left] [Fintype F.left]
|
||||
|
|
@ -311,6 +327,8 @@ instance diagramVertexPropDecidable
|
|||
(fun _ => P.preFeynmanRuleDecEq𝓱𝓔) _ _ _)) _) _)
|
||||
(P.diagramVertexProp_iff F f).symm
|
||||
|
||||
/-- The proposition `DiagramEdgeProp` is decidable given various decidablity and finite
|
||||
conditions. -/
|
||||
instance diagramEdgePropDecidable
|
||||
[IsFinitePreFeynmanRule P] {𝓔 𝓥 : Type} [Fintype 𝓔] [DecidableEq 𝓔]
|
||||
(F : Over (P.HalfEdgeLabel × 𝓔 × 𝓥)) [DecidableEq F.left] [Fintype F.left]
|
||||
|
|
@ -434,6 +452,8 @@ class IsFiniteDiagram (F : FeynmanDiagram P) where
|
|||
/-- The type of half-edges is decidable. -/
|
||||
𝓱𝓔DecidableEq : DecidableEq F.𝓱𝓔
|
||||
|
||||
/-- The instance of a finite diagram given explicit finiteness and decidable conditions
|
||||
on the various maps making it up. -/
|
||||
instance {𝓔 𝓥 𝓱𝓔 : Type} [h1 : Fintype 𝓔] [h2 : DecidableEq 𝓔]
|
||||
[h3 : Fintype 𝓥] [h4 : DecidableEq 𝓥] [h5 : Fintype 𝓱𝓔] [h6 : DecidableEq 𝓱𝓔]
|
||||
(𝓔𝓞 : 𝓔 → P.EdgeLabel) (𝓥𝓞 : 𝓥 → P.VertexLabel)
|
||||
|
|
@ -597,11 +617,16 @@ instance {F G : FeynmanDiagram P} [IsFiniteDiagram F] [IsFinitePreFeynmanRule P]
|
|||
(𝓥 : F.𝓥 → G.𝓥) : Decidable (∀ x, G.𝓥𝓞.hom (𝓥 x) = F.𝓥𝓞.hom x) :=
|
||||
@Fintype.decidableForallFintype _ _ (fun _ => preFeynmanRuleDecEq𝓥 P _ _) _
|
||||
|
||||
/-- Given maps between parts of two Feynman diagrams, it is decidable to determine
|
||||
whether on mapping half-edges, the corresponding half-edge labels, edges and vertices
|
||||
are consistent. -/
|
||||
instance {F G : FeynmanDiagram P} [IsFiniteDiagram F] [IsFiniteDiagram G] [IsFinitePreFeynmanRule P]
|
||||
(𝓔 : F.𝓔 → G.𝓔) (𝓥 : F.𝓥 → G.𝓥) (𝓱𝓔 : F.𝓱𝓔 → G.𝓱𝓔) :
|
||||
Decidable (∀ x, G.𝓱𝓔To𝓔𝓥.hom (𝓱𝓔 x) = edgeVertexMap 𝓔 𝓥 (F.𝓱𝓔To𝓔𝓥.hom x)) :=
|
||||
@Fintype.decidableForallFintype _ _ (fun _ => fintypeProdHalfEdgeLabel𝓔𝓥 _ _) _
|
||||
|
||||
/-- The condition on whether a map of maps of edges, vertices and half-edges can be
|
||||
lifted to a morphism of Feynman diagrams is decidable. -/
|
||||
instance {F G : FeynmanDiagram P} [IsFiniteDiagram F] [IsFiniteDiagram G] [IsFinitePreFeynmanRule P]
|
||||
(𝓔 : F.𝓔 → G.𝓔) (𝓥 : F.𝓥 → G.𝓥) (𝓱𝓔 : F.𝓱𝓔 → G.𝓱𝓔) : Decidable (Cond 𝓔 𝓥 𝓱𝓔) :=
|
||||
instDecidableAnd
|
||||
|
|
@ -704,6 +729,7 @@ def symmetryTypeEquiv :
|
|||
left_inv _ := rfl
|
||||
right_inv _ := rfl
|
||||
|
||||
/-- For a finite Feynman diagram, the type of automorphisms of that Feynman diagram is finite. -/
|
||||
instance [IsFinitePreFeynmanRule P] [IsFiniteDiagram F] : Fintype F.SymmetryType :=
|
||||
Fintype.ofEquiv _ F.symmetryTypeEquiv.symm
|
||||
|
||||
|
|
@ -739,13 +765,15 @@ A feynman diagram is connected if its simple graph is connected.
|
|||
-/
|
||||
|
||||
/-- A relation on the vertices of Feynman diagrams. The proposition is true if the two
|
||||
vertices are not equal and are connected by a single edge. -/
|
||||
vertices are not equal and are connected by a single edge.
|
||||
This is the adjacency relation. -/
|
||||
@[simp]
|
||||
def AdjRelation : F.𝓥 → F.𝓥 → Prop := fun x y =>
|
||||
x ≠ y ∧
|
||||
∃ (a b : F.𝓱𝓔), ((F.𝓱𝓔To𝓔𝓥.hom a).2.1 = (F.𝓱𝓔To𝓔𝓥.hom b).2.1
|
||||
∧ (F.𝓱𝓔To𝓔𝓥.hom a).2.2 = x ∧ (F.𝓱𝓔To𝓔𝓥.hom b).2.2 = y)
|
||||
|
||||
/-- The condition on whether two vertices are adjacent is deciable. -/
|
||||
instance [IsFiniteDiagram F] : DecidableRel F.AdjRelation := fun _ _ =>
|
||||
@instDecidableAnd _ _ _ $
|
||||
@Fintype.decidableExistsFintype _ _ (fun _ => @Fintype.decidableExistsFintype _ _
|
||||
|
|
@ -766,19 +794,26 @@ def toSimpleGraph : SimpleGraph F.𝓥 where
|
|||
intro x h
|
||||
simp at h
|
||||
|
||||
/-- The adjacency relation for a simple graph created by a finite Feynman diagram
|
||||
is a decidable relation. -/
|
||||
instance [IsFiniteDiagram F] : DecidableRel F.toSimpleGraph.Adj :=
|
||||
instDecidableRel𝓥AdjRelationOfIsFiniteDiagram F
|
||||
|
||||
/-- For a finite feynman diagram it is deciable whether it is preconnected and has
|
||||
the Feynman diagram has a non-empty type of vertices. -/
|
||||
instance [IsFiniteDiagram F] :
|
||||
Decidable (F.toSimpleGraph.Preconnected ∧ Nonempty F.𝓥) :=
|
||||
@instDecidableAnd _ _ _ $ decidable_of_iff _ Finset.univ_nonempty_iff
|
||||
|
||||
/-- For a finite Feynman diagram it is decidable whether the simple graph corresponding to it
|
||||
is connected. -/
|
||||
instance [IsFiniteDiagram F] : Decidable F.toSimpleGraph.Connected :=
|
||||
decidable_of_iff _ (SimpleGraph.connected_iff F.toSimpleGraph).symm
|
||||
|
||||
/-- A Feynman diagram is connected if its simple graph is connected. -/
|
||||
def Connected : Prop := F.toSimpleGraph.Connected
|
||||
|
||||
/-- For a finite Feynman diagram it is decidable whether or not it is connected. -/
|
||||
instance [IsFiniteDiagram F] : Decidable (Connected F) :=
|
||||
instDecidableConnected𝓥ToSimpleGraphOfIsFiniteDiagram F
|
||||
|
||||
|
|
|
|||
|
|
@ -21,7 +21,7 @@ def Imports.NoDocStringDef (imp : Import) : MetaM UInt32 := do
|
|||
if loc.toList.length > 0 then
|
||||
IO.println "\n"
|
||||
IO.println s!"Module {imp.module} has the following definitions without doc strings:"
|
||||
IO.println (String.intercalate "\n" loc.toList)
|
||||
IO.println (String.intercalate "\n" loc.toList.mergeSort)
|
||||
pure 0
|
||||
|
||||
def Imports.NoDocStringLemma (imp : Import) : MetaM UInt32 := do
|
||||
|
|
@ -33,7 +33,7 @@ def Imports.NoDocStringLemma (imp : Import) : MetaM UInt32 := do
|
|||
if loc.toList.length > 0 then
|
||||
IO.println "\n"
|
||||
IO.println s!"Module {imp.module} has the following lemmas without doc strings:"
|
||||
IO.println (String.intercalate "\n" loc.toList)
|
||||
IO.println (String.intercalate "\n" loc.toList.mergeSort)
|
||||
pure 0
|
||||
|
||||
unsafe def main (args : List String) : IO UInt32 := do
|
||||
|
|
|
|||
Loading…
Add table
Add a link
Reference in a new issue