OAI/AlgebraicGeometry/CharacterVarieties/Frames/FramedFlags.lean

GitHub source file

45 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.IntegralCharacterVarieties.SurfacePresentation.Diagram.portNamedColumns line 12
2. def OAI.IntegralCharacterVarieties.SurfacePresentation.Diagram.portChildMatch line 17
3. lemma OAI.IntegralCharacterVarieties.SurfacePresentation.Diagram.portParentRank_match line 21
4. lemma OAI.IntegralCharacterVarieties.SurfacePresentation.Diagram.side_child_congr line 25
5. lemma OAI.IntegralCharacterVarieties.SurfacePresentation.Diagram.portChildRank_match line 29
6. def OAI.IntegralCharacterVarieties.SurfacePresentation.Diagram.portColumnMatch line 38
7. def OAI.IntegralCharacterVarieties.SurfacePresentation.Diagram.portParentMatch line 42
8. def OAI.IntegralCharacterVarieties.SurfacePresentation.Diagram.namedColumnsMatch line 46
9. lemma OAI.IntegralCharacterVarieties.SurfacePresentation.Diagram.namedColumnsMatch_refl line 51
10. lemma OAI.IntegralCharacterVarieties.SurfacePresentation.Diagram.portColumnMatch_named_forward line 57
11. lemma OAI.IntegralCharacterVarieties.SurfacePresentation.Diagram.portColumnMatch_named line 71
12. lemma OAI.IntegralCharacterVarieties.SurfacePresentation.Diagram.portColumnMatch_named_left line 77
13. lemma OAI.IntegralCharacterVarieties.SurfacePresentation.Diagram.namedColumnsMatch_index line 85
14. lemma OAI.IntegralCharacterVarieties.SurfacePresentation.Diagram.portColumnMatch_index line 93
15. lemma OAI.IntegralCharacterVarieties.SurfacePresentation.Diagram.portColumnMatch_from_index line 113
16. lemma OAI.IntegralCharacterVarieties.SurfacePresentation.Diagram.portParentMatch_from_index line 122
17. lemma OAI.IntegralCharacterVarieties.SameFramedFlag.refl line 139
18. lemma OAI.IntegralCharacterVarieties.SameFramedFlag.symm line 140
19. lemma OAI.IntegralCharacterVarieties.SameFramedFlag.trans line 145
20. lemma OAI.IntegralCharacterVarieties.SameFramedFlag.postcompose line 150

    Source documentation

    Parent transport preserves the named grade maps.

    lemma postcompose (hf : SameFramedFlag a f g) (e : V ≃ₗ[R] W) :
        SameFramedFlag a (f.trans e) (g.trans e) := by
    …

    Mentions: OAI.IntegralCharacterVarieties.SameFramedFlag

21. lemma OAI.IntegralCharacterVarieties.OccurrenceIncidence.VertexTable.AtomicData.reframe_seam_post line 175
22. lemma OAI.IntegralCharacterVarieties.NamedBandGrades.IdentifiedBand.mirror_basis_at_color line 204
23. lemma OAI.IntegralCharacterVarieties.NamedBandGrades.IdentifiedBand.mirror_principal_basis line 227
24. lemma OAI.IntegralCharacterVarieties.NamedBandGrades.IdentifiedBand.mirror_principal_frame line 250
25. def OAI.IntegralCharacterVarieties.NamedBandGrades.IdentifiedBand.mirrorAlignedFrame line 271

    Source documentation

    The mirror frame in the coordinate labels of the original port.

    def mirrorAlignedFrame (T : MatrixIso K (Fin r) (Fin r))
        (v : Fin (w.shape.atomicBand.length+1)) (p : (w.shape.atomicBand.kind v).table.Port) :=
    …

    Mentions: OAI.IntegralCharacterVarieties.MatrixIso

