Theorem: Profinite.extensivity (Profinite/ExplicitSheaves.lean)

State before:
α : Type
x✝ : Fintype α
X : Profinite
Z : α → Profinite
i : (a : α) → Z a ⟶ X
Y : Profinite
f : Y ⟶ X
H : IsIso (Sigma.desc i)
⊢ IsIso (Sigma.desc fun x => Limits.pullback.fst)
Tactic:
let θ := Sigma.mapIso (fun a => fromExplicitIso f (i a))
State after:
α : Type
x✝ : Fintype α
X : Profinite
Z : α → Profinite
i : (a : α) → Z a ⟶ X
Y : Profinite
f : Y ⟶ X
H : IsIso (Sigma.desc i)
θ : (∐ fun a => pullback f (i a)) ≅ ∐ fun a => Limits.pullback f (i a) := Sigma.mapIso fun a => fromExplicitIso f (i a)
⊢ IsIso (Sigma.desc fun x => Limits.pullback.fst)

State before:
α : Type
x✝ : Fintype α
X : Profinite
Z : α → Profinite
i : (a : α) → Z a ⟶ X
Y : Profinite
f : Y ⟶ X
H : IsIso (Sigma.desc i)
θ : (∐ fun a => pullback f (i a)) ≅ ∐ fun a => Limits.pullback f (i a) := Sigma.mapIso fun a => fromExplicitIso f (i a)
⊢ IsIso (θ.hom ≫ Sigma.desc fun x => Limits.pullback.fst)
Tactic:
let δ := FromFiniteCoproductIso (fun a => Profinite.pullback f (i a))
State after:
α : Type
x✝ : Fintype α
X : Profinite
Z : α → Profinite
i : (a : α) → Z a ⟶ X
Y : Profinite
f : Y ⟶ X
H : IsIso (Sigma.desc i)
θ : (∐ fun a => pullback f (i a)) ≅ ∐ fun a => Limits.pullback f (i a) := Sigma.mapIso fun a => fromExplicitIso f (i a)
δ : (finiteCoproduct fun a => pullback f (i a)) ≅ ∐ fun a => pullback f (i a) :=
  FromFiniteCoproductIso fun a => pullback f (i a)
⊢ IsIso (θ.hom ≫ Sigma.desc fun x => Limits.pullback.fst)

State before:
α : Type
x✝ : Fintype α
X : Profinite
Z : α → Profinite
i : (a : α) → Z a ⟶ X
Y : Profinite
f : Y ⟶ X
H : IsIso (Sigma.desc i)
θ : (∐ fun a => pullback f (i a)) ≅ ∐ fun a => Limits.pullback f (i a) := Sigma.mapIso fun a => fromExplicitIso f (i a)
δ : (finiteCoproduct fun a => pullback f (i a)) ≅ ∐ fun a => pullback f (i a) :=
  FromFiniteCoproductIso fun a => pullback f (i a)
HIso : IsIso (finiteCoproduct.desc (fun a => Z a) i)
⊢ IsIso (δ.hom ≫ θ.hom ≫ Sigma.desc fun x => Limits.pullback.fst)
Tactic:
convert extensivity_explicit f HIso
State after:
case h.e'_5
α : Type
x✝ : Fintype α
X : Profinite
Z : α → Profinite
i : (a : α) → Z a ⟶ X
Y : Profinite
f : Y ⟶ X
H : IsIso (Sigma.desc i)
θ : (∐ fun a => pullback f (i a)) ≅ ∐ fun a => Limits.pullback f (i a) := Sigma.mapIso fun a => fromExplicitIso f (i a)
δ : (finiteCoproduct fun a => pullback f (i a)) ≅ ∐ fun a => pullback f (i a) :=
  FromFiniteCoproductIso fun a => pullback f (i a)
HIso : IsIso (finiteCoproduct.desc (fun a => Z a) i)
⊢ (δ.hom ≫ θ.hom ≫ Sigma.desc fun x => Limits.pullback.fst) =
    finiteCoproduct.desc (fun a => pullback f (i a)) fun a => pullback.fst f (i a)

