Module

AutomorphismDescent.lean

Nyll.EtaleFundamentalGroups.GaloisCategories.AutomorphismDescent

4 declarations indexed from sourceView source ↗

Module documentation

Descent of automorphisms of finite-valued functors

Objects and morphisms descend through a family of stage functors. A family of automorphisms compatible with refinement consequently glues to a unique automorphism. The descent assumptions concern objects and morphisms in the underlying categories, not existence or bijectivity of a fundamental-group comparison map.

Imports1

Nyll.EtaleFundamentalGroups.GaloisCategories.Functoriality

Imported by2

theorem

commutes_iso_inv

L27 ↗

CategoryTheory.PreGaloisCategory.commutes_iso_inv

Source context 4 commands

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

noncomputable section
open CategoryTheory
namespace CategoryTheory.PreGaloisCategory
universe u v u' v' w t

Lean source · statement

theorem commutes_iso_inv
    {D : Type u} [Category.{v} D] {X Y : D}
    (e : X ≅ Y) (a : X ⟶ X) (b : Y ⟶ Y)
    (h : e.hom ≫ b = a ≫ e.hom) :
    e.inv ≫ a = b ≫ e.inv

theorem

stageAut_naturality_of_eventualHom

L46 ↗

CategoryTheory.PreGaloisCategory.stageAut_naturality_of_eventualHom

Documentation

Eventual descent of morphisms makes a compatible family of stage automorphisms natural across different stages.

Source context 11 commands

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

noncomputable section
open CategoryTheory
namespace CategoryTheory.PreGaloisCategory
universe u v u' v' w t
variable {I : Type t} [Preorder I]
variable {C : Type u} [Category.{v} C]
variable (Cstage : I → Type u') [∀ i, Category.{v'} (Cstage i)]
variable (H : ∀ i, Cstage i ⥤ C)
variable (T : ∀ {i j : I}, i ≤ j → Cstage i ⥤ Cstage j)
variable (e : ∀ {i j : I} (hij : i ≤ j), H i ≅ T hij ⋙ H j)
variable (F : C ⥤ FintypeCat.{w})

Lean source · statement

theorem stageAut_naturality_of_eventualHom
    (hhom : ∀ (i j : I) (A : Cstage i) (B : Cstage j)
      (f : (H i).obj A ⟶ (H j).obj B),
      ∃ (k : I) (hik : i ≤ k) (hjk : j ≤ k)
        (g : (T hik).obj A ⟶ (T hjk).obj B),
        f = (e hik).hom.app A ≫ (H k).map g ≫ (e hjk).inv.app B)
    (σ : ∀ i, Aut (H i ⋙ F))
    (hσ : ∀ (i j : I) (hij : i ≤ j) (A : Cstage i),
      F.map ((e hij).hom.app A) ≫ (σ j).hom.app ((T hij).obj A) =
        (σ i).hom.app A ≫ F.map ((e hij).hom.app A))
    (i j : I) (A : Cstage i) (B : Cstage j)
    (f : (H i).obj A ⟶ (H j).obj B) :
    F.map f ≫ (σ j).hom.app B = (σ i).hom.app A ≫ F.map f

theorem

existsUnique_aut_of_joint_essSurj

L79 ↗

CategoryTheory.PreGaloisCategory.existsUnique_aut_of_joint_essSurj

Documentation

Joint essential surjectivity and naturality on all stage-image morphisms give a unique global automorphism. The proof chooses object models and proves independence through the given morphisms.

Source context 12 commands

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

noncomputable section
open CategoryTheory
namespace CategoryTheory.PreGaloisCategory
universe u v u' v' w t
variable {I : Type t} [Preorder I]
variable {C : Type u} [Category.{v} C]
variable (Cstage : I → Type u') [∀ i, Category.{v'} (Cstage i)]
variable (H : ∀ i, Cstage i ⥤ C)
variable (T : ∀ {i j : I}, i ≤ j → Cstage i ⥤ Cstage j)
variable (e : ∀ {i j : I} (hij : i ≤ j), H i ≅ T hij ⋙ H j)
variable (F : C ⥤ FintypeCat.{w})
omit [Preorder I] in

Lean source · statement

theorem existsUnique_aut_of_joint_essSurj
    (hobj : ∀ X : C, ∃ (i : I) (A : Cstage i), Nonempty ((H i).obj A ≅ X))
    (σ : ∀ i, Aut (H i ⋙ F))
    (hnat : ∀ (i j : I) (A : Cstage i) (B : Cstage j)
      (f : (H i).obj A ⟶ (H j).obj B),
      F.map f ≫ (σ j).hom.app B = (σ i).hom.app A ≫ F.map f) :
    ∃! a : Aut F, ∀ (i : I) (A : Cstage i),
      a.hom.app ((H i).obj A) = (σ i).hom.app A

theorem

existsUnique_aut_of_eventualHom

L139 ↗

CategoryTheory.PreGaloisCategory.existsUnique_aut_of_eventualHom

Documentation

Compatible automorphisms descend uniquely once objects and morphisms descend. No equality descent or faithfulness of a single stage functor is required for this automorphism statement.

Source context 11 commands

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

noncomputable section
open CategoryTheory
namespace CategoryTheory.PreGaloisCategory
universe u v u' v' w t
variable {I : Type t} [Preorder I]
variable {C : Type u} [Category.{v} C]
variable (Cstage : I → Type u') [∀ i, Category.{v'} (Cstage i)]
variable (H : ∀ i, Cstage i ⥤ C)
variable (T : ∀ {i j : I}, i ≤ j → Cstage i ⥤ Cstage j)
variable (e : ∀ {i j : I} (hij : i ≤ j), H i ≅ T hij ⋙ H j)
variable (F : C ⥤ FintypeCat.{w})

Lean source · statement

theorem existsUnique_aut_of_eventualHom
    (hobj : ∀ X : C, ∃ (i : I) (A : Cstage i), Nonempty ((H i).obj A ≅ X))
    (hhom : ∀ (i j : I) (A : Cstage i) (B : Cstage j)
      (f : (H i).obj A ⟶ (H j).obj B),
      ∃ (k : I) (hik : i ≤ k) (hjk : j ≤ k)
        (g : (T hik).obj A ⟶ (T hjk).obj B),
        f = (e hik).hom.app A ≫ (H k).map g ≫ (e hjk).inv.app B)
    (σ : ∀ i, Aut (H i ⋙ F))
    (hσ : ∀ (i j : I) (hij : i ≤ j) (A : Cstage i),
      F.map ((e hij).hom.app A) ≫ (σ j).hom.app ((T hij).obj A) =
        (σ i).hom.app A ≫ F.map ((e hij).hom.app A)) :
    ∃! a : Aut F, ∀ (i : I) (A : Cstage i),
      a.hom.app ((H i).obj A) = (σ i).hom.app A

Module documentation

Descent of automorphisms of finite-valued functors

Declarations

commutes_iso_inv

stageAut_naturality_of_eventualHom

existsUnique_aut_of_joint_essSurj

existsUnique_aut_of_eventualHom