RegularStrips.lean`

GitHub source file

26 declarations, 0 contain sorry, 0 declared as axioms

def OAI.IntegralCharacterVarieties.ExactSequenceChart.Chart.normalized line 15
Source documentation
A chart normalized on its identified quotient.
```
def normalized : (U × Q) ≃ₗ[R] V :=
…
```
theorem OAI.IntegralCharacterVarieties.ExactSequenceChart.Chart.normalized_apply line 18
theorem OAI.IntegralCharacterVarieties.ExactSequenceChart.Chart.normalized_inl line 22
theorem OAI.IntegralCharacterVarieties.ExactSequenceChart.Chart.g_normalized line 25
theorem OAI.IntegralCharacterVarieties.ExactSequenceChart.Chart.left_normalized line 28
theorem OAI.IntegralCharacterVarieties.ExactSequenceChart.Chart.normalized_symm line 31
def OAI.IntegralCharacterVarieties.IntrinsicInterval.Transport.stripShear line 48
Source documentation
The free extension term is read from old transport and the chosen splittings. It is not set to zero or replaced by a block-diagonal premise.
```
def stripShear : D.QG →ₗ[R] E.UG :=
…
```
def OAI.IntegralCharacterVarieties.IntrinsicInterval.Transport.stripForward line 52
Source documentation
Old transport in independently chosen normalized regular frames.
```
def stripForward : (D.UG × D.QG) ≃ₗ[R] (E.UG × E.QG) :=
…
```
theorem OAI.IntegralCharacterVarieties.IntrinsicInterval.Transport.onGrade_normalized line 55
theorem OAI.IntegralCharacterVarieties.IntrinsicInterval.Transport.stripForward_apply line 61
Source documentation
Both diagonal maps are the induced subquotient transports; only the permitted strictly lowering block is free.
```
theorem stripForward_apply (u : D.UG) (q : D.QG) :
    g.stripForward C B (u,q)=
      (g.onUGrade u+g.stripShear C B q,g.onQGrade q) := by
…
```
def OAI.IntegralCharacterVarieties.IntrinsicInterval.Transport.childDiagonal line 72
Source documentation
Inverse CHILD transport gives the correct oriented seam convention.
```
def childDiagonal : (E.UG × E.QG) ≃ₗ[R] (D.UG × D.QG) :=
…
```
def OAI.IntegralCharacterVarieties.IntrinsicInterval.Transport.stripResidual line 75
theorem OAI.IntegralCharacterVarieties.IntrinsicInterval.Transport.stripResidual_apply line 78
theorem OAI.IntegralCharacterVarieties.IntrinsicInterval.Transport.stripForward_comp line 88
Source documentation
Successive strip charts reconstruct the original composite transport.
```
theorem stripForward_comp :
    (g.followedBy h).stripForward C A=
      (g.stripForward C B).trans (h.stripForward B A) := by
…
```
Mentions: OAI.IntegralCharacterVarieties.IntrinsicInterval.Transport.stripForward
theorem OAI.IntegralCharacterVarieties.IntrinsicInterval.Transport.stripShear_comp line 100
Source documentation
The shear cocycle is forced by transport. This is the compatibility needed when a retained old occurrence is traversed through several patches.
```
theorem stripShear_comp :
    (g.followedBy h).stripShear C A=
      h.onUGrade.toLinearMap.comp (g.stripShear C B)+
        (h.stripShear B A).comp g.onQGrade.toLinearMap := by
…
```
Mentions: OAI.IntegralCharacterVarieties.IntrinsicInterval.Transport.stripShear
def OAI.IntegralCharacterVarieties.RegularStripCoordinates.grade line 124
def OAI.IntegralCharacterVarieties.RegularStripCoordinates.coordinates line 126
def OAI.IntegralCharacterVarieties.RegularStripCoordinates.residualCoordinates line 129
theorem OAI.IntegralCharacterVarieties.RegularStripCoordinates.residual_lower line 132
theorem OAI.IntegralCharacterVarieties.RegularStripCoordinates.residual_upper line 139
theorem OAI.IntegralCharacterVarieties.RegularStripCoordinates.residual_identified_flag line 146
Source documentation
Old parallel transport gives the IDENTIFIED flag equations in the regular lower two-block seam, with its full upper shear retained.
```
theorem residual_identified_flag :
    SameCoordinateFlag (grade (L:=L) (T:=T)) (residualCoordinates g C B u q) := by
…
```
Mentions: OAI.IntegralCharacterVarieties.SameCoordinateFlag, OAI.IntegralCharacterVarieties.RegularStripCoordinates.grade, OAI.IntegralCharacterVarieties.RegularStripCoordinates.residualCoordinates
def OAI.IntegralCharacterVarieties.RegularStripCoordinates.parentFrame line 164
def OAI.IntegralCharacterVarieties.RegularStripCoordinates.childFrame line 167
theorem OAI.IntegralCharacterVarieties.RegularStripCoordinates.comparison_is_residual line 170
theorem OAI.IntegralCharacterVarieties.RegularStripCoordinates.regular_seam_law line 178
Source documentation
This is precisely the source regular seam law: transported source frame and target frame with inverse child transports have the same named grades.
```
theorem regular_seam_law :
    SameFramedFlag (grade (L:=L) (T:=T)) (parentFrame g C u q) (childFrame g B u q) := by
…
```
Mentions: OAI.IntegralCharacterVarieties.SameFramedFlag, OAI.IntegralCharacterVarieties.RegularStripCoordinates.grade, OAI.IntegralCharacterVarieties.RegularStripCoordinates.parentFrame, OAI.IntegralCharacterVarieties.RegularStripCoordinates.childFrame
theorem OAI.IntegralCharacterVarieties.IntrinsicInterval.Data.actual_chart_exists line 191
Source documentation
Applied to the induced old interval: exactness is already proved, not a hypothesis of the forward producer. Over a field every quotient is free.
```
theorem actual_chart_exists : Nonempty (Chart D.includeU D.projectQ) :=
…
```