Same-side transmission through a presented vertex wedge

This file transports the exact same-left and same-right profiles from the concrete vertex wedge to any ambient graph equipped with a VertexWedgePresentation. It supplies both existential interfaces and the explicit mapped divisors needed when wedge decompositions are used recursively.

@[simp]

theorem Utilities.VertexWedgePresentation.transmissionExists_sameLeft_iff {K : CFGraph} {G : CFGraph} {H : CFGraph} {x : G.V} {y : H.V} (P : VertexWedgePresentation K G H x y) (p q : G.V) (tau : AspPerm) : TransmissionExists K (P.leftMap p) (P.leftMap q) tau ↔ TransmissionExists (vertexWedge G H x y) (Sum.inl p) (Sum.inl q) tau

Same-left transmission existence on a presented graph is exactly existence on its concrete vertex-wedge model.

theorem Utilities.VertexWedgePresentation.transmissionExists_sameLeft_of_profile {K : CFGraph} {G : CFGraph} {H : CFGraph} {x : G.V} {y : H.V} (P : VertexWedgePresentation K G H x y) (p q : G.V) (tau : AspPerm) (D : CFDiv G) (E : CFDiv H) (hProfile : WedgeSameLeftTransmissionProfile G H x y D E p q tau) : TransmissionExists K (P.leftMap p) (P.leftMap q) tau

A same-left factor profile gives a transmission witness on any graph carrying the corresponding wedge presentation.

theorem Utilities.VertexWedgePresentation.satisfiesTransmission_map_wedgeAddDivisor_sameLeft_of_profile {K : CFGraph} {G : CFGraph} {H : CFGraph} {x : G.V} {y : H.V} (P : VertexWedgePresentation K G H x y) (p q : G.V) (tau : AspPerm) (D : CFDiv G) (E : CFDiv H) (hProfile : WedgeSameLeftTransmissionProfile G H x y D E p q tau) : SatisfiesTransmission K (P.leftMap p) (P.leftMap q) tau (P.graphIso.mapDiv (wedgeAddDivisor G H x y D E))

Explicit ambient divisor constructed from a same-left factor profile.

@[simp]

theorem Utilities.VertexWedgePresentation.transmissionExists_sameRight_iff {K : CFGraph} {G : CFGraph} {H : CFGraph} {x : G.V} {y : H.V} (P : VertexWedgePresentation K G H x y) (p q : H.V) (tau : AspPerm) : TransmissionExists K (P.rightMap p) (P.rightMap q) tau ↔ TransmissionExists (vertexWedge G H x y) (wedgeRightVertex G H x y p) (wedgeRightVertex G H x y q) tau

Same-right transmission existence on a presented graph is exactly existence on its concrete vertex-wedge model.

theorem Utilities.VertexWedgePresentation.transmissionExists_sameRight_of_profile {K : CFGraph} {G : CFGraph} {H : CFGraph} {x : G.V} {y : H.V} (P : VertexWedgePresentation K G H x y) (p q : H.V) (tau : AspPerm) (D : CFDiv G) (E : CFDiv H) (hProfile : WedgeSameRightTransmissionProfile G H x y D E p q tau) : TransmissionExists K (P.rightMap p) (P.rightMap q) tau

A same-right factor profile gives a transmission witness on any graph carrying the corresponding wedge presentation.

theorem Utilities.VertexWedgePresentation.satisfiesTransmission_map_wedgeAddDivisor_sameRight_of_profile {K : CFGraph} {G : CFGraph} {H : CFGraph} {x : G.V} {y : H.V} (P : VertexWedgePresentation K G H x y) (p q : H.V) (tau : AspPerm) (D : CFDiv G) (E : CFDiv H) (hProfile : WedgeSameRightTransmissionProfile G H x y D E p q tau) : SatisfiesTransmission K (P.rightMap p) (P.rightMap q) tau (P.graphIso.mapDiv (wedgeAddDivisor G H x y D E))

Explicit ambient divisor constructed from a same-right factor profile.