Skip to content

Commit

Permalink
clean up & simplify things a lot
Browse files Browse the repository at this point in the history
forked-from-1kasper committed Dec 26, 2023
1 parent f6903ab commit b11fafa
Showing 3 changed files with 72 additions and 100 deletions.
74 changes: 22 additions & 52 deletions GroundZero/Modal/Disc.lean
Original file line number Diff line number Diff line change
@@ -9,96 +9,66 @@ namespace GroundZero.HITs.Infinitesimal
universe u v w

-- infinitesimally close
hott def infinitesimallyClose {A : Type u} (a b : A) := ι a = ι b
hott definition infinitesimallyClose {A : Type u} (a b : A) := ι a = ι b
infix:80 " ~ " => infinitesimallyClose

hott def Disc {A : Type u} (a : A) := Σ b, a ~ b
hott definition Disc {A : Type u} (a : A) := Σ b, a ~ b
notation "𝔻" => Disc

hott def discBundle (A : Type u) := Σ (a : A), 𝔻 a
hott definition discBundle (A : Type u) := Σ (a : A), 𝔻 a
notation "T∞" => discBundle

hott def center {A : Type u} (a : A) : 𝔻 a := ⟨a, idp (ι a)⟩
hott definition center {A : Type u} (a : A) : 𝔻 a := ⟨a, idp (ι a)⟩

noncomputable section
section
variable {A : Type u} {B : Type v} (f : A → B)

hott def infProxAp {a b : A} : a ~ b → f a ~ f b :=
λ ρ, (Im.naturality f a)⁻¹ ⬝ Id.ap (Im.ap f) ρ ⬝ Im.naturality f b
hott definition infProxAp {a b : A} : a ~ b → f a ~ f b :=
λ ρ, Id.ap (Im.ap f) ρ

hott def d (x : A) : 𝔻 x → 𝔻 (f x) :=
hott definition d (x : A) : 𝔻 x → 𝔻 (f x) :=
λ ε, ⟨f ε.1, infProxAp f ε.2

hott def bundleAp : T∞ A → T∞ B :=
hott definition bundleAp : T∞ A → T∞ B :=
λ τ, ⟨f τ.1, d f τ.1 τ.2
end

noncomputable hott def infProxApIdp {A : Type u} {a b : A} (ρ : a ~ b) : infProxAp idfun ρ = ρ :=
hott lemma infProxApIdp {A : Type u} {a b : A} (ρ : a ~ b) : infProxAp idfun ρ = ρ :=
begin
symmetry; transitivity; symmetry; apply Equiv.idmap;
transitivity; apply mapWithHomotopy _ _ Im.apIdfun;
apply bimap (· ⬝ _ ⬝ ·); apply Im.indεβrule;
transitivity; apply Id.ap; apply Im.indεβrule; apply Id.invInv
transitivity; apply mapWithHomotopy; apply Im.apIdfun;
transitivity; apply Id.rid; apply Equiv.idmap
end

noncomputable hott def infProxApCom {A : Type u} {B : Type v} {C : Type w} (f : B → C) (g : A → B)
hott lemma infProxApCom {A : Type u} {B : Type v} {C : Type w} (f : B → C) (g : A → B)
{a b : A} (ρ : a ~ b) : infProxAp (f ∘ g) ρ = infProxAp f (infProxAp g ρ) :=
begin
transitivity; apply Id.ap (_ ⬝ · ⬝ _);
transitivity; apply mapWithHomotopy _ _ (Im.apCom _ _);
apply bimap; apply bimap; apply Im.indεβrule;
apply mapOverComp; apply Id.ap; apply Im.indεβrule;

transitivity; apply Id.ap (· ⬝ _); apply Id.assoc;
transitivity; apply Id.ap (· ⬝ _ ⬝ _); apply Id.assoc;
transitivity; symmetry; apply Id.assoc;

symmetry; transitivity; apply Id.ap (_ ⬝ · ⬝ _); transitivity;
apply mapFunctoriality; apply Id.ap (· ⬝ _); apply mapFunctoriality;