26. lemma OAI.IntegralCharacterVarieties.NamedBandGrades.IdentifiedBand.mirror_canonical_frame line 280
27. def OAI.IntegralCharacterVarieties.NamedBandGrades.IdentifiedBand.mirrorFirstFrame line 293
28. def OAI.IntegralCharacterVarieties.NamedBandGrades.IdentifiedBand.mirrorLastFrame line 297
29. lemma OAI.IntegralCharacterVarieties.NamedBandGrades.IdentifiedBand.mirrorFirstFrame_eq line 302
30. lemma OAI.IntegralCharacterVarieties.NamedBandGrades.IdentifiedBand.mirrorLastFrame_eq line 306
31. lemma OAI.IntegralCharacterVarieties.NamedBandGrades.IdentifiedBand.mirrorFirstFrame_holds line 310
32. lemma OAI.IntegralCharacterVarieties.NamedBandGrades.IdentifiedBand.mirrorLastFrame_holds line 316
33. lemma OAI.IntegralCharacterVarieties.NamedBandGrades.cut_short_first line 336

    Source documentation

    The short seam at the original negative endpoint has identity parent and child transports and preserves each named quotient.

    lemma cut_short_first : SameFramedFlag (fun i : ((i : Fin n) × Fin (s i)) => i.1.val) f w.firstFrame := w.firstFrame_holds.symm

    Mentions: OAI.IntegralCharacterVarieties.SameFramedFlag

34. lemma OAI.IntegralCharacterVarieties.NamedBandGrades.cut_short_last line 340

    Source documentation

    The original child transports remain on the positive port, while the last frame is transported by the cut handle coordinate J.

    lemma cut_short_last (hold : SameFramedFlag (fun i : ((i : Fin n) × Fin (s i)) => i.1.val) (f.trans P) (U.trans g)) :
        SameFramedFlag (fun i : ((i : Fin n) × Fin (s i)) => i.1.val) (w.lastFrame.trans J) (U.trans g) := by
    …

    Mentions: OAI.IntegralCharacterVarieties.SameFramedFlag

35. def OAI.IntegralCharacterVarieties.NamedBandGrades.cutInnerLinear line 348

    Source documentation

    The inner boundary is the inverse-cut word T⁻¹ J⁻¹ P T.

    def cutInnerLinear : (Fin r → K) ≃ₗ[K] (Fin r → K) :=
    …

36. lemma OAI.IntegralCharacterVarieties.NamedBandGrades.cutInner_after_mirror line 351
37. lemma OAI.IntegralCharacterVarieties.NamedBandGrades.cut_short_mirror line 362

    Source documentation

    The mirror wraps in the opposite direction with principal basis T⁻¹.

    lemma cut_short_mirror : SameFramedFlag (fun i : ((i : Fin n) × Fin (s i)) => i.1.val)
        ((w.mirrorFirstFrame T).trans (cutInnerLinear (r:=r) P J T)) (w.mirrorLastFrame T) := by
    …

    Mentions: OAI.IntegralCharacterVarieties.SameFramedFlag, OAI.IntegralCharacterVarieties.NamedBandGrades.cutInnerLinear

38. lemma OAI.IntegralCharacterVarieties.SurfacePresentation.Diagram.localFrameFlag_match line 377

    Source documentation

    Framed-flag transport respecting the seam child enumeration.

    lemma localFrameFlag_match (f : D.PortFrames (R:=R))
    …

39. lemma OAI.IntegralCharacterVarieties.SurfacePresentation.Diagram.frameValues_seam_flag_of_ports line 412

    Source documentation

    Attached negative and positive ports determine the seam framed-flag condition.

    lemma frameValues_seam_flag_of_ports (f : D.PortFrames (R:=R))
    …