State before:
case h.e'_5
α : Type
x✝ : Fintype α
X : Profinite
Z : α → Profinite
i : (a : α) → Z a ⟶ X
Y : Profinite
f : Y ⟶ X
H : IsIso (Sigma.desc i)
θ : (∐ fun a => pullback f (i a)) ≅ ∐ fun a => Limits.pullback f (i a) := Sigma.mapIso fun a => fromExplicitIso f (i a)
δ : (finiteCoproduct fun a => pullback f (i a)) ≅ ∐ fun a => pullback f (i a) :=
  FromFiniteCoproductIso fun a => pullback f (i a)
HIso : IsIso (finiteCoproduct.desc (fun a => Z a) i)
⊢ (δ.hom ≫ θ.hom ≫ Sigma.desc fun x => Limits.pullback.fst) =
    finiteCoproduct.desc (fun a => pullback f (i a)) fun a => pullback.fst f (i a)
Tactic:
refine' finiteCoproduct.hom_ext _ _ _ (fun a => _)
State after:
case h.e'_5
α : Type
x✝ : Fintype α
X : Profinite
Z : α → Profinite
i : (a : α) → Z a ⟶ X
Y : Profinite
f : Y ⟶ X
H : IsIso (Sigma.desc i)
θ : (∐ fun a => pullback f (i a)) ≅ ∐ fun a => Limits.pullback f (i a) := Sigma.mapIso fun a => fromExplicitIso f (i a)
δ : (finiteCoproduct fun a => pullback f (i a)) ≅ ∐ fun a => pullback f (i a) :=
  FromFiniteCoproductIso fun a => pullback f (i a)
HIso : IsIso (finiteCoproduct.desc (fun a => Z a) i)
a : α
⊢ (finiteCoproduct.ι (fun a => pullback f (i a)) a ≫ δ.hom ≫ θ.hom ≫ Sigma.desc fun x => Limits.pullback.fst) =
    finiteCoproduct.ι (fun a => pullback f (i a)) a ≫
      finiteCoproduct.desc (fun a => pullback f (i a)) fun a => pullback.fst f (i a)

State before:
case h.e'_5
α : Type
x✝ : Fintype α
X : Profinite
Z : α → Profinite
i : (a : α) → Z a ⟶ X
Y : Profinite
f : Y ⟶ X
H : IsIso (Sigma.desc i)
θ : (∐ fun a => pullback f (i a)) ≅ ∐ fun a => Limits.pullback f (i a) := Sigma.mapIso fun a => fromExplicitIso f (i a)
δ : (finiteCoproduct fun a => pullback f (i a)) ≅ ∐ fun a => pullback f (i a) :=
  FromFiniteCoproductIso fun a => pullback f (i a)
HIso : IsIso (finiteCoproduct.desc (fun a => Z a) i)
a : α
⊢ (finiteCoproduct.ι (fun a => pullback f (i a)) a ≫ δ.hom ≫ θ.hom ≫ Sigma.desc fun x => Limits.pullback.fst) =
    finiteCoproduct.ι (fun a => pullback f (i a)) a ≫
      finiteCoproduct.desc (fun a => pullback f (i a)) fun a => pullback.fst f (i a)
Tactic:
simp [← Category.assoc, finiteCoproduct.ι_desc, fromExplicit]
State after:
no goals

State before:
α : Type
x✝ : Fintype α
X : Profinite
Z : α → Profinite
i : (a : α) → Z a ⟶ X
Y : Profinite
f : Y ⟶ X
H : IsIso (Sigma.desc i)
θ : (∐ fun a => pullback f (i a)) ≅ ∐ fun a => Limits.pullback f (i a) := Sigma.mapIso fun a => fromExplicitIso f (i a)
this : IsIso (θ.hom ≫ Sigma.desc fun x => Limits.pullback.fst)
⊢ IsIso (Sigma.desc fun x => Limits.pullback.fst)
Tactic:
apply IsIso.of_isIso_comp_left θ.hom
State after:
no goals

