Kurosh Cover Star

Adapted for Lean Pool from Arthur742Ramos/KuroshSubgroupTheorem, commit 911707126c8b9bb0c764bf853008fe1053c0aad9: imports, API compatibility, and proof organization were revised.

@[instance_reducible]

noncomputable def GraphCoveringTheory.Kurosh.kuroshCoverStarDecidableEq (α : Type u_1) : DecidableEq α

Classical equality used locally in this part of the Kurosh construction.

Equations

• GraphCoveringTheory.Kurosh.kuroshCoverStarDecidableEq α = Classical.decEq α

theorem GraphCoveringTheory.Kurosh.Internal.rawBassSerreEdgeData_action_injective {ι : Type v} (G : ι → Type u) [(i : ι) → Group (G i)] (H : Subgroup (FreeProduct G)) {h k : ↥H} (e : rawBassSerreEdgeData G) (he : ↑h • e = ↑k • e) : h = k

theorem GraphCoveringTheory.Kurosh.Internal.rawBassSerreEdgeDataOf_cast {ι : Type v} (G : ι → Type u) [(i : ι) → Group (G i)] {a b a' b' : RawBassSerreVertex G} (ha : a = a') (hb : b = b') (e : a ⟶ b) : rawBassSerreEdgeDataOf G (Quiver.Hom.cast ha hb e) = rawBassSerreEdgeDataOf G e

theorem GraphCoveringTheory.Kurosh.Internal.coverEdgeMap_data {ι : Type v} (G : ι → Type u) [(i : ι) → Group (G i)] (H : Subgroup (FreeProduct G)) {x y : CoverVertex G H} (d : x ⟶ y) : rawBassSerreEdgeDataOf G (coverEdgeMap G H d) = ↑((treeKuroshProductToH G H) (↑d).1 * quotientEdgeCoherentSourceAlign G H (↑d).2.snd.snd) • quotientEdgeRawData G H (↑d).2.snd.snd

theorem GraphCoveringTheory.Kurosh.Internal.coverVertexMap_orbit {ι : Type v} (G : ι → Type u) [(i : ι) → Group (G i)] (H : Subgroup (FreeProduct G)) (x : CoverVertex G H) : actionOrbitMk (↥H) (RawBassSerreVertex G) (coverVertexMap G H x) = x.fst

noncomputable def GraphCoveringTheory.Kurosh.rawEdgeAlign {ι : Type v} (G : ι → Type u) [(i : ι) → Group (G i)] (H : Subgroup (FreeProduct G)) {e f : rawBassSerreEdgeData G} (h : actionOrbitMk (↥H) (rawBassSerreEdgeData G) e = actionOrbitMk (↥H) (rawBassSerreEdgeData G) f) : ↥H

Choose a subgroup element translating between representatives of the same edge orbit.

Equations

• GraphCoveringTheory.Kurosh.rawEdgeAlign G H h = Classical.choose ⋯

theorem GraphCoveringTheory.Kurosh.Internal.rawEdgeAlign_spec {ι : Type v} (G : ι → Type u) [(i : ι) → Group (G i)] (H : Subgroup (FreeProduct G)) {e f : rawBassSerreEdgeData G} (h : actionOrbitMk (↥H) (rawBassSerreEdgeData G) e = actionOrbitMk (↥H) (rawBassSerreEdgeData G) f) : ↑(rawEdgeAlign G H h) • e = f

theorem GraphCoveringTheory.Kurosh.Internal.quotientEdgeRawData_cast {ι : Type v} (G : ι → Type u) [(i : ι) → Group (G i)] (H : Subgroup (FreeProduct G)) {a b a' b' : RawBassSerreOrbitVertex G H} (ha : a = a') (hb : b = b') (e : a ⟶ b) : quotientEdgeRawData G H (Quiver.Hom.cast ha hb e) = quotientEdgeRawData G H e

theorem GraphCoveringTheory.Kurosh.Internal.quotientEdgeRawData_orbit_of_raw {ι : Type v} (G : ι → Type u) [(i : ι) → Group (G i)] (H : Subgroup (FreeProduct G)) {a b : RawBassSerreVertex G} (f : a ⟶ b) : actionOrbitMk (↥H) (rawBassSerreEdgeData G) (quotientEdgeRawData G H (rawBassSerreOrbitEdgeMap G H f)) = actionOrbitMk (↥H) (rawBassSerreEdgeData G) (rawBassSerreEdgeDataOf G f)

theorem GraphCoveringTheory.Kurosh.Internal.rawStar_eq_of_data_eq {ι : Type v} (G : ι → Type u) [(i : ι) → Group (G i)] {a b c : RawBassSerreVertex G} (f : a ⟶ b) (g : a ⟶ c) (h : rawBassSerreEdgeDataOf G f = rawBassSerreEdgeDataOf G g) : ⟨b, f⟩ = ⟨c, g⟩

