Kurosh Cover Local

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

@[instance_reducible]

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

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

Equations

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

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

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

Lift an incoming Bass-Serre edge ending 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_costar_inv {ι : Type v} (G : ι → Type u) [(i : ι) → Group (G i)] (H : Subgroup (FreeProduct G)) (x : CoverVertex G H) (f : Quiver.Costar (coverVertexMap G H x)) : (coverPrefunctor G H).costar x (coverCostarInv G H x f) = f

theorem GraphCoveringTheory.Kurosh.Internal.coverCostar_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 : y ⟶ x) (e : z ⟶ x) (h : (coverPrefunctor G H).costar x ⟨y, d⟩ = (coverPrefunctor G H).costar x ⟨z, e⟩) : rawBassSerreEdgeDataOf G (coverEdgeMap G H d) = rawBassSerreEdgeDataOf G (coverEdgeMap G H e)

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

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

theorem GraphCoveringTheory.Kurosh.Internal.coverTarget_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 : coverEdgeTarget G H (p, e) = x) (hf : coverEdgeTarget G H (q, f) = x) : rightCosetMk (treeKuroshVertexInclusion G H e.snd.fst).range (p * (coverEdgeLetter G H e)⁻¹) = rightCosetMk (treeKuroshVertexInclusion G H e.snd.fst).range (q * (coverEdgeLetter G H e)⁻¹)

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

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

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

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

theorem GraphCoveringTheory.Kurosh.Internal.coverPrefunctor_isCovering {ι : Type v} (G : ι → Type u) [(i : ι) → Group (G i)] (H : Subgroup (FreeProduct G)) : (coverPrefunctor G H).IsCovering