transitivity; apply Id.ap (_ ⬝ · ⬝ _); symmetry; apply Id.assoc;
transitivity; apply Id.ap (· ⬝ _); apply Id.assoc;
transitivity; symmetry; apply Id.assoc (_ ⬝ Id.ap _ _);
transitivity; apply Id.ap (_⁻¹ ⬝ _ ⬝ ·); symmetry; apply Id.assoc;
transitivity; apply Id.assoc (_⁻¹ ⬝ _);

apply bimap (· ⬝ _ ⬝ ·) <;> symmetry;
{ transitivity; apply Id.ap; symmetry; apply Id.assoc;
transitivity; apply Id.assoc; transitivity; apply Id.ap (· ⬝ _);
apply Id.invComp; reflexivity };
{ transitivity; apply Id.ap (· ⬝ _);
transitivity; apply Id.explodeInv; apply Id.ap; apply Id.explodeInv;
transitivity; apply Id.ap (· ⬝ _); apply Id.assoc;
transitivity; symmetry; apply Id.assoc;
transitivity; apply Id.ap; apply Id.invComp;
transitivity; apply Id.rid; apply bimap;
{ transitivity; apply Id.ap; apply Id.mapInv; apply Id.invInv };
{ apply Id.invInv } }
transitivity; apply mapWithHomotopy; apply Im.apCom;
transitivity; apply Id.rid; apply mapOverComp
end

noncomputable hott def diffComHom {A : Type u} {B : Type v} {C : Type w}
hott definition diffComHom {A : Type u} {B : Type v} {C : Type w}
(f : B → C) (g : A → B) {x : A} (ε : 𝔻 x) : d (f ∘ g) x ε = d f (g x) (d g x ε) :=
Id.ap (Sigma.mk _) (infProxApCom f g _)

hott def diffCom {A : Type u} {B : Type v} {C : Type w} (f : B → C) (g : A → B)
hott theorem diffCom {A : Type u} {B : Type v} {C : Type w} (f : B → C) (g : A → B)
{x : A} : d (f ∘ g) x = (d f) (g x) ∘ d g x :=
Theorems.funext (diffComHom f g)

noncomputable hott def diffIdfun {A : Type u} (x : A) (ε : 𝔻 x) : d idfun x ε = ε :=
hott lemma diffIdfun {A : Type u} (x : A) (ε : 𝔻 x) : d idfun x ε = ε :=
Id.ap (Sigma.mk _) (infProxApIdp _)

hott def isHomogeneous (A : Type u) :=
hott definition isHomogeneous (A : Type u) :=
Σ (e : A) (t : A → A ≃ A), Π x, t x e = x

hott def Homogeneous :=
hott definition Homogeneous :=
Σ (A : Type u), isHomogeneous A

noncomputable instance : Coe Homogeneous (Type u) := ⟨Sigma.fst⟩

hott def Homogeneous.trivial : Homogeneous :=
hott definition Homogeneous.trivial : Homogeneous :=
⟨𝟏, ★, λ _, ideqv 𝟏, λ ★, idp ★⟩

hott def Homogeneous.cart (A B : Homogeneous) : Homogeneous :=
hott definition Homogeneous.cart (A B : Homogeneous) : Homogeneous :=
⟨A.1 × B.1, ⟨(A.2.1, B.2.1), λ w, prodEquiv (A.2.2.1 w.1) (B.2.2.1 w.2),
λ w, Product.prod (A.2.2.2 w.1) (B.2.2.2 w.2)⟩⟩

20 changes: 10 additions & 10 deletions GroundZero/Modal/Etale.lean
Original file line number Diff line number Diff line change
@@ -8,22 +8,22 @@ open GroundZero.Proto
namespace GroundZero.HITs.Infinitesimal
universe u v w

noncomputable section
section
variable {A : Type u} {B : Type v} (f : A → B)

hott def naturalitySquare : hcommSquare A (ℑ A) B (ℑ B) :=
hott definition naturalitySquare : hcommSquare A (ℑ A) B (ℑ B) :=
⟨Im.ap f, ι, ι, f, Theorems.funext (Im.naturality f)⟩

hott def etale := (naturalitySquare f).isPullback
hott definition etale := (naturalitySquare f).isPullback
notation "étale" => etale
end

noncomputable section
hott def EtaleMap (A : Type u) (B : Type v) :=
section
hott definition EtaleMap (A : Type u) (B : Type v) :=
Σ (f : A → B), étale f
infixr:70 " ─ét→ " => EtaleMap