noncomputable def GraphCoveringTheory.Kurosh.coverStarInv {ι : Type v} (G : ι → Type u) [(i : ι) → Group (G i)] (H : Subgroup (FreeProduct G)) (x : CoverVertex G H) : Quiver.Star (coverVertexMap G H x) → Quiver.Star x

Lift an outgoing Bass-Serre edge starting at the image of a covering vertex.

Equations

• One or more equations did not get rendered due to their size.

theorem GraphCoveringTheory.Kurosh.Internal.coverPrefunctor_star_inv {ι : Type v} (G : ι → Type u) [(i : ι) → Group (G i)] (H : Subgroup (FreeProduct G)) (x : CoverVertex G H) (f : Quiver.Star (coverVertexMap G H x)) : (coverPrefunctor G H).star x (coverStarInv G H x f) = f

theorem GraphCoveringTheory.Kurosh.Internal.coverStar_data_eq {ι : Type v} (G : ι → Type u) [(i : ι) → Group (G i)] (H : Subgroup (FreeProduct G)) (x : CoverVertex G H) {y z : CoverVertex G H} (d : x ⟶ y) (e : x ⟶ z) (h : (coverPrefunctor G H).star x ⟨y, d⟩ = (coverPrefunctor G H).star x ⟨z, e⟩) : rawBassSerreEdgeDataOf G (coverEdgeMap G H d) = rawBassSerreEdgeDataOf G (coverEdgeMap G H e)

theorem GraphCoveringTheory.Kurosh.Internal.coverEdge_eq_of_val_eq {ι : Type v} (G : ι → Type u) [(i : ι) → Group (G i)] (H : Subgroup (FreeProduct G)) {a b c : RawBassSerreOrbitVertex G H} (e : a ⟶ b) (f : a ⟶ c) (h : ↑e = ↑f) : ⟨a, ⟨b, e⟩⟩ = ⟨a, ⟨c, f⟩⟩

theorem GraphCoveringTheory.Kurosh.Internal.coverEdge_eq_of_base_val_eq {ι : Type v} (G : ι → Type u) [(i : ι) → Group (G i)] (H : Subgroup (FreeProduct G)) {e f : CoverEdge G H} (hs : e.fst = f.fst) (hv : ↑e.snd.snd = ↑f.snd.snd) : e = f

theorem GraphCoveringTheory.Kurosh.Internal.coverSource_coset_eq_of_edge_eq {ι : Type v} (G : ι → Type u) [(i : ι) → Group (G i)] (H : Subgroup (FreeProduct G)) {x : CoverVertex G H} {p q : CoverSource G H} {e f : CoverEdge G H} (hef : e = f) (he : coverEdgeSource G H (p, e) = x) (hf : coverEdgeSource G H (q, f) = x) : rightCosetMk (treeKuroshVertexInclusion G H e.fst).range p = rightCosetMk (treeKuroshVertexInclusion G H e.fst).range q

theorem GraphCoveringTheory.Kurosh.Internal.coverEdge_base_eq_of_map_data_eq {ι : Type v} (G : ι → Type u) [(i : ι) → Group (G i)] (H : Subgroup (FreeProduct G)) (x : CoverVertex G H) {y z : CoverVertex G H} (d : x ⟶ y) (e : x ⟶ z) (h : rawBassSerreEdgeDataOf G (coverEdgeMap G H d) = rawBassSerreEdgeDataOf G (coverEdgeMap G H e)) : (↑d).2 = (↑e).2

theorem GraphCoveringTheory.Kurosh.Internal.coverEdge_pair_eq_of_map_data_eq {ι : Type v} (G : ι → Type u) [(i : ι) → Group (G i)] (H : Subgroup (FreeProduct G)) (x : CoverVertex G H) {y z : CoverVertex G H} (d : x ⟶ y) (e : x ⟶ z) (h : rawBassSerreEdgeDataOf G (coverEdgeMap G H d) = rawBassSerreEdgeDataOf G (coverEdgeMap G H e)) : ↑d = ↑e

theorem GraphCoveringTheory.Kurosh.Internal.coverStar_eq_of_pair_eq {ι : Type v} (G : ι → Type u) [(i : ι) → Group (G i)] (H : Subgroup (FreeProduct G)) {x y z : CoverVertex G H} (d : x ⟶ y) (e : x ⟶ z) (hp : ↑d = ↑e) : ⟨y, d⟩ = ⟨z, e⟩

theorem GraphCoveringTheory.Kurosh.Internal.coverPrefunctor_star_injective {ι : Type v} (G : ι → Type u) [(i : ι) → Group (G i)] (H : Subgroup (FreeProduct G)) (x : CoverVertex G H) : Function.Injective ((coverPrefunctor G H).star x)

theorem GraphCoveringTheory.Kurosh.Internal.coverPrefunctor_star_bijective {ι : Type v} (G : ι → Type u) [(i : ι) → Group (G i)] (H : Subgroup (FreeProduct G)) (x : CoverVertex G H) : Function.Bijective ((coverPrefunctor G H).star x)