Module

AlgebraicPullbacks.lean

Nyll.ProCGroups.Categorical.AlgebraicPullbacks

32 declarations indexed from sourceView source ↗

Module documentation

Pro C Groups / Categorical / Algebraic Pullbacks

This module develops concrete fiber products of groups, identifies them with the categorical pullback in GrpCat, and proves comparison and kernel criteria for the associated lift maps.

Imports3

Mathlib.Algebra.Category.Grp.Limits
Mathlib.GroupTheory.QuotientGroup.Basic
Mathlib.CategoryTheory.Limits.Shapes.Pullback.IsPullback.Defs

Imported by2

def

subgroup

L32 ↗

ProCGroups.Categorical.FiberProduct.subgroup

Documentation

Concrete pullback subgroup of \(\beta_1\) and \(\beta_2\).

Source context 7 commands

Surrounding namespaces, section variables, and local commands at this declaration.

namespace ProCGroups.Categorical
open CategoryTheory Limits
open scoped Pointwise
universe u v
section
variable {A G H H₁ H₂ : Type u} {K : Type v}
variable [Group A] [Group G] [Group H] [Group H₁] [Group H₂] [Group K]

Lean source · full declaration

def FiberProduct.subgroup (β₁ : H₁ →* H) (β₂ : H₂ →* H) : Subgroup (H₁ × H₂) where
  carrier := { x | β₁ x.1 = β₂ x.2 }
  one_mem' := by simp only [Set.mem_ofPred_eq, Prod.fst_one, map_one, Prod.snd_one]
  mul_mem' := by
    intro x y hx hy
    change β₁ x.1 = β₂ x.2 at hx
    change β₁ y.1 = β₂ y.2 at hy
    simpa [map_mul] using congrArg₂ (· * ·) hx hy
  inv_mem' := by
    intro x hx
    simpa [map_inv, hx]

abbrev

carrier

L45 ↗

ProCGroups.Categorical.FiberProduct.carrier

Documentation

Concrete pullback attached to \(\beta_1\) and \(\beta_2\).

Source context 7 commands

Surrounding namespaces, section variables, and local commands at this declaration.

namespace ProCGroups.Categorical
open CategoryTheory Limits
open scoped Pointwise
universe u v
section
variable {A G H H₁ H₂ : Type u} {K : Type v}
variable [Group A] [Group G] [Group H] [Group H₁] [Group H₂] [Group K]

Lean source · statement

abbrev FiberProduct.carrier (β₁ : H₁ →* H) (β₂ : H₂ →* H)

theorem

mem_pullbackSubgroup_iff

L49 ↗

ProCGroups.Categorical.mem_pullbackSubgroup_iff

Documentation

Membership in the pullback subgroup is equivalent to the displayed coordinate condition.

Source context 7 commands

Surrounding namespaces, section variables, and local commands at this declaration.

namespace ProCGroups.Categorical
open CategoryTheory Limits
open scoped Pointwise
universe u v
section
variable {A G H H₁ H₂ : Type u} {K : Type v}
variable [Group A] [Group G] [Group H] [Group H₁] [Group H₂] [Group K]

Lean source · statement

theorem mem_pullbackSubgroup_iff {β₁ : H₁ →* H} {β₂ : H₂ →* H}
    {x : H₁ × H₂} :
    x ∈ FiberProduct.subgroup β₁ β₂ ↔ β₁ x.1 = β₂ x.2

def

fst

L55 ↗

ProCGroups.Categorical.FiberProduct.fst

Documentation

The first projection from the concrete pullback.

Source context 7 commands

Surrounding namespaces, section variables, and local commands at this declaration.

namespace ProCGroups.Categorical
open CategoryTheory Limits
open scoped Pointwise
universe u v
section
variable {A G H H₁ H₂ : Type u} {K : Type v}
variable [Group A] [Group G] [Group H] [Group H₁] [Group H₂] [Group K]

Lean source · full declaration

def FiberProduct.fst (β₁ : H₁ →* H) (β₂ : H₂ →* H) : FiberProduct.carrier β₁ β₂ →* H₁ where
  toFun := fun x => x.1.1
  map_one' := rfl
  map_mul' := by
    intro x y
    rfl

def

snd

L63 ↗

ProCGroups.Categorical.FiberProduct.snd

Documentation

The second projection from the concrete pullback.

Source context 7 commands

Surrounding namespaces, section variables, and local commands at this declaration.

namespace ProCGroups.Categorical
open CategoryTheory Limits
open scoped Pointwise
universe u v
section
variable {A G H H₁ H₂ : Type u} {K : Type v}
variable [Group A] [Group G] [Group H] [Group H₁] [Group H₂] [Group K]

Lean source · full declaration

def FiberProduct.snd (β₁ : H₁ →* H) (β₂ : H₂ →* H) : FiberProduct.carrier β₁ β₂ →* H₂ where
  toFun := fun x => x.1.2
  map_one' := rfl
  map_mul' := by
    intro x y
    rfl