hott def SurjectiveEtaleMap (A : Type u) (B : Type v) :=
hott definition SurjectiveEtaleMap (A : Type u) (B : Type v) :=
Σ (f : A → B), étale f × surjective f
infixr:70 " ─ét↠ " => SurjectiveEtaleMap
end
@@ -35,12 +35,12 @@ section
instance : CoeFun (A ─ét↠ B) (λ _, A → B) := ⟨Sigma.fst⟩
end

noncomputable section
hott def isManifold (V : Type u) (M : Type v) :=
section
hott definition isManifold (V : Type u) (M : Type v) :=
Σ (U : Type (max u v)), (U ─ét→ V) × (U ─ét↠ M)

hott def Manifold (V : Type u) :=
hott definition Manifold (V : Type u) :=
Σ (M : Type v), isManifold V M
end

end GroundZero.HITs.Infinitesimal
end GroundZero.HITs.Infinitesimal
78 changes: 40 additions & 38 deletions GroundZero/Modal/Infinitesimal.lean
Original file line number Diff line number Diff line change
@@ -18,78 +18,80 @@ open GroundZero.Proto
namespace GroundZero.HITs.Infinitesimal
universe u v w

axiom Im : Type u → Type u
hott axiom Im (A : Type u) : Type u := Opaque A

notation "ℑ" => Im

axiom ι {A : Type u} : A → ℑ A
axiom μ {A : Type u} : ℑ (ℑ A) → ℑ A
section
variable {A : Type u}

axiom μcom {A : Type u} : μ ∘ ι ~ @idfun (ℑ A)
axiom ιcoh {A : Type u} : ι ∘ μ ~ @idfun (ℑ (ℑ A))
hott axiom ι : A → ℑ A := Opaque.intro
hott axiom μ : ℑ (ℑ A) → ℑ A := Opaque.value

section
variable {A : Type u} {B : ℑ A → Type v}
hott axiom Im.ind {B : ℑ A → Type v} (f : Π x, ℑ (B (ι x))) : Π x, ℑ (B x) := Opaque.ind f

axiom Im.ind (f : Π x, ℑ (B (ι x))) : Π x, ℑ (B x)
axiom Im.indβrule {f : Π x, ℑ (B (ι x))} (a : A) : Im.ind f (ι a) = f a
hott axiom κ {a b : ℑ A} : ℑ (a = b) → a = b := Opaque.value
end

axiom κ {A : Type u} {a b : ℑ A} : ℑ (a = b) → a = b
axiom κ.idp {A : Type u} {a : ℑ A} : κ (ι (idp a)) = idp a
hott definition Im.indβrule {A : Type u} {B : ℑ A → Type v} {f : Π x, ℑ (B (ι x))} (a : A) : Im.ind f (ι a) = f a :=
idp (f a)

hott definition μcom {A : Type u} : μ ∘ ι ~ @idfun (ℑ A) :=
idp

hott definition ιcoh {A : Type u} : ι ∘ μ ~ @idfun (ℑ (ℑ A)) :=
λ w, κ (@Im.ind (ℑ A) (λ x, ι (μ x) = x) (λ x, ι (idp (ι x))) w)

noncomputable hott def κ.right {A : Type u} {a b : ℑ A} : @κ A a b ∘ ι ~ idfun :=
@Id.rec (ℑ A) a (λ b p, κ (ι p) = p) κ.idp b
hott definition κ.right {A : Type u} {a b : ℑ A} : @κ A a b ∘ ι ~ idfun :=
idp

noncomputable hott def κ.left {A : Type u} {a b : ℑ A} : ι ∘ @κ A a b ~ idfun :=
hott definition κ.left {A : Type u} {a b : ℑ A} : ι ∘ @κ A a b ~ idfun :=
λ ρ, κ (@Im.ind (a = b) (λ ρ, ι (κ ρ) = ρ) (λ p, ι (ap ι (κ.right p))) ρ)

hott def isCoreduced (A : Type u) := biinv (@ι A)
hott definition isCoreduced (A : Type u) := biinv (@ι A)

