text:
import category_theory.products.basic
import category_theory.limits.concrete_category

import for_mathlib.Cech.adjunction
import for_mathlib.simplicial.iso

import polyhedral_lattice.cosimplicial_extra

import prop_92.prop_92
import normed_snake_dual
import thm95.double_complex
import thm95.col_exact_prep
import thm95.double_complex
import thm95.pfpng_iso

noncomputable theory

open_locale nnreal big_operators nat
open category_theory opposite simplex_category
local attribute [instance] type_pow

universe variables u v u₀ uₘ
-- set_option pp.universes true

namespace thm95

variables (BD : breen_deligne.data) (κ : ℕ → ℝ≥0) [BD.suitable κ]
variables (r r' : ℝ≥0)
variables (V : SemiNormedGroup.{v})
variables (Λ : PolyhedralLattice.{u}) (M : ProFiltPseuNormGrpWithTinv.{u} r')
variables (N : ℕ) [fact (0 < N)] (n : ℕ)

@[simps obj map]
def scale_factorial : system_of_complexes.{u} ⥤ system_of_complexes.{u} :=
(whiskering_right _ _ _).obj $
homological_complex.modify_functor
  (λ m, SemiNormedGroup.rescale m!) (λ m₁ m₂, SemiNormedGroup.scale _ _)
.

namespace scale_factorial
open system_of_complexes SemiNormedGroup homological_complex

lemma is_weak_bounded_exact {C : system_of_complexes} {k K : ℝ≥0} [fact (1 ≤ k)] {m : ℕ} {c₀ : ℝ≥0}
  (hC : C.is_weak_bounded_exact k K m c₀) :
  (scale_factorial.obj C).is_weak_bounded_exact k (K * (m + 1)) m c₀ :=
begin
  intros c hc i hi x ε hε,
  let δ := ε * i!,
  have hδ : 0 < δ := mul_pos hε (nat.cast_pos.2 (nat.factorial_pos i)),
  have hifact : ¬(↑(i!) : ℝ) = 0 := by exact_mod_cast nat.factorial_ne_zero _,
  have him : 1 ≤ (↑m + 1) * ((↑i : ℝ) + 1)⁻¹,
  { refine le_trans _ (mul_le_mul_of_nonneg_right (show (↑i : ℝ) + 1 ≤ (↑m + 1),
      by rwa [add_le_add_iff_right, nat.cast_le])
      (inv_nonneg.2 (add_nonneg ((@nat.cast_nonneg ℝ _ i)) zero_le_one))),
    rw mul_inv_cancel (ne_of_lt (add_pos_of_nonneg_of_pos (@nat.cast_nonneg ℝ _ i) zero_lt_one)).symm },
  obtain ⟨_, _, rfl, rfl, y, hy⟩ := hC c hc i hi ((of_rescale i!).app _ x) δ hδ,
  refine ⟨_, _, rfl, rfl, ((SemiNormedGroup.to_rescale (i - 1)!).app _ y), _⟩,
  erw [rescale.norm_def, rescale.norm_def],
  simp only [nnreal.coe_nat_cast, nnreal.coe_add, nat.cast_succ, nat.factorial_succ,
    nat.cast_mul, nnreal.coe_one, nnreal.coe_mul, div_eq_mul_inv],
  rw [mul_inv_le_iff], swap, { exact_mod_cast nat.factorial_pos i },
  refine hy.trans _,
  rw [left_distrib, mul_inv, ← mul_assoc ↑i!, mul_comm ↑i!, mul_assoc _ ↑i!, mul_comm ↑i!,
    mul_assoc _ _ ↑i!, inv_mul_cancel_right₀ hifact, mul_comm _ ε, add_le_add_iff_right,
    mul_assoc ↑K],
  refine mul_le_mul_of_nonneg_left _ (nnreal.coe_nonneg _),
  rw [mul_comm _ ((↑i : ℝ) + 1)⁻¹, ← mul_assoc],
  refine le_trans (le_mul_of_one_le_left (by simp only [one_mul, norm_nonneg]) him)
    (mul_le_mul_of_nonneg_left _ (mul_nonneg (add_nonneg (nat.cast_nonneg m) zero_le_one)
    (inv_nonneg.2 (add_nonneg (nat.cast_nonneg i) zero_le_one)))),
  simpa using le_refl _
end

end scale_factorial

section
open PolyhedralLattice

def CLCFP' : (ProFiltPseuNormGrpWithTinv r')ᵒᵖ ⥤ ℝ≥0ᵒᵖ ⥤ SemiNormedGroup :=
(ProFiltPseuNormGrpWithTinv.Pow r' n ⋙ (_root_.Filtration r').flip).op ⋙
  functor.op_hom _ _ ⋙ (whiskering_right ℝ≥0ᵒᵖ Profiniteᵒᵖ _).obj (CLC V)