def

lift

L71 ↗

ProCGroups.Categorical.FiberProduct.lift

Documentation

The canonical homomorphism into the concrete pullback.

Source context 7 commands

Surrounding namespaces, section variables, and local commands at this declaration.

namespace ProCGroups.Categorical
open CategoryTheory Limits
open scoped Pointwise
universe u v
section
variable {A G H H₁ H₂ : Type u} {K : Type v}
variable [Group A] [Group G] [Group H] [Group H₁] [Group H₂] [Group K]

Lean source · full declaration

def FiberProduct.lift (β₁ : H₁ →* H) (β₂ : H₂ →* H)
    (φ₁ : K →* H₁) (φ₂ : K →* H₂)
    (h : ∀ k, β₁ (φ₁ k) = β₂ (φ₂ k)) : K →* FiberProduct.carrier β₁ β₂ where
  toFun := fun k => ⟨(φ₁ k, φ₂ k), h k⟩
  map_one' := by
    apply Subtype.ext
    simp only [map_one, OneMemClass.coe_one, Prod.mk_eq_one, and_self]
  map_mul' := by
    intro x y
    apply Subtype.ext
    simp only [map_mul, Subgroup.coe_mul, Prod.mk_mul_mk]

def

cone

L84 ↗

ProCGroups.Categorical.FiberProduct.cone

Documentation

The concrete group pullback as a categorical pullback cone in GrpCat.

Source context 7 commands

Surrounding namespaces, section variables, and local commands at this declaration.

namespace ProCGroups.Categorical
open CategoryTheory Limits
open scoped Pointwise
universe u v
section
variable {A G H H₁ H₂ : Type u} {K : Type v}
variable [Group A] [Group G] [Group H] [Group H₁] [Group H₂] [Group K]

Lean source · statement

def FiberProduct.cone (β₁ : H₁ →* H) (β₂ : H₂ →* H) :
    PullbackCone (GrpCat.ofHom β₁) (GrpCat.ofHom β₂)

def

isLimitCone

L95 ↗

ProCGroups.Categorical.FiberProduct.isLimitCone

Documentation

The concrete group pullback cone is a limit cone in GrpCat.

Source context 7 commands

Surrounding namespaces, section variables, and local commands at this declaration.

namespace ProCGroups.Categorical
open CategoryTheory Limits
open scoped Pointwise
universe u v
section
variable {A G H H₁ H₂ : Type u} {K : Type v}
variable [Group A] [Group G] [Group H] [Group H₁] [Group H₂] [Group K]

Lean source · statement

def FiberProduct.isLimitCone (β₁ : H₁ →* H) (β₂ : H₂ →* H) :
    IsLimit (FiberProduct.cone β₁ β₂)

theorem

isPullback

L128 ↗

ProCGroups.Categorical.FiberProduct.isPullback

Documentation

The concrete group fiber product is a pullback in mathlib's bundled category of groups.

Source context 7 commands

Surrounding namespaces, section variables, and local commands at this declaration.

namespace ProCGroups.Categorical
open CategoryTheory Limits
open scoped Pointwise
universe u v
section
variable {A G H H₁ H₂ : Type u} {K : Type v}
variable [Group A] [Group G] [Group H] [Group H₁] [Group H₂] [Group K]

Lean source · statement

theorem FiberProduct.isPullback (β₁ : H₁ →* H) (β₂ : H₂ →* H) :
    CategoryTheory.IsPullback
      (GrpCat.ofHom (FiberProduct.fst β₁ β₂))
      (GrpCat.ofHom (FiberProduct.snd β₁ β₂))
      (GrpCat.ofHom β₁) (GrpCat.ofHom β₂)

theorem

ker_pullbackLift

L139 ↗

ProCGroups.Categorical.ker_pullbackLift

Documentation

The kernel of the canonical map into a concrete pullback is the intersection of the two coordinate kernels.

Source context 7 commands

Surrounding namespaces, section variables, and local commands at this declaration.

namespace ProCGroups.Categorical
open CategoryTheory Limits
open scoped Pointwise
universe u v
section
variable {A G H H₁ H₂ : Type u} {K : Type v}
variable [Group A] [Group G] [Group H] [Group H₁] [Group H₂] [Group K]

Lean source · statement

theorem ker_pullbackLift (β₁ : H₁ →* H) (β₂ : H₂ →* H)
    (φ₁ : K →* H₁) (φ₂ : K →* H₂)
    (h : ∀ k, β₁ (φ₁ k) = β₂ (φ₂ k)) :
    (FiberProduct.lift β₁ β₂ φ₁ φ₂ h).ker = φ₁.ker ⊓ φ₂.ker

theorem

pullbackLift_injective_iff

L157 ↗

ProCGroups.Categorical.pullbackLift_injective_iff

Documentation

