PortValues.lean`

GitHub source file

6 declarations, 0 contain sorry, 0 declared as axioms

lemma OAI.IntegralCharacterVarieties.SurfacePresentation.Diagram.frameValues_canonical line 12
Source documentation
Frame values depend only on the ports and ranks, hence are unchanged by the choice of boundary enumeration.
```
lemma frameValues_canonical {F S V K : Type} {arity : S → ℕ}
    [CommRing K] [Finite S] (D : Diagram F S V arity)
    (frames : D.PortFrames (R:=K)) (s : S) (b : Bool) :
…
```
Mentions: OAI.IntegralCharacterVarieties.SurfacePresentation.Diagram
lemma OAI.IntegralCharacterVarieties.SurfacePresentation.Diagram.valuesFromPorts_frame_canonical line 20
Source documentation
A frame generator evaluates in the canonical boundary presentation using the same port frame.
```
lemma valuesFromPorts_frame_canonical {F S V K : Type} {arity : S → ℕ}
    [CommRing K] [Finite S] (D : Diagram F S V arity)
    (frames : D.PortFrames (R:=K)) (side : D.SideValues (R:=K))
…
```
Mentions: OAI.IntegralCharacterVarieties.SurfacePresentation.Diagram
lemma OAI.IntegralCharacterVarieties.SurfacePresentation.Diagram.valuesFromPorts_frameCoordinates_canonical line 28
Source documentation
Evaluating and reindexing a frame does not depend on the boundary enumeration.
```
lemma valuesFromPorts_frameCoordinates_canonical {F S V K α β : Type} {arity : S → ℕ}
    [CommRing K] [Finite S] [Fintype α] [Fintype β] (D : Diagram F S V arity)
    (frames : D.PortFrames (R:=K)) (side : D.SideValues (R:=K))
…
```
Mentions: OAI.IntegralCharacterVarieties.SurfacePresentation.Diagram
lemma OAI.IntegralCharacterVarieties.SurfacePresentation.Diagram.valuesFromPorts_parentCoordinates_canonical line 38
Source documentation
The evaluated parent coordinates use only the port and rank data.
```
lemma valuesFromPorts_parentCoordinates_canonical {F S V K R α : Type} {arity : S → ℕ}
    [CommRing K] [CommRing R] [Finite S] [Fintype α] (D : Diagram F S V arity)
    (frames : D.PortFrames (R:=K)) (side : D.SideValues (R:=K))
…
```
Mentions: OAI.IntegralCharacterVarieties.SurfacePresentation.Diagram
lemma OAI.IntegralCharacterVarieties.SurfacePresentation.Diagram.valuesFromPorts_childCoordinates_canonical line 55
Source documentation
The evaluated inverse child coordinates use only the port and rank data.
```
lemma valuesFromPorts_childCoordinates_canonical {F S V K R α : Type} {arity : S → ℕ}
    [CommRing K] [CommRing R] [Finite S] [Fintype α] (D : Diagram F S V arity)
    (frames : D.PortFrames (R:=K)) (side : D.SideValues (R:=K))
…
```
Mentions: OAI.IntegralCharacterVarieties.SurfacePresentation.Diagram
lemma OAI.IntegralCharacterVarieties.SurfacePresentation.Diagram.valuesFromPorts_childWord_coordinates line 69
Source documentation
Child coordinates for values induced by ports and side transports.
```
lemma valuesFromPorts_childWord_coordinates
    {F S V R K : Type} {arity : S → ℕ} [CommRing R] [Field K]
    (D : Diagram F S V arity) (s : S) (φ : R →+* K)
    (frames : D.PortFrames (R:=K)) (side : D.SideValues (R:=K))
…
```
Mentions: OAI.IntegralCharacterVarieties.SurfacePresentation.Diagram