ContactSlices.lean`

22 declarations, 0 contain sorry, 0 declared as axioms

def OAI.IntegralCharacterVarieties.OldContactSlice.slice line 16
Source documentation
The image of U on a NAMED old graded fiber. This definition does not choose an unrelated subspace with the same dimension.
```
def slice : Submodule R ({i // a i=k} → R) :=
…
```
lemma OAI.IntegralCharacterVarieties.OldContactSlice.mem_slice_iff line 19
theorem OAI.IntegralCharacterVarieties.OldContactSlice.invariant line 25
Source documentation
Both flag equality AND its quotient identification are used.
```
theorem invariant {f : (α → R) ≃ₗ[R] V} (h : SameFramedFlag a e f) :
    slice a e U k=slice a f U k := by
…
```
Mentions: OAI.IntegralCharacterVarieties.SameFramedFlag, OAI.IntegralCharacterVarieties.OldContactSlice.slice
lemma OAI.IntegralCharacterVarieties.OldContactSlice.grade_zero_iff line 36
def OAI.IntegralCharacterVarieties.OldContactSlice.toSlice line 55
Source documentation
The induced U map retains its inclusion in the old graded module.
```
def toSlice : ↥(U ⊓ framedPrefix a e (k+1)) →ₗ[R] slice a e U k :=
…
```
Mentions: OAI.IntegralCharacterVarieties.framedPrefix, OAI.IntegralCharacterVarieties.OldContactSlice.slice
lemma OAI.IntegralCharacterVarieties.OldContactSlice.toSlice_surjective line 59
theorem OAI.IntegralCharacterVarieties.OldContactSlice.toSlice_ker line 65
def OAI.IntegralCharacterVarieties.OldContactSlice.data line 73
Source documentation
The old adjacent interval, before any coordinate choice on U or Q.
```
def data : IntrinsicInterval.Data R V where
…
```
Mentions: OAI.IntegralCharacterVarieties.IntrinsicInterval.Data
def OAI.IntegralCharacterVarieties.OldContactSlice.gradeMap line 79
lemma OAI.IntegralCharacterVarieties.OldContactSlice.gradeMap_surjective line 82
lemma OAI.IntegralCharacterVarieties.OldContactSlice.gradeMap_ker line 96
def OAI.IntegralCharacterVarieties.OldContactSlice.namedGrade line 101
Source documentation
This is the graded module identified by the old seam, not merely an isomorphic module of the same rank. The formula on representatives is literal.
```
def namedGrade : (data a e U k).G ≃ₗ[R] ({i // a i=k} → R) :=
…
```
Mentions: OAI.IntegralCharacterVarieties.OldContactSlice.data
theorem OAI.IntegralCharacterVarieties.OldContactSlice.namedGrade_mk line 105
theorem OAI.IntegralCharacterVarieties.OldContactSlice.namedGrade_subsystem line 109
Source documentation
The intersection grade maps onto exactly the old named submodule.
```
theorem namedGrade_subsystem :
    (data a e U k).S.map (namedGrade a e U k).toLinearMap=slice a e U k := by
…
```
Mentions: OAI.IntegralCharacterVarieties.OldContactSlice.data, OAI.IntegralCharacterVarieties.OldContactSlice.namedGrade, OAI.IntegralCharacterVarieties.OldContactSlice.slice
def OAI.IntegralCharacterVarieties.OldContactSlice.namedU line 120
Source documentation
A canonical extraction of the U-quotient into the named old grade.
```
def namedU : (data a e U k).UG ≃ₗ[R] slice a e U k :=
…
```
Mentions: OAI.IntegralCharacterVarieties.OldContactSlice.data, OAI.IntegralCharacterVarieties.OldContactSlice.slice
theorem OAI.IntegralCharacterVarieties.OldContactSlice.namedU_val line 124
def OAI.IntegralCharacterVarieties.OldContactSlice.namedQ line 128
Source documentation
The NAMED old quotient, modulo its extracted submodule, is the induced quotient-subsystem grade.
```
def namedQ : (({i // a i=k} → R) ⧸ slice a e U k) ≃ₗ[R] (data a e U k).QG :=
…
```
Mentions: OAI.IntegralCharacterVarieties.OldContactSlice.slice, OAI.IntegralCharacterVarieties.OldContactSlice.data
theorem OAI.IntegralCharacterVarieties.OldContactSlice.namedQ_mk line 132
theorem OAI.IntegralCharacterVarieties.OldContactSlice.transported line 145
Source documentation
Moving the old ambient fiber moves the old subsystem with it; the named child slice itself is unchanged. This retains transports, not just ranks.
```
theorem transported {W : Type*} [AddCommGroup W] [Module R W] (t : V ≃ₗ[R] W) :
    slice a (e.trans t) (U.map t.toLinearMap) k=slice a e U k := by
…
```
Mentions: OAI.IntegralCharacterVarieties.OldContactSlice.slice

theorem OAI.IntegralCharacterVarieties.SurfacePresentation.Diagram.oldSeam_slice line 171

Source documentation

The right-hand word includes inverse CHILD transport.

theorem oldSeam_slice (s : S) (U : Submodule A (Fin (D.seamDim s) → A)) (k : ℕ) :
    OldContactSlice.slice (D.seamGrade s)
      (matrixUnitEquiv ((D.seamLeft s).eval (algebraMap R A) g.val.val)) U k=
    OldContactSlice.slice (D.seamGrade s)
      (matrixUnitEquiv ((D.seamRight s).eval (algebraMap R A) g.val.val)) U k :=
…

Mentions: OAI.IntegralCharacterVarieties.OldContactSlice.slice

theorem OAI.IntegralCharacterVarieties.SurfacePresentation.Diagram.oldVertex_slice line 179
Source documentation
Split, merge, continuation and interchange use their old vertex comparison. At an interchange its grade is the coarsened A⊕B grade, so this is the SAME U_* on which the complementary contact construction operates.
```
theorem oldVertex_slice (v : V)
    (U : Submodule A ((D.vertexComparison g.val.val v).Target → A)) (k : ℕ) :
    OldContactSlice.slice (D.vertexComparison g.val.val v).grade
      (D.vertexComparison g.val.val v).left.linearEquiv U k=
    OldContactSlice.slice (D.vertexComparison g.val.val v).grade
      (D.vertexComparison g.val.val v).right.linearEquiv U k :=
…
```
Mentions: OAI.IntegralCharacterVarieties.OldContactSlice.slice
theorem OAI.IntegralCharacterVarieties.SurfacePresentation.Diagram.oldVertex_extraction line 188