The canonical map into a concrete pullback is injective iff the two coordinate kernels intersect trivially.

Source context 7 commands

Surrounding namespaces, section variables, and local commands at this declaration.

namespace ProCGroups.Categorical
open CategoryTheory Limits
open scoped Pointwise
universe u v
section
variable {A G H H₁ H₂ : Type u} {K : Type v}
variable [Group A] [Group G] [Group H] [Group H₁] [Group H₂] [Group K]

Lean source · statement

theorem pullbackLift_injective_iff (β₁ : H₁ →* H) (β₂ : H₂ →* H)
    {φ₁ : K →* H₁} {φ₂ : K →* H₂}
    (h : ∀ k, β₁ (φ₁ k) = β₂ (φ₂ k)) :
    Function.Injective (FiberProduct.lift β₁ β₂ φ₁ φ₂ h) ↔ φ₁.ker ⊓ φ₂.ker = ⊥

theorem

ker_sup_le_ker_comp_of_comp_eq

L167 ↗

ProCGroups.Categorical.ker_sup_le_ker_comp_of_comp_eq

Documentation

The supremum of the two kernels is contained in the kernel of the composite when the composites agree.

Source context 7 commands

Surrounding namespaces, section variables, and local commands at this declaration.

namespace ProCGroups.Categorical
open CategoryTheory Limits
open scoped Pointwise
universe u v
section
variable {A G H H₁ H₂ : Type u} {K : Type v}
variable [Group A] [Group G] [Group H] [Group H₁] [Group H₂] [Group K]

Lean source · statement

theorem ker_sup_le_ker_comp_of_comp_eq
    (β₁ : H₁ →* H) (β₂ : H₂ →* H)
    (φ₁ : K →* H₁) (φ₂ : K →* H₂)
    (hcomp : β₁.comp φ₁ = β₂.comp φ₂) :
    φ₁.ker ⊔ φ₂.ker ≤ (β₁.comp φ₁).ker

theorem

pullbackLift_surjective_iff_ker_comp_le_sup_ker

L187 ↗

ProCGroups.Categorical.pullbackLift_surjective_iff_ker_comp_le_sup_ker

Documentation

The algebraic pullback lift is surjective exactly when the composite kernel is contained in the supremum of the two coordinate kernels.

Source context 7 commands

Surrounding namespaces, section variables, and local commands at this declaration.

namespace ProCGroups.Categorical
open CategoryTheory Limits
open scoped Pointwise
universe u v
section
variable {A G H H₁ H₂ : Type u} {K : Type v}
variable [Group A] [Group G] [Group H] [Group H₁] [Group H₂] [Group K]

Lean source · full declaration