40. lemma OAI.IntegralCharacterVarieties.MatrixIso.sameFramedFlag_of_coordinates line 445
41. lemma OAI.IntegralCharacterVarieties.MatrixIso.sameFramedFlag_of_matching_coordinates line 457
42. lemma OAI.IntegralCharacterVarieties.MatrixIso.linearEquiv_trans_eq line 479
43. lemma OAI.IntegralCharacterVarieties.SurfacePresentation.Diagram.seamHolds_of_coordinates line 494

    Source documentation

    Reindex all four factors of a seam into common coordinates, including the parent and child transports.

    lemma seamHolds_of_coordinates
        (e : α ≃ Fin (D.seamDim s)) (f : β ≃ Fin (D.seamDim s))
        (a : α → ℕ) (x y : (α → K) ≃ₗ[K] (β → K))
        (p : (β → K) ≃ₗ[K] (β → K)) (u : (α → K) ≃ₗ[K] (α → K))
        (ha : ∀ i,D.seamGrade s (e i)=a i)
        (hx : ((MatrixIso.unit (g (.frame s false))).reindex e f).linearEquiv=x)
        (hy : ((MatrixIso.unit (g (.frame s true))).reindex e f).linearEquiv=y)
        (hp : ((MatrixIso.unit ((D.parentWord s).eval φ g)).reindex f f).linearEquiv=p)
        (hu : ((MatrixIso.unit ((Term.block (D.childDim s)
          (fun j => Term.inv (D.childWord s j))).eval φ g)).reindex e e).linearEquiv=u)
        (hh : SameFramedFlag a (x.trans p) (u.trans y)) :
        SameFramedFlag (D.seamGrade s)
    …

    Mentions: OAI.IntegralCharacterVarieties.MatrixIso.unit, OAI.IntegralCharacterVarieties.SameFramedFlag

44. lemma OAI.IntegralCharacterVarieties.SurfacePresentation.Diagram.parentWord_coordinates line 521

    Source documentation

    Transport of the parent word over its coefficient ring.

    lemma parentWord_coordinates {n : ℕ}
        (h : D.rank (D.ports.facet ⟨s,none⟩)=n)
        (p : (Matrix (Fin n) (Fin n) K)ˣ)
        (hp : rebaseUnit h (g (.side ⟨s,none⟩))=p)
        (f : Fin n ≃ Fin (D.seamDim s))
        (hf : f=finCongr (h.symm.trans (D.seamRank s))) :
        ((MatrixIso.unit ((D.parentWord s).eval φ g)).reindex f f).linearEquiv=
          (MatrixIso.unit p).linearEquiv := by
    …

    Mentions: OAI.IntegralCharacterVarieties.SurfacePresentation.Diagram.rebaseUnit, OAI.IntegralCharacterVarieties.MatrixIso.unit

45. lemma OAI.IntegralCharacterVarieties.SurfacePresentation.Diagram.childWord_coordinates line 542

    Source documentation

    A block child inverse preserves named fibers under a child-index identification over the coefficient ring.

    lemma childWord_coordinates {m : ℕ} (d : Fin m → ℕ)
        (c : Fin m ≃ Fin (arity s))
        (hc : ∀ i,d i=D.childDim s (c i))
        (old : (i : Fin m) → (Matrix (Fin (d i)) (Fin (d i)) K)ˣ)
        (ho : ∀ i,rebaseUnit (hc i).symm (g (.side ⟨s,some (c i)⟩))=old i)
        (e : ((i : Fin m) × Fin (d i)) ≃ Fin (D.seamDim s))
        (he : e=(Equiv.sigmaCongr c (fun i=>finCongr (hc i))).trans
          (blockIndex (D.childDim s)).symm) :
        ((MatrixIso.unit ((Term.block (D.childDim s)
          (fun j => Term.inv (D.childWord s j))).eval φ g)).reindex e e).linearEquiv=
          (MatrixIso.block (fun i=>MatrixIso.unit (old i)⁻¹)).linearEquiv := by
    …

    Mentions: OAI.IntegralCharacterVarieties.SurfacePresentation.Diagram.rebaseUnit, OAI.IntegralCharacterVarieties.MatrixIso.unit, OAI.IntegralCharacterVarieties.MatrixIso.block