State before:
α : Type
x✝ : Fintype α
X : Profinite
Z : α → Profinite
i : (a : α) → Z a ⟶ X
Y : Profinite
f : Y ⟶ X
H : IsIso (Sigma.desc i)
θ : (∐ fun a => pullback f (i a)) ≅ ∐ fun a => Limits.pullback f (i a) := Sigma.mapIso fun a => fromExplicitIso f (i a)
δ : (finiteCoproduct fun a => pullback f (i a)) ≅ ∐ fun a => pullback f (i a) :=
  FromFiniteCoproductIso fun a => pullback f (i a)
this : IsIso (δ.hom ≫ θ.hom ≫ Sigma.desc fun x => Limits.pullback.fst)
⊢ IsIso (θ.hom ≫ Sigma.desc fun x => Limits.pullback.fst)
Tactic:
apply IsIso.of_isIso_comp_left δ.hom
State after:
no goals

State before:
α : Type
x✝ : Fintype α
X : Profinite
Z : α → Profinite
i : (a : α) → Z a ⟶ X
Y : Profinite
f : Y ⟶ X
H : IsIso (Sigma.desc i)
θ : (∐ fun a => pullback f (i a)) ≅ ∐ fun a => Limits.pullback f (i a) := Sigma.mapIso fun a => fromExplicitIso f (i a)
δ : (finiteCoproduct fun a => pullback f (i a)) ≅ ∐ fun a => pullback f (i a) :=
  FromFiniteCoproductIso fun a => pullback f (i a)
⊢ IsIso (finiteCoproduct.desc (fun a => Z a) i)
Tactic:
let ε := ToFiniteCoproductIso Z
State after:
α : Type
x✝ : Fintype α
X : Profinite
Z : α → Profinite
i : (a : α) → Z a ⟶ X
Y : Profinite
f : Y ⟶ X
H : IsIso (Sigma.desc i)
θ : (∐ fun a => pullback f (i a)) ≅ ∐ fun a => Limits.pullback f (i a) := Sigma.mapIso fun a => fromExplicitIso f (i a)
δ : (finiteCoproduct fun a => pullback f (i a)) ≅ ∐ fun a => pullback f (i a) :=
  FromFiniteCoproductIso fun a => pullback f (i a)
ε : ∐ Z ≅ finiteCoproduct Z := ToFiniteCoproductIso Z
⊢ IsIso (finiteCoproduct.desc (fun a => Z a) i)

State before:
α : Type
x✝ : Fintype α
X : Profinite
Z : α → Profinite
i : (a : α) → Z a ⟶ X
Y : Profinite
f : Y ⟶ X
H : IsIso (Sigma.desc i)
θ : (∐ fun a => pullback f (i a)) ≅ ∐ fun a => Limits.pullback f (i a) := Sigma.mapIso fun a => fromExplicitIso f (i a)
δ : (finiteCoproduct fun a => pullback f (i a)) ≅ ∐ fun a => pullback f (i a) :=
  FromFiniteCoproductIso fun a => pullback f (i a)
ε : ∐ Z ≅ finiteCoproduct Z := ToFiniteCoproductIso Z
⊢ IsIso (ε.hom ≫ finiteCoproduct.desc Z i)
Tactic:
convert H
State after:
case h.e'_5
α : Type
x✝ : Fintype α
X : Profinite
Z : α → Profinite
i : (a : α) → Z a ⟶ X
Y : Profinite
f : Y ⟶ X
H : IsIso (Sigma.desc i)
θ : (∐ fun a => pullback f (i a)) ≅ ∐ fun a => Limits.pullback f (i a) := Sigma.mapIso fun a => fromExplicitIso f (i a)
δ : (finiteCoproduct fun a => pullback f (i a)) ≅ ∐ fun a => pullback f (i a) :=
  FromFiniteCoproductIso fun a => pullback f (i a)