theorem pullbackLift_surjective_iff_ker_comp_le_sup_ker
    {β₁ : H₁ →* H} (β₂ : H₂ →* H)
    {φ₁ : K →* H₁} {φ₂ : K →* H₂}
    (hφ₁ : Function.Surjective φ₁) (hφ₂ : Function.Surjective φ₂)
    (hcomp : β₁.comp φ₁ = β₂.comp φ₂) :
    Function.Surjective (FiberProduct.lift β₁ β₂ φ₁ φ₂
        (fun k => DFunLike.congr_fun hcomp k)) ↔
      (β₁.comp φ₁).ker ≤ φ₁.ker ⊔ φ₂.ker := by
  constructor
  · intro hsurj k hk
    let z : FiberProduct.carrier β₁ β₂ :=
      ⟨(φ₁ k, 1), by
        change β₁ (φ₁ k) = β₂ 1
        simpa using hk⟩
    rcases hsurj z with ⟨a, ha⟩
    have hφ₁a : φ₁ a = φ₁ k := by
      exact congrArg (fun y => FiberProduct.fst β₁ β₂ y) ha
    have hφ₂a : φ₂ a = 1 := by
      exact congrArg (fun y => FiberProduct.snd β₁ β₂ y) ha
    have ha_ker₂ : a ∈ φ₂.ker := by
      simpa using hφ₂a
    have ha_inv_mul_ker₁ : a⁻¹ * k ∈ φ₁.ker := by
      change φ₁ (a⁻¹ * k) = 1
      simp only [map_mul, map_inv, hφ₁a, inv_mul_cancel]
    have hprod : a * (a⁻¹ * k) ∈ φ₁.ker ⊔ φ₂.ker :=
      (φ₁.ker ⊔ φ₂.ker).mul_mem
        ((le_sup_right : φ₂.ker ≤ φ₁.ker ⊔ φ₂.ker) ha_ker₂)
        ((le_sup_left : φ₁.ker ≤ φ₁.ker ⊔ φ₂.ker) ha_inv_mul_ker₁)
    simpa [mul_assoc] using hprod
  · intro hker_le z
    rcases hφ₁ z.1.1 with ⟨a₁, ha₁⟩
    rcases hφ₂ z.1.2 with ⟨a₂, ha₂⟩
    have hEq : β₁ (φ₁ a₁) = β₁ (φ₁ a₂) := by
      calc
        β₁ (φ₁ a₁) = β₁ z.1.1 := by simp only [ha₁]
        _ = β₂ z.1.2 := z.2
        _ = β₂ (φ₂ a₂) := by simp only [ha₂]
        _ = β₁ (φ₁ a₂) := by
          exact (DFunLike.congr_fun hcomp a₂).symm
    have hgker : a₁ * a₂⁻¹ ∈ (β₁.comp φ₁).ker := by
      change β₁ (φ₁ (a₁ * a₂⁻¹)) = 1
      simp only [map_mul, map_inv, hEq, mul_inv_cancel]
    have hgjoin : a₁ * a₂⁻¹ ∈ (φ₁.ker : Subgroup K) ⊔ (φ₂.ker : Subgroup K) :=
      hker_le hgker
    have hgjoin' : a₁ * a₂⁻¹ ∈ ((φ₁.ker : Set K) * (φ₂.ker : Set K)) := by
      rw [← Subgroup.mul_normal (φ₁.ker) (φ₂.ker)]
      simpa [SetLike.mem_coe] using hgjoin
    rcases (show ∃ y ∈ (φ₁.ker : Set K), ∃ z ∈ (φ₂.ker : Set K),
        y * z = a₁ * a₂⁻¹ from by
          simpa [Set.mem_mul] using hgjoin') with ⟨k₁, hk₁, k₂, hk₂, hkprod⟩
    have hk₁' : φ₁ k₁ = 1 := by simpa using hk₁
    have hk₂' : φ₂ k₂ = 1 := by simpa using hk₂
    have haeq : a₁ = k₁ * k₂ * a₂ := by
      calc
        a₁ = (a₁ * a₂⁻¹) * a₂ := by simp only [mul_assoc, inv_mul_cancel, mul_one]
        _ = (k₁ * k₂) * a₂ := by rw [hkprod]
        _ = k₁ * k₂ * a₂ := by simp only [mul_assoc]
    refine ⟨k₂ * a₂, ?_⟩
    apply Subtype.ext
    apply Prod.ext
    · calc
        φ₁ (k₂ * a₂) = φ₁ (k₁ * k₂ * a₂) := by
          simp only [map_mul, mul_assoc, hk₁', one_mul]
        _ = φ₁ a₁ := by rw [haeq]
        _ = z.1.1 := ha₁
    · calc
        φ₂ (k₂ * a₂) = φ₂ k₂ * φ₂ a₂ := by rw [map_mul]
        _ = 1 * φ₂ a₂ := by simp only [hk₂', one_mul]
        _ = z.1.2 := by simp only [ha₂, one_mul]

theorem

pullbackLift_surjective_iff_ker_eq

L258 ↗

ProCGroups.Categorical.pullbackLift_surjective_iff_ker_eq

Documentation

Surjectivity of the algebraic pullback lift is equivalent to the required kernel equality.

Source context 7 commands

Surrounding namespaces, section variables, and local commands at this declaration.

namespace ProCGroups.Categorical
open CategoryTheory Limits
open scoped Pointwise
universe u v
section
variable {A G H H₁ H₂ : Type u} {K : Type v}
variable [Group A] [Group G] [Group H] [Group H₁] [Group H₂] [Group K]

Lean source · full declaration

theorem pullbackLift_surjective_iff_ker_eq
    {β₁ : H₁ →* H} (β₂ : H₂ →* H)
    {φ₁ : K →* H₁} {φ₂ : K →* H₂}
    (hφ₁ : Function.Surjective φ₁) (hφ₂ : Function.Surjective φ₂)
    (hcomp : β₁.comp φ₁ = β₂.comp φ₂) :
    Function.Surjective (FiberProduct.lift β₁ β₂ φ₁ φ₂
        (fun k => DFunLike.congr_fun hcomp k)) ↔
      (β₁.comp φ₁).ker = φ₁.ker ⊔ φ₂.ker := by
  constructor
  · intro hsurj
    exact le_antisymm
      ((pullbackLift_surjective_iff_ker_comp_le_sup_ker
        (β₁ := β₁) (β₂ := β₂) (φ₁ := φ₁) (φ₂ := φ₂) hφ₁ hφ₂ hcomp).1 hsurj)
      (ker_sup_le_ker_comp_of_comp_eq β₁ β₂ φ₁ φ₂ hcomp)
  · intro hker
    exact (pullbackLift_surjective_iff_ker_comp_le_sup_ker
      (β₁ := β₁) (β₂ := β₂) (φ₁ := φ₁) (φ₂ := φ₂) hφ₁ hφ₂ hcomp).2 (by
        intro k hk
        rw [← hker]
        exact hk)

theorem

pullbackFst_pullbackLift

L280 ↗

ProCGroups.Categorical.pullbackFst_pullbackLift

Documentation

Composing the first projection with the canonical pullback lift gives \(\varphi_1\).

Source context 7 commands

Surrounding namespaces, section variables, and local commands at this declaration.

namespace ProCGroups.Categorical
open CategoryTheory Limits
open scoped Pointwise
universe u v
section
variable {A G H H₁ H₂ : Type u} {K : Type v}
variable [Group A] [Group G] [Group H] [Group H₁] [Group H₂] [Group K]

Lean source · statement

theorem pullbackFst_pullbackLift (β₁ : H₁ →* H) (β₂ : H₂ →* H)
    (φ₁ : K →* H₁) (φ₂ : K →* H₂)
    (h : ∀ k, β₁ (φ₁ k) = β₂ (φ₂ k)) :
    (FiberProduct.fst β₁ β₂).comp (FiberProduct.lift β₁ β₂ φ₁ φ₂ h) = φ₁

theorem

pullbackSnd_pullbackLift

L288 ↗

ProCGroups.Categorical.pullbackSnd_pullbackLift

Documentation

Composing the second projection with the canonical pullback lift gives \(\varphi_2\).

Source context 7 commands

Surrounding namespaces, section variables, and local commands at this declaration.

namespace ProCGroups.Categorical
open CategoryTheory Limits
open scoped Pointwise
universe u v
section
variable {A G H H₁ H₂ : Type u} {K : Type v}
variable [Group A] [Group G] [Group H] [Group H₁] [Group H₂] [Group K]

Lean source · statement

theorem pullbackSnd_pullbackLift (β₁ : H₁ →* H) (β₂ : H₂ →* H)
    (φ₁ : K →* H₁) (φ₂ : K →* H₂)
    (h : ∀ k, β₁ (φ₁ k) = β₂ (φ₂ k)) :
    (FiberProduct.snd β₁ β₂).comp (FiberProduct.lift β₁ β₂ φ₁ φ₂ h) = φ₂

theorem

pullbackLift_injective_of_left_injective

L298 ↗

ProCGroups.Categorical.pullbackLift_injective_of_left_injective

Documentation

If \(\varphi_1\) is injective, then the canonical map into the concrete pullback is injective.

Source context 7 commands

Surrounding namespaces, section variables, and local commands at this declaration.

namespace ProCGroups.Categorical
open CategoryTheory Limits
open scoped Pointwise
universe u v
section
variable {A G H H₁ H₂ : Type u} {K : Type v}
variable [Group A] [Group G] [Group H] [Group H₁] [Group H₂] [Group K]

Lean source · statement

theorem pullbackLift_injective_of_left_injective (β₁ : H₁ →* H) (β₂ : H₂ →* H)
    (φ₁ : K →* H₁) (φ₂ : K →* H₂)
    (h : ∀ k, β₁ (φ₁ k) = β₂ (φ₂ k))
    (hφ₁ : Function.Injective φ₁) :
    Function.Injective (FiberProduct.lift β₁ β₂ φ₁ φ₂ h)

theorem

pullbackLift_injective_of_right_injective

L310 ↗

ProCGroups.Categorical.pullbackLift_injective_of_right_injective

Documentation

If \(\varphi_2\) is injective, then the canonical map into the concrete pullback is injective.

Source context 7 commands

Surrounding namespaces, section variables, and local commands at this declaration.

namespace ProCGroups.Categorical
open CategoryTheory Limits
open scoped Pointwise
universe u v
section
variable {A G H H₁ H₂ : Type u} {K : Type v}
variable [Group A] [Group G] [Group H] [Group H₁] [Group H₂] [Group K]

Lean source · statement

theorem pullbackLift_injective_of_right_injective (β₁ : H₁ →* H) (β₂ : H₂ →* H)
    (φ₁ : K →* H₁) (φ₂ : K →* H₂)
    (h : ∀ k, β₁ (φ₁ k) = β₂ (φ₂ k))
    (hφ₂ : Function.Injective φ₂) :
    Function.Injective (FiberProduct.lift β₁ β₂ φ₁ φ₂ h)

theorem

hom_ext

L320 ↗

ProCGroups.Categorical.FiberProduct.hom_ext

Documentation

Two homomorphisms into the concrete pullback are equal once both coordinates agree.

Source context 7 commands

Surrounding namespaces, section variables, and local commands at this declaration.

namespace ProCGroups.Categorical
open CategoryTheory Limits
open scoped Pointwise
universe u v
section
variable {A G H H₁ H₂ : Type u} {K : Type v}
variable [Group A] [Group G] [Group H] [Group H₁] [Group H₂] [Group K]

Lean source · statement

theorem FiberProduct.hom_ext {β₁ : H₁ →* H} {β₂ : H₂ →* H}
    {K : Type v} [Group K]
    {ψ ψ' : K →* FiberProduct.carrier β₁ β₂}
    (h₁ : ∀ k, FiberProduct.fst β₁ β₂ (ψ k) = FiberProduct.fst β₁ β₂ (ψ' k))
    (h₂ : ∀ k, FiberProduct.snd β₁ β₂ (ψ k) = FiberProduct.snd β₁ β₂ (ψ' k)) :
    ψ = ψ'

def

congr

L333 ↗

ProCGroups.Categorical.FiberProduct.congr

Documentation

Transport a concrete fiber product across equal cospan maps.

Source context 8 commands

Surrounding namespaces, section variables, and local commands at this declaration.

namespace ProCGroups.Categorical
open CategoryTheory Limits
open scoped Pointwise
universe u v
section
variable {A G H H₁ H₂ : Type u} {K : Type v}
variable [Group A] [Group G] [Group H] [Group H₁] [Group H₂] [Group K]
namespace FiberProduct

Lean source · statement

def congr {β₁ β₁' : H₁ →* H} {β₂ β₂' : H₂ →* H}
    (h₁ : β₁ = β₁') (h₂ : β₂ = β₂') :
    carrier β₁ β₂ ≃* carrier β₁' β₂'

theorem

pullbackLift_eta

L343 ↗

ProCGroups.Categorical.pullbackLift_eta

Documentation

The concrete pullback is reconstructed from its two projections by the canonical lift.

Source context 7 commands

Surrounding namespaces, section variables, and local commands at this declaration.

namespace ProCGroups.Categorical
open CategoryTheory Limits
open scoped Pointwise
universe u v
section
variable {A G H H₁ H₂ : Type u} {K : Type v}
variable [Group A] [Group G] [Group H] [Group H₁] [Group H₂] [Group K]

Lean source · full declaration

theorem pullbackLift_eta {β₁ : H₁ →* H} {β₂ : H₂ →* H}
    {K : Type v} [Group K]
    (ψ : K →* FiberProduct.carrier β₁ β₂) :
    FiberProduct.lift β₁ β₂
      ((FiberProduct.fst β₁ β₂).comp ψ)
      ((FiberProduct.snd β₁ β₂).comp ψ)
      (fun k => by exact (ψ k).2) = ψ := by
  apply FiberProduct.hom_ext
  · intro k
    rfl
  · intro k
    rfl

def

pullbackSwap

L357 ↗

ProCGroups.Categorical.pullbackSwap

Documentation

Symmetry of the concrete pullback.

Source context 7 commands

Surrounding namespaces, section variables, and local commands at this declaration.

namespace ProCGroups.Categorical
open CategoryTheory Limits
open scoped Pointwise
universe u v
section
variable {A G H H₁ H₂ : Type u} {K : Type v}
variable [Group A] [Group G] [Group H] [Group H₁] [Group H₂] [Group K]

Lean source · full declaration

def pullbackSwap (β₁ : H₁ →* H) (β₂ : H₂ →* H) :
    FiberProduct.carrier β₁ β₂ ≃* FiberProduct.carrier β₂ β₁ where
  toFun := fun x => ⟨(x.1.2, x.1.1), x.2.symm⟩
  invFun := fun x => ⟨(x.1.2, x.1.1), x.2.symm⟩
  left_inv := by
    intro x
    apply Subtype.ext
    rfl
  right_inv := by
    intro x
    apply Subtype.ext
    rfl
  map_mul' := by
    intro x y
    apply Subtype.ext
    rfl

theorem

pullbackFst_pullbackSwap

L375 ↗

ProCGroups.Categorical.pullbackFst_pullbackSwap

Documentation

The first projection after swapping equals the original second projection.

Source context 7 commands

Surrounding namespaces, section variables, and local commands at this declaration.

namespace ProCGroups.Categorical
open CategoryTheory Limits
open scoped Pointwise
universe u v
section
variable {A G H H₁ H₂ : Type u} {K : Type v}
variable [Group A] [Group G] [Group H] [Group H₁] [Group H₂] [Group K]

Lean source · statement

theorem pullbackFst_pullbackSwap (β₁ : H₁ →* H) (β₂ : H₂ →* H)
    (x : FiberProduct.carrier β₁ β₂) :
    FiberProduct.fst β₂ β₁ (pullbackSwap β₁ β₂ x) = FiberProduct.snd β₁ β₂ x

theorem

pullbackSnd_pullbackSwap

L381 ↗

ProCGroups.Categorical.pullbackSnd_pullbackSwap

Documentation

The second projection after swapping equals the original first projection.

Source context 7 commands

Surrounding namespaces, section variables, and local commands at this declaration.

namespace ProCGroups.Categorical
open CategoryTheory Limits
open scoped Pointwise
universe u v
section
variable {A G H H₁ H₂ : Type u} {K : Type v}
variable [Group A] [Group G] [Group H] [Group H₁] [Group H₂] [Group K]

Lean source · statement

theorem pullbackSnd_pullbackSwap (β₁ : H₁ →* H) (β₂ : H₂ →* H)
    (x : FiberProduct.carrier β₁ β₂) :
    FiberProduct.snd β₂ β₁ (pullbackSwap β₁ β₂ x) = FiberProduct.fst β₁ β₂ x

theorem

pullbackSwap_symm

L390 ↗

ProCGroups.Categorical.pullbackSwap_symm

Documentation

The symmetry map for the algebraic pullback is inverse to the corresponding swapped pullback comparison.

Source context 7 commands

Surrounding namespaces, section variables, and local commands at this declaration.

namespace ProCGroups.Categorical
open CategoryTheory Limits
open scoped Pointwise
universe u v
section
variable {A G H H₁ H₂ : Type u} {K : Type v}
variable [Group A] [Group G] [Group H] [Group H₁] [Group H₂] [Group K]

Lean source · statement

theorem pullbackSwap_symm (β₁ : H₁ →* H) (β₂ : H₂ →* H) :
    (pullbackSwap β₁ β₂).symm = pullbackSwap β₂ β₁

theorem

pullbackFst_surjective_of_right_surjective

L396 ↗

ProCGroups.Categorical.pullbackFst_surjective_of_right_surjective

Documentation

If the right cospan map is surjective, then the first projection from the fiber product is surjective.

Source context 7 commands

Surrounding namespaces, section variables, and local commands at this declaration.

namespace ProCGroups.Categorical
open CategoryTheory Limits
open scoped Pointwise
universe u v
section
variable {A G H H₁ H₂ : Type u} {K : Type v}
variable [Group A] [Group G] [Group H] [Group H₁] [Group H₂] [Group K]

Lean source · statement

theorem pullbackFst_surjective_of_right_surjective
    (β₁ : H₁ →* H) (β₂ : H₂ →* H)
    (hβ₂ : Function.Surjective β₂) :
    Function.Surjective (FiberProduct.fst β₁ β₂)

theorem

pullbackSnd_surjective_of_left_surjective

L407 ↗

ProCGroups.Categorical.pullbackSnd_surjective_of_left_surjective

Documentation

If the left cospan map is surjective, then the second projection from the fiber product is surjective.

Source context 7 commands

Surrounding namespaces, section variables, and local commands at this declaration.

namespace ProCGroups.Categorical
open CategoryTheory Limits
open scoped Pointwise
universe u v
section
variable {A G H H₁ H₂ : Type u} {K : Type v}
variable [Group A] [Group G] [Group H] [Group H₁] [Group H₂] [Group K]

Lean source · statement

theorem pullbackSnd_surjective_of_left_surjective
    (β₁ : H₁ →* H) (β₂ : H₂ →* H)
    (hβ₁ : Function.Surjective β₁) :
    Function.Surjective (FiberProduct.snd β₁ β₂)

theorem

pullbackFst_injective_of_right_injective

L417 ↗

ProCGroups.Categorical.pullbackFst_injective_of_right_injective

Documentation

If \(\beta_2\) is injective, then the first pullback projection is injective.

Source context 7 commands

Surrounding namespaces, section variables, and local commands at this declaration.

namespace ProCGroups.Categorical
open CategoryTheory Limits
open scoped Pointwise
universe u v
section
variable {A G H H₁ H₂ : Type u} {K : Type v}
variable [Group A] [Group G] [Group H] [Group H₁] [Group H₂] [Group K]

Lean source · statement

theorem pullbackFst_injective_of_right_injective
    (β₁ : H₁ →* H) (β₂ : H₂ →* H)
    (hβ₂ : Function.Injective β₂) :
    Function.Injective (FiberProduct.fst β₁ β₂)

theorem

pullbackSnd_injective_of_left_injective

L433 ↗

ProCGroups.Categorical.pullbackSnd_injective_of_left_injective

Documentation

If \(\beta_1\) is injective, then the second pullback projection is injective.

Source context 7 commands

Surrounding namespaces, section variables, and local commands at this declaration.

namespace ProCGroups.Categorical
open CategoryTheory Limits
open scoped Pointwise
universe u v
section
variable {A G H H₁ H₂ : Type u} {K : Type v}
variable [Group A] [Group G] [Group H] [Group H₁] [Group H₂] [Group K]

Lean source · statement

theorem pullbackSnd_injective_of_left_injective
    (β₁ : H₁ →* H) (β₂ : H₂ →* H)
    (hβ₁ : Function.Injective β₁) :
    Function.Injective (FiberProduct.snd β₁ β₂)

theorem

surjective_pullbackLift_of_ker_eq

L450 ↗

ProCGroups.Categorical.surjective_pullbackLift_of_ker_eq

Documentation

Surjective coordinate maps whose composite kernel is the supremum of their kernels induce a surjective map into the concrete fiber product.

Source context 7 commands

Surrounding namespaces, section variables, and local commands at this declaration.

namespace ProCGroups.Categorical
open CategoryTheory Limits
open scoped Pointwise
universe u v
section
variable {A G H H₁ H₂ : Type u} {K : Type v}
variable [Group A] [Group G] [Group H] [Group H₁] [Group H₂] [Group K]

Lean source · full declaration

theorem surjective_pullbackLift_of_ker_eq
    (β₁ : H₁ →* H) (β₂ : H₂ →* H)
    (φ₁ : A →* H₁) (φ₂ : A →* H₂)
    (hφ₁ : Function.Surjective φ₁) (hφ₂ : Function.Surjective φ₂)
    (hcomp : β₁.comp φ₁ = β₂.comp φ₂)
    (hker : (β₁.comp φ₁).ker = φ₁.ker ⊔ φ₂.ker) :
    Function.Surjective (FiberProduct.lift β₁ β₂ φ₁ φ₂ (fun a => by
      exact DFunLike.congr_fun hcomp a)) := by
  exact (pullbackLift_surjective_iff_ker_eq (β₁ := β₁) (β₂ := β₂) (φ₁ := φ₁) (φ₂ := φ₂) hφ₁ hφ₂
      hcomp).2 hker

theorem

bijective_pullbackLift_of_left_injective_of_ker_eq

L465 ↗

ProCGroups.Categorical.bijective_pullbackLift_of_left_injective_of_ker_eq

Documentation

The algebraic pullback lift is bijective when the left map is injective and the required kernel equality holds.

Source context 7 commands

Surrounding namespaces, section variables, and local commands at this declaration.

namespace ProCGroups.Categorical
open CategoryTheory Limits
open scoped Pointwise
universe u v
section
variable {A G H H₁ H₂ : Type u} {K : Type v}
variable [Group A] [Group G] [Group H] [Group H₁] [Group H₂] [Group K]

Lean source · full declaration

theorem bijective_pullbackLift_of_left_injective_of_ker_eq
    (β₁ : H₁ →* H) (β₂ : H₂ →* H)
    (φ₁ : A →* H₁) (φ₂ : A →* H₂)
    (hφ₁surj : Function.Surjective φ₁) (hφ₂surj : Function.Surjective φ₂)
    (hcomp : β₁.comp φ₁ = β₂.comp φ₂)
    (hker : (β₁.comp φ₁).ker = φ₁.ker ⊔ φ₂.ker)
    (hφ₁inj : Function.Injective φ₁) :
    Function.Bijective (FiberProduct.lift β₁ β₂ φ₁ φ₂ (fun a => by
      exact DFunLike.congr_fun hcomp a)) := by
  refine ⟨?_, ?_⟩
  · exact pullbackLift_injective_of_left_injective β₁ β₂ φ₁ φ₂
      (fun a => DFunLike.congr_fun hcomp a) hφ₁inj
  · exact (pullbackLift_surjective_iff_ker_eq
      (β₁ := β₁) (β₂ := β₂) (φ₁ := φ₁) (φ₂ := φ₂) hφ₁surj hφ₂surj hcomp).2 hker

theorem

bijective_pullbackLift_of_right_injective_of_ker_eq

L484 ↗

ProCGroups.Categorical.bijective_pullbackLift_of_right_injective_of_ker_eq

Documentation

The algebraic pullback lift is bijective when the right map is injective and the required kernel equality holds.

Source context 7 commands

Surrounding namespaces, section variables, and local commands at this declaration.

namespace ProCGroups.Categorical
open CategoryTheory Limits
open scoped Pointwise
universe u v
section
variable {A G H H₁ H₂ : Type u} {K : Type v}
variable [Group A] [Group G] [Group H] [Group H₁] [Group H₂] [Group K]

Lean source · full declaration

theorem bijective_pullbackLift_of_right_injective_of_ker_eq
    (β₁ : H₁ →* H) (β₂ : H₂ →* H)
    (φ₁ : A →* H₁) (φ₂ : A →* H₂)
    (hφ₁surj : Function.Surjective φ₁) (hφ₂surj : Function.Surjective φ₂)
    (hcomp : β₁.comp φ₁ = β₂.comp φ₂)
    (hker : (β₁.comp φ₁).ker = φ₁.ker ⊔ φ₂.ker)
    (hφ₂inj : Function.Injective φ₂) :
    Function.Bijective (FiberProduct.lift β₁ β₂ φ₁ φ₂ (fun a => by
      exact DFunLike.congr_fun hcomp a)) := by
  refine ⟨?_, ?_⟩
  · exact pullbackLift_injective_of_right_injective β₁ β₂ φ₁ φ₂
      (fun a => DFunLike.congr_fun hcomp a) hφ₂inj
  · exact (pullbackLift_surjective_iff_ker_eq
      (β₁ := β₁) (β₂ := β₂) (φ₁ := φ₁) (φ₂ := φ₂) hφ₁surj hφ₂surj hcomp).2 hker

Module documentation

Pro C Groups / Categorical / Algebraic Pullbacks

Declarations