ProCGroups.Categorical.PushoutSquares
This module studies pushout squares for pro cgroups. The abstract free product used as the carrier before imposing pushout relations. The relators identifying the two legs of a group cospan inside the free product.
import
- Mathlib.GroupTheory.Coprod.Basic
- ProCGroups.Profinite.Basic
- ProCGroups.Topologies.ContinuousMulEquiv
abbrev PushoutFreeProduct (H₁ H₂ : Type u) [Group H₁] [Group H₂] :=
Monoid.Coprod H₁ H₂The abstract free product used as the carrier before imposing pushout relations.
def pushoutRelators (β₁ : H →* H₁) (β₂ : H →* H₂) :
Set (PushoutFreeProduct H₁ H₂) :=
{z | ∃ h : H,
z = (Monoid.Coprod.inl (β₁ h) : PushoutFreeProduct H₁ H₂)⁻¹ *
(Monoid.Coprod.inr (β₂ h) : PushoutFreeProduct H₁ H₂)}The relators identifying the two legs of a group cospan inside the free product.
def pushoutNormalClosure (β₁ : H →* H₁) (β₂ : H →* H₂) :
Subgroup (PushoutFreeProduct H₁ H₂) :=
Subgroup.normalClosure (pushoutRelators β₁ β₂)The normal subgroup generated by the cospan-identifying relators.
instance pushoutNormalClosure_normal (β₁ : H →* H₁) (β₂ : H →* H₂) :
(pushoutNormalClosure β₁ β₂).Normal :=
Subgroup.normalClosure_normalThe relator closure used in the concrete pushout is normal.
abbrev Carrier (β₁ : H →* H₁) (β₂ : H →* H₂) :=
PushoutFreeProduct H₁ H₂ ⧸ pushoutNormalClosure β₁ β₂Algebraic group pushout carrier: the free product modulo the normal closure of \(\operatorname{inl}(\beta_1 h)^{-1} * \operatorname{inr}(\beta_2 h)\).
def inl (β₁ : H →* H₁) (β₂ : H →* H₂) :
H₁ →* Carrier β₁ β₂ :=
(QuotientGroup.mk' (pushoutNormalClosure β₁ β₂)).comp Monoid.Coprod.inlThe left structural map into the algebraic pushout.
def inr (β₁ : H →* H₁) (β₂ : H →* H₂) :
H₂ →* Carrier β₁ β₂ :=
(QuotientGroup.mk' (pushoutNormalClosure β₁ β₂)).comp Monoid.Coprod.inrThe right structural map into the algebraic pushout.
theorem inl_comp_eq_inr_comp
(β₁ : H →* H₁) (β₂ : H →* H₂) :
(inl β₁ β₂).comp β₁ = (inr β₁ β₂).comp β₂The algebraic pushout maps coequalize the original cospan.
Show proof
by
ext h
change QuotientGroup.mk' (pushoutNormalClosure β₁ β₂)
(Monoid.Coprod.inl (β₁ h) : PushoutFreeProduct H₁ H₂) =
QuotientGroup.mk' (pushoutNormalClosure β₁ β₂)
(Monoid.Coprod.inr (β₂ h) : PushoutFreeProduct H₁ H₂)
apply QuotientGroup.eq.2
exact Subgroup.subset_normalClosure ⟨h, rfl⟩Proof. Unfold the algebraic pushout as the quotient of the free product by the normal closure of the identifying relators. The two canonical maps agree on the common subgroup by construction, and a descent map out of the pushout is obtained from compatible maps on the two factors. The defining relators are killed exactly by the compatibility hypothesis, and uniqueness follows from the universal property of the quotient and the free product.
□noncomputable def concretePushoutDesc
(β₁ : H →* H₁) (β₂ : H →* H₂)
{K : Type u} [Group K]
(φ₁ : H₁ →* K) (φ₂ : H₂ →* K)
(hφ : φ₁.comp β₁ = φ₂.comp β₂) :
Carrier β₁ β₂ →* K :=
let F : PushoutFreeProduct H₁ H₂ →* K := Monoid.Coprod.lift φ₁ φ₂
QuotientGroup.lift (pushoutNormalClosure β₁ β₂) F <| by
refine Subgroup.normalClosure_le_normal ?_
rintro z ⟨h, rfl⟩
change F ((Monoid.Coprod.inl (β₁ h) : PushoutFreeProduct H₁ H₂)⁻¹ *
(Monoid.Coprod.inr (β₂ h) : PushoutFreeProduct H₁ H₂)) = 1
rw [map_mul, map_inv]
have hleft :
F (Monoid.Coprod.inl (β₁ h) : PushoutFreeProduct H₁ H₂) = φ₁ (β₁ h) :=
DFunLike.congr_fun (Monoid.Coprod.lift_comp_inl φ₁ φ₂) (β₁ h)
have hright :
F (Monoid.Coprod.inr (β₂ h) : PushoutFreeProduct H₁ H₂) = φ₂ (β₂ h) :=
DFunLike.congr_fun (Monoid.Coprod.lift_comp_inr φ₁ φ₂) (β₂ h)
have hcomp : φ₁ (β₁ h) = φ₂ (β₂ h) := DFunLike.congr_fun hφ h
rw [hleft, hright, hcomp]
simp only [inv_mul_cancel]The concrete pushout descent map is characterized by its compatibility with the two canonical inclusions.
@[simp 900] theorem concretePushoutDesc_inl
(β₁ : H →* H₁) (β₂ : H →* H₂)
{K : Type u} [Group K]
(φ₁ : H₁ →* K) (φ₂ : H₂ →* K)
(hφ : φ₁.comp β₁ = φ₂.comp β₂) :
(concretePushoutDesc β₁ β₂ φ₁ φ₂ hφ).comp (inl β₁ β₂) = φ₁The concrete pushout descent map is compatible with the left inclusion.
Show proof
by
ext x
change concretePushoutDesc β₁ β₂ φ₁ φ₂ hφ
(QuotientGroup.mk' (pushoutNormalClosure β₁ β₂)
(Monoid.Coprod.inl x : PushoutFreeProduct H₁ H₂)) = φ₁ x
simp only [concretePushoutDesc, QuotientGroup.mk'_apply, QuotientGroup.lift_mk, Monoid.Coprod.lift_apply_inl]Proof. Unfold the algebraic pushout as the quotient of the free product by the normal closure of the identifying relators. The two canonical maps agree on the common subgroup by construction, and a descent map out of the pushout is obtained from compatible maps on the two factors. The defining relators are killed exactly by the compatibility hypothesis, and uniqueness follows from the universal property of the quotient and the free product.
□@[simp 900] theorem concretePushoutDesc_inr
(β₁ : H →* H₁) (β₂ : H →* H₂)
{K : Type u} [Group K]
(φ₁ : H₁ →* K) (φ₂ : H₂ →* K)
(hφ : φ₁.comp β₁ = φ₂.comp β₂) :
(concretePushoutDesc β₁ β₂ φ₁ φ₂ hφ).comp (inr β₁ β₂) = φ₂The concrete pushout descent map is compatible with the right inclusion.
Show proof
by
ext x
change concretePushoutDesc β₁ β₂ φ₁ φ₂ hφ
(QuotientGroup.mk' (pushoutNormalClosure β₁ β₂)
(Monoid.Coprod.inr x : PushoutFreeProduct H₁ H₂)) = φ₂ x
simp only [concretePushoutDesc, QuotientGroup.mk'_apply, QuotientGroup.lift_mk, Monoid.Coprod.lift_apply_inr]Proof. Unfold the algebraic pushout as the quotient of the free product by the normal closure of the identifying relators. The two canonical maps agree on the common subgroup by construction, and a descent map out of the pushout is obtained from compatible maps on the two factors. The defining relators are killed exactly by the compatibility hypothesis, and uniqueness follows from the universal property of the quotient and the free product.
□def IsPushoutSquare (β₁ : H →* H₁) (β₂ : H →* H₂)
(α₁ : H₁ →* G) (α₂ : H₂ →* G) : Prop :=
α₁.comp β₁ = α₂.comp β₂ ∧
∀ ⦃K : Type u⦄ [Group K] (φ₁ : H₁ →* K) (φ₂ : H₂ →* K),
φ₁.comp β₁ = φ₂.comp β₂ →
∃! φ : G →* K, φ.comp α₁ = φ₁ ∧ φ.comp α₂ = φ₂Pushout squares in the category of groups.
theorem concretePushout_isPushoutSquare (β₁ : H →* H₁) (β₂ : H →* H₂) :
IsPushoutSquare β₁ β₂ (inl β₁ β₂) (inr β₁ β₂)The algebraic pushout carrier satisfies the ordinary group pushout universal property.
Show proof
by
refine ⟨inl_comp_eq_inr_comp β₁ β₂, ?_⟩
intro K _ φ₁ φ₂ hφ
refine ⟨concretePushoutDesc β₁ β₂ φ₁ φ₂ hφ, ⟨concretePushoutDesc_inl β₁ β₂ φ₁ φ₂ hφ,
concretePushoutDesc_inr β₁ β₂ φ₁ φ₂ hφ⟩, ?_⟩
intro ψ hψ
let q : PushoutFreeProduct H₁ H₂ →* Carrier β₁ β₂ :=
QuotientGroup.mk' (pushoutNormalClosure β₁ β₂)
let F : PushoutFreeProduct H₁ H₂ →* K := Monoid.Coprod.lift φ₁ φ₂
have hψq : ψ.comp q = F := by
apply Monoid.Coprod.hom_ext
· calc
(ψ.comp q).comp Monoid.Coprod.inl = ψ.comp (inl β₁ β₂) := rfl
_ = φ₁ := hψ.1
_ = F.comp Monoid.Coprod.inl := (Monoid.Coprod.lift_comp_inl φ₁ φ₂).symm
· calc
(ψ.comp q).comp Monoid.Coprod.inr = ψ.comp (inr β₁ β₂) := rfl
_ = φ₂ := hψ.2
_ = F.comp Monoid.Coprod.inr := (Monoid.Coprod.lift_comp_inr φ₁ φ₂).symm
have hdescq : (concretePushoutDesc β₁ β₂ φ₁ φ₂ hφ).comp q = F := by
apply Monoid.Coprod.hom_ext
· calc
((concretePushoutDesc β₁ β₂ φ₁ φ₂ hφ).comp q).comp Monoid.Coprod.inl =
(concretePushoutDesc β₁ β₂ φ₁ φ₂ hφ).comp (inl β₁ β₂) := rfl
_ = φ₁ := concretePushoutDesc_inl β₁ β₂ φ₁ φ₂ hφ
_ = F.comp Monoid.Coprod.inl := (Monoid.Coprod.lift_comp_inl φ₁ φ₂).symm
· calc
((concretePushoutDesc β₁ β₂ φ₁ φ₂ hφ).comp q).comp Monoid.Coprod.inr =
(concretePushoutDesc β₁ β₂ φ₁ φ₂ hφ).comp (inr β₁ β₂) := rfl
_ = φ₂ := concretePushoutDesc_inr β₁ β₂ φ₁ φ₂ hφ
_ = F.comp Monoid.Coprod.inr := (Monoid.Coprod.lift_comp_inr φ₁ φ₂).symm
apply MonoidHom.ext
intro y
rcases QuotientGroup.mk'_surjective (pushoutNormalClosure β₁ β₂) y with ⟨z, rfl⟩
change ψ (q z) = concretePushoutDesc β₁ β₂ φ₁ φ₂ hφ (q z)
exact congrArg (fun f : PushoutFreeProduct H₁ H₂ →* K => f z)
(hψq.trans hdescq.symm)Proof. Unfold the algebraic pushout as the quotient of the free product by the normal closure of the identifying relators. The two canonical maps agree on the common subgroup by construction, and a descent map out of the pushout is obtained from compatible maps on the two factors. The defining relators are killed exactly by the compatibility hypothesis, and uniqueness follows from the universal property of the quotient and the free product.
□noncomputable def pushoutDesc
{β₁ : H →* H₁} {β₂ : H →* H₂}
{α₁ : H₁ →* G} {α₂ : H₂ →* G}
{K : Type u} [Group K]
(hpo : IsPushoutSquare β₁ β₂ α₁ α₂)
(φ₁ : H₁ →* K) (φ₂ : H₂ →* K)
(hφ : φ₁.comp β₁ = φ₂.comp β₂) : G →* K :=
Classical.choose (ExistsUnique.exists (hpo.2 φ₁ φ₂ hφ))The pushout universal property supplies the induced morphism.
theorem pushoutDesc_spec
{β₁ : H →* H₁} {β₂ : H →* H₂}
{α₁ : H₁ →* G} {α₂ : H₂ →* G}
{K : Type u} [Group K]
(hpo : IsPushoutSquare β₁ β₂ α₁ α₂)
(φ₁ : H₁ →* K) (φ₂ : H₂ →* K)
(hφ : φ₁.comp β₁ = φ₂.comp β₂) :
(pushoutDesc hpo φ₁ φ₂ hφ).comp α₁ = φ₁ ∧
(pushoutDesc hpo φ₁ φ₂ hφ).comp α₂ = φ₂The chosen pushout descent map has the prescribed left and right composites.
Show proof
Classical.choose_spec (ExistsUnique.exists (hpo.2 φ₁ φ₂ hφ))Proof. Unfold the algebraic pushout as the quotient of the free product by the normal closure of the identifying relators. The two canonical maps agree on the common subgroup by construction, and a descent map out of the pushout is obtained from compatible maps on the two factors. The defining relators are killed exactly by the compatibility hypothesis, and uniqueness follows from the universal property of the quotient and the free product.
□@[simp] theorem pushoutDesc_left
{β₁ : H →* H₁} {β₂ : H →* H₂}
{α₁ : H₁ →* G} {α₂ : H₂ →* G}
{K : Type u} [Group K]
(hpo : IsPushoutSquare β₁ β₂ α₁ α₂)
(φ₁ : H₁ →* K) (φ₂ : H₂ →* K)
(hφ : φ₁.comp β₁ = φ₂.comp β₂) :
(pushoutDesc hpo φ₁ φ₂ hφ).comp α₁ = φ₁The left composite of the chosen pushout descent map is the prescribed left leg.
Show proof
(pushoutDesc_spec hpo φ₁ φ₂ hφ).1Proof. Unfold the algebraic pushout as the quotient of the free product by the normal closure of the identifying relators. The two canonical maps agree on the common subgroup by construction, and a descent map out of the pushout is obtained from compatible maps on the two factors. The defining relators are killed exactly by the compatibility hypothesis, and uniqueness follows from the universal property of the quotient and the free product.
□@[simp] theorem pushoutDesc_right
{β₁ : H →* H₁} {β₂ : H →* H₂}
{α₁ : H₁ →* G} {α₂ : H₂ →* G}
{K : Type u} [Group K]
(hpo : IsPushoutSquare β₁ β₂ α₁ α₂)
(φ₁ : H₁ →* K) (φ₂ : H₂ →* K)
(hφ : φ₁.comp β₁ = φ₂.comp β₂) :
(pushoutDesc hpo φ₁ φ₂ hφ).comp α₂ = φ₂The right composite of the chosen pushout descent map is the prescribed right leg.
Show proof
(pushoutDesc_spec hpo φ₁ φ₂ hφ).2Proof. Unfold the algebraic pushout as the quotient of the free product by the normal closure of the identifying relators. The two canonical maps agree on the common subgroup by construction, and a descent map out of the pushout is obtained from compatible maps on the two factors. The defining relators are killed exactly by the compatibility hypothesis, and uniqueness follows from the universal property of the quotient and the free product.
□theorem pushoutDesc_uniq
{β₁ : H →* H₁} {β₂ : H →* H₂}
{α₁ : H₁ →* G} {α₂ : H₂ →* G}
{K : Type u} [Group K]
(hpo : IsPushoutSquare β₁ β₂ α₁ α₂)
(φ₁ : H₁ →* K) (φ₂ : H₂ →* K)
(hφ : φ₁.comp β₁ = φ₂.comp β₂)
{ψ : G →* K}
(hψ : ψ.comp α₁ = φ₁ ∧ ψ.comp α₂ = φ₂) :
ψ = pushoutDesc hpo φ₁ φ₂ hφUniqueness of the chosen pushout descent map.
Show proof
by
rcases hpo.2 φ₁ φ₂ hφ with ⟨u, hu, huuniq⟩
have hψ' : ψ = u := huuniq _ hψ
have hdesc : pushoutDesc hpo φ₁ φ₂ hφ = u :=
huuniq _ (pushoutDesc_spec hpo φ₁ φ₂ hφ)
exact hψ'.trans hdesc.symmProof. Unfold the algebraic pushout as the quotient of the free product by the normal closure of the identifying relators. The two canonical maps agree on the common subgroup by construction, and a descent map out of the pushout is obtained from compatible maps on the two factors. The defining relators are killed exactly by the compatibility hypothesis, and uniqueness follows from the universal property of the quotient and the free product.
□@[simp] theorem pushoutDesc_self
{β₁ : H →* H₁} {β₂ : H →* H₂}
{α₁ : H₁ →* G} {α₂ : H₂ →* G}
(hpo : IsPushoutSquare β₁ β₂ α₁ α₂) :
pushoutDesc hpo α₁ α₂ hpo.1 = MonoidHom.id GThe distinguished map from a pushout object to itself is the identity.
Show proof
by
symm
exact pushoutDesc_uniq hpo α₁ α₂ hpo.1 (ψ := MonoidHom.id G) (by simp only [MonoidHom.CompTriple.comp_eq, and_self])Proof. Unfold the algebraic pushout as the quotient of the free product by the normal closure of the identifying relators. The two canonical maps agree on the common subgroup by construction, and a descent map out of the pushout is obtained from compatible maps on the two factors. The defining relators are killed exactly by the compatibility hypothesis, and uniqueness follows from the universal property of the quotient and the free product.
□theorem pushout_hom_ext
{β₁ : H →* H₁} {β₂ : H →* H₂}
{α₁ : H₁ →* G} {α₂ : H₂ →* G}
{K : Type u} [Group K]
(hpo : IsPushoutSquare β₁ β₂ α₁ α₂)
{ψ ψ' : G →* K}
(h₁ : ψ.comp α₁ = ψ'.comp α₁)
(h₂ : ψ.comp α₂ = ψ'.comp α₂) :
ψ = ψ'Extensionality of morphisms out of a pushout object.
Show proof
by
have hφ : (ψ.comp α₁).comp β₁ = (ψ.comp α₂).comp β₂ := by
simpa using congrArg (fun f : H →* G => ψ.comp f) hpo.1
have hψ :
ψ = pushoutDesc hpo (ψ.comp α₁) (ψ.comp α₂) hφ := by
exact pushoutDesc_uniq hpo (ψ.comp α₁) (ψ.comp α₂) hφ (ψ := ψ) ⟨rfl, rfl⟩
have hψ' :
ψ' = pushoutDesc hpo (ψ.comp α₁) (ψ.comp α₂) hφ := by
exact pushoutDesc_uniq hpo (ψ.comp α₁) (ψ.comp α₂) hφ (ψ := ψ') ⟨h₁.symm, h₂.symm⟩
exact hψ.trans hψ'.symmProof. Unfold the algebraic pushout as the quotient of the free product by the normal closure of the identifying relators. The two canonical maps agree on the common subgroup by construction, and a descent map out of the pushout is obtained from compatible maps on the two factors. The defining relators are killed exactly by the compatibility hypothesis, and uniqueness follows from the universal property of the quotient and the free product.
□noncomputable def pushoutMapOfIsPushout
{α₁ : H₁ →* G} {α₂ : H₂ →* G}
{α₁' : H₁ →* G'} {α₂' : H₂ →* G'}
(β₁ : H →* H₁) (β₂ : H →* H₂)
(hpo : IsPushoutSquare β₁ β₂ α₁ α₂)
(hpo' : IsPushoutSquare β₁ β₂ α₁' α₂') :
G →* G' :=
pushoutDesc hpo α₁' α₂' hpo'.1The canonical comparison map between two pushout objects of the same cospan.
@[simp 900] theorem pushoutMapOfIsPushout_self
{α₁ : H₁ →* G} {α₂ : H₂ →* G}
(β₁ : H →* H₁) (β₂ : H →* H₂)
(hpo : IsPushoutSquare β₁ β₂ α₁ α₂) :
pushoutMapOfIsPushout β₁ β₂ hpo hpo = MonoidHom.id GThe canonical comparison map from a pushout object to itself is the identity.
Show proof
by
change pushoutDesc hpo α₁ α₂ hpo.1 = MonoidHom.id G
exact pushoutDesc_self (hpo := hpo)Proof. Unfold the algebraic pushout as the quotient of the free product by the normal closure of the identifying relators. The two canonical maps agree on the common subgroup by construction, and a descent map out of the pushout is obtained from compatible maps on the two factors. The defining relators are killed exactly by the compatibility hypothesis, and uniqueness follows from the universal property of the quotient and the free product.
□@[simp 900] theorem pushoutMapOfIsPushout_left
{α₁ : H₁ →* G} {α₂ : H₂ →* G}
{α₁' : H₁ →* G'} {α₂' : H₂ →* G'}
(β₁ : H →* H₁) (β₂ : H →* H₂)
(hpo : IsPushoutSquare β₁ β₂ α₁ α₂)
(hpo' : IsPushoutSquare β₁ β₂ α₁' α₂') :
(pushoutMapOfIsPushout β₁ β₂ hpo hpo').comp α₁ = α₁'The left composite of the canonical comparison map between pushout objects is the prescribed left leg.
Show proof
by
change (pushoutDesc hpo α₁' α₂' hpo'.1).comp α₁ = α₁'
exact pushoutDesc_left hpo α₁' α₂' hpo'.1Proof. Unfold the algebraic pushout as the quotient of the free product by the normal closure of the identifying relators. The two canonical maps agree on the common subgroup by construction, and a descent map out of the pushout is obtained from compatible maps on the two factors. The defining relators are killed exactly by the compatibility hypothesis, and uniqueness follows from the universal property of the quotient and the free product.
□@[simp 900] theorem pushoutMapOfIsPushout_right
{α₁ : H₁ →* G} {α₂ : H₂ →* G}
{α₁' : H₁ →* G'} {α₂' : H₂ →* G'}
(β₁ : H →* H₁) (β₂ : H →* H₂)
(hpo : IsPushoutSquare β₁ β₂ α₁ α₂)
(hpo' : IsPushoutSquare β₁ β₂ α₁' α₂') :
(pushoutMapOfIsPushout β₁ β₂ hpo hpo').comp α₂ = α₂'The right composite of the canonical comparison map between pushout objects is the prescribed right leg.
Show proof
by
change (pushoutDesc hpo α₁' α₂' hpo'.1).comp α₂ = α₂'
exact pushoutDesc_right hpo α₁' α₂' hpo'.1Proof. Unfold the algebraic pushout as the quotient of the free product by the normal closure of the identifying relators. The two canonical maps agree on the common subgroup by construction, and a descent map out of the pushout is obtained from compatible maps on the two factors. The defining relators are killed exactly by the compatibility hypothesis, and uniqueness follows from the universal property of the quotient and the free product.
□theorem bijective_pushoutMapOfIsPushout
{α₁ : H₁ →* G} {α₂ : H₂ →* G}
{α₁' : H₁ →* G'} {α₂' : H₂ →* G'}
(β₁ : H →* H₁) (β₂ : H →* H₂)
(hpo : IsPushoutSquare β₁ β₂ α₁ α₂)
(hpo' : IsPushoutSquare β₁ β₂ α₁' α₂') :
Function.Bijective (pushoutMapOfIsPushout β₁ β₂ hpo hpo')Any two pushout objects of the same cospan are canonically isomorphic.
Show proof
by
let φ : G →* G' := pushoutMapOfIsPushout β₁ β₂ hpo hpo'
let ψ : G' →* G := pushoutMapOfIsPushout β₁ β₂ hpo' hpo
have hleft : ψ.comp φ = MonoidHom.id G := by
apply pushout_hom_ext hpo
· calc
(ψ.comp φ).comp α₁ = ψ.comp (φ.comp α₁) := by rfl
_ = ψ.comp α₁' := by rw [pushoutMapOfIsPushout_left β₁ β₂ hpo hpo']
_ = α₁ := pushoutMapOfIsPushout_left β₁ β₂ hpo' hpo
· calc
(ψ.comp φ).comp α₂ = ψ.comp (φ.comp α₂) := by rfl
_ = ψ.comp α₂' := by rw [pushoutMapOfIsPushout_right β₁ β₂ hpo hpo']
_ = α₂ := pushoutMapOfIsPushout_right β₁ β₂ hpo' hpo
have hright : φ.comp ψ = MonoidHom.id G' := by
apply pushout_hom_ext hpo'
· calc
(φ.comp ψ).comp α₁' = φ.comp (ψ.comp α₁') := by rfl
_ = φ.comp α₁ := by rw [pushoutMapOfIsPushout_left β₁ β₂ hpo' hpo]
_ = α₁' := pushoutMapOfIsPushout_left β₁ β₂ hpo hpo'
· calc
(φ.comp ψ).comp α₂' = φ.comp (ψ.comp α₂') := by rfl
_ = φ.comp α₂ := by rw [pushoutMapOfIsPushout_right β₁ β₂ hpo' hpo]
_ = α₂' := pushoutMapOfIsPushout_right β₁ β₂ hpo hpo'
refine ⟨?_, ?_⟩
· intro x y hxy
have hx : ψ (φ x) = x := by
simpa [φ, ψ] using congrArg (fun f : G →* G => f x) hleft
have hy : ψ (φ y) = y := by
simpa [φ, ψ] using congrArg (fun f : G →* G => f y) hleft
calc
x = ψ (φ x) := hx.symm
_ = ψ (φ y) := by simpa [φ] using congrArg ψ hxy
_ = y := hy
· intro y
refine ⟨ψ y, ?_⟩
simpa [φ, ψ] using congrArg (fun f : G' →* G' => f y) hrightProof. Unfold the algebraic pushout as the quotient of the free product by the normal closure of the identifying relators. The two canonical maps agree on the common subgroup by construction, and a descent map out of the pushout is obtained from compatible maps on the two factors. The defining relators are killed exactly by the compatibility hypothesis, and uniqueness follows from the universal property of the quotient and the free product.
□noncomputable def pushoutEquivOfIsPushout
{α₁ : H₁ →* G} {α₂ : H₂ →* G}
{α₁' : H₁ →* G'} {α₂' : H₂ →* G'}
(β₁ : H →* H₁) (β₂ : H →* H₂)
(hpo : IsPushoutSquare β₁ β₂ α₁ α₂)
(hpo' : IsPushoutSquare β₁ β₂ α₁' α₂') :
G ≃* G' :=
MulEquiv.ofBijective
(pushoutMapOfIsPushout β₁ β₂ hpo hpo')
(bijective_pushoutMapOfIsPushout β₁ β₂ hpo hpo')The canonical multiplicative equivalence between two pushout objects of the same cospan.
@[simp] theorem pushoutEquivOfIsPushout_left
{α₁ : H₁ →* G} {α₂ : H₂ →* G}
{α₁' : H₁ →* G'} {α₂' : H₂ →* G'}
(β₁ : H →* H₁) (β₂ : H →* H₂)
(hpo : IsPushoutSquare β₁ β₂ α₁ α₂)
(hpo' : IsPushoutSquare β₁ β₂ α₁' α₂') :
(pushoutEquivOfIsPushout β₁ β₂ hpo hpo').toMonoidHom.comp α₁ = α₁'The left composite of the canonical pushout equivalence is the prescribed left leg.
Show proof
by
change (pushoutMapOfIsPushout β₁ β₂ hpo hpo').comp α₁ = α₁'
exact pushoutMapOfIsPushout_left β₁ β₂ hpo hpo'Proof. Unfold the algebraic pushout as the quotient of the free product by the normal closure of the identifying relators. The two canonical maps agree on the common subgroup by construction, and a descent map out of the pushout is obtained from compatible maps on the two factors. The defining relators are killed exactly by the compatibility hypothesis, and uniqueness follows from the universal property of the quotient and the free product.
□@[simp 900] theorem pushoutEquivOfIsPushout_right
{α₁ : H₁ →* G} {α₂ : H₂ →* G}
{α₁' : H₁ →* G'} {α₂' : H₂ →* G'}
(β₁ : H →* H₁) (β₂ : H →* H₂)
(hpo : IsPushoutSquare β₁ β₂ α₁ α₂)
(hpo' : IsPushoutSquare β₁ β₂ α₁' α₂') :
(pushoutEquivOfIsPushout β₁ β₂ hpo hpo').toMonoidHom.comp α₂ = α₂'The right composite of the canonical pushout equivalence is the prescribed right leg.
Show proof
by
change (pushoutMapOfIsPushout β₁ β₂ hpo hpo').comp α₂ = α₂'
exact pushoutMapOfIsPushout_right β₁ β₂ hpo hpo'Proof. Unfold the algebraic pushout as the quotient of the free product by the normal closure of the identifying relators. The two canonical maps agree on the common subgroup by construction, and a descent map out of the pushout is obtained from compatible maps on the two factors. The defining relators are killed exactly by the compatibility hypothesis, and uniqueness follows from the universal property of the quotient and the free product.
□def HasTopologicalPushoutProperty (β₁ : H →ₜ* H₁) (β₂ : H →ₜ* H₂)
(α₁ : H₁ →ₜ* G) (α₂ : H₂ →ₜ* G) : Prop :=
α₁.comp β₁ = α₂.comp β₂ ∧
∀ ⦃K : Type u⦄ [Group K] [TopologicalSpace K] [IsTopologicalGroup K],
∀ (φ₁ : H₁ →ₜ* K) (φ₂ : H₂ →ₜ* K),
φ₁.comp β₁ = φ₂.comp β₂ →
∃! φ : G →ₜ* K, φ.comp α₁ = φ₁ ∧ φ.comp α₂ = φ₂The continuous pushout property is tested by all topological-group target objects.
def HasProfiniteTestPushoutProperty (β₁ : H →ₜ* H₁) (β₂ : H →ₜ* H₂)
(α₁ : H₁ →ₜ* G) (α₂ : H₂ →ₜ* G) : Prop :=
α₁.comp β₁ = α₂.comp β₂ ∧
∀ ⦃K : Type u⦄ [Group K] [TopologicalSpace K] [IsTopologicalGroup K],
IsProfiniteGroup K →
∀ (φ₁ : H₁ →ₜ* K) (φ₂ : H₂ →ₜ* K),
φ₁.comp β₁ = φ₂.comp β₂ →
∃! φ : G →ₜ* K, φ.comp α₁ = φ₁ ∧ φ.comp α₂ = φ₂structure IsProfinitePushoutSquare (β₁ : H →ₜ* H₁) (β₂ : H →ₜ* H₂)
(α₁ : H₁ →ₜ* G) (α₂ : H₂ →ₜ* G) : Prop where
source_profinite : IsProfiniteGroup H
left_profinite : IsProfiniteGroup H₁
right_profinite : IsProfiniteGroup H₂
pushout_profinite : IsProfiniteGroup G
property : HasProfiniteTestPushoutProperty β₁ β₂ α₁ α₂A genuine profinite pushout square: all four objects are profinite, and the square has the continuous universal property tested by profinite target objects.
noncomputable def pushoutDescCont
{β₁ : H →ₜ* H₁} {β₂ : H →ₜ* H₂}
{α₁ : H₁ →ₜ* G} {α₂ : H₂ →ₜ* G}
{K : Type u} [Group K] [TopologicalSpace K] [IsTopologicalGroup K]
(hpo : HasProfiniteTestPushoutProperty β₁ β₂ α₁ α₂)
(hK : IsProfiniteGroup K)
(φ₁ : H₁ →ₜ* K) (φ₂ : H₂ →ₜ* K)
(hφ : φ₁.comp β₁ = φ₂.comp β₂) : G →ₜ* K :=
Classical.choose (ExistsUnique.exists (hpo.2 (K := K) hK φ₁ φ₂ hφ))Chosen continuous morphism induced by the profinite pushout universal property.
theorem pushoutDescCont_spec
{β₁ : H →ₜ* H₁} {β₂ : H →ₜ* H₂}
{α₁ : H₁ →ₜ* G} {α₂ : H₂ →ₜ* G}
{K : Type u} [Group K] [TopologicalSpace K] [IsTopologicalGroup K]
(hpo : HasProfiniteTestPushoutProperty β₁ β₂ α₁ α₂)
(hK : IsProfiniteGroup K)
(φ₁ : H₁ →ₜ* K) (φ₂ : H₂ →ₜ* K)
(hφ : φ₁.comp β₁ = φ₂.comp β₂) :
(pushoutDescCont hpo hK φ₁ φ₂ hφ).comp α₁ = φ₁ ∧
(pushoutDescCont hpo hK φ₁ φ₂ hφ).comp α₂ = φ₂Specification of the chosen continuous pushout descent map.
Show proof
Classical.choose_spec (ExistsUnique.exists (hpo.2 (K := K) hK φ₁ φ₂ hφ))Proof. Unfold the algebraic pushout as the quotient of the free product by the normal closure of the identifying relators. The two canonical maps agree on the common subgroup by construction, and a descent map out of the pushout is obtained from compatible maps on the two factors. The defining relators are killed exactly by the compatibility hypothesis, and uniqueness follows from the universal property of the quotient and the free product.
□@[simp] theorem pushoutDescCont_left
{β₁ : H →ₜ* H₁} {β₂ : H →ₜ* H₂}
{α₁ : H₁ →ₜ* G} {α₂ : H₂ →ₜ* G}
{K : Type u} [Group K] [TopologicalSpace K] [IsTopologicalGroup K]
(hpo : HasProfiniteTestPushoutProperty β₁ β₂ α₁ α₂)
(hK : IsProfiniteGroup K)
(φ₁ : H₁ →ₜ* K) (φ₂ : H₂ →ₜ* K)
(hφ : φ₁.comp β₁ = φ₂.comp β₂) :
(pushoutDescCont hpo hK φ₁ φ₂ hφ).comp α₁ = φ₁The left composite of the chosen continuous pushout descent map is the prescribed left leg.
Show proof
(pushoutDescCont_spec hpo hK φ₁ φ₂ hφ).1Proof. Unfold the algebraic pushout as the quotient of the free product by the normal closure of the identifying relators. The two canonical maps agree on the common subgroup by construction, and a descent map out of the pushout is obtained from compatible maps on the two factors. The defining relators are killed exactly by the compatibility hypothesis, and uniqueness follows from the universal property of the quotient and the free product.
□@[simp] theorem pushoutDescCont_right
{β₁ : H →ₜ* H₁} {β₂ : H →ₜ* H₂}
{α₁ : H₁ →ₜ* G} {α₂ : H₂ →ₜ* G}
{K : Type u} [Group K] [TopologicalSpace K] [IsTopologicalGroup K]
(hpo : HasProfiniteTestPushoutProperty β₁ β₂ α₁ α₂)
(hK : IsProfiniteGroup K)
(φ₁ : H₁ →ₜ* K) (φ₂ : H₂ →ₜ* K)
(hφ : φ₁.comp β₁ = φ₂.comp β₂) :
(pushoutDescCont hpo hK φ₁ φ₂ hφ).comp α₂ = φ₂The right composite of the chosen continuous pushout descent map is the prescribed right leg.
Show proof
(pushoutDescCont_spec hpo hK φ₁ φ₂ hφ).2Proof. Unfold the algebraic pushout as the quotient of the free product by the normal closure of the identifying relators. The two canonical maps agree on the common subgroup by construction, and a descent map out of the pushout is obtained from compatible maps on the two factors. The defining relators are killed exactly by the compatibility hypothesis, and uniqueness follows from the universal property of the quotient and the free product.
□theorem pushoutDescCont_uniq
{β₁ : H →ₜ* H₁} {β₂ : H →ₜ* H₂}
{α₁ : H₁ →ₜ* G} {α₂ : H₂ →ₜ* G}
{K : Type u} [Group K] [TopologicalSpace K] [IsTopologicalGroup K]
(hpo : HasProfiniteTestPushoutProperty β₁ β₂ α₁ α₂)
(hK : IsProfiniteGroup K)
(φ₁ : H₁ →ₜ* K) (φ₂ : H₂ →ₜ* K)
(hφ : φ₁.comp β₁ = φ₂.comp β₂)
{ψ : G →ₜ* K}
(hψ : ψ.comp α₁ = φ₁ ∧ ψ.comp α₂ = φ₂) :
ψ = pushoutDescCont hpo hK φ₁ φ₂ hφUniqueness of the chosen continuous pushout descent map.
Show proof
by
rcases hpo.2 (K := K) hK φ₁ φ₂ hφ with ⟨u, hu, huuniq⟩
have hψ' : ψ = u := huuniq _ hψ
have hdesc : pushoutDescCont hpo hK φ₁ φ₂ hφ = u :=
huuniq _ (pushoutDescCont_spec hpo hK φ₁ φ₂ hφ)
exact hψ'.trans hdesc.symmProof. Unfold the algebraic pushout as the quotient of the free product by the normal closure of the identifying relators. The two canonical maps agree on the common subgroup by construction, and a descent map out of the pushout is obtained from compatible maps on the two factors. The defining relators are killed exactly by the compatibility hypothesis, and uniqueness follows from the universal property of the quotient and the free product.
□@[simp 900] theorem pushoutDescCont_self
{β₁ : H →ₜ* H₁} {β₂ : H →ₜ* H₂}
{α₁ : H₁ →ₜ* G} {α₂ : H₂ →ₜ* G}
(hpo : HasProfiniteTestPushoutProperty β₁ β₂ α₁ α₂)
(hG : IsProfiniteGroup G) :
pushoutDescCont hpo hG α₁ α₂ hpo.1 = ContinuousMonoidHom.id GThe distinguished map from a profinite pushout object to itself is the identity.
Show proof
by
symm
exact
pushoutDescCont_uniq (K := G) hpo hG α₁ α₂ hpo.1
(ψ := ContinuousMonoidHom.id G) ⟨rfl, rfl⟩Proof. Unfold the algebraic pushout as the quotient of the free product by the normal closure of the identifying relators. The two canonical maps agree on the common subgroup by construction, and a descent map out of the pushout is obtained from compatible maps on the two factors. The defining relators are killed exactly by the compatibility hypothesis, and uniqueness follows from the universal property of the quotient and the free product.
□theorem pushoutCont_hom_ext
{β₁ : H →ₜ* H₁} {β₂ : H →ₜ* H₂}
{α₁ : H₁ →ₜ* G} {α₂ : H₂ →ₜ* G}
{K : Type u} [Group K] [TopologicalSpace K] [IsTopologicalGroup K]
(hpo : HasProfiniteTestPushoutProperty β₁ β₂ α₁ α₂)
{ψ ψ' : G →ₜ* K}
(hK : IsProfiniteGroup K)
(h₁ : ψ.comp α₁ = ψ'.comp α₁)
(h₂ : ψ.comp α₂ = ψ'.comp α₂) :
ψ = ψ'Extensionality of continuous morphisms out of a profinite pushout object.
Show proof
by
have hφ : (ψ.comp α₁).comp β₁ = (ψ.comp α₂).comp β₂ := by
simpa using congrArg (fun f : H →ₜ* G => ψ.comp f) hpo.1
have hψ :
ψ = pushoutDescCont hpo hK (ψ.comp α₁) (ψ.comp α₂) hφ := by
exact pushoutDescCont_uniq hpo hK (ψ.comp α₁) (ψ.comp α₂) hφ (ψ := ψ) ⟨rfl, rfl⟩
have hψ' :
ψ' = pushoutDescCont hpo hK (ψ.comp α₁) (ψ.comp α₂) hφ := by
exact pushoutDescCont_uniq hpo hK (ψ.comp α₁) (ψ.comp α₂) hφ
(ψ := ψ') ⟨h₁.symm, h₂.symm⟩
exact hψ.trans hψ'.symmProof. Unfold the algebraic pushout as the quotient of the free product by the normal closure of the identifying relators. The two canonical maps agree on the common subgroup by construction, and a descent map out of the pushout is obtained from compatible maps on the two factors. The defining relators are killed exactly by the compatibility hypothesis, and uniqueness follows from the universal property of the quotient and the free product.
□noncomputable def pushoutContMapOfIsPushout
{α₁ : H₁ →ₜ* G} {α₂ : H₂ →ₜ* G}
{α₁' : H₁ →ₜ* G'} {α₂' : H₂ →ₜ* G'}
(β₁ : H →ₜ* H₁) (β₂ : H →ₜ* H₂)
(hpo : HasProfiniteTestPushoutProperty β₁ β₂ α₁ α₂)
(hpo' : HasProfiniteTestPushoutProperty β₁ β₂ α₁' α₂')
(hG' : IsProfiniteGroup G') :
G →ₜ* G' :=
pushoutDescCont hpo hG' α₁' α₂' hpo'.1The canonical comparison map between two profinite pushout objects of the same cospan.
@[simp 900] theorem pushoutContMapOfIsPushout_self
{α₁ : H₁ →ₜ* G} {α₂ : H₂ →ₜ* G}
(β₁ : H →ₜ* H₁) (β₂ : H →ₜ* H₂)
(hpo : HasProfiniteTestPushoutProperty β₁ β₂ α₁ α₂)
(hG : IsProfiniteGroup G) :
pushoutContMapOfIsPushout β₁ β₂ hpo hpo hG = ContinuousMonoidHom.id GThe canonical comparison map from a profinite pushout object to itself is the identity.
Show proof
by
change pushoutDescCont hpo hG α₁ α₂ hpo.1 = ContinuousMonoidHom.id G
exact pushoutDescCont_self (hpo := hpo) (hG := hG)Proof. Unfold the algebraic pushout as the quotient of the free product by the normal closure of the identifying relators. The two canonical maps agree on the common subgroup by construction, and a descent map out of the pushout is obtained from compatible maps on the two factors. The defining relators are killed exactly by the compatibility hypothesis, and uniqueness follows from the universal property of the quotient and the free product.
□@[simp 900] theorem pushoutContMapOfIsPushout_left
{α₁ : H₁ →ₜ* G} {α₂ : H₂ →ₜ* G}
{α₁' : H₁ →ₜ* G'} {α₂' : H₂ →ₜ* G'}
(β₁ : H →ₜ* H₁) (β₂ : H →ₜ* H₂)
(hpo : HasProfiniteTestPushoutProperty β₁ β₂ α₁ α₂)
(hpo' : HasProfiniteTestPushoutProperty β₁ β₂ α₁' α₂')
(hG' : IsProfiniteGroup G') :
(pushoutContMapOfIsPushout β₁ β₂ hpo hpo' hG').comp α₁ = α₁'The left composite of the canonical comparison map between profinite pushout objects is the prescribed left leg.
Show proof
by
change (pushoutDescCont hpo hG' α₁' α₂' hpo'.1).comp α₁ = α₁'
exact pushoutDescCont_left hpo hG' α₁' α₂' hpo'.1Proof. Unfold the algebraic pushout as the quotient of the free product by the normal closure of the identifying relators. The two canonical maps agree on the common subgroup by construction, and a descent map out of the pushout is obtained from compatible maps on the two factors. The defining relators are killed exactly by the compatibility hypothesis, and uniqueness follows from the universal property of the quotient and the free product.
□@[simp 900] theorem pushoutContMapOfIsPushout_right
{α₁ : H₁ →ₜ* G} {α₂ : H₂ →ₜ* G}
{α₁' : H₁ →ₜ* G'} {α₂' : H₂ →ₜ* G'}
(β₁ : H →ₜ* H₁) (β₂ : H →ₜ* H₂)
(hpo : HasProfiniteTestPushoutProperty β₁ β₂ α₁ α₂)
(hpo' : HasProfiniteTestPushoutProperty β₁ β₂ α₁' α₂')
(hG' : IsProfiniteGroup G') :
(pushoutContMapOfIsPushout β₁ β₂ hpo hpo' hG').comp α₂ = α₂'The right composite of the canonical comparison map between profinite pushout objects is the prescribed right leg.
Show proof
by
change (pushoutDescCont hpo hG' α₁' α₂' hpo'.1).comp α₂ = α₂'
exact pushoutDescCont_right hpo hG' α₁' α₂' hpo'.1Proof. Unfold the algebraic pushout as the quotient of the free product by the normal closure of the identifying relators. The two canonical maps agree on the common subgroup by construction, and a descent map out of the pushout is obtained from compatible maps on the two factors. The defining relators are killed exactly by the compatibility hypothesis, and uniqueness follows from the universal property of the quotient and the free product.
□theorem bijective_pushoutContMapOfIsPushout
{α₁ : H₁ →ₜ* G} {α₂ : H₂ →ₜ* G}
{α₁' : H₁ →ₜ* G'} {α₂' : H₂ →ₜ* G'}
(β₁ : H →ₜ* H₁) (β₂ : H →ₜ* H₂)
(hpo : HasProfiniteTestPushoutProperty β₁ β₂ α₁ α₂)
(hpo' : HasProfiniteTestPushoutProperty β₁ β₂ α₁' α₂')
(hG : IsProfiniteGroup G) (hG' : IsProfiniteGroup G') :
Function.Bijective (pushoutContMapOfIsPushout β₁ β₂ hpo hpo' hG')Any two profinite pushout objects of the same cospan are canonically bijective.
Show proof
by
let φ : G →ₜ* G' := pushoutContMapOfIsPushout β₁ β₂ hpo hpo' hG'
let ψ : G' →ₜ* G := pushoutContMapOfIsPushout β₁ β₂ hpo' hpo hG
have hleft : ψ.comp φ = ContinuousMonoidHom.id G := by
apply pushoutCont_hom_ext hpo hG
· calc
(ψ.comp φ).comp α₁ = ψ.comp (φ.comp α₁) := by rfl
_ = ψ.comp α₁' := by rw [pushoutContMapOfIsPushout_left β₁ β₂ hpo hpo' hG']
_ = α₁ := pushoutContMapOfIsPushout_left β₁ β₂ hpo' hpo hG
· calc
(ψ.comp φ).comp α₂ = ψ.comp (φ.comp α₂) := by rfl
_ = ψ.comp α₂' := by rw [pushoutContMapOfIsPushout_right β₁ β₂ hpo hpo' hG']
_ = α₂ := pushoutContMapOfIsPushout_right β₁ β₂ hpo' hpo hG
have hright : φ.comp ψ = ContinuousMonoidHom.id G' := by
apply pushoutCont_hom_ext hpo' hG'
· calc
(φ.comp ψ).comp α₁' = φ.comp (ψ.comp α₁') := by rfl
_ = φ.comp α₁ := by rw [pushoutContMapOfIsPushout_left β₁ β₂ hpo' hpo hG]
_ = α₁' := pushoutContMapOfIsPushout_left β₁ β₂ hpo hpo' hG'
· calc
(φ.comp ψ).comp α₂' = φ.comp (ψ.comp α₂') := by rfl
_ = φ.comp α₂ := by rw [pushoutContMapOfIsPushout_right β₁ β₂ hpo' hpo hG]
_ = α₂' := pushoutContMapOfIsPushout_right β₁ β₂ hpo hpo' hG'
refine ⟨?_, ?_⟩
· intro x y hxy
have hx : ψ (φ x) = x := by
simpa [φ, ψ] using congrArg (fun f : G →ₜ* G => f x) hleft
have hy : ψ (φ y) = y := by
simpa [φ, ψ] using congrArg (fun f : G →ₜ* G => f y) hleft
calc
x = ψ (φ x) := hx.symm
_ = ψ (φ y) := by simpa [φ] using congrArg ψ hxy
_ = y := hy
· intro y
refine ⟨ψ y, ?_⟩
simpa [φ, ψ] using congrArg (fun f : G' →ₜ* G' => f y) hrightProof. Unfold the algebraic pushout as the quotient of the free product by the normal closure of the identifying relators. The two canonical maps agree on the common subgroup by construction, and a descent map out of the pushout is obtained from compatible maps on the two factors. The defining relators are killed exactly by the compatibility hypothesis, and uniqueness follows from the universal property of the quotient and the free product.
□noncomputable def pushoutContEquivOfIsPushout
{α₁ : H₁ →ₜ* G} {α₂ : H₂ →ₜ* G}
{α₁' : H₁ →ₜ* G'} {α₂' : H₂ →ₜ* G'}
(β₁ : H →ₜ* H₁) (β₂ : H →ₜ* H₂)
(hpo : HasProfiniteTestPushoutProperty β₁ β₂ α₁ α₂)
(hpo' : HasProfiniteTestPushoutProperty β₁ β₂ α₁' α₂')
(hG : IsProfiniteGroup G) (hG' : IsProfiniteGroup G') :
G ≃ₜ* G' := by
letI : CompactSpace G := IsProfiniteGroup.compactSpace hG
letI : T2Space G' := IsProfiniteGroup.t2Space hG'
exact ContinuousMulEquiv.ofBijectiveCompactToT2
(pushoutContMapOfIsPushout β₁ β₂ hpo hpo' hG')
(pushoutContMapOfIsPushout β₁ β₂ hpo hpo' hG').continuous_toFun
(bijective_pushoutContMapOfIsPushout β₁ β₂ hpo hpo' hG hG')The canonical continuous multiplicative equivalence between two profinite pushout objects.
@[simp] theorem pushoutContEquivOfIsPushout_left
{α₁ : H₁ →ₜ* G} {α₂ : H₂ →ₜ* G}
{α₁' : H₁ →ₜ* G'} {α₂' : H₂ →ₜ* G'}
(β₁ : H →ₜ* H₁) (β₂ : H →ₜ* H₂)
(hpo : HasProfiniteTestPushoutProperty β₁ β₂ α₁ α₂)
(hpo' : HasProfiniteTestPushoutProperty β₁ β₂ α₁' α₂')
(hG : IsProfiniteGroup G) (hG' : IsProfiniteGroup G') :
((pushoutContEquivOfIsPushout β₁ β₂ hpo hpo' hG hG' : G →ₜ* G').comp α₁) = α₁'The left composite of the canonical continuous pushout equivalence is the prescribed left leg.
Show proof
by
change (pushoutContMapOfIsPushout β₁ β₂ hpo hpo' hG').comp α₁ = α₁'
exact pushoutContMapOfIsPushout_left β₁ β₂ hpo hpo' hG'Proof. Unfold the algebraic pushout as the quotient of the free product by the normal closure of the identifying relators. The two canonical maps agree on the common subgroup by construction, and a descent map out of the pushout is obtained from compatible maps on the two factors. The defining relators are killed exactly by the compatibility hypothesis, and uniqueness follows from the universal property of the quotient and the free product.
□@[simp] theorem pushoutContEquivOfIsPushout_right
{α₁ : H₁ →ₜ* G} {α₂ : H₂ →ₜ* G}
{α₁' : H₁ →ₜ* G'} {α₂' : H₂ →ₜ* G'}
(β₁ : H →ₜ* H₁) (β₂ : H →ₜ* H₂)
(hpo : HasProfiniteTestPushoutProperty β₁ β₂ α₁ α₂)
(hpo' : HasProfiniteTestPushoutProperty β₁ β₂ α₁' α₂')
(hG : IsProfiniteGroup G) (hG' : IsProfiniteGroup G') :
((pushoutContEquivOfIsPushout β₁ β₂ hpo hpo' hG hG' : G →ₜ* G').comp α₂) = α₂'The right composite of the canonical continuous pushout equivalence is the prescribed right leg.
Show proof
by
change (pushoutContMapOfIsPushout β₁ β₂ hpo hpo' hG').comp α₂ = α₂'
exact pushoutContMapOfIsPushout_right β₁ β₂ hpo hpo' hG'Proof. Unfold the algebraic pushout as the quotient of the free product by the normal closure of the identifying relators. The two canonical maps agree on the common subgroup by construction, and a descent map out of the pushout is obtained from compatible maps on the two factors. The defining relators are killed exactly by the compatibility hypothesis, and uniqueness follows from the universal property of the quotient and the free product.
□@[simp 900] theorem pushoutEquivOfIsPushout_symm_left
{α₁ : H₁ →* G} {α₂ : H₂ →* G}
{α₁' : H₁ →* G'} {α₂' : H₂ →* G'}
(β₁ : H →* H₁) (β₂ : H →* H₂)
(hpo : IsPushoutSquare β₁ β₂ α₁ α₂)
(hpo' : IsPushoutSquare β₁ β₂ α₁' α₂') :
(pushoutEquivOfIsPushout β₁ β₂ hpo hpo').symm.toMonoidHom.comp α₁' = α₁Left-leg formula for the inverse pushout comparison equivalence.
Show proof
by
ext x
let e := pushoutEquivOfIsPushout β₁ β₂ hpo hpo'
exact e.injective <| by
calc
e ((e.symm.toMonoidHom.comp α₁') x) = α₁' x := by
simp only [MulEquiv.toMonoidHom_eq_coe, MonoidHom.comp_apply, MonoidHom.coe_coe, MulEquiv.apply_symm_apply]
_ = e (α₁ x) := by
simpa using
(congrArg (fun f : H₁ →* G' => f x)
(pushoutEquivOfIsPushout_left β₁ β₂ hpo hpo')).symmProof. Unfold the algebraic pushout as the quotient of the free product by the normal closure of the identifying relators. The two canonical maps agree on the common subgroup by construction, and a descent map out of the pushout is obtained from compatible maps on the two factors. The defining relators are killed exactly by the compatibility hypothesis, and uniqueness follows from the universal property of the quotient and the free product.
□@[simp 900] theorem pushoutEquivOfIsPushout_symm_right
{α₁ : H₁ →* G} {α₂ : H₂ →* G}
{α₁' : H₁ →* G'} {α₂' : H₂ →* G'}
(β₁ : H →* H₁) (β₂ : H →* H₂)
(hpo : IsPushoutSquare β₁ β₂ α₁ α₂)
(hpo' : IsPushoutSquare β₁ β₂ α₁' α₂') :
(pushoutEquivOfIsPushout β₁ β₂ hpo hpo').symm.toMonoidHom.comp α₂' = α₂Right-leg formula for the inverse pushout comparison equivalence.
Show proof
by
ext x
let e := pushoutEquivOfIsPushout β₁ β₂ hpo hpo'
exact e.injective <| by
calc
e ((e.symm.toMonoidHom.comp α₂') x) = α₂' x := by
simp only [MulEquiv.toMonoidHom_eq_coe, MonoidHom.comp_apply, MonoidHom.coe_coe, MulEquiv.apply_symm_apply]
_ = e (α₂ x) := by
simpa using
(congrArg (fun f : H₂ →* G' => f x)
(pushoutEquivOfIsPushout_right β₁ β₂ hpo hpo')).symmProof. Unfold the algebraic pushout as the quotient of the free product by the normal closure of the identifying relators. The two canonical maps agree on the common subgroup by construction, and a descent map out of the pushout is obtained from compatible maps on the two factors. The defining relators are killed exactly by the compatibility hypothesis, and uniqueness follows from the universal property of the quotient and the free product.
□@[simp 900] theorem pushoutContEquivOfIsPushout_symm_left
{α₁ : H₁ →ₜ* G} {α₂ : H₂ →ₜ* G}
{α₁' : H₁ →ₜ* G'} {α₂' : H₂ →ₜ* G'}
(β₁ : H →ₜ* H₁) (β₂ : H →ₜ* H₂)
(hpo : HasProfiniteTestPushoutProperty β₁ β₂ α₁ α₂)
(hpo' : HasProfiniteTestPushoutProperty β₁ β₂ α₁' α₂')
(hG : IsProfiniteGroup G) (hG' : IsProfiniteGroup G') :
(((pushoutContEquivOfIsPushout β₁ β₂ hpo hpo' hG hG').symm : G' →ₜ* G).comp α₁') = α₁Left-leg formula for the inverse profinite pushout comparison equivalence.
Show proof
by
ext x
let e := pushoutContEquivOfIsPushout β₁ β₂ hpo hpo' hG hG'
exact e.injective <| by
calc
e ((((e.symm : G' →ₜ* G).comp α₁') x)) = α₁' x := by
change e (e.symm (α₁' x)) = α₁' x
simp only [ContinuousMulEquiv.apply_symm_apply]
_ = e (α₁ x) := by
have hleft :
(pushoutContMapOfIsPushout β₁ β₂ hpo hpo' hG').comp α₁ = α₁' :=
pushoutContMapOfIsPushout_left β₁ β₂ hpo hpo' hG'
have hleft_apply :
pushoutContMapOfIsPushout β₁ β₂ hpo hpo' hG' (α₁ x) = α₁' x := by
exact congrFun (congrArg (fun f : H₁ →ₜ* G' => (f : H₁ → G')) hleft) x
change α₁' x = pushoutContMapOfIsPushout β₁ β₂ hpo hpo' hG' (α₁ x)
simpa using hleft_apply.symmProof. Unfold the algebraic pushout as the quotient of the free product by the normal closure of the identifying relators. The two canonical maps agree on the common subgroup by construction, and a descent map out of the pushout is obtained from compatible maps on the two factors. The defining relators are killed exactly by the compatibility hypothesis, and uniqueness follows from the universal property of the quotient and the free product.
□@[simp 900] theorem pushoutContEquivOfIsPushout_symm_right
{α₁ : H₁ →ₜ* G} {α₂ : H₂ →ₜ* G}
{α₁' : H₁ →ₜ* G'} {α₂' : H₂ →ₜ* G'}
(β₁ : H →ₜ* H₁) (β₂ : H →ₜ* H₂)
(hpo : HasProfiniteTestPushoutProperty β₁ β₂ α₁ α₂)
(hpo' : HasProfiniteTestPushoutProperty β₁ β₂ α₁' α₂')
(hG : IsProfiniteGroup G) (hG' : IsProfiniteGroup G') :
(((pushoutContEquivOfIsPushout β₁ β₂ hpo hpo' hG hG').symm : G' →ₜ* G).comp α₂') = α₂Right-leg formula for the inverse profinite pushout comparison equivalence.
Show proof
by
ext x
let e := pushoutContEquivOfIsPushout β₁ β₂ hpo hpo' hG hG'
exact e.injective <| by
calc
e ((((e.symm : G' →ₜ* G).comp α₂') x)) = α₂' x := by
change e (e.symm (α₂' x)) = α₂' x
simp only [ContinuousMulEquiv.apply_symm_apply]
_ = e (α₂ x) := by
have hright :
(pushoutContMapOfIsPushout β₁ β₂ hpo hpo' hG').comp α₂ = α₂' :=
pushoutContMapOfIsPushout_right β₁ β₂ hpo hpo' hG'
have hright_apply :
pushoutContMapOfIsPushout β₁ β₂ hpo hpo' hG' (α₂ x) = α₂' x := by
exact congrFun (congrArg (fun f : H₂ →ₜ* G' => (f : H₂ → G')) hright) x
change α₂' x = pushoutContMapOfIsPushout β₁ β₂ hpo hpo' hG' (α₂ x)
simpa using hright_apply.symmProof. Unfold the algebraic pushout as the quotient of the free product by the normal closure of the identifying relators. The two canonical maps agree on the common subgroup by construction, and a descent map out of the pushout is obtained from compatible maps on the two factors. The defining relators are killed exactly by the compatibility hypothesis, and uniqueness follows from the universal property of the quotient and the free product.
□