noncomputable hott def Im.coreduced (A : Type u) : isCoreduced (ℑ A) :=
hott definition Im.coreduced (A : Type u) : isCoreduced (ℑ A) :=
Qinv.toBiinv ι ⟨μ, (ιcoh, μcom)⟩

noncomputable hott def Im.idCoreduced {A : Type u} (a b : ℑ A) : isCoreduced (a = b) :=
hott definition Im.idCoreduced {A : Type u} (a b : ℑ A) : isCoreduced (a = b) :=
Qinv.toBiinv ι ⟨κ, (κ.left, κ.right)⟩

noncomputable hott def Im.indε {A : Type u} {B : ℑ A → Type v} (η : Π i, isCoreduced (B i))
(f : Π x, B (ι x)) : Π x, B x :=
hott definition Im.indε {A : Type u} {B : ℑ A → Type v}
(η : Π i, isCoreduced (B i)) (f : Π x, B (ι x)) : Π x, B x :=
λ a, (η a).1.1 (@Im.ind A B (λ x, ι (f x)) a)

noncomputable def Im.indεβrule {A : Type u} {B : ℑ A → Type v} (η : Π i, isCoreduced (B i))
(f : Π x, B (ι x)) : Π x, Im.indε η f (ι x) = f x :=
λ a, ap (η (ι a)).1.1 (Im.indβrule a) ⬝ (η (ι a)).1.2 (f a)
hott definition Im.indεβrule {A : Type u} {B : ℑ A → Type v}
(η : Π i, isCoreduced (B i)) (f : Π x, B (ι x)) : Π x, Im.indε η f (ι x) = f x :=
λ x, (η (ι x)).1.2 (f x)

noncomputable section
section
variable {A : Type u} {B : Type v} (f : A → ℑ B)

hott def Im.rec : Im A → ℑ B := Im.ind f
hott def Im.recβrule : Π x, Im.rec f (ι x) = f x := Im.indβrule
hott definition Im.rec : Im A → ℑ B := Im.ind f
hott definition Im.recβrule : Π x, Im.rec f (ι x) = f x := Im.indβrule
end

noncomputable section
section
variable {A : Type u} {B : Type v} (η : isCoreduced B) (f : A → B)

hott def Im.recε : Im A → B := Im.indε (λ _, η) f
hott definition Im.recε : Im A → B := Im.indε (λ _, η) f

hott def Im.recεβrule : Π x, Im.recε η f (ι x) = f x :=
hott definition Im.recεβrule : Π x, Im.recε η f (ι x) = f x :=
Im.indεβrule (λ _, η) f
end

noncomputable section
section
variable {A : Type u} {B : Type v} (f : A → B)

hott def Im.ap : ℑ A → ℑ B := Im.rec (ι ∘ f)

hott def Im.naturality (x : A) : Im.ap f (ι x) = ι (f x) := Im.recβrule _ x
hott definition Im.ap : ℑ A → ℑ B := Im.rec (ι ∘ f)
hott definition Im.naturality (x : A) : Im.ap f (ι x) = ι (f x) := idp (ι (f x))
end

noncomputable hott def Im.apIdfun {A : Type u} : @idfun (ℑ A) ~ Im.ap idfun :=
Im.indε (λ _, Im.idCoreduced _ _) (λ _, (Im.naturality idfun _)⁻¹)
hott definition Im.apIdfun {A : Type u} : Im.ap idfun ~ @idfun (ℑ A) :=
Im.indε (λ _, Im.idCoreduced _ _) (λ x, idp (ι x))

noncomputable hott def Im.apCom {A : Type u} {B : Type v} {C : Type w}
hott definition Im.apCom {A : Type u} {B : Type v} {C : Type w}
(f : B → C) (g : A → B) : Im.ap (f ∘ g) ~ Im.ap f ∘ Im.ap g :=
Im.indε (λ _, Im.idCoreduced _ _) (λ _, Im.naturality _ _
⬝ (Im.naturality f _)⁻¹
⬝ Id.ap (ap f) (Im.naturality g _)⁻¹)
Im.indε (λ _, Im.idCoreduced _ _) (λ x, idp (ι (f (g x))))

end GroundZero.HITs.Infinitesimal

0 comments on commit b11fafa

Please sign in to comment.