lemma CLCFP'_map_app {M₁ M₂ : (ProFiltPseuNormGrpWithTinv r')ᵒᵖ} (f : M₁ ⟶ M₂) (c : ℝ≥0ᵒᵖ) :
  ((CLCFP' r' V n).map f).app c = (CLCFP V r' c.unop n).map f := rfl

lemma CLCFP'_obj_map (M₁ : (ProFiltPseuNormGrpWithTinv r')ᵒᵖ) (c₁ c₂ : ℝ≥0ᵒᵖ) (h : c₁ ⟶ c₂) :
  ((CLCFP' r' V n).obj M₁).map h =
    (by haveI : fact (c₂.unop ≤ c₁.unop) := ⟨le_of_hom h.unop⟩;
      exact (CLCFP.res V r' c₁.unop c₂.unop n).app M₁) :=
rfl

lemma FLC_arrow_hom' {M₁ M₂ : ProFiltPseuNormGrpWithTinv r'} (f : M₁ ⟶ M₂) (c : ℝ≥0) :
  (FLC_complex_arrow f.to_comphaus_filtered_pseudo_normed_group_hom f.strict c).hom =
    ((Filtration r').obj c).map f :=
rfl

section

variables [fact (0 < r')] [fact (r' ≤ 1)]

def Cech_nerve' :
  cosimplicial_object.augmented (ℝ≥0ᵒᵖ ⥤ SemiNormedGroup) :=
(cosimplicial_object.augmented.whiskering_obj.{u} _ _ (CLCFP' r' V n)).obj
  (Cech_nerve r' Λ M N)

lemma Cech_nerve'_hom_zero :
  (Cech_nerve'.{u} r' V Λ M N n).hom.app (mk 0) =
    (CLCFP' r' V n).map (Cech_augmentation_map.{u} r' Λ M N).op :=
begin
  dsimp only [Cech_nerve', cosimplicial_object.augmented.whiskering_obj],
  simp only [whisker_right_app, category.id_comp, functor.right_op_map, nat_trans.comp_app,
    functor.const_comp_inv_app, Cech_nerve_hom_zero],
end

@[simps obj map]
def Cech_nerve_level : ℝ≥0 ⥤ simplicial_object.augmented Profinite.{u} :=
(ProFiltPseuNormGrpWithTinv.Pow r' n ⋙ (Filtration r').flip).flip ⋙
  (simplicial_object.augmented.whiskering _ _).flip.obj (Cech_nerve.{u} r' Λ M N).left_op
.

lemma Cech_nerve_level_left_map (c : ℝ≥0) (i j : simplex_categoryᵒᵖ) (g : i ⟶ j) :
  ((Cech_nerve_level r' Λ M N n).obj c).left.map g =
    ((Filtration r').obj c).map ((ProFiltPseuNormGrpWithTinv.Pow r' n).map
      ((Hom M).map ((Cech_conerve (Λ.diagonal_embedding N)).map g.unop).op)) :=
rfl

lemma Cech_nerve_level_left_map' (c : ℝ≥0) (i j : simplex_categoryᵒᵖ) (g : i ⟶ j)
  (x : ((Cech_nerve_level r' Λ M N n).obj c).left.obj i) (k : fin n) :
  (((Cech_nerve_level r' Λ M N n).obj c).left.map g x).1 k =
    add_monoid_hom.comp (x.1 k) (polyhedral_lattice.conerve.map
      (Λ.diagonal_embedding N) ⇑(hom.to_order_hom g.unop)).to_add_monoid_hom :=
rfl

lemma Cech_nerve_level_hom_app (c : ℝ≥0) :
  ((Cech_nerve_level r' Λ M N n).obj c).hom.app (op (mk 0)) =
    ((Filtration r').obj c).map
      ((ProFiltPseuNormGrpWithTinv.Pow r' n).map (Cech_augmentation_map r' Λ M N)) :=
begin
  dsimp only [Cech_nerve_level_obj, nat_trans.comp_app, whisker_right_app,
    functor.const_comp_hom_app],
  erw [category.comp_id],
  dsimp only [nat_trans.left_op_app, unop_op],
  rw [Cech_nerve_hom_zero],
  dsimp only [functor.flip_obj_map, functor.comp_map, quiver.hom.unop_op,
    functor.flip_map_app],
  refl
end

@[simps X d]
def col_complex_aux : cochain_complex (ℝ≥0ᵒᵖ ⥤ SemiNormedGroup) ℕ :=
(Cech_nerve' r' V Λ M N n).to_cocomplex
.

@[simps obj obj_d map]
def col_complex_level : system_of_complexes :=
((whiskering_right _ _ _).obj $ FLC_functor' V).obj (Cech_nerve_level r' Λ M N n).op
.

@[simps obj obj_d map]
def col_complex : system_of_complexes :=
(col_complex_aux r' V Λ M N n).as_functor
.

def col_complex_level_iso_obj_X (c : ℝ≥0ᵒᵖ) :
  Π (i : ℕ), ((col_complex_level r' V Λ M N n).obj c).X i ≅ ((col_complex r' V Λ M N n).obj c).X i
| 0     := iso.refl _
| (i+1) := iso.refl _

lemma col_complex_level_iso_obj_comm (c : ℝ≥0ᵒᵖ) (i : ℕ) :
  (col_complex_level_iso_obj_X r' V Λ M N n c i).hom ≫
    ((col_complex r' V Λ M N n).obj c).d i (i + 1) =
  ((col_complex_level r' V Λ M N n).obj c).d i (i + 1) ≫
    (col_complex_level_iso_obj_X r' V Λ M N n c (i + 1)).hom :=
begin
  cases i,
  all_goals {
    dsimp only [col_complex_level_iso_obj_X],
    simp only [iso.refl_hom, category.id_comp, category.comp_id],
    dsimp only [col_complex_obj_d, col_complex_level_obj_d,
      cosimplicial_object.augmented.cocomplex,
      cosimplicial_object.augmented.to_cocomplex_d_2,
      cosimplicial_object.augmented.to_cocomplex_d,
      functor.const_comp_hom_app, functor.const_comp_inv_app,
      nat_trans.comp_app, whisker_right_app, nat_trans.right_op_app, nat_trans.left_op_app,
      cosimplicial_object.augmented.drop_obj, cosimplicial_object.coboundary,
      cosimplicial_object.δ, cosimplicial_object.whiskering_obj_obj_map],
    rw [dif_pos rfl, eq_to_hom_refl, category.comp_id,
        dif_pos rfl, eq_to_hom_refl, category.comp_id], },
  { erw [Cech_nerve'_hom_zero, SemiNormedGroup.LCC_obj_map', category.id_comp],
    dsimp only [unop_op],
    erw [Cech_nerve_hom_zero, op_id, category.id_comp],
    refl },
  { simp only [nat_trans.app_sum, nat_trans.app_zsmul],
    apply fintype.sum_congr, intro j, congr' 1,
    rw [SemiNormedGroup.LCC_obj_map'],
    refl, }
end

def col_complex_level_iso_obj (c : ℝ≥0ᵒᵖ) :
  (col_complex_level r' V Λ M N n).obj c ≅ (col_complex r' V Λ M N n).obj c :=
homological_complex.hom.iso_of_components (col_complex_level_iso_obj_X r' V Λ M N n c)
(by { rintro i j (rfl : i + 1 = j), apply col_complex_level_iso_obj_comm })

lemma col_complex_level_iso_comm (c₁ c₂ : ℝ≥0ᵒᵖ) (h : c₁ ⟶ c₂) (i : ℕ) :
  ((col_complex_level r' V Λ M N n).map h ≫ (col_complex_level_iso_obj r' V Λ M N n c₂).hom).f i =
    ((col_complex_level_iso_obj r' V Λ M N n c₁).hom ≫ (col_complex r' V Λ M N n).map h).f i :=
begin
  cases i,
  all_goals {
    dsimp only [col_complex_level_iso_obj, col_complex_level_iso_obj_X,
      homological_complex.comp_f, homological_complex.hom.iso_of_components_hom_f, iso.refl_hom],
      rw [category.id_comp, category.comp_id],
    dsimp only [col_complex_level_map, col_complex_map, whisker_right_app,
      cosimplicial_object.augmented.cocomplex,
      cosimplicial_object.augmented.point_map,
      cosimplicial_object.augmented.drop_map],
      rw [SemiNormedGroup.LCC_obj_map'], refl },
end

def col_complex_level_iso :
  col_complex_level r' V Λ M N n ≅ col_complex r' V Λ M N n :=
nat_iso.of_components (col_complex_level_iso_obj r' V Λ M N n)
(by { intros c₁ c₂ h, ext i : 2, apply col_complex_level_iso_comm })

lemma col_complex_level_iso_strict (c : ℝ≥0ᵒᵖ) (i : ℕ) :
  isometry (((col_complex_level_iso r' V Λ M N n).hom.app c).f i) :=
by { cases i; exact isometry_id }

def aug_map :=
((ProFiltPseuNormGrpWithTinv.Pow r' n).map (Cech_augmentation_map r' Λ M N))
  .to_comphaus_filtered_pseudo_normed_group_hom

section open comphaus_filtered_pseudo_normed_group_with_Tinv_hom
lemma aug_map_strict : (aug_map r' Λ M N n).strict :=
to_profinitely_filtered_pseudo_normed_group_hom_strict _
end

section open category_theory.simplicial_object

@[simps left right]
def Cech_nerve_level_hom' (c : ℝ≥0) :
  augmented.to_arrow.obj ((Cech_nerve_level r' Λ M N n).obj c) ⟶
    FLC_complex_arrow _ (aug_map_strict r' Λ M N n) c :=
@arrow.hom_mk _ _
  (augmented.to_arrow.obj ((Cech_nerve_level r' Λ M N n).obj c))
  (FLC_complex_arrow _ (aug_map_strict r' Λ M N n) c)
  (𝟙 _) (𝟙 _)
begin
  erw [category.comp_id, category.id_comp, augmented.to_arrow_obj_hom],
  dsimp only [Cech_nerve_level_obj, nat_trans.comp_app, whisker_right_app,
    functor.const_comp_hom_app, nat_trans.left_op_app, unop_op,
    functor.flip_obj_map, functor.comp_map, functor.flip_map_app],
  erw [category.comp_id, Cech_nerve_hom_zero],
  refl,
end

@[simps left right]
def Cech_nerve_level_inv' (c : ℝ≥0) :
  FLC_complex_arrow _ (aug_map_strict r' Λ M N n) c ⟶
    augmented.to_arrow.obj ((Cech_nerve_level r' Λ M N n).obj c) :=
@arrow.hom_mk _ _
  (FLC_complex_arrow _ (aug_map_strict r' Λ M N n) c)
  (augmented.to_arrow.obj ((Cech_nerve_level r' Λ M N n).obj c))
  (𝟙 _) (𝟙 _)
begin
  erw [category.comp_id, category.id_comp, augmented.to_arrow_obj_hom],
  dsimp only [Cech_nerve_level_obj, nat_trans.comp_app, whisker_right_app,
    functor.const_comp_hom_app, nat_trans.left_op_app, unop_op,
    functor.flip_obj_map, functor.comp_map, functor.flip_map_app],
  erw [category.comp_id, Cech_nerve_hom_zero],
  refl,
end

@[simps left right]
def Cech_nerve_level_hom (c : ℝ≥0) :
  (Cech_nerve_level r' Λ M N n).obj c ⟶
    (FLC_complex_arrow _ (aug_map_strict r' Λ M N n) c).augmented_cech_nerve :=
equivalence_left_to_right _ _ $ Cech_nerve_level_hom' _ _ _ _ _ _
.

lemma Cech_nerve_level_hom_injective' (c : ℝ≥0) (i : simplex_categoryᵒᵖ)
  (x y: ((((Cech_nerve_level r' Λ M N n).obj c).left.obj i)))
  (h : ∀ (j : (fin ((unop i).len + 1))),
    (((Cech_nerve_level r' Λ M N n).obj c).left.map ((unop i).const j).op) x =
    (((Cech_nerve_level r' Λ M N n).obj c).left.map ((unop i).const j).op) y) : x = y :=
begin
  ext j : 2,
  let π := (polyhedral_lattice.conerve.π
    (Λ.diagonal_embedding N) (i.unop.len + 1)).to_add_monoid_hom,
  have hπ : function.surjective π := polyhedral_lattice.conerve.π_surjective _ _,
  rw ← add_monoid_hom.cancel_right hπ, -- Bingo!
  apply finsupp.add_hom_ext',
  intro k, specialize h k,
  rw subtype.ext_iff at h,
  replace h := congr_fun h j,
  rw add_monoid_hom.ext_iff at h ⊢,
  intro l, specialize h ((Cech_conerve.obj_zero_iso _).inv l),
  dsimp only [Cech_nerve_level_obj, Cech_nerve_level_map,
    whiskering_obj_obj_map, functor.flip_obj_map, functor.flip_map_app,
    functor.comp_map, functor.left_op_map, quiver.hom.unop_op,
    Cech_nerve, cosimplicial_object.augmented.whiskering_obj, cosimplicial_object.whiskering,
    whiskering_right_obj_obj, whiskering_right_obj_map,
    functor.right_op_map, unop_op,
    cosimplicial_object.augmented.drop_obj, cosimplicial_object.augmented.drop_map,
    augmented_cosimplicial, augmented_Cech_conerve,
    cosimplicial_object.augment_right, Cech_conerve_map,
    Filtration_obj_map_apply, ProFiltPseuNormGrpWithTinv.Pow_map,
    Hom_obj, Hom_map_to_fun, polyhedral_lattice.Hom,
    comphaus_filtered_pseudo_normed_group_with_Tinv_hom.level,
    profinitely_filtered_pseudo_normed_group_with_Tinv.pi_map_to_fun,
    profinitely_filtered_pseudo_normed_group_with_Tinv.pi_lift_to_fun,
    comphaus_filtered_pseudo_normed_group_with_Tinv_hom.comp_to_fun,
    pseudo_normed_group.level, finsupp.single_add_hom_apply,
    subtype.coe_mk, add_monoid_hom.coe_mk_from_pi, add_monoid_hom.comp_apply] at h ⊢,
  erw [Cech_conerve.map_const_obj_zero_iso] at h,
  exact h,
end
.

open category_theory.limits.wide_pullback

lemma Cech_nerve_level_hom_injective (c : ℝ≥0) (i : simplex_categoryᵒᵖ) :
  function.injective ⇑((Cech_nerve_level_hom r' Λ M N n c).left.app i) :=
begin
  let F := FLC_complex_arrow _ (aug_map_strict r' Λ M N n) c,
  let G := (Cech_nerve_level_hom r' Λ M N n c).left.app i,
  intros x y h,
  replace h : ∀ j, π (λ i, F.hom) j (G x) = π (λ i, F.hom) j (G y), { intros j, rw h },
  have aux := λ j, (augmented_cech_nerve.left_map_comp_obj_zero_iso F i.unop j).symm,
  dsimp only [unop_op] at aux,
  simp only [← comp_apply, aux] at h,
  have aux' := (Cech_nerve_level_hom r' Λ M N n c).left.naturality,
  simp only [← category.assoc, ← aux'] at h, clear aux aux',
  simp only [category.assoc, Cech_nerve_level_hom, augmented_cech_nerve.left_obj_zero_iso_hom,
    equivalence_left_to_right_left_app_zero_comp_π, Cech_nerve_level_hom'_left,
    coe_comp, function.comp, id_apply] at h,
  apply Cech_nerve_level_hom_injective',
  exact h
end
.

namespace Cech_nerve_level_hom

/-! The goal is to build a section to `Cech_nerve_level_hom` -/

variables {r' Λ M N n}
variables {c : ℝ≥0} {i : simplex_categoryᵒᵖ}
variables (y : (FLC_complex_arrow _ (aug_map_strict r' Λ M N n) c).augmented_cech_nerve.left.obj i)

def z₀' := limits.wide_pullback.base
(λ _, (FLC_complex_arrow _ (aug_map_strict r' Λ M N n) c).hom) y

def z' := λ j, limits.wide_pullback.π
(λ _, (FLC_complex_arrow _ (aug_map_strict r' Λ M N n) c).hom) j y

lemma hz' : ∀ j, ((FLC_complex_arrow _ (aug_map_strict r' Λ M N n) c).hom (z' y j)) = z₀' y :=
begin
  intro j,
  dsimp only [z₀', z'],
  rw [← comp_apply, limits.wide_pullback.π_arrow],
end

def z₀ := (Cech_nerve_level_inv' r' Λ M N n c).right (z₀' y)

def z := λ j, (Cech_nerve_level_inv' r' Λ M N n c).left (z' y j)

lemma hz : ∀ j, (augmented.to_arrow.obj ((Cech_nerve_level r' Λ M N n).obj c)).hom (z y j) = z₀ y :=
begin
  intro j, dsimp only [z₀, z],
  have := (Cech_nerve_level_inv' r' Λ M N n c).w,
  simp only [functor.id_map, augmented.to_arrow_obj_hom] at this,
  erw [← comp_apply, this, comp_apply, hz'],
  refl
end

def s' (y : (FLC_complex_arrow _ (aug_map_strict r' Λ M N n) c).augmented_cech_nerve.left.obj i) :
  (ProFiltPseuNormGrpWithTinv.Pow r' n).obj
    ((augmented.drop.obj (Cech_nerve r' Λ M N).left_op).obj i) :=
begin
  refine λ k,
    cosimplicial_lift Λ N _
      ((z₀ y).1 k)
      (λ j, add_monoid_hom.comp ((z y j).1 k)
        (Cech_conerve.obj_zero_iso (Λ.diagonal_embedding N)).inv.to_add_monoid_hom) _,
  intros j l,
  dsimp only [add_monoid_hom.comp_apply, subtype.coe_mk,
    polyhedral_lattice_hom.coe_to_add_monoid_hom],
  rw [← hz y j],
  dsimp only [augmented.to_arrow_obj_hom],
  rw [Cech_nerve_level_hom_app],
  dsimp only [Filtration_obj_map_apply, Cech_augmentation_map,
    comphaus_filtered_pseudo_normed_group_with_Tinv_hom.level,
    pseudo_normed_group.level,
    ProFiltPseuNormGrpWithTinv.Pow_map,
    profinitely_filtered_pseudo_normed_group_with_Tinv.pi_map_to_fun,
    cosimplicial_augmentation_map,
    Hom_map_to_fun, add_monoid_hom.comp_apply, subtype.coe_mk,
    polyhedral_lattice_hom.coe_to_add_monoid_hom, quiver.hom.unop_op,
    PolyhedralLattice.Cech_augmentation_map],
  refl,
end
.

def s (y : (FLC_complex_arrow _ (aug_map_strict r' Λ M N n) c).augmented_cech_nerve.left.obj i) :
  ((Cech_nerve_level r' Λ M N n).obj c).left.obj i :=
begin
  refine ⟨s' y, _⟩,
  intros k,
  apply cosimplicial_lift_mem_filtration,
  intros j c' l hl,
  dsimp only [add_monoid_hom.comp_apply, polyhedral_lattice_hom.coe_to_add_monoid_hom],
  apply (z y j).property,
  rw [seminormed_add_comm_group.mem_filtration_iff] at hl ⊢,
  refine le_trans _ hl,
  exact (Cech_conerve.obj_zero_iso (Λ.diagonal_embedding N)).inv.strict l
end
.

set_option pp.universes true

lemma surjective (c : ℝ≥0) (i : simplex_categoryᵒᵖ) :
  function.surjective ⇑((Cech_nerve_level_hom r' Λ M N n c).left.app i) :=
begin
  let F := FLC_complex_arrow (aug_map r' Λ M N n) _ c,
  intro y,
  refine ⟨Cech_nerve_level_hom.s y, _⟩,
  { apply limits.concrete.wide_pullback_ext'.{0} (λ i, F.hom),
    rotate, { apply_instance },
    { haveI := limits.preserves_limits_of_size_shrink.{0 u 0 u} (forget.{u+1} Profinite.{u}),
      apply_instance, },
    intro j,
    erw [← augmented_cech_nerve.left_map_comp_obj_zero_iso _ _ j, ← comp_apply,
      ← category.assoc, ← (Cech_nerve_level_hom r' Λ M N n c).left.naturality,
      augmented_cech_nerve.left_map_comp_obj_zero_iso _ _ j, category.assoc],
    dsimp only [Cech_nerve_level_hom, augmented_cech_nerve.left_obj_zero_iso],
    erw [equivalence_left_to_right_left_app_zero_comp_π, Cech_nerve_level_hom'_left,
      category.comp_id],
    apply subtype.ext, apply funext, rintro k, -- ext k : 2
    have := Cech_nerve_level_left_map' r' Λ M N n c i _ (i.unop.const j).op,
    simp only [subtype.val_eq_coe] at this,
    erw this _ k, clear this,
    apply add_monoid_hom.ext, rintro l', -- ext1 l'
    obtain ⟨l, rfl⟩ : ∃ l, quotient_add_group.mk l = l',
    { exact quotient.surjective_quotient_mk' l' },
    dsimp only [z₀, z, s', s, add_monoid_hom.comp_apply, subtype.coe_mk,
      polyhedral_lattice_hom.coe_to_add_monoid_hom,
      polyhedral_lattice.conerve.map_apply,
      add_monoid_hom.to_fun_eq_coe,
      polyhedral_lattice.conerve.map_add_hom_mk,
      cosimplicial_lift, polyhedral_lattice.conerve.lift'],
    refine (quotient_add_group.lift_mk'
      (polyhedral_lattice.conerve.L (Λ.diagonal_embedding N) ((unop i).len + 1)) _ _).trans _,
    dsimp only [finsupp.lift_add_hom_apply, finsupp.map_domain.add_monoid_hom_apply,
      unop_op],
    rw [finsupp.sum_map_domain_index_add_monoid_hom, finsupp.sum_fintype,
      fin.sum_univ_succ, finset.sum_eq_zero, add_zero],
    swap, { intros m hm, exfalso, change fin 0 at m, exact nat.not_lt_zero m m.2 },
    swap, { intro, rw add_monoid_hom.map_zero },
    dsimp only [add_monoid_hom.comp_apply, subtype.coe_mk,
      polyhedral_lattice_hom.coe_to_add_monoid_hom,
      Cech_nerve_level_inv'_left, Cech_conerve.obj_zero_iso,
      iso.trans_inv, subtype.val_eq_coe, quiver.hom.unop_op],
    rw [id_apply, comp_apply, Cech_conerve.obj_zero_iso'_inv,
      Cech_conerve.finsupp_fin_one_iso_inv],
    suffices : finsupp.single_add_hom 0 (l 0) = l,
    { cases j, rw this, refl },
    apply finsupp.ext, rintro m, apply finsupp.ext, rintro o, -- ext m o
    change fin 1 at m,
    have hm : m = 0, { exact subsingleton.elim _ _ },
    simp only [hm, finsupp.single_add_hom_apply, finsupp.single_apply, if_pos rfl], }
end

end Cech_nerve_level_hom

instance Cech_nerve_level_hom_is_iso (c : ℝ≥0) : is_iso (Cech_nerve_level_hom r' Λ M N n c) :=
begin
  refine @simplicial_object.augmented.is_iso_of _ _ _ _ _ (id _) (id _),
  swap, { exact is_iso.id _ },
  intro i,
  apply Profinite.is_iso_of_bijective,
  exact ⟨Cech_nerve_level_hom_injective r' Λ M N n c i,
        Cech_nerve_level_hom.surjective c i⟩,
end

def Cech_nerve_level_iso (c : ℝ≥0) :
  (Cech_nerve_level r' Λ M N n).obj c ≅
    (FLC_complex_arrow _ (aug_map_strict r' Λ M N n) c).augmented_cech_nerve :=
as_iso (Cech_nerve_level_hom r' Λ M N n c)

def FLC_complex_aug_iso_obj (c : ℝ≥0ᵒᵖ) :
  (FLC_complex V _ (aug_map_strict r' Λ M N n)).obj c ≅ (col_complex_level r' V Λ M N n).obj c :=
(FLC_functor' V).map_iso (Cech_nerve_level_iso r' Λ M N n c.unop).op

def FLC_complex_aug_iso :
  FLC_complex V _ (aug_map_strict r' Λ M N n) ≅ col_complex_level r' V Λ M N n :=
nat_iso.of_components (FLC_complex_aug_iso_obj r' V Λ M N n)
begin
  intros c₁ c₂ h,
  dsimp only [FLC_complex, col_complex_level, FLC_functor, FLC_complex_aug_iso_obj,
    functor.comp_map, functor.map_iso_hom, whiskering_right_obj_obj,
    Cech_nerve_level_iso, iso.op_hom, as_iso_hom, functor.op_map],
  simp only [← category_theory.functor.map_comp, ← op_comp, quiver.hom.unop_op],
  congr' 2,
  apply simplicial_object.hom_ext,
  { dsimp only [unop_op],
    let f := FLC_complex_arrow _ (aug_map_strict r' Λ M N n) (unop c₁),
    rw ← cancel_mono (augmented_cech_nerve.left_obj_zero_iso f).hom,
    dsimp only [comma.comp_left, nat_trans.comp_app,
      Cech_nerve_level_hom, augmented_cech_nerve_map, arrow.map_augmented_cech_nerve_left,
      cech_nerve_map, arrow.map_cech_nerve_app,
      arrow.hom_mk_right, arrow.hom_mk_left, augmented_cech_nerve.left_obj_zero_iso_hom],
    simp only [category.assoc, limits.wide_pullback.lift_π,
      simplicial_object.equivalence_left_to_right_left_app_zero_comp_π],
    erw [← category.assoc, simplicial_object.equivalence_left_to_right_left_app_zero_comp_π],
    refl, },
  { dsimp only [equivalence_right_to_left_right, comma.comp_right, Cech_nerve_level_hom_right],
    erw [category.comp_id, category.id_comp],
    refl, }
end

end

lemma FLC_complex_aug_iso_strict (c : ℝ≥0ᵒᵖ) (i : ℕ) :
  isometry (((FLC_complex_aug_iso r' V Λ M N n).hom.app c).f i) :=
begin
  rw [← iso.app_hom, ← homological_complex.hom.iso_app_hom],
  refine SemiNormedGroup.iso_isometry_of_norm_noninc _ _ _;
  [ rw [homological_complex.hom.iso_app_hom, iso.app_hom],
    rw [homological_complex.hom.iso_app_inv, iso.app_inv] ];
  { apply cosimplicial_object.augmented.cocomplex_map_norm_noninc;
    intros; apply SemiNormedGroup.LCC_obj_map_norm_noninc, },
end

def col_complex_obj_iso_X_zero (c : ℝ≥0ᵒᵖ) :
  ((col_complex r' V Λ M N n).obj c).X 0 ≅
    ((FLC_functor V).obj (op $ FLC_complex_arrow _ (aug_map_strict r' Λ M N n) (c.unop))).X 0 :=
iso.refl _

section
open profinitely_filtered_pseudo_normed_group

def FLC_arrow_iso_aux :
  ((ProFiltPseuNormGrpWithTinv.Pow r' n).obj
    (unop ((Cech_nerve r' Λ M N).right.obj (mk 0)))) ≅
  ProFiltPseuNormGrpWithTinv.of r' (rescale ↑N (((↥Λ →+ (↥M: Type u)) ^ n) ^ N)) :=
(ProFiltPseuNormGrpWithTinv.Pow r' n).map_iso
    (Hom_cosimplicial_zero_iso Λ N r' M N rfl) ≪≫
  (ProFiltPseuNormGrpWithTinv.Pow_rescale_Pow_iso.{u u} r' N N n).app
    (polyhedral_lattice.Hom ↥Λ (↥M: Type u))
.

section open ProFiltPseuNormGrpWithTinv

--move this
attribute [simps] linear_equiv.to_add_equiv

lemma FLC_arrow_iso_w (c : ℝ≥0) :
  ((((Filtration r').obj c).map_iso (FLC_arrow_iso_aux r' Λ M N n)).hom ≫
    (FLC_complex_arrow _ (sum_hom_strict ((↥Λ →+ ↥M) ^ n) N) c).hom : _) =
  ((FLC_complex_arrow _ (aug_map_strict r' Λ M N n) c).hom) :=
begin
  rw [← iso.eq_inv_comp],
  ext x i l,
  dsimp only [FLC_arrow_iso_aux, iso.trans_inv, functor.map_iso_inv, aug_map,
    Pow_rescale_Pow_iso, iso.app_inv, iso.symm_inv,
    nat_trans.comp_app, functor.associator_hom_app, functor.associator_inv_app,
    iso_whisker_left_inv, iso_whisker_right_inv, whisker_left_app, whisker_right_app,
    Pow_comm, Pow_rescale, FLC_arrow_hom'],
  erw [category.id_comp, category.id_comp, FLC_arrow_hom',
    ← ((Filtration r').obj c).map_comp, category.assoc, ← (Pow r' n).map_comp,
    Cech_augmentation_map_eq_Hom_sum],
  dsimp only [FLC_complex_arrow, arrow.mk_hom,
    Filtration_obj_map_apply, comp_apply,
    continuous_map.coe_mk, pseudo_normed_group.level, subtype.coe_mk,
    comphaus_filtered_pseudo_normed_group_with_Tinv_hom.to_comphaus_filtered_pseudo_normed_group_hom,
    comphaus_filtered_pseudo_normed_group_hom.mk_of_strict,
    comphaus_filtered_pseudo_normed_group_hom.mk_of_bound,
    comphaus_filtered_pseudo_normed_group_hom.coe_mk,
    add_monoid_hom.to_fun_eq_coe,
    comphaus_filtered_pseudo_normed_group_with_Tinv_hom.coe_to_add_monoid_hom,
    ProFiltPseuNormGrpWithTinv.Pow_map, nat_iso.of_components.hom_app, id,
    comphaus_filtered_pseudo_normed_group_with_Tinv_hom.level_coe],
  erw [comp_apply, comp_apply, iso_of_equiv_of_strict'_hom_apply],
  dsimp only [profinitely_filtered_pseudo_normed_group_with_Tinv.pi_map_to_fun,
    ProFiltPseuNormGrpWithTinv.Pow_mul_inv, Pow_comm, Pow_mul_comm,
    Pow_mul_comm_obj_hom_to_fun, Pow_mul_comm_obj_inv_to_fun,
    nat_iso.of_components.inv_app, Pow_rescale_aux_apply],
  simp only [comp_apply, rescale.of, equiv.refl_apply, equiv.refl_symm,
    nat_iso.of_components.inv_app, id, iso_of_equiv_of_strict'_inv_apply,
    rescale_map, rescale.map_comphaus_filtered_pseudo_normed_group_with_Tinv_hom_to_fun,
    ProFiltPseuNormGrpWithTinv.Pow_mul_hom,
    equiv.symm_apply_apply, ProFiltPseuNormGrpWithTinv.Pow_Pow_X_hom_to_fun,
    ProFiltPseuNormGrpWithTinv.Pow_Pow_X_inv_to_fun,
    Pow_Pow_X_equiv_apply, Pow_Pow_X_equiv_symm_apply,
    Pow_mul_comm_obj_hom_to_fun, Pow_mul_comm_obj_inv_to_fun],
  rw [sum_hom_apply, Hom_sum_apply, finset.sum_apply],
  congr' 1,
  refine fintype.sum_congr _ _ _,
  intro j,
  simp only [function.comp_apply, equiv.refl_apply, comp_apply],
  simp only [Pow_Pow_X_equiv_apply, Pow_Pow_X_equiv_symm_apply,
    ProFiltPseuNormGrpWithTinv.Pow_Pow_X_hom_to_fun,
    ProFiltPseuNormGrpWithTinv.Pow_Pow_X_inv_to_fun,
    Pow_mul_comm_obj_hom_to_fun, Pow_mul_comm_obj_inv_to_fun, comp_apply,
    equiv.symm_trans_apply, equiv.symm_symm, equiv.curry_apply, equiv.curry_symm_apply,
    function.curry, function.uncurry, equiv.arrow_congr_symm, equiv.arrow_congr_apply,
    function.comp, equiv.refl_apply, equiv.refl_symm, equiv.trans_apply,
    linear_equiv.to_add_equiv_symm_apply, equiv.prod_comm_apply,
    linear_equiv.inv_fun_eq_symm, equiv.inv_fun_as_coe,
    linear_equiv.trans_apply, linear_equiv.symm_apply_apply, linear_equiv.symm_trans_apply,
    linear_equiv.fun_congr_left_symm, linear_equiv.fun_congr_left_apply, linear_map.fun_left_apply,
    equiv.symm_apply_apply, equiv.apply_symm_apply, equiv.prod_comm_symm],
  refl
end

end

def FLC_arrow_iso (c : ℝ≥0) :
  FLC_complex_arrow _ (aug_map_strict r' Λ M N n) c ≅
  FLC_complex_arrow _ (sum_hom_strict ((↥Λ →+ ↥M) ^ n) N) c :=
arrow.iso_mk (((Filtration r').obj c).map_iso (FLC_arrow_iso_aux r' Λ M N n)) (iso.refl _)
begin
  erw [functor.map_iso_hom, iso.refl_hom, category.comp_id],
  exact (FLC_arrow_iso_w r' Λ M N n c : _),
end

-- lemma FLC_arrow_iso_left_eq (c₁ c₂ : ℝ≥0) {_ : fact (c₁ ≤ c₂)}
--   (x : ((FLC_complex_arrow _ (aug_map_strict r' Λ M N n) c₁).left.to_Top)) :
--   pseudo_normed_group.cast_le (((FLC_arrow_iso r' Λ M N n c₁).hom.left) x) =
--     ((FLC_arrow_iso r' Λ M N n c₂).hom.left) (pseudo_normed_group.cast_le x) :=
-- by admit

-- lemma FLC_arrow_iso_right_eq (c₁ c₂ : ℝ≥0) {_ : fact (c₁ ≤ c₂)}
--   (x : ((FLC_complex_arrow _ (aug_map_strict r' Λ M N n) c₁).right.to_Top)) :
--   pseudo_normed_group.cast_le (((FLC_arrow_iso r' Λ M N n c₁).hom.right) x) =
--     ((FLC_arrow_iso r' Λ M N n c₂).hom.right) (pseudo_normed_group.cast_le x) :=
-- by admit

def col_complex_iso_obj (c : ℝ≥0ᵒᵖ) :
  (FLC_complex V _ (sum_hom_strict ((↥Λ →+ ↥M) ^ n) N)).obj c ≅
    (FLC_complex V _ (aug_map_strict r' Λ M N n)).obj c :=
begin
  refine (cosimplicial_object.augmented.cocomplex.map_iso _),
  refine functor.map_iso _ _,
  refine functor.map_iso _ _,
  refine functor.map_iso _ _,
  refine iso.op _,
  exact FLC_arrow_iso r' Λ M N n c.unop
end

def col_complex_iso_aux2 :
  FLC_complex V _ (sum_hom_strict ((↥Λ →+ ↥M) ^ n) N) ≅
  FLC_complex V _ (aug_map_strict r' Λ M N n) :=
nat_iso.of_components (col_complex_iso_obj r' V Λ M N n)
begin
  intros c₁ c₂ h,
  dsimp only [FLC_complex, FLC_functor, FLC_functor', col_complex_iso_obj, functor.comp_map,
    functor.map_iso_hom, iso.op_hom],
  simp only [← category_theory.functor.map_comp, ← op_comp],
  refl
end

section open cosimplicial_object

lemma col_complex_iso_aux2_strict (c : ℝ≥0ᵒᵖ) (i : ℕ) :
  isometry (((col_complex_iso_aux2 r' V Λ M N n).hom.app c).f i) :=
begin
  rw [← iso.app_hom, ← homological_complex.hom.iso_app_hom],
  refine SemiNormedGroup.iso_isometry_of_norm_noninc _ _ _;
  [ rw [homological_complex.hom.iso_app_hom, iso.app_hom],
    rw [homological_complex.hom.iso_app_inv, iso.app_inv] ];
  { dsimp only [col_complex_iso_aux2, col_complex_iso_obj, nat_iso.of_components, functor.comp_map,
      functor.map_iso_hom, iso.op_hom, quiver.hom.unop_op, functor.op_map,
      cosimplicial_object.augmented.whiskering_obj_2,
      cosimplicial_object.augmented.whiskering_obj],
    apply augmented.cocomplex_map_norm_noninc;
    { intros, apply SemiNormedGroup.LCC_obj_map_norm_noninc, }, },
end

end

def col_complex_iso :
  FLC_complex V _ (sum_hom_strict ((↥Λ →+ ↥M)^n) N) ≅
  col_complex r' V Λ M N n :=
col_complex_iso_aux2 r' V Λ M N n ≪≫ FLC_complex_aug_iso r' V Λ M N n ≪≫ col_complex_level_iso r' V Λ M N n

lemma col_complex_iso_strict (c : ℝ≥0ᵒᵖ) (i : ℕ) :
  isometry (((col_complex_iso r' V Λ M N n).hom.app c).f i) :=
begin
  refine isometry.comp _ (col_complex_iso_aux2_strict r' V Λ M N n c i),
  exact (col_complex_level_iso_strict r' V Λ M N n c i).comp
    (FLC_complex_aug_iso_strict r' V Λ M N n c i),
end

end

lemma col_complex.is_weak_bounded_exact (d : ℝ≥0) [pseudo_normed_group.splittable ((Λ →+ M)^n) N d]
  (k : ℝ≥0) [fact (1 ≤ k)] (m : ℕ) (c₀ : ℝ≥0) (hdkc₀N : d ≤ (k - 1) * c₀ / N) :
  (col_complex r' V Λ M N n).is_weak_bounded_exact k 1 m c₀ :=
begin
  have key := FLC_complex.weak_bounded_exact V ((Λ →+ M)^n) N d k m c₀ hdkc₀N,
  exact key.of_iso _ (λ c, col_complex_iso_strict r' V Λ M N n (op c)),
end

@[simps obj map]
def col_complex_rescaled : system_of_complexes :=
scale_factorial.obj (col_complex r' V Λ M N n)
.

lemma col_complex_rescaled.is_weak_bounded_exact
  (d : ℝ≥0) [pseudo_normed_group.splittable ((Λ →+ M)^n) N d]
  (k : ℝ≥0) [fact (1 ≤ k)] (m : ℕ) (c₀ : ℝ≥0) (hdkc₀N : d ≤ (k - 1) * c₀ / N) :
  (col_complex_rescaled r' V Λ M N n).is_weak_bounded_exact k (m+1) m c₀ :=
begin
  have := scale_factorial.is_weak_bounded_exact
    (col_complex.is_weak_bounded_exact r' V Λ M N n d k m c₀ hdkc₀N),
  rwa [one_mul] at this,
end

end

end

namespace col_complex_rescaled

open polyhedral_lattice (Hom)
open PolyhedralLattice (cosimplicial)

instance move_pls (r' : ℝ≥0) (c : ℝ≥0ᵒᵖ) : fact (unop (r'.MulLeft.op.obj c) ≤ r' * unop c) :=
⟨le_rfl⟩

instance move_pls2 [fact (r' < 1)] (c : ℝ≥0ᵒᵖ) : fact (unop (r'.MulLeft.op.obj c) ≤ unop c) :=
by { dsimp [nnreal.MulLeft], apply_instance }

variables [fact (0 < r)] [fact (0 < r')] [fact (r' < 1)]

def T_inv_sub_Tinv_f_succ [normed_with_aut r V] (c : ℝ≥0ᵒᵖ) (i : ℕ) :
  ((col_complex_rescaled.{u} r' V Λ M N n).obj c).X (i + 1) ⟶
    (((col_complex_rescaled.{u} r' V Λ M N n).scale_index_left r').obj c).X (i + 1) :=
(SemiNormedGroup.rescale (i+1)!).map $ (CLCFP.T_inv_sub_Tinv r r' V _ _ n).app _

def T_inv_sub_Tinv_f [normed_with_aut r V] (c : ℝ≥0ᵒᵖ) :
  Π i, ((col_complex_rescaled.{u} r' V Λ M N n).obj c).X i ⟶
  (((col_complex_rescaled.{u} r' V Λ M N n).scale_index_left r').obj c).X i
| 0     := (SemiNormedGroup.rescale 0!).map $ (CLCFP.T_inv_sub_Tinv r r' V _ _ n).app _
| (i+1) := T_inv_sub_Tinv_f_succ r r' V Λ M N n c i

section open system_of_complexes category_theory.preadditive category_theory.cosimplicial_object
  homological_complex

lemma T_inv_sub_Tinv_comm_zero [normed_with_aut r V] (c : ℝ≥0ᵒᵖ) :
  T_inv_sub_Tinv_f r r' V Λ M N n c 0 ≫
    (((col_complex_rescaled r' V Λ M N n).scale_index_left r').obj c).d 0 1 =
  ((col_complex_rescaled r' V Λ M N n).obj c).d 0 1 ≫
    T_inv_sub_Tinv_f r r' V Λ M N n c 1 :=
begin
  dsimp only [T_inv_sub_Tinv_f, T_inv_sub_Tinv_f_succ, scale_index_left, col_complex_rescaled],
  refine SemiNormedGroup.scale_comm _ _ _ _ _ _ _,
  dsimp,
  rw [if_pos rfl, category.comp_id],
  dsimp only [augmented.to_cocomplex_d],
  erw [Cech_nerve'_hom_zero],
  dsimp only [CLCFP'_map_app],
  erw nat_trans.naturality,
  refl
end
.

lemma T_inv_sub_Tinv_comm_succ [normed_with_aut r V] (c : ℝ≥0ᵒᵖ) (i : ℕ) :
  T_inv_sub_Tinv_f r r' V Λ M N n c (i+1) ≫
    (((col_complex_rescaled r' V Λ M N n).scale_index_left r').obj c).d (i+1) (i+2) =
  ((col_complex_rescaled r' V Λ M N n).obj c).d (i+1) (i+2) ≫
    T_inv_sub_Tinv_f r r' V Λ M N n c (i+2) :=
begin
  dsimp only [T_inv_sub_Tinv_f, T_inv_sub_Tinv_f_succ, scale_index_left, col_complex_rescaled],
  refine SemiNormedGroup.scale_comm _ _ _ _ _ _ _,
  dsimp,
  rw [if_pos rfl, category.comp_id],
  dsimp only [augmented.to_cocomplex_d, coboundary, augmented.drop_obj, Cech_nerve',
    augmented.whiskering_obj_2, augmented.whiskering_obj, cosimplicial_object.δ,
    whiskering_obj_obj_map],
  simp only [nat_trans.app_sum, nat_trans.app_zsmul, sum_comp, comp_sum, zsmul_comp, comp_zsmul],
  apply fintype.sum_congr,
  intro j,
  congr' 1,
  dsimp only [CLCFP'_map_app],
  erw nat_trans.naturality,
  refl,
end
.

lemma T_inv_sub_Tinv_naturality_zero [normed_with_aut r V] (c₁ c₂ : ℝ≥0ᵒᵖ) (h : c₁ ⟶ c₂) :
  ((col_complex_rescaled r' V Λ M N n).map h).f 0 ≫ T_inv_sub_Tinv_f r r' V Λ M N n c₂ 0 =
    T_inv_sub_Tinv_f r r' V Λ M N n c₁ 0 ≫
      (((col_complex_rescaled r' V Λ M N n).scale_index_left r').map h).f 0 :=
begin
  dsimp only [T_inv_sub_Tinv_f, scale_index_left, ScaleIndexLeft_obj_map,
    col_complex_rescaled, scale_factorial_obj, functor.comp_map, modify_functor_map_f,
    col_complex_map, augmented.to_cocomplex_obj, augmented.point_obj, Cech_nerve',
    augmented.whiskering_obj],
  simp only [← category_theory.functor.map_comp],
  congr' 1,
  dsimp only [CLCFP'_obj_map, CLCFP.T_inv_sub_Tinv, nnreal.MulLeft, functor.op_obj, unop_op],
  simp only [nat_trans.app_sub, comp_sub, sub_comp, ← nat_trans.comp_app],
  congr' 2,
  { rw [category.assoc, ← CLCFP.res_comp_T_inv],
    haveI : fact (c₂.unop ≤ c₁.unop) := ⟨le_of_hom h.unop⟩,
    simp only [← category.assoc, CLCFP.res_comp_res], },
  { dsimp only [CLCFP.Tinv, CLCFP.res, CLC, LC],
    simp only [← whisker_right_comp, ← nat_trans.op_comp],
    refl, }
end
.

lemma T_inv_sub_Tinv_naturality_succ [normed_with_aut r V] (c₁ c₂ : ℝ≥0ᵒᵖ) (h : c₁ ⟶ c₂) (i : ℕ) :
  ((col_complex_rescaled r' V Λ M N n).map h).f (i+1) ≫ T_inv_sub_Tinv_f r r' V Λ M N n c₂ (i+1) =
    T_inv_sub_Tinv_f r r' V Λ M N n c₁ (i+1) ≫
      (((col_complex_rescaled r' V Λ M N n).scale_index_left r').map h).f (i+1) :=
begin
  dsimp only [T_inv_sub_Tinv_f, T_inv_sub_Tinv_f_succ, scale_index_left, ScaleIndexLeft_obj_map,
    col_complex_rescaled, scale_factorial_obj, functor.comp_map, modify_functor_map_f,
    col_complex_map, augmented.to_cocomplex_obj, augmented.drop_obj, Cech_nerve',
    augmented.whiskering_obj, whiskering_obj_obj_obj],
  simp only [← category_theory.functor.map_comp],
  congr' 1,
  dsimp only [CLCFP'_obj_map, CLCFP.T_inv_sub_Tinv, nnreal.MulLeft, functor.op_obj, unop_op],
  simp only [nat_trans.app_sub, comp_sub, sub_comp],
  erw [← nat_trans.comp_app, ← nat_trans.comp_app, ← nat_trans.comp_app, ← nat_trans.comp_app],
  congr' 2,
  { rw [category.assoc, ← CLCFP.res_comp_T_inv],
    haveI : fact (c₂.unop ≤ c₁.unop) := ⟨le_of_hom h.unop⟩,
    simp only [← category.assoc, CLCFP.res_comp_res], },
  { dsimp only [CLCFP.Tinv, CLCFP.res, CLC, LC],
    simp only [← whisker_right_comp, ← nat_trans.op_comp],
    refl, }
end

end

def T_inv_sub_Tinv [normed_with_aut r V] :
  col_complex_rescaled r' V Λ M N n ⟶ (col_complex_rescaled r' V Λ M N n).scale_index_left r' :=
{ app := λ c,
  { f := T_inv_sub_Tinv_f r r' V Λ M N n c,
    comm' :=
    begin
      rintros i j (rfl : i + 1 = j),
      cases i, { apply T_inv_sub_Tinv_comm_zero }, { apply T_inv_sub_Tinv_comm_succ }
    end },
  naturality' :=
  begin
    intros c₁ c₂ h, ext i : 2, cases i,
    { apply T_inv_sub_Tinv_naturality_zero },
    { apply T_inv_sub_Tinv_naturality_succ },
  end }

def T_inv_sub_Tinv' (c : ℝ≥0) [normed_with_aut r V] :=
(system_of_complexes.ScaleIndexRight c).map
  (col_complex_rescaled.T_inv_sub_Tinv r r' V Λ M N n)

end col_complex_rescaled

namespace double_complex

open polyhedral_lattice (Hom)

local attribute [semireducible] CLCFPTinv CLCFPTinv₂ CLCFP -- CLCTinv

variables [fact (0 < r)] [fact (0 < r')] [fact (r < r')] [fact (r' < 1)]

@[simps obj map]
def col'_aux [normed_with_aut r V] (n : ℕ) : system_of_complexes :=
(double_complex' BD κ r r' V Λ M N).col n

@[simps obj map]
def col' [normed_with_aut r V] (n : ℕ) : system_of_complexes :=
scale_factorial.obj (col'_aux BD κ r r' V Λ M N n)
.

def col_iso_obj_X [normed_with_aut r V] (c : ℝ≥0ᵒᵖ) :
  Π m, (((double_complex.{u} BD κ r r' V Λ M N).col n).obj c).X m ≅
  ((col'.{u} BD κ r r' V Λ M N n).obj c).X m
| 0     := (SemiNormedGroup.iso_rescale _).app _
| 1     := (SemiNormedGroup.iso_rescale _).app _
| (m+2) := iso.refl _

section

open homological_complex system_of_complexes

lemma col_iso_comm₁_0 [normed_with_aut r V] (c : ℝ≥0ᵒᵖ) :
  (col_iso_obj_X BD κ r r' V Λ M N n c 0).hom ≫
    ((col' BD κ r r' V Λ M N n).obj c).d 0 1 =
  (((double_complex BD κ r r' V Λ M N).col n).obj c).d 0 1 ≫
    (col_iso_obj_X BD κ r r' V Λ M N n c 1).hom :=
by { dsimp only [col_iso_obj_X], ext, refl }
.

lemma col_iso_comm₁_1 [normed_with_aut r V] (c : ℝ≥0ᵒᵖ) :
  (col_iso_obj_X BD κ r r' V Λ M N n c 1).hom ≫
    ((col' BD κ r r' V Λ M N n).obj c).d 1 2 =
  (((double_complex BD κ r r' V Λ M N).col n).obj c).d 1 2 ≫
    (col_iso_obj_X BD κ r r' V Λ M N n c 2).hom :=
begin
  delta col_iso_obj_X,
  simp only [iso.refl_hom, nat.rec_add_one, category.id_comp, category.comp_id,
    system_of_double_complexes.col_obj_d],
  dsimp only [col'_obj, col'_aux_obj, double_complex', double_complex,
    double_complex_aux_rescaled, as_functor_obj, modify_d, eval_obj, eval_map,
    functor.map_homological_complex_obj_d, functor.map_homological_complex_obj_X,
    nat_trans.comp_app, comp_f, rescale_functor, rescale_nat_trans,
    system_of_complexes.rescale, scale],
  refl
end
.

lemma col_iso_comm₂_0 [normed_with_aut r V] (c₁ c₂ : ℝ≥0ᵒᵖ) (h : c₁ ⟶ c₂) :
  (((double_complex.{u} BD κ r r' V Λ M N).col n).map h).f 0 ≫
    (col_iso_obj_X BD κ r r' V Λ M N n c₂ 0).hom =
  (col_iso_obj_X BD κ r r' V Λ M N n c₁ 0).hom ≫
    ((col'.{u} BD κ r r' V Λ M N n).map h).f 0 :=
by { dsimp only [col_iso_obj_X], ext, refl }
.

lemma col_iso_comm₂_1 [normed_with_aut r V] (c₁ c₂ : ℝ≥0ᵒᵖ) (h : c₁ ⟶ c₂) :
  (((double_complex.{u} BD κ r r' V Λ M N).col n).map h).f 1 ≫
    (col_iso_obj_X BD κ r r' V Λ M N n c₂ 1).hom =
  (col_iso_obj_X BD κ r r' V Λ M N n c₁ 1).hom ≫
    ((col'.{u} BD κ r r' V Λ M N n).map h).f 1 :=
by { dsimp only [col_iso_obj_X], ext, refl }
.

local attribute [irreducible] CLCFPTinv CLCFPTinv₂ CLCFP
  SemiNormedGroup.rescale SemiNormedGroup.scale
  double_complex_aux

lemma col_iso_comm₁_succ [normed_with_aut r V] (c : ℝ≥0ᵒᵖ) (i : ℕ) :
  (col_iso_obj_X BD κ r r' V Λ M N n c i.succ.succ).hom ≫
    ((col'.{u} BD κ r r' V Λ M N n).obj c).d i.succ.succ (i.succ.succ + 1) =
  (((double_complex.{u} BD κ r r' V Λ M N).col n).obj c).d i.succ.succ (i.succ.succ + 1) ≫
    (col_iso_obj_X BD κ r r' V Λ M N n c (i.succ.succ + 1)).hom :=
begin
  dsimp only [col_iso_obj_X, iso.refl_hom],
  simp only [category.id_comp, category.comp_id, system_of_double_complexes.col_obj_d],
  refl,
end
.

lemma col_iso_comm₂_succ [normed_with_aut r V] (c₁ c₂ : ℝ≥0ᵒᵖ) (h : c₁ ⟶ c₂) (i : ℕ) :
  (((double_complex.{u} BD κ r r' V Λ M N).col n).map h).f (i+2) ≫
    (col_iso_obj_X BD κ r r' V Λ M N n c₂ (i+2)).hom =
  (col_iso_obj_X BD κ r r' V Λ M N n c₁ (i+2)).hom ≫
    ((col'.{u} BD κ r r' V Λ M N n).map h).f (i+2) :=
begin
  dsimp only [col_iso_obj_X, iso.refl_hom],
  simp only [category.id_comp, category.comp_id, system_of_double_complexes.col_obj_d],
  refl
end

lemma col_iso_comm₂ [normed_with_aut r V] (c₁ c₂ : ℝ≥0ᵒᵖ) (h : c₁ ⟶ c₂) :
  ∀ i, (((double_complex.{u} BD κ r r' V Λ M N).col n).map h).f i ≫
    (col_iso_obj_X BD κ r r' V Λ M N n c₂ i).hom =
  (col_iso_obj_X BD κ r r' V Λ M N n c₁ i).hom ≫
    ((col'.{u} BD κ r r' V Λ M N n).map h).f i
| 0     := col_iso_comm₂_0 _ _ _ _ _ _ _ _ _ _ _ _
| 1     := col_iso_comm₂_1 _ _ _ _ _ _ _ _ _ _ _ _
| (i+2) := col_iso_comm₂_succ _ _ _ _ _ _ _ _ _ _ _ _ _
.

end

section

open homological_complex

-- set_option pp.universes true

@[simps]
def col_iso [normed_with_aut r V] :
  (double_complex.{u} BD κ r r' V Λ M N).col n ≅
  col'.{u} BD κ r r' V Λ M N n :=
nat_iso.of_components (λ c, hom.iso_of_components (col_iso_obj_X.{u} BD κ r r' V Λ M N n _)
  begin
    rintro i j (rfl : i + 1 = j),
    cases i, { exact col_iso_comm₁_0 BD κ r r' V Λ M N n c, },
    cases i, { exact col_iso_comm₁_1 BD κ r r' V Λ M N n c, },
    { exact col_iso_comm₁_succ BD κ r r' V Λ M N n c i, },
  end)
  begin
    intros c₁ c₂ h, ext i : 2,
    dsimp only [comp_f, hom.iso_of_components_hom_f],
    exact col_iso_comm₂ BD κ r r' V Λ M N n c₁ c₂ h i,
  end
.

lemma col_iso_strict [normed_with_aut r V] (c : ℝ≥0ᵒᵖ) (i : ℕ) :
  isometry (hom.iso_app ((col_iso BD κ r r' V Λ M N n).app c) i).hom :=
begin
  dsimp only [hom.iso_app_hom, nat_iso.app_hom, col_iso_hom_app_f],
  cases i, { delta col_iso_obj_X, apply SemiNormedGroup.iso_rescale_isometry, exact nat.cast_one },
  cases i, { delta col_iso_obj_X, apply SemiNormedGroup.iso_rescale_isometry, exact nat.cast_one },
  { delta col_iso_obj_X, exact isometry_id }
end

lemma col_iso_inv_strict [normed_with_aut r V] (c : ℝ≥0ᵒᵖ) (i : ℕ) :
  isometry (hom.iso_app ((col_iso BD κ r r' V Λ M N n).app c) i).inv :=
(col_iso_strict BD κ r r' V Λ M N n c i).right_inv $
λ x, by rw [← comp_apply, iso.inv_hom_id, id_apply]

end

lemma col_obj_X_zero [normed_with_aut r V] (c : ℝ≥0ᵒᵖ) :
  (((double_complex BD κ r r' V Λ M N).col n).obj c).X 0 =
  (CLCFPTinv r V r' (c.unop * κ n) (BD.X n)).obj (op $ Hom Λ M) := rfl

-- local attribute [semireducible] opposite

def col_ι_f_succ [normed_with_aut r V] (c : ℝ≥0ᵒᵖ) (i : ℕ) :
  ((col'.{u} BD κ r r' V Λ M N n).obj c).X (i+1) ⟶
    (((col_complex_rescaled.{u} r' V Λ M N (BD.X n)).scale_index_right (κ n)).obj c).X (i+1) :=
(SemiNormedGroup.rescale (i+1)!).map (CLCTinv.ι r V _ _)

def col_ι_f [normed_with_aut r V] (c : ℝ≥0ᵒᵖ) :
  Π i, ((col'.{u} BD κ r r' V Λ M N n).obj c).X i ⟶
    (((col_complex_rescaled.{u} r' V Λ M N (BD.X n)).scale_index_right (κ n)).obj c).X i
| 0     := (SemiNormedGroup.rescale 0!).map (CLCTinv.ι r V _ _)
| (i+1) := col_ι_f_succ _ _ _ _ _ _ _ _ _ _ i

section open homological_complex system_of_complexes breen_deligne

lemma col_ι_f_comm_zero [normed_with_aut r V] (c : ℝ≥0ᵒᵖ) :
  col_ι_f BD κ r r' V Λ M N n c 0 ≫
    (((col_complex_rescaled r' V Λ M N (BD.X n)).scale_index_right (κ n)).obj c).d 0 1 =
  ((col' BD κ r r' V Λ M N n).obj c).d 0 1 ≫ col_ι_f BD κ r r' V Λ M N n c 1 :=
begin
  dsimp only [col_ι_f, col_ι_f_succ, col'_obj, functor.map_homological_complex_obj_d,
    modify_d, eval_map, scale_index_right, ScaleIndexRight_obj_obj, col_complex_rescaled_obj,
    scale'_app],
  refine SemiNormedGroup.scale_comm _ _ _ _ _ _ _,
  rw [dif_pos rfl, dif_pos rfl],
  simp only [cosimplicial_object.augmented.to_cocomplex_d, eq_to_hom_refl, category.comp_id],
  erw [Cech_nerve'_hom_zero, cosimplicial_system_of_complexes_hom_zero],
  dsimp only [data.system_map, data.complex, data.complex₂_map_f, CLCFPTinv₂, CLCTinv.F_map],
  symmetry,
  apply CLCTinv.map_comp_ι,
end

section open category_theory.preadditive

lemma col_ι_f_comm_succ [normed_with_aut r V] (c : ℝ≥0ᵒᵖ) (i : ℕ) :
  col_ι_f BD κ r r' V Λ M N n c (i + 1) ≫
    (((col_complex_rescaled r' V Λ M N (BD.X n)).scale_index_right (κ n)).obj c).d (i+1) (i+2) =
  ((col' BD κ r r' V Λ M N n).obj c).d (i + 1) (i + 2) ≫ col_ι_f BD κ r r' V Λ M N n c (i+2) :=
begin
  dsimp only [col_ι_f, col_ι_f_succ, col'_obj, functor.map_homological_complex_obj_d,
    modify_d, eval_map, scale_index_right, ScaleIndexRight_obj_obj, col_complex_rescaled_obj,
    scale'_app],
  refine SemiNormedGroup.scale_comm _ _ _ _ _ _ _,
  rw [dif_pos rfl, dif_pos rfl],
  simp only [cosimplicial_object.augmented.to_cocomplex_d, eq_to_hom_refl, category.comp_id,
    cosimplicial_object.coboundary, nat_trans.app_sum, nat_trans.app_zsmul,
    ← homological_complex.hom.f_add_monoid_hom_apply, add_monoid_hom.map_sum,
    add_monoid_hom.map_zsmul, sum_comp, comp_sum, zsmul_comp, comp_zsmul],
  symmetry,
  apply fintype.sum_congr,
  intro j,
  refl,
end

end

lemma col_ι_f_comm [normed_with_aut r V] (c : ℝ≥0ᵒᵖ) :
  ∀ i, col_ι_f BD κ r r' V Λ M N n c i ≫
    (((col_complex_rescaled r' V Λ M N (BD.X n)).scale_index_right (κ n)).obj c).d i (i + 1) =
  ((col' BD κ r r' V Λ M N n).obj c).d i (i + 1) ≫ col_ι_f BD κ r r' V Λ M N n c (i + 1)
| 0     := by apply col_ι_f_comm_zero
| (i+1) := by apply col_ι_f_comm_succ

section open category_theory.cosimplicial_object

lemma col_ι_naturality_zero [normed_with_aut r V] (c₁ c₂ : ℝ≥0ᵒᵖ) (h : c₁ ⟶ c₂) :
  ((col' BD κ r r' V Λ M N n).map h).f 0 ≫ col_ι_f BD κ r r' V Λ M N n c₂ 0 =
  col_ι_f BD κ r r' V Λ M N n c₁ 0 ≫ (((col_complex_rescaled r' V Λ M N (BD.X n)).scale_index_right (κ n)).map h).f 0 :=
begin
  dsimp only [col'_map, functor.map_homological_complex_map_f, eval_map,
    modify_functor_map_f, col_ι_f,
    scale_index_right, ScaleIndexRight_obj_map, col_complex_rescaled_map],
  simp only [← category_theory.functor.map_comp],
  congr' 1,
  dsimp only [augmented.to_cocomplex_obj, augmented.point_obj, cosimplicial_system_of_complexes,
    Cech_nerve', augmented.whiskering_obj, CLCFP',
    data.system_obj, data.complex, data.complex₂_obj_X, CLCFPTinv₂.res, CLCTinv.map_nat,
    functor.comp_obj, functor.comp_map, functor.op_obj, functor.op_map, whiskering_right_obj_obj,
    functor.op_hom_obj, unop_op, functor.flip_obj_map],
  apply CLCTinv.map_comp_ι,
end
.

lemma col_ι_naturality_succ [normed_with_aut r V] (c₁ c₂ : ℝ≥0ᵒᵖ) (h : c₁ ⟶ c₂) (i : ℕ) :
  ((col' BD κ r r' V Λ M N n).map h).f (i+1) ≫ col_ι_f BD κ r r' V Λ M N n c₂ (i+1) =
  col_ι_f BD κ r r' V Λ M N n c₁ (i+1) ≫ (((col_complex_rescaled r' V Λ M N (BD.X n)).scale_index_right (κ n)).map h).f (i+1) :=
begin
  dsimp only [col'_map, functor.map_homological_complex_map_f, eval_map,
    modify_functor_map_f, col_ι_f, col_ι_f_succ,
    scale_index_right, ScaleIndexRight_obj_map, col_complex_rescaled_map],
  simp only [← category_theory.functor.map_comp],
  congr' 1,
  dsimp only [augmented.to_cocomplex_obj, augmented.drop_obj, cosimplicial_system_of_complexes,
    Cech_nerve', augmented.whiskering_obj, CLCFP', whiskering_obj_obj_obj,
    data.system_obj, data.complex, data.complex₂_obj_X, CLCFPTinv₂.res, CLCTinv.map_nat,
    functor.comp_obj, functor.comp_map, functor.op_obj, functor.op_map, whiskering_right_obj_obj,
    functor.op_hom_obj, unop_op, functor.flip_obj_map],
  apply CLCTinv.map_comp_ι,
end
.

end

end

def col_ι [normed_with_aut r V] :
  col'.{u} BD κ r r' V Λ M N n ⟶
    (col_complex_rescaled.{u} r' V Λ M N (BD.X n)).scale_index_right (κ n) :=
{ app := λ c,
  { f := col_ι_f BD κ r r' V Λ M N n c,
    comm' := by { rintro i j (rfl : i + 1 = j), apply col_ι_f_comm } },
  naturality' :=
  begin
    intros c₁ c₂ h, ext i : 2,
    cases i,
    { apply col_ι_naturality_zero },
    { apply col_ι_naturality_succ },
  end }

variables [normed_with_aut r V] (c : ℝ≥0ᵒᵖ) (i : ℕ)

lemma col_ι_range :
  (((double_complex.col_ι BD κ r r' V Λ M N n).app c).f i).range =
  (((col_complex_rescaled.T_inv_sub_Tinv' r r' V Λ M N (BD.X n) (κ n)).app c).f i).ker :=
begin
  cases i;
  { refine SemiNormedGroup.rescale_exact _ _ _ _,
    rw CLCTinv.ι_range',
    ext1 x,
    refl, },
end

lemma col_ι_isometry :
  isometry (((double_complex.col_ι BD κ r r' V Λ M N n).app c).f i) :=
begin
  cases i;
  { refine SemiNormedGroup.rescale_map_isometry _ _,
    apply add_monoid_hom_class.isometry_of_norm,
    intro, refl },
end

end double_complex

namespace col_complex_rescaled

variables [fact (0 < r')] [fact (r' ≤ 1)]

lemma d_zero_norm_noninc (c : ℝ≥0) :
  (@system_of_complexes.d (col_complex_rescaled r' V Λ M N n) c 0 1).norm_noninc :=
begin
  apply normed_add_group_hom.norm_noninc.norm_noninc_iff_norm_le_one.2,
  refine normed_add_group_hom.norm_comp_le_of_le' (1:ℕ) _ 1 _ (SemiNormedGroup.norm_scale_le _ _ _) _,
  { simp only [mul_one, nat.factorial_zero, nat.factorial_one, nat.cast_one, div_one, nnreal.coe_one]},
  apply SemiNormedGroup.norm_rescale_map_le,
  have : (1 : ℝ) = ∑ i : fin 1, 1,
  { simp only [finset.card_fin, mul_one, finset.sum_const, nsmul_eq_mul, nat.cast_id,
      nat.cast_bit1, nat.cast_add, nat.cast_one] },
  dsimp [system_of_complexes.rescale_functor, double_complex_aux,
    cosimplicial_object.augmented.to_cocomplex_d],
  erw [category.comp_id, if_pos rfl, Cech_nerve'_hom_zero, nat.cast_one],
  apply normed_add_group_hom.norm_noninc.norm_noninc_iff_norm_le_one.1,
  apply CLC.map_norm_noninc,
end

lemma d_succ_norm_noninc (c : ℝ≥0) (p : ℕ) :
  (@system_of_complexes.d (col_complex_rescaled r' V Λ M N n) c (p+1) (p+2)).norm_noninc :=
begin
  apply normed_add_group_hom.norm_noninc.norm_noninc_iff_norm_le_one.2,
  refine normed_add_group_hom.norm_comp_le_of_le' (p+2:ℕ) _ 1 _ (SemiNormedGroup.norm_scale_le _ _ _) _,
  { norm_cast,
    rw [mul_comm, ← mul_div_assoc, eq_comm, ← nat.cast_mul, nat.factorial_succ], apply div_self,
    norm_num [nat.factorial_ne_zero] },
  apply SemiNormedGroup.norm_rescale_map_le,
  have : (p+1+1 : ℝ) = ∑ i : fin (p+1+1), 1,
  { simp only [finset.card_fin, mul_one, finset.sum_const, nsmul_eq_mul, nat.cast_id,
      nat.cast_bit1, nat.cast_add, nat.cast_one] },
  dsimp [system_of_complexes.rescale_functor, double_complex_aux,
    cosimplicial_object.augmented.to_cocomplex_d],
  erw [category.comp_id, if_pos rfl],
  dsimp [cosimplicial_object.coboundary],
  rw [add_assoc, show (1 : ℝ)+1=2, by norm_num] at this,
  simp only [← nat_trans.app_hom_apply, add_monoid_hom.map_sum, add_monoid_hom.map_zsmul,
    ← homological_complex.hom.f_add_monoid_hom_apply, nat.cast_add, nat.cast_bit0, nat.cast_one,
    this],
  apply norm_sum_le_of_le,
  rintro i -,
  refine le_trans (norm_zsmul_le _ _) _,
  rw [← int.norm_cast_real, int.cast_pow, norm_pow, int.cast_neg, int.cast_one, norm_neg, norm_one,
    one_pow, one_mul],
  apply normed_add_group_hom.norm_noninc.norm_noninc_iff_norm_le_one.1,
  apply CLC.map_norm_noninc
end

lemma admissible : (col_complex_rescaled r' V Λ M N n).admissible :=
{ d_norm_noninc' :=
  begin
    rintro c i j rfl, cases i,
    { apply d_zero_norm_noninc, },
    { apply d_succ_norm_noninc, }
  end,
  res_norm_noninc :=
  begin
    intros c₁ c₂ i h,
    apply normed_add_group_hom.norm_noninc.norm_noninc_iff_norm_le_one.2,
    cases i;
    { apply SemiNormedGroup.norm_rescale_map_le,
      apply normed_add_group_hom.norm_noninc.norm_noninc_iff_norm_le_one.1,
      apply CLC.map_norm_noninc, },
  end }

end col_complex_rescaled

variables [fact (0 < r)] [fact (0 < r')] [fact (r' < 1)]

lemma col_exact'_aux1 [normed_with_aut r V] (c : ℝ≥0ᵒᵖ) (i : ℕ) :
  ∀ x, ∥(((col_complex_rescaled.T_inv_sub_Tinv' r r' V Λ M N (BD.X n) (κ n)).app c).f i) x∥ ≤
    (1 + r⁻¹) * ∥x∥ :=
begin
  intro x,
  cases i;
  { apply normed_add_group_hom.le_of_op_norm_le,
    refine @SemiNormedGroup.norm_rescale_map_le _ _ _ _ _ (1 + r⁻¹) _,
    exact CLCFP.norm_T_inv_sub_Tinv_le _ _ _ _ _ _ _ }
end

variables [fact (r < r')]

lemma col_exact'_aux2 [normed_with_aut r V] (c : ℝ≥0ᵒᵖ) (i : ℕ) :
  ∀ y, ∃ x,
    (((col_complex_rescaled.T_inv_sub_Tinv' r r' V Λ M N (BD.X n) (κ n)).app c).f i) x = y ∧
    ∥x∥ ≤ ↑(r / (1 - r) + 1) * ∥y∥ :=
begin
  haveI : fact (r < 1) := ⟨@lt_trans _ _ r r' 1 (fact.out _) (fact.out _)⟩,
  cases i;
  { refine SemiNormedGroup.rescale_exists_norm_le _ _ _ _,
    intro y,
    obtain ⟨x, h1, h2⟩ := CLCFP.T_inv_sub_Tinv_exists_preimage r r' y 1 zero_lt_one,
    refine ⟨x, h1, _⟩,
    rwa [nnreal.coe_add, nnreal.coe_div, nnreal.coe_sub],
    exact fact.out _ }
end

lemma col_exact' [normed_with_aut r V] [fact (r < 1)]
  (d : ℝ≥0) [pseudo_normed_group.splittable (Λ →+ M) N d]
  (k : ℝ≥0) [fact (1 ≤ k)] (m : ℕ) (c₀ : ℝ≥0) (hdkc₀N : d ≤ (k - 1) * c₀ / N)
  (k' K' : ℝ≥0) [fact (1 ≤ k')] (hk' : k * k ≤ k')
  (hK' : (m + 2 + (r + 1) / (r * (1 - r)) * (m + 2)^2 : ℝ≥0) ≤ K')
  (c₁ c₂ : ℝ≥0) [fact (c₀ ≤ r' * c₁)] [fact (c₀ ≤ κ n * c₂)] [fact (c₁ ≤ κ n * c₂)] :
  (double_complex.col'.{u} BD κ r r' V Λ M N n).is_weak_bounded_exact k' K' m c₂ :=
begin
  have adm := (col_complex_rescaled.admissible.{u} r' V Λ M N (BD.X n)),
  have adm2 := adm.scale_index_left r',
  let T_T := col_complex_rescaled.T_inv_sub_Tinv' r r' V Λ M N (BD.X n) (κ n),
  have H := (col_complex_rescaled.is_weak_bounded_exact.{u}
    r' V Λ M N (BD.X n) d k (m+1) c₀ hdkc₀N),
  have H1 := H.scale_index_right _ c₂ (κ n) adm,
  have H2 := (H.scale_index_left _ c₁ r' adm).scale_index_right _ c₂ (κ n) adm2,
  have key := weak_normed_snake_dual
    (double_complex.col'.{u} BD κ r r' V Λ M N n) _ _
    (double_complex.col_ι BD κ r r' V Λ M N n) T_T
    k _ ((m + 1) + 1) _ (1 + r⁻¹) (r / (1 - r) + 1) (by simpa using H1) H2 (adm.scale_index_right _),
  have h_isom : _ := _,
  apply (key _ _ _ h_isom).of_le _ ⟨hk'⟩ _ le_rfl ⟨le_rfl⟩,
  any_goals { clear key adm2 H1 H2 },
  { intros, apply col_exact'_aux1 },
  { intros, apply col_exact'_aux2 },
  { intros c i, apply double_complex.col_ι_range },
  { apply system_of_complexes.admissible_of_isometry (adm.scale_index_right _) h_isom, },
  { refine ⟨le_trans (le_of_eq _) hK'⟩,
    rw [pow_two, ← mul_assoc],
    simp only [nat.cast_add, nat.cast_one, bit0, ← add_assoc, or_false, add_eq_zero_iff,
      one_ne_zero, add_right_inj, mul_eq_mul_right_iff, and_false, div_eq_mul_inv],
    have hr0 : r ≠ 0, { exact ne_of_gt (fact.out _) },
    have h1r : 1 - r ≠ 0,
    { rw [← nnreal.coe_injective.ne_iff, nnreal.coe_sub, nnreal.coe_zero, sub_ne_zero],
      { norm_cast, exact ne_of_gt (fact.out _) },
      { exact fact.out _ } },
    calc (1 + r⁻¹) * (r * (1 - r)⁻¹ + 1)
        = (1 + r⁻¹) * (r * (1 - r)⁻¹ + (1 - r) * (1 - r)⁻¹) : by rw [mul_inv_cancel h1r]
    ... = (1 + r⁻¹) * (1 - r)⁻¹ : congr_arg _ _
    ... = (1 + r⁻¹) * (r * r⁻¹) * (1 - r)⁻¹ : by rw [mul_inv_cancel hr0, mul_one]
    ... = ((1 + r⁻¹) * r) * (r⁻¹ * (1 - r)⁻¹) : by simp only [mul_assoc]
    ... = (r + 1) * (r * (1 - r))⁻¹ : _,
    { rw [← add_mul, add_comm, tsub_add_cancel_of_le, one_mul], exact fact.out _ },
    { rw [add_mul, one_mul, inv_mul_cancel, mul_inv],
      exact ne_of_gt (fact.out _) } },
  { intros c i, apply double_complex.col_ι_isometry, }
end

lemma col_exact [normed_with_aut r V] [fact (r < 1)]
  (d : ℝ≥0) [pseudo_normed_group.splittable (Λ →+ M) N d]
  (k : ℝ≥0) [fact (1 ≤ k)] (m : ℕ) (c₀ : ℝ≥0) (hdkc₀N : d ≤ (k - 1) * c₀ / N)
  (k' K' : ℝ≥0) [fact (1 ≤ k')] (hk' : k * k ≤ k')
  (hK' : (m + 2 + (r + 1) / (r * (1 - r)) * (m + 2)^2 : ℝ≥0) ≤ K')
  (c₁ c₂ : ℝ≥0) (_ : fact (c₀ ≤ r' * c₁)) (_ : fact (c₀ ≤ κ n * c₂)) (_ : fact (c₁ ≤ κ n * c₂)) :
  ((double_complex.{u} BD κ r r' V Λ M N).col n).is_weak_bounded_exact k' K' m c₂ :=
begin
  have key := col_exact' BD κ r r' V Λ M N n d k m c₀ hdkc₀N k' K' hk' hK' c₁ c₂,
  apply key.of_iso (double_complex.col_iso BD κ r r' V Λ M N n).symm,
  intros,
  apply double_complex.col_iso_inv_strict
end

end thm95

subset_name: curated


TITLE: Boundary value problem and eigenvalues (Sturm-Liouville)
QUESTION [0 upvotes]: I'm having problems doing this BVP eigenvalue problem, and would appreicate if someone can help me through the next step
(Question was:)
By setting $y=u/x$, find all eigenvalues and eigenfunctions of the Sturm-Liouville problem:
$$xy''+2y'+\lambda xy=0$$
for $x \in [\pi, 2\pi]$ with BV's of $y(\pi)=y(2\pi)=0$
So I managed the first step, doing $y=u/x$ I changed the ODE into:
$$u''+\lambda u=0$$
So then i'm supposed to find the lambda eigenvalues, but i'm having issues.
The only examples i've ever seen involve $y''+\lambda y=0$ with BV's $y(0)=y(L)=0$ never with $y=u/x$ and $y(\pi)=y(2\pi)=0$
I understand that I need to try $\lambda > 0$, with general solution:
$$u= a\cos(\sqrt{\lambda}x)+b\sin(\sqrt{\lambda}x)$$
(therefore:)
$$y= a\cos(\sqrt{\lambda}x)+b\sin(\sqrt{\lambda}x)/x$$
But I don't know where to go from there, do I just sub the BV's $\pi$ and $2\pi$ in? I'm really confused. Any help would be greatly appriecated thanks.

REPLY [1 votes]: $\newcommand{\+}{^{\dagger}}%
 \newcommand{\angles}[1]{\left\langle #1 \right\rangle}%
 \newcommand{\braces}[1]{\left\lbrace #1 \right\rbrace}%
 \newcommand{\bracks}[1]{\left\lbrack #1 \right\rbrack}%
 \newcommand{\ceil}[1]{\,\left\lceil #1 \right\rceil\,}%
 \newcommand{\dd}{{\rm d}}%
 \newcommand{\ds}[1]{\displaystyle{#1}}%
 \newcommand{\equalby}[1]{{#1 \atop {= \atop \vphantom{\huge A}}}}%
 \newcommand{\expo}[1]{\,{\rm e}^{#1}\,}%
 \newcommand{\fermi}{\,{\rm f}}%
 \newcommand{\floor}[1]{\,\left\lfloor #1 \right\rfloor\,}%
 \newcommand{\half}{{1 \over 2}}%
 \newcommand{\ic}{{\rm i}}%
 \newcommand{\iff}{\Longleftrightarrow}
 \newcommand{\imp}{\Longrightarrow}%
 \newcommand{\isdiv}{\,\left.\right\vert\,}%
 \newcommand{\ket}[1]{\left\vert #1\right\rangle}%
 \newcommand{\ol}[1]{\overline{#1}}%
 \newcommand{\pars}[1]{\left( #1 \right)}%
 \newcommand{\partiald}[3][]{\frac{\partial^{#1} #2}{\partial #3^{#1}}}
 \newcommand{\pp}{{\cal P}}%
 \newcommand{\root}[2][]{\,\sqrt[#1]{\,#2\,}\,}%
 \newcommand{\sech}{\,{\rm sech}}%
 \newcommand{\sgn}{\,{\rm sgn}}%
 \newcommand{\totald}[3][]{\frac{{\rm d}^{#1} #2}{{\rm d} #3^{#1}}}
 \newcommand{\ul}[1]{\underline{#1}}%
 \newcommand{\verts}[1]{\left\vert\, #1 \,\right\vert}$
Write your solution as
$$
A\sin\pars{\root{\lambda}\bracks{x - {3\pi \over 2}}} + B\cos\pars{\root{\lambda}\bracks{x - {3\pi \over 2}}}
$$
We get
$$\left\lbrace%
\begin{array}{rcrcl}
-\sin\pars{\root{\lambda}\,{\pi \over 2}}A
& + &
\cos\pars{\root{\lambda}\,{\pi \over 2}}B & = & 0
\\[1mm]
\sin\pars{\root{\lambda}\,{\pi \over 2}}A
& + &
\cos\pars{\root{\lambda}\,{\pi \over 2}}B & = & 0
\end{array}\right.
$$
Eigenvalues are given by $\sin\pars{\root{\lambda}\pi} = 0\quad\imp\quad
\root{\lambda_{n}}\pi = n\pi$ where $n \in \mathbb{Z}$: $\lambda_{n} = n^{2}$.
\begin{align}
&\left\lbrace%
\begin{array}{rcl}
\mbox{Eigenfunction} & \propto & \sin\pars{2n\bracks{x - {3\pi \over 2}}}
\propto \sin\pars{2nx}
\\
\mbox{Eigenvalue}: && 4n^{2}\,,\quad n \in \mathbb{Z}
\end{array}\right.
\\[3mm]
&\left\lbrace%
\begin{array}{rcl}
\mbox{Eigenfunction} & \propto &
\cos\pars{\bracks{2n + 1}\bracks{x - {3\pi \over 2}}}
\propto \sin\pars{\bracks{2n + 1}x}
\\
\mbox{Eigenvalue}: && \pars{2n + 1}^{2}\,,\quad n \in \mathbb{Z}
\end{array}\right.
\end{align}


TITLE: $a+b=21$ and $\frac{1}{a}+\frac{1}{b} =\frac{7}{18} $. What is $ab$?
QUESTION [0 upvotes]: $ab$ is:
A. $18$
B. $36$
C. $54$
D. $72$
E. $90$
Would like to know if there is a way other than testing out each option to get the answer.

REPLY [1 votes]: Just from a style point of view, I prefer to avoid fractions until the very end, so I'll just multiply both sides of the 2nd equation by $18ab$.
$$\begin{align}
\frac{1}{a}+\frac{1}{b} &= \frac{7}{18}\\
18ab\bigg(\frac{1}{a}+\frac{1}{b}\bigg) &= 18ab\bigg(\frac{7}{18}\bigg)\\
\frac{18ab}{a}+\frac{18ab}{b} &= \frac{7\cdot18ab}{18}\\
18b+18a &=7ab\\
7ab &= 18(\color{green}{a+b)}\\
7ab &= 18\cdot \color{green}{21}\\
ab & = \frac{18\cdot 21}{7} = \frac{18\cdot 3 \cdot 7}{7} = 18\cdot 3 = 54
\end{align}$$


TITLE: Best program for 3D plotting
QUESTION [2 upvotes]: I've hit a roadblock with pgfplots where it has difficulty plotting multiple functions at the same time in 3D. As it states in the manual on page 114, "it cannot combine different \addplot commands, those will be drawn in the order of appearance." So something that should be behind another object might not be if you plot it last.
Does this same roadblock occur in gnuplot and Asymptote? I'd prefer to stay open source, but will move to Mathematica or Maple if I have to. And the quality/prettiness of the graphics is important to me, which is one reason I wanted pgfplots to work!

REPLY [0 votes]: Just thought I would mention for those with less money and/or more programming knowledge, Python has matplotlib, which is quite similar to matlab's plotting capability (except free and more flexible to use). There is also plotly.
R also has 3d plotting capability (e.g. see here). The "free Matlab" Octave is also an option.
Finally, for complicated, huge functions that are moving in time (i.e. animating evolving surfaces, large meshes, or vector fields of data in the, say, millions of points), which one wishes to look at (rotate, translate, zoom) as it moves, very few tools can cope. The only solution I have found is to write my own OpenGL visualizers in these cases. Pretty much every language has bindings for this and performance will never be an issue again :)


text:
\section{Defining the invariant}
\label{sec:DefTheta}

The aim of this section is to spell out the details that go into the
definition of the invariant $\theta$ sketched in
Section~\ref{sec:Introduction}, and, indeed to prove that its value
depends only on the topology of the Heegaard decomposition of the
three-manifold. We complete the proof of Theorem~\ref{thm:WellDefined}
in Section~\ref{sec:Splicing}, where we prove, among other things,
that $\theta$ remains invariant under stabilization.

Fix an oriented three-manifold $Y$ whose first Betti number
$b_1(Y)>0$. The definition of the invariant makes reference to a
genus $g$ Heegaard decomposition of $Y=U_0\cup_{\Sigma}U_1$; so we
discuss some objects naturally associated to such a decomposition.

We give first a convenient definition of the Jacobian of an oriented
$2$-manifold $\Sigma$ of genus $g$, endowed with a Riemannian metric
$\met$. Fix a Hermitian line bundle $E$ over $\Sigma$ whose Euler
number is $g-1$. A Hermitian connection $A$ over $E$ is said to have
{\em normalized curvature form} if its curvature form satisfies $$F_A
=
\OneHalf F_{K(\met)},$$ where $K(\met)$ is the Levi-Civita connection on the
canonical bundle for the metric $\met$.  Then the Jacobian $\Jac_\met$
is the space of Hermitian connections $A$ with normalized curvature
form, modulo the gauge group of circle-valued functions
$\Maps(\Sigma,S^1)$.  The group $H^1(\Sigma;\R)$ acts simply
transitively on $\Jac_\met$, with stabilizer $H^1(\Sigma;\Z)$ and so a
point in $\Jac_\met$ gives an identification of $\Jac_\met$ with the
$2g$-dimensional torus $$\Jac_\met\cong
\frac{H^1(\Sigma;\R)}{H^1(\Sigma;\Z)}=H^1(\Sigma;S^1).$$
Moreover, a spin structure on $\Sigma$ naturally gives rise to a point
in $\Jac_\met$, and hence an identification $$\Jac_\met\cong
H^1(\Sigma;S^1).$$ When it is clear from the context, we drop the
metric $\met$ from the notation for the Jacobian.

We will typically work in a certain cover of the Jacobian which is
associated to the Heegaard decomposition. Specifically, the long exact
sequence in cohomology for the decomposition induces a (surjective)
coboundary map $\delta\colon H^1(\Sigma;\Z)\longrightarrow H^2(Y;\Z)$,
whose kernel we denote by $\OurG$ (alternatively, this is the subgroup
of $H^1(\Sigma;\Z)$ generated by the image of $H^1(U_0;\Z)\oplus
H^1(U_1;\Z)$ under the obvious inclusion map).  We find it convenient,
then, to consider the cover $\OurJac$ of $\Jac$, the space of
connections in $E$ with normalized curvature form, modulo the action
by gauge transformations in the kernel of the composite $$\begin{CD}
\Maps(\Sigma;S^1)@>>> H^1(\Sigma;\Z) @>{\delta}>> H^2(Y;\Z)
\end{CD}
$$ The space $\OurJac$ inherits a natural action of $H^1(\Sigma;\R)$,
and the action of $H^1(\Sigma;\Z)$ on $\OurJac$ descends to a free
action of $$\frac{H^1(\Sigma;\Z)}{\OurG}\cong H^2(Y;\Z)$$ on
$\OurJac$, whose quotient is canonically identified with $\Jac$.  The
condition that $b_1(Y)>0$ is equivalent to the condition that
$\OurJac$ is a non-compact space.

Given a metric $\met$, there is an ``Abel-Jacobi map''
$$\Theta_\met\colon \Sym^{g-1}(\Sigma)\longrightarrow
\Jac_\met,$$
where $\Sym^{g-1}(\Sigma)$ is the space of effective degree $g-1$
divisors on $\Sigma$, i.e. $g-1$-fold symmetric power of $\Sigma$
(note that our conventions are slightly different from those typical
in Riemann surface theory, where the Jacobian is often thought of as
the group of complex structures on a topologically trivial line
bundle, rather than the positive spinor bundle).  Given a divisor
$D\in
\Sym^{g-1}(\Sigma)$, the corresponding connection $\Theta_\met(D)$ is
characterized by its curvature form (half that of the canonical bundle
with metric $\met$) and its associated $\DBar$-operator, which we
require to admit a holomorphic section which vanishes exactly at
$D$. The image of this map in $\Jac$ is called the {\em theta
divisor}. Once, again, we find it convenient to work in a lift
$\OurSym$ of $\Sym^{g-1}(\Sigma)$. This lift corresponds to the
subgroup of $\pi_1(\Sym^{g-1}(\Sigma))$ which is the kernel of the
composite $$\begin{CD}
\pi_1(\Sym^{g-1}(\Sigma))@>>>
H_1(\Sym^{g-1}(\Sigma))@>{(\Theta_\met)_*}>>
H_1(\Jac)\cong H^1(\Sigma;\Z) @>{\delta}>> H^2(Y;\Z),
\end{CD}
$$ where the first map is the Hurewicz homomorphism. Clearly,
$(\Theta_{\met})_*$ is independent of the Riemannian metric.  Thus, we
have a map $$\OurTheta_\met\colon \OurSym\longrightarrow \OurJac$$
which fits into a commutative diagram $$\begin{CD}
\OurSym @>{\OurTheta_\met}>> \OurJac \\
@VVV  @VVV \\
\Sym^{g-1}(\Sigma) @>{\Theta_\met}>> \Jac.
\end{CD}
$$

Note that standard Hodge theory gives an identification between the
Jacobian and the theta divisor given here with the definitions used in
the introduction.

Fix a handlebody $U$ which bounds $\Sigma$, and view the group
$H^1(U;\R)$ as a subgroup of $H^1(\Sigma;\R)$ using the natural
inclusion.  There is a natural quotient map
$$\Quot_U\colon\Jac\longrightarrow
\frac{H^1(\Sigma;S^1)}{H^1(U;S^1)}\cong H^2(U,\Sigma;S^1),$$
given as follows. Fix
a $\Spin$ structure $\spin_0$ on $U$, and let $p\in\Jac$ be the
induced point in the Jacobian. Given any $B\in\Jac$, there is a unique
$a\in H^1(\Sigma;S^1)$ so that $B=p+a$; we define $\Quot_U(B)$ to be
$a$ (modulo $H^1(U;S^1)$). This coset is independent of the spin
structure on $U$ since any two spin structures on $U$ differ by a
translation by a cohomology class coming from $H^1(U;S^1)$. The torus
$\Lag(U)$ defined in the introduction, then, is the preimage
$\Quot_U^{-1}(0)$.  Given a point $B\in\Jac$ and a homology class
$[\gamma]\in H_1(\Sigma;\Z)$ which bounds in $U$ there is a
well-defined holonomy, $\Hol_{\gamma}(B)\in S^1$, which is the
Kronecker pairing of $\Quot_U(B)$ with $[\gamma]$.

For a Heegaard decomposition of $Y$, let $\Lag_0$ and $\Lag_1$ denote
the associated tori $\Lag(U_0)$ and $\Lag(U_1)$ in $\Jac$.  A $\SpinC$
structure $\spinc$ on $Y$ gives rise to a pair of $g$-dimensional tori
$L_0(\spinc)$ and $L_1(\spinc)$ in $\OurJac$, up to simultaneous
translation by $H^2(Y;\Z)$, as follows. Let $\spin_0$ be a spin
structure on $Y$ and let $p$, $L_0$ and $L_1$ be as above.  Any
$\SpinC$ structure $\spinc$ on $Y$ can be written as $\spin_0+\ell$,
where $\ell\in H^2(Y;\Z)$.  Let ${\widetilde p}$ be any lift of $p$ to
$\OurJac$. Then, $L_0(\spinc)$ is the lift of $\Lag_0$ to $\OurJac$
which passes through ${\widetilde p}$, and $L_1(\spinc)$ is the lift
of $\Lag_1$ which passes through ${\widetilde p}+\ell$ (the translate
of ${\widetilde p}$ by the natural action of $H^2(Y;\Z)$ on
$\OurJac$).  Once again, it is easy to see that the subspaces are
independent of the spin structure $\spin_0$.  Since the intersection
in $H^1(\Sigma;\R)$ of the image of $H^1(U_0;\R)$ with $\OurG$ is
$H^1(U_0;\Z)$, it follows that $L_0(\spinc)$, and similarly
$L_1(\spinc)$, are both $g$-dimensional tori embedded in $\OurJac$.  A
{\em torsion $\SpinC$ structure} is a $\SpinC$ structure whose
associated real cohomology class ${\underline\spinc}=0$ (this is
equivalent to the condition that its first Chern class is torsion).
Note that $\spinc$ is torsion if and only if $L_0(\spinc)$ and
$L_1(\spinc)$ intersect. In fact, if $\spinc$ is torsion, then
$L_0(\spinc)\cap L_1(\spinc)$ is identified with $H^1(Y;\R)/H^1(Y;\Z)$.

Having introduced the basic topological objects associated to a Heegaard
decomposition, we must flesh out the notion of allowable metrics
used in the definition of the invariant $\theta$. The definition
corresponds to degenerations of the metric on $\Sigma$. We describe
these presently.

Let $\{\gamma_1,...,\gamma_{\NumCurves}\}$ be a collection of disjoint
simple, closed curves in $\Sigma$. Choose a tubular neighborhood $\nu$
of $\coprod_{i=1}^g\gamma_i$, and let $\met$ be a metric which extends
the product metric over $\nu$ arising naturally from an identification
$$\nu\cong
\coprod_{i=1}^g [-1,1]\times S^1.$$ Such a metric will be called {\em
product-like near the $\gamma_i$}. Given such a metric, let
$\met(T_1,...,T_{\NumCurves})$ denote the metric
obtained by inserting a tube of length $2T_i$ around the curve
$\gamma_i$, i.e. $\met(T_1,...,T_\NumCurves)$ is obtained by attaching
$$\coprod_{i=1}^g [-T_i,T_i]\times S^1$$ to $(\Sigma-\nu,\met)$ in the
obvious manner. The following lemma, whose proof is given in
Section~\ref{sec:MoveTheta}, describes what happens to the theta
divisor as the metric is stretched normal to curves in this way.

\begin{lemma}
\label{lemma:MissTheta}
Let $U$ be a handlebody with boundary $\Sigma$, and let
$\{\gamma_1,...,\gamma_g\}$ be a complete set of attaching circles for
$U$. Then, for any compact set of metrics ${\mathcal H}$ on $\Sigma$
which are product-like near the $\gamma_i$, as the metrics are
stretched out normal to the $\gamma_i$, the theta divisor converges as
a point set, into $$\Hol_{\gamma_1}^{-1}(\OneHalf)\cup ... \cup
\Hol_{\gamma_g}^{-1}(\OneHalf);$$
i.e. given any $\epsilon$, there is a $T_0$ so that for all metrics
$h\in{\mathcal H}$, and for all $g$-tuples $(T_1,...,T_g)$ for which each
$T_i>T_0$, we have that $$
\Theta_{\met(T_1,...,T_g)}(\Sym^{g-1}(\Sigma))
\subset \bigcup_{i=1}^g \Hol_{\gamma_i}^{-1}
(\OneHalf-\epsilon, \OneHalf + \epsilon).$$
\end{lemma}

Note that $L(U)$ could be described as the set of points
$B\in\Jac(\Sigma)$ with $\Hol_{\gamma_i}B=0$ for all $i$.
Thus, the above lemma says that for all metrics which are sufficiently
stretched out normal to all the $\gamma_i$, the theta divisor misses the
torus $L(U)$.  Indeed, it allows us to identify a special
(path-connected) class of metrics.

\begin{defn}
\label{def:CurveAllowable}
Let $U$ be a handlebody, and let $\{\gamma_1,...,\gamma_g\}$ be a complete
set of attaching circles for $U$. Fix a metric $\metk_0$
on $\Sigma$ which is sufficiently stretched out normal to the
$\{\gamma_i\}$ according to Lemma~\ref{lemma:MissTheta}. Another
metric $\metk_1$ on $\Sigma$ is called {\em allowable for
$\{\gamma_1,...,\gamma_g\}$}, or simply
$\{\gamma_1,...,\gamma_g\}$-allowable if there is a path $\metk_t$
connecting $\metk_0$ to $\metk_1$, so that
$$\Theta_{\metk_t}(\Sym^{g-1}(\Sigma))\cap L(U)=\emptyset$$
\end{defn}

In fact, Lemma~\ref{lemma:MissTheta} shows that the notion of
allowable is independent of the fixed metric $\metk_0$.  It appears,
however, to depend on the choice of the
$\{\gamma_1,...,\gamma_g\}$. The following proposition shows that this
is not the case: the notion of allowable depends only on the
handlebody $U$:

\begin{prop}
\label{prop:AllowableIsOK}
The class of allowable metrics depends only on the handlebody $U$;
i.e. if $\{\gamma_1,...,\gamma_g\}$ and $\{\gamma_1',...,\gamma_g'\}$
are any two complete sets of attaching circles for $U$, then a metric
is $\{\gamma_1,...,\gamma_g\}$-allowable if and only if it is
$\{\gamma_1',...,\gamma_g'\}$-allowable.
\end{prop}

The proof relies on the following lemma, whose proof is given in
Section~\ref{sec:MoveTheta}.

\begin{lemma}
\label{lemma:MissThetaHS}
Let $U$ be a handlebody with boundary $\Sigma$, and  let
$\{\gamma_1,...,\gamma_g\}$ be a complete set of attaching circles for
$U$. Then, for any compact set of metrics
${\mathcal H}$ on $\Sigma$ which are product-like near the $\gamma_i$
for $i=1,...,g-1$, given any $\epsilon>0$, there is a $T_0$ so that
for all $g-1$ tuples $(T_1,...,T_{g-1})$ with $T_i\geq T_0$ for all
$i$, and all metrics $\met\in{\mathcal H}$, we have that
$$\Theta^{-1}_{\met(T_1,...,T_{g-1})}(\Hol_{\gamma_1}^{-1}(0)\cap...\cap
\Hol_{\gamma_{g-1}}^{-1}(0))\subset \Hol_{\gamma_g}^{-1}(\OneHalf-\epsilon,\OneHalf+\epsilon).$$
\end{lemma}

The above lemma implies the following corollary:

\begin{cor}
\label{cor:OneCurveAtATime}
Let $\Sigma$, $\{\gamma_1,...,\gamma_g\}$, and $U$ be as in
Lemma~\ref{lemma:MissTheta}. For any  metric $\met$ which is
product-like around $\{\gamma_1,...,\gamma_{g-1}\}$, there is a constant
$T_0$ so that for all collections $T_i\geq T_0$, the metric
$\met(T_1,...,T_{g-1})$ is $\{\gamma_1,...,\gamma_g\}$-allowable.
\end{cor}

\begin{proof}
Fix an initial metric $\metk$ which is product-like along all
$\{\gamma_1,...,\gamma_g\}$, and which agrees with $\met$ away from a
tubular neighborhood of $\gamma_g$. Lemma~\ref{lemma:MissTheta} gives
us a constant $C_0$ so that for all $g$-tuples $(T_1,...,T_g)$ with
$T_i\geq C_0$, $\metk(T_1,...,T_g)$ is allowable.  We can view the
metric $$\met_t(T_1,...,T_{g-1}) = t
\met(T_1,...,T_{g-1}) + (1-t)
\metk(T_1,...,T_{g-1},C_0)$$ as the result of inserting
tubes with
parameters $T_1,...,T_{g-1}$ into a one-parameter (compact) family of
metrics away from the $\{\gamma_1,...,\gamma_{g-1}\}$. Thus,
Lemma~\ref{lemma:MissThetaHS} gives us a number $C_1$ with the
property that if all $T_i\geq C_1$, then for all metrics in the path
$\met_t(T_1,...,T_{g-1})$, the theta divisor misses $L(U)$. Hence,
if $T_1,...,T_{g-1} \geq\max(C_0,C_1)$, then
$\met(T_1,...,T_{g-1})$ is a $\{\gamma_1,...,\gamma_g\}$-allowable
metric.
\end{proof}

Proposition~\ref{prop:AllowableIsOK}, then, follows easily:

\vskip0.3cm
\noindent{\bf{Proof of Proposition~\ref{prop:AllowableIsOK}.}}
Fix $U$, and let $\{\gamma_1,...,\gamma_g\}$,
$\{\gamma_1',...,\gamma_g'\}$ be two complete sets of attaching
circles.  By standard Kirby calculus~\cite{KirbyCalc}, we see that it is
always possible to move between any two collections
$\{\gamma_1,...,\gamma_g\}$ and $\{\gamma_1',...,\gamma_g'\}$, through
a sequence of handle-slides.  Since a handle-slide fixes $g-1$ of the
curves, Corollary~\ref{cor:OneCurveAtATime} shows that the notion of
allowable remains unchanged.
\qed
\vspace{0.2in}

Proposition~\ref{prop:AllowableIsOK} allows us to refine the earlier
definition of allowable metrics:

\begin{defn}
\label{def:Allowable}
Let $U$ be a handlebody. A metric $\metk$ on $U$ is called {\em
$U$-allowable} provided that there is a complete set of attaching circles
$\{\gamma_1,...,\gamma_g\}$ for which the metric is allowable.
\end{defn}

With this background in place, we now give a definition of
$\theta(\spinc)$, where $\spinc\in\SpinC(Y)$.
Fix a smooth path of metrics $\{\met_t\}_{t\in[0,1]}$ for which $\met_0$ is $U_0$-allowable,
and $\met_1$ is $U_1$-allowable.
Consider the smooth map
$$\ParTheta\colon \Sym^{g-1}(\Sigma)\times\{(s,t)\in [0,1]\times[0,1] \big|
s\leq t\}\longrightarrow \frac{H^1(\Sigma;S^1)}{H^1(U_0;S^1)}
\times
\frac{H^1(\Sigma;S^1)}{H^1(U_1;S^1)}=\Targ,$$ defined by
$$\ParTheta(D,s,t)=\Quot_0(\Theta_{\met_s}(D))\times
\Quot_1(\Theta_{\met_t}(D)),$$ where $\Quot_i$ denotes the quotient map $\Quot_{U_i}$ for $i=0,1$,
and let $M_{\eta_0\times \eta_1}$ denote the pre-image under
$\ParTheta$ of the point $\eta_0\times \eta_1 \in
\Targ$.
By Sard's theorem, for generic $\eta_0\times\eta_1$, this fiber is a
compact, oriented zero-dimensional manifold which misses the locus of
points $(D,s,t)$ where $s=t$.  Moreover, the points in
$M_{\eta_0\times\eta_1}$ can naturally be partitioned into subsets
indexed by the various $\SpinC$ structures on $Y$. Specifically, for a
choice of $\SpinC$ structure on $Y$ and corresponding lifts
$\Lag_i(\spinc)$ of $\Lag_i$ (for $i=0,1$), there is a subset of
$M_{\eta_0\times\eta_1}$, denoted $M_{\eta_0\times\eta_1}(\spinc)$,
corresponding to points $$\{(D,s,t)\in\OurSym\times[0,1]\times[0,1]
\big| \OurTheta_{\met_s}(D)\in \Lag_0(\spinc)+\eta_0, \OurTheta_{\met_t}(D)\in
\Lag_1(\spinc)+\eta_1, s\leq t\}$$ (where, in the above expression, $L_i(\spinc)+\eta_i$ denotes
the translate of the subset $L_i(\spinc)$ by $\eta_i$). Then,
$\theta_{\eta_0\times\eta_1}(\spinc)$ is defined to be the signed
number of points in this subset.  In the next two propositions, we
shall see that (given $\met_t$) there is an open neighborhood
$\NdZero$ of zero in $\Targ$ with the property that
$\theta_{\eta_0\times\eta_1}$ is independent of the particular
(generic) choice of $\eta_0\times\eta_1\in \NdZero$. This is
technically somewhat easier when $b_1(Y)>1$, so we consider that case
first. But before we do that, we pause for a moment to discuss signs.

Since $\Sym^{g-1}(\Sigma)\times[0,1]\times[0,1]$ is naturally
oriented, the sign of $\theta$ is determined by an orientation for the
torus $$\frac{H^1(\Sigma;S^1)}{H^1(U_0;S^1)} \times
\frac{H^1(\Sigma;S^1)}{H^1(U_1;S^1)},$$ which in turn is determined by
an ordering of the attaching circles $\{\alpha_1,...,\alpha_g\}$ and
$\{\beta_1,...,\beta_g\}$. We use an ordering for these attaching
circles which is consistent with the orientation of $H_*(Y)$, arising
from Poincar\'e duality, in the following sense.  We explain what this consistence means. The
Heegaard decomposition gives a chain complex for $Y$ with one
zero-cell, $g$ one-cells in one-to-one correspondence with the circles
$\{\alpha_i\}$, $g$ two-cells which correspond to the $\{\beta_i\}$,
and one three-cell.  In general, an orientation for a (finite
dimensional) chain complex is canonically equivalent to an orientation
for its real homology, since there is a splitting: $$\bigoplus_i C_i =
\bigoplus_i \left((\partial B_{i+1})\oplus H_i
\oplus B_i\right),$$ where $B_i\subset C_i$ is a vector space which is
mapped isomorphically under the boundary homomorphism to the group of
boundaries in $C_{i-1}$, which givesa natural identification of
$$\bigoplus_i C_i = \left(\bigoplus_i H_i\right)
\oplus \left(\bigoplus_i
B_i \oplus (\partial B_i) \right)$$ as oriented vector spaces; and the
vector space $\bigoplus_i (B_i \oplus (\partial B_i))$ is canonically
oriented as follows: if $\{b_j\}$ is a basis for $\bigoplus_i B_i$, we
declare that $$\bigoplus_j (b_j \oplus \partial b_j)$$ is a positive
oriented basis for $\bigoplus_i (B_i \oplus (\partial B_i))$.  The
orientation on $Y$ gives a canonical orientation of $H_0=C_0$,
$H_3=C_3$. Thus, in light of the above remarks, the orientation of
$H_*(Y)$ induces an orientation of $C_1\oplus C_2$, and hence an
ordering of the attaching circles.

Having nailed down the sign, we state the result we have been aiming
for, first in the case where $b_1(Y)>1$.

\begin{prop}
\label{prop:IndepOfMetBig}
When $b_1(Y)>1$, the invariant $\theta(\spinc)$ depends only on the
Heegaard decomposition of $Y$; i.e. it is independent of the metrics
and perturbations used. More precisely, given any one-parameter family
$\met_t$ of metrics which connect a $U_0$-allowable metric to a
$U_1$-allowable metric, there is an open neighborhood $\NdZero$ of
$0\in\Targ$ and an integer $\theta_{\met_t}(\spinc)$ with the
property that for all generic $\eta_0\times\eta_1\in \NdZero$, we have
that
$$\theta_{\met_t,\eta_0\times\eta_1}(\spinc)=\theta_{\met_t}(\spinc).$$
Moreover, if $\met_t'$ is another path of metrics connecting a
$U_0$-allowable metric with a $U_1$-allowable metric, then
$$\theta_{\met_t}(\spinc)=\theta_{\met_t'}(\spinc).$$
\end{prop}

\begin{proof}
According to Sard's theorem, for any generic
$\eta_0\times\eta_1\in\Targ$, the fiber
$$M_{\met_t,\eta_0\times\eta_1}=
\{(s,t,D)\big| \Theta_{\met_s}(D)\in \Lag_0 + \eta_0,
\Theta_{\met_t}(D)\in \Lag_1 + \eta_1, s\leq t\}$$
is a compact, canonically oriented,
zero-dimensional manifold. We investigate the conditions necessary to
show that the fiber misses the boundary of the domain of $\ParTheta$.

The set of points $\eta_0\times\eta_1\in\Targ$ for which the fiber
$M_{\met_t,\eta_0\times\eta_1}$ does not contain boundary points of
the form $(s,1,D)$ or $(0,t,D)$ is an open set which contains $0$
(since $\met_i$ is $U_i$-allowable for $i=0,1$). Let $\NdZero$ be a
connected neighborhood of $0$ in this set. Moreover, the fiber
$M_{\met_t,\eta_0\times\eta_1}$ cannot contain points of the form
$(t,t,D)$ if the spaces $\Lag_0+\eta_0$ and $\Lag_1+\eta_1$ are
disjoint; but $(\Lag_0+\eta_0)\cap (\Lag_1+\eta_1)\neq \emptyset$ is
equivalent to the condition that the image of $\delta(\eta_0-\eta_1)=0
\in H^2(Y;S^1)$. This is a codimension $b_1(Y)$ sub-torus
${\Wall}$ of $\Targ$, so its complement is dense.

Thus, for a dense set of perturbations $\eta_0\times\eta_1\in
\NdZero$, the fiber $M_{\eta_0\times\eta_1}$ is a smooth submanifold
which misses the boundary of the domain of $\ParTheta$. Moreover, given
two generic perturbations $\eta_0\times\eta_1, \eta_0'\times\eta_1'\in
\NdZero$, a generic path in $\NdZero$ misses the locus ${\Wall}$ as
well, since it has codimension $b_1(Y)>1$ (this is what distinguishes
the case where $b_1(Y)>1$ from the case $b_1(Y)=1$).  By Sard's
theorem, then, a generic such path induces a compact cobordism between
$M_{\eta_0\times\eta_1}$ and $M_{\eta_0'\times\eta_1'}$. By lifting to
the covering space $\OurSym$, one can easily see that the cobordism
respects the partitioning into $\SpinC$ structures. Thus, $\NdZero$
has the required property.

Fix $\met_t$ and $\met_t'$. Since the space of $U$-allowable metrics
is path connected and the space of metrics over $\Sigma$ is
simply-connected, we can connect $\met_t$ and $\met_t'$ by a
two-parameter family of metrics with $\metk_{t,0}=\met_t$,
$\metk_{t,1}=\met_t'$, $\metk_{0,t}$ is $U_0$-allowable and
$\metk_{1,t}$ is $U_1$-allowable. This, together with a small generic
perturbation, gives rise to a cobordism between
$M_{\eta_0\times\eta_1,\met_t}$ and $M_{\eta_0'\times\eta_1',\met_t'}$
(which once again respects the partitioning into $\SpinC$ structures).
This completes the proof of the proposition.
\end{proof}

The invariance statement in Proposition~\ref{prop:IndepOfMetBig} holds
when $b_1(Y)=1$ as well, but the argument is more involved. The point
is that ${\Wall}$ now separates $G$ into two components. The above
proof shows that if we pick two paths of metrics and two perturbations in
the same component, then the invariant remains unchanged. So, from now
on, we can drop the path $\met_t$ from the notation for $\theta$. We
must show, then, that the invariant is actually independent of the
component. It will be convenient to make use of the involution on the
set of $\SpinC$ structures introduced in
Section~\ref{sec:Introduction}, $\spinc\mapsto{\overline\spinc}$. This
is the map which sends the complex spinor bundle $W$ of $\spinc$ to
the same underlying real bundle, given its conjugate complex structure
(and naturally induced Clifford action). Note that this action fixes
those $\SpinC$ structures which arise from $\Spin$ structures, and
moreover $\Conj{\spinc+\ell}=\Conj{\spinc}-\ell$, for any
$\spinc\in\SpinC(Y)$ and $\ell\in H^2(Y;\Z)$. The invariant is
preserved by this involution in the following sense:

\begin{lemma}
\label{lemma:Involution}
Let $Y$ be an oriented three-manifold with $b_1(Y)>0$. Then,
$$\theta_{\eta_0\times \eta_1}(\spinc)=\theta_{-\eta_0\times
-\eta_1}({\overline \spinc})$$
\end{lemma}

\begin{proof}
To see this, we make use of the Serre duality map. Serre duality gives
rise to a natural involution on $\Jac$, with the property that
$\Conj{q+x}=\Conj{q}-x$ for any $q\in\Jac$ and $x\in
H^1(\Sigma;\R)$. For any given metric $\met_t$, this involution
preserves the theta divisor (by Serre duality), and fixes the points
associated to spin structures.  The involution on $\Jac$ can be lifted
to an involution of $\OurJac$ which we can assume fixes
$\Lag_0(\spinc)$. The involution then carries $\Lag_1(\spinc)$ to
$\Lag_1({\overline \spinc})$. Unfortunately, this involution is not
defined on the symmetric product.  Instead, it gives an involution on
the set of points in the symmetric product which map injectively to
the theta divisor, and more generally, it gives a relation. We write
$D_1\sim_{h}D_2$ if $\Theta_{h}(D_1)=\Conj{\Theta_{h}(D_2)}$.

For any $y\in[0,1]$, let $M_y$ denote the moduli space
$$M_y=\left\{(D,s,t)\Bigg|
\begin{array}l
s\leq t, \\
\exists D', D'' \in \Sym^{g-1}(\Sigma),
D'\sim_{h_s} D, D'' \sim_{h_x} D, \\
\Theta_{h_s}(D')\in \Lag_0+\eta_0, \\
\Theta_{h_t}(D'')\in \Lag_1+\eta_1,
\end{array} \right\}, $$
where $x=s+y(t-s)$.  For generic $\eta_0$, $\eta_1$, $\met_t$, $M_y$
is a smooth cobordism from $M_0$ to $M_1$. This follows from the fact
that the set of points in $\Sym^{g-1}(\Sigma)$ which do not map
injectively into the theta divisor is empty if $g=2$ and has complex
codimension $2$ for generic $h$ if $g>2$
(see p. 250 of~\cite{ArbCornalGriffHar}).
As before, $M_y$ can be
partitioned according to $\SpinC$ structures; let $M_y(\spinc)$ denote
the corresponding set. The same dimesnion counting also shows that
for generic $\met_t$, $\eta_0$, and $\eta_1$,
\begin{eqnarray*}
M_0(\spinc)=M_{\met_t,\eta_0\times \eta_1}(\spinc)
&{\text{and}}&
M_1(\spinc)=M_{\met_t,-\eta_0\times -\eta_1}({\overline\spinc}).
\end{eqnarray*}
This proves the lemma.
\end{proof}

If $Y$ is an integral homology $S^1\times S^2$, the invariance of
$\theta$ is an easy consequence of this lemma:

\begin{prop}
\label{prop:IndepOfMetOneZ}
If $Y$ is an integral homology $S^1\times S^2$, then the invariant
$\theta(\spinc)$ is independent of metrics and perturbations as well.
\end{prop}

\begin{proof}
If $\spinc$ is not a torsion
class, then $\Lag_0(\spinc)$ and $\Lag_1(\spinc)$ are disjoint, so the
proof of Proposition~\ref{prop:IndepOfMetBig} applies.

For the torsion $\SpinC$ structure $\spinc$ (i.e. the one corresponding to the
spin structure), there are {\em a priori} two invariants, depending on
the sign $\delta(\eta_0-\eta_1)$ for the perturbation $\eta_0\times
\eta_1$. But Lemma~\ref{lemma:Involution} guarantees that
$$\theta_{\eta_0\times \eta_1}(\spinc)=\theta_{-\eta_0\times
-\eta_1}({\overline \spinc});$$ and since $\spinc$ comes from the spin
structure, ${\overline\spinc}=\spinc$, while
$$\delta(\eta_0-\eta_1)=-\delta(-\eta_0-(-\eta_1)),$$ so
the invariants for both perturbations are equal.
\end{proof}

More generally, we have:

\begin{prop}
\label{prop:IndepOfMetOne}
If $Y$ is a rational homology $S^1\times S^2$, then the invariant
$\theta(\spinc)$ is independent of metrics and perturbations.
\end{prop}

This general case involves a study of spectral flow, and takes us
slightly out of the general framework of the preceding discussion (and
it is surprisingly more involved than the special case), so we
relegate that case to Section~\ref{sec:WallCross} (where it is
restated as Proposition~\ref{prop:IndepOfMetOneGen}).

Our final goal in this section is to prove
Proposition~\ref{prop:StandardProperties}.

\vskip0.3cm
\noindent{\bf{Proof of Proposition~\ref{prop:StandardProperties}}.}
The finiteness statement is clear from the fact that the fibers of
$\ParTheta$ are compact.

The statement about involution invariance follows from
Lemma~\ref{lemma:Involution}. When we reverse the orientation of $Y$,
then the corresponding orientation of $H^*(Y)$ changes by a factor of
$(-1)^{b_1+1}$, so the last statement follows from the discussion
preceding Proposition~\ref{prop:IndepOfMetBig}.
\qed
\vspace{0.2in}

In Section~\ref{sec:Splicing}, we establish the final step towards
proving topological invariance, showing that $\theta(\spinc)$ remains
invariant under stabilization. It must be shown that if one begins
with $\Sigma$, then the associated invariant agrees with the invariant
calculated from the Riemann surface obtained by a connected sum
$\Sigma\# (S^1\times S^1)$, using the handlebodies $U_0\# (D^2\times
S^1)$ and $U_1 \# (S^1\times D^2)$. This result fits naturally into
the context of a splicing construction, which also proves a technical
device which underpins the calculations of the invariants. We defer
these results to Section~\ref{sec:Splicing}, addressing first the
lemmas which we have stated thus far without proof.

config: arxiv


TITLE: Show that$ \sum_{k=0}^m \binom{m}{k}\frac{(-1)^k}{k+n+1}=\frac{n!\,m!}{(n+m+1)!}$
QUESTION [5 upvotes]: I want to show that
\begin{align}
&\sum_{k=0}^m \binom{m}{k}\frac{(-1)^k}{k+n+1}=\frac{n!\,m!}{(n+m+1)!}\\
\end{align}
I came across this when trying to prove
\begin{align} \int_0^1 (1-x)^m x^n dx =\frac{n!\,m!}{(n+m+1)!}\\
\end{align}
My teacher proved it by using the substitution $x=\sin^2 (t)$ and then using the Wallis formula but I tried to prove it by using Binomial Theorem and integrating each term and I got stuck at this step.

REPLY [0 votes]: There is the “Linear algebra” way. Let $E$ be the space of functions from $(0,\infty)$ to $\Bbb R$ and define the operator $S\colon f\mapsto Sf$ on $E$ by $$Sf(x):=f(x+1),\quad f\in E,\ x>0.$$
Let the difference operator $\Delta:=\mathrm{Id}_E-S$. Since
$\mathrm{Id}_E$ and $-S$ commute, the Binomial theorem gives you $\Delta^m$ for any integer $m\ge0$:
$$\Delta^m=\sum_{k=0}^m\binom mk(\mathrm{Id}_E)^{m-k}(-S)^k,$$
that is
$$\Delta^mf(x)=\sum_{k=0}^m\binom mk(-1)^kf(x+k).\tag{$\star$}$$
Now consider $f\in E$ given by $f(x):=\frac1x$. We can see that
\begin{align*}
\Delta f(x)&=\frac1x-\frac1{x+1}=\frac1{x(x+1)},\\[.4em]
\Delta^2f(x):=\Delta(\Delta f)(x)&=\frac1{x(x+1)}-\frac1{(x+1)(x+2)}=\frac2{x(x+1)(x+2)},
\end{align*}
and an immediate induction shows that
$$\Delta^m f(x)=\frac{m!}{x(x+1)\cdots(x+m)}.$$
Thus $(\star)$ reads
$$\frac{m!}{x(x+1)\cdots(x+m)}=\sum_{k=0}^m\binom mk(-1)^k\frac1{x+k}.$$
This is an identity between functions of the variable $x>0$ and it suffices to take $x:=n+1$ to establish your claim.


TITLE: Grouping vectors together
QUESTION [6 upvotes]: Given $n$ unit vectors in $\mathbb{R}^n$ s.t. $0 \leq u\cdot v<1$ for all pair of distinct vectors $u,v$. These vectors span a $d$-dimensional subspace s.t. $d< n$. We conjecture that it is possible to partition the $n$ vectors into $d$ groups such that all the vectors within the same group are pairwise non-orthogonal. It trivially holds when $d\in\{1,2,n-1,n-2\}$. However, we have not been able to show for general $d$. Does the conjecture hold for any $d< n$? If yes, how to prove it? Any thoughts/hints would be appreciated. Thanks in advance.

REPLY [5 votes]: Kahn--Kalai's counterexample to Borsuk's conjecture is a collection of vertices of the unit cube.
Imagine that this cube sits in a coordinate hyperplane $x_1=s$ of $\mathbb R^{n+1}$, so that the origin projects to the center of the cube.
Project this cube centrally to the unit sphere.
For a right choice of $s$, you get a counterexample to your statement.


TITLE: Number of ways a group of three boys and three girls can be formed from ten boys and five girls if two particular boys cannot be selected together
QUESTION [2 upvotes]: There are ten boys B1, B2, ...., B10 and five girls G1,
G2, ...., G5 in a class. Then the number of ways of
forming a group consisting of three boys and three
girls, if both B1 and B2 together should not be the
members of a group, is__________.
Official Ans. by NTA (1120)
DOUBT:
ATQ if we need both the boys out of group,
can't we just exclude them from group of boys and select from 8 boys and 5 girls?
Making 8c3*5c3 = 560 the answer ?

REPLY [3 votes]: Alternative approach:
$$\left[\binom{10}{3} \times \binom{5}{3}\right] - \left[\binom{8}{1} \times \binom{5}{3}\right] \tag1 $$
$$= [120 \times 10] - [8 \times 10] = 1120.$$
In (1) above, the first term represents the total number of ways of making the selections, without any regard for whether the two boys are selected together.
In (1) above, the second term represents the total number of ways of violating the constraint against the two boys being together, while making the selections.


TITLE: Does $\mathbb C\mathbb P^\infty$ have a group structure?
QUESTION [42 upvotes]: Does $\mathbb C\mathbb P^\infty$ have a (commutative) group structure? More specifically, is it homeomorphic to $FS^2$, (the connected component of) the free commutative group on $S^2$?
$\mathbb C\mathbb P^\infty$ is well known to have the homotopy type of the classifying space of a commutative group, $\mathbb C^\times$. One model for the classifying space is the bar construction, which is a functor from groups to spaces and is product preserving, so the classifying space of a commutative group is again a commutative group (since the group operation is a homomorphism iff the group is a commutative). The Dold-Thom theorem says that the component of the free commutative group on $S^n$ is a $K(\mathbb Z,n)$. So those are two fairly nice group models. But is either actually homeomorphic to the space we started with, $\mathbb C\mathbb P^\infty$?
By $\mathbb C\mathbb P^\infty$ I mean the colimit of the $\mathbb C\mathbb P^n$ under the closed inclusions. Similarly, I topologize the free commutative group on a space $X$ as the colimit of the inclusions of the subset of words of length $n$, which is topologized as a quotient of $(X\times\{\pm1\}\cup\{*\})^n$, that is, sequences of $n$ letters, each of which may be a generator, the inverse of a generator, or the identity element. So $\mathbb C\mathbb P^\infty$, $BS^1$, and $FS^2$ are CW complexes with finite skeleta. Are they all locally modeled on $\mathbb R^\infty$? Do such infinite dimensional manifolds have homeomorphism types determined by their homotopy types?
Appendix: Motivation
In the question, I invoked the Dold-Thom theorem to motivate the particular model $FS^2$ under consideration. But this case is easy and should motivate the general theorem, rather than vice versa. So I will suggest a proof. Moreover, I will motivate the choice of space, how we get from $\mathbb C\mathbb P^\infty$ to $FS^2=F\mathbb C\mathbb P^1$. We want to make a model for $B\mathbb C^\times$ that is as nice as possible. If we identify $\mathbb C^\infty=\mathbb C[x]$, it is a ring, so its multiplication makes $\mathbb C\mathbb P^\infty=\mathbb P(\mathbb C[x])$ into an topological monoid. That’s a pretty nice structure; it just lacks inverses. So we should consider $\mathbb P(\mathbb C(x))$. For any reasonable topology on $\mathbb C(x)$, the vector space is contractible, as is the complement of the origin; and the multiplication on the ring is continuous. Thus $\mathbb P(\mathbb C(x))$ is a topological monoid homotopy equivalent to $\mathbb C\mathbb P^\infty$. This is better than the previous model because every element has an inverse. However, the inversion map is continuous only for some topologies. For counterexample, the finest possible topology is given by making the topological vector space the colimit of its finite dimensional subspaces (a colimit indexed by an uncountable filtering poset). But then the inverse is not continuous: the copy of $\mathbb C$ given by $y\mapsto x-y$ has inverses a set of linearly independent vectors, thus discrete.
Turning away from topological vector spaces, how else can we put a topology on $P(\mathbb C(x))$? A polynomial is determined (up to scale) by its zeros and a rational function by its zeros and poles. Then we can think of $\mathbb P(\mathbb C[x])$ as something like the free commutative monoid on $S^2=\mathbb C\mathbb P^1$ (specifically, the free monoid modulo the point at infinity). Similarly, $\mathbb P(\mathbb C(x))$ is the component of the free commutative group on $\mathbb C\mathbb P^1$, that is, $F\mathbb C\mathbb P^1$. To put the zeros and poles on the same footing, we need the topology described from the beginning.

REPLY [19 votes]: I noticed that this question still has no accepted answer and all existing answers are rather long. It seems that the answer can be easily obtained using some results of infinite-dimensional topology, namely, the theory of manifolds modeled on the direct limit $\mathbb R^\infty$ of Euclidean spaces (see Chapter 5 of Sakai's book).
Two results of this theory will be important for our purposes:
Characterization Theorem 5.4.1. A topological space $X$ is is homeomorphic to an open subspace of $\mathbb R^\infty$ if and only if any embedding $f:B\to X$ of a closed subspace $B$ of a finite-dimensional compact metrizable space $A$ can be extended to an embedding $\bar f:A\to X$.
Classification Theorem 5.5.1. Two $\mathbb R^\infty$-manifolds are homeomorphic if and only if they are homotopically equivalent.
Now using the Characterization Theorem, it can be shown that $\mathbb{CP^\infty}$ is an $\mathbb R^\infty$-manifold.
Next, in his question Ben Wieland writes that $\mathbb{CP}^\infty$ is homotopically equivalent to the connected component $G_0$ of the free topological Abelian group $G$ over the sphere. Using the Characterization Theorem of Sakai once more, one can show (and this was done by Zarichnyi in 1982) that $G_0$ is an $\mathbb R^\infty$-manifold. Since $\mathbb{CP}^\infty$ and $G_0$ are two homotopically equivalent $\mathbb R^\infty$-manifolds, the Classification Theorem ensures that $\mathbb{CP}^\infty$ is homeomorphic to $G_0$ and hence has a compatible topogical group structure.