ε : ∐ Z ≅ finiteCoproduct Z := ToFiniteCoproductIso Z
⊢ ε.hom ≫ finiteCoproduct.desc Z i = Sigma.desc i

State before:
case h.e'_5
α : Type
x✝ : Fintype α
X : Profinite
Z : α → Profinite
i : (a : α) → Z a ⟶ X
Y : Profinite
f : Y ⟶ X
H : IsIso (Sigma.desc i)
θ : (∐ fun a => pullback f (i a)) ≅ ∐ fun a => Limits.pullback f (i a) := Sigma.mapIso fun a => fromExplicitIso f (i a)
δ : (finiteCoproduct fun a => pullback f (i a)) ≅ ∐ fun a => pullback f (i a) :=
  FromFiniteCoproductIso fun a => pullback f (i a)
ε : ∐ Z ≅ finiteCoproduct Z := ToFiniteCoproductIso Z
⊢ ε.hom ≫ finiteCoproduct.desc Z i = Sigma.desc i
Tactic:
refine' Sigma.hom_ext _ _ (fun a => _)
State after:
case h.e'_5
α : Type
x✝ : Fintype α
X : Profinite
Z : α → Profinite
i : (a : α) → Z a ⟶ X
Y : Profinite
f : Y ⟶ X
H : IsIso (Sigma.desc i)
θ : (∐ fun a => pullback f (i a)) ≅ ∐ fun a => Limits.pullback f (i a) := Sigma.mapIso fun a => fromExplicitIso f (i a)
δ : (finiteCoproduct fun a => pullback f (i a)) ≅ ∐ fun a => pullback f (i a) :=
  FromFiniteCoproductIso fun a => pullback f (i a)
ε : ∐ Z ≅ finiteCoproduct Z := ToFiniteCoproductIso Z
a : α
⊢ Sigma.ι Z a ≫ ε.hom ≫ finiteCoproduct.desc Z i = Sigma.ι Z a ≫ Sigma.desc i

State before:
case h.e'_5
α : Type
x✝ : Fintype α
X : Profinite
Z : α → Profinite
i : (a : α) → Z a ⟶ X
Y : Profinite
f : Y ⟶ X
H : IsIso (Sigma.desc i)
θ : (∐ fun a => pullback f (i a)) ≅ ∐ fun a => Limits.pullback f (i a) := Sigma.mapIso fun a => fromExplicitIso f (i a)
δ : (finiteCoproduct fun a => pullback f (i a)) ≅ ∐ fun a => pullback f (i a) :=
  FromFiniteCoproductIso fun a => pullback f (i a)
ε : ∐ Z ≅ finiteCoproduct Z := ToFiniteCoproductIso Z
a : α
⊢ Sigma.ι Z a ≫ ε.hom ≫ finiteCoproduct.desc Z i = Sigma.ι Z a ≫ Sigma.desc i
Tactic:
simp [← Category.assoc]
State after:
no goals

State before:
α : Type
x✝ : Fintype α
X : Profinite
Z : α → Profinite
i : (a : α) → Z a ⟶ X
Y : Profinite
f : Y ⟶ X
H : IsIso (Sigma.desc i)
θ : (∐ fun a => pullback f (i a)) ≅ ∐ fun a => Limits.pullback f (i a) := Sigma.mapIso fun a => fromExplicitIso f (i a)
δ : (finiteCoproduct fun a => pullback f (i a)) ≅ ∐ fun a => pullback f (i a) :=
  FromFiniteCoproductIso fun a => pullback f (i a)
ε : ∐ Z ≅ finiteCoproduct Z := ToFiniteCoproductIso Z
this : IsIso (ε.hom ≫ finiteCoproduct.desc Z i)
⊢ IsIso (finiteCoproduct.desc (fun a => Z a) i)
Tactic:
apply IsIso.of_isIso_comp_left ε.hom
State after:
no goals