Mathlib.Algebra.Group.Kernel.Quotient

npa-mathlib

Packages

Module

Theorem

750

Declarations

1016

信頼境界外の sidecar

Source text や表示 overlay は提示用メタデータです。信頼する証拠は署名済み証明書と checker の結果です。

Theorem

Definition

Inductive type

Axiom

Declarations

KerSetoid

forall (G : Sort succ u), forall (H : Sort succ v), forall (f : forall (x : G), H), @Setoid.{u} G

definition

KerQuot

forall (G : Sort succ u), forall (H : Sort succ v), forall (f : forall (x : G), H), Sort succ u

definition

KerQuotMk

forall (G : Sort succ u), forall (H : Sort succ v), forall (f : forall (x : G), H), forall (a : G), @KerQuot.{u,v} G H f

definition

KerQuotToH

forall (G : Sort succ u), forall (H : Sort succ v), forall (f : forall (x : G), H), forall (q : @KerQuot.{u,v} G H f), H

definition

ker_quot_sound

forall (G : Sort succ u), forall (H : Sort succ v), forall (f : forall (x : G), H), forall (a : G), forall (b : G), forall (h : @KerRel.{succ u,succ v} G H f a...

theorem

ker_quot_to_h_mk

forall (G : Sort succ u), forall (H : Sort succ v), forall (f : forall (x : G), H), forall (a : G), @Eq.{succ v} H (@KerQuotToH.{u,v} G H f (@KerQuotMk.{u,v} G...

theorem

ker_quot_to_h_mul_mk

forall (G : Sort succ u), forall (oneG : G), forall (mulG : forall (a : G), forall (b : G), G), forall (invG : forall (a : G), G), forall (H : Sort succ v), for...

theorem

Eq.rec

axiom

Hashes

source: sha256:d2f77c8524c46be7531a84cfa888c18517f3c9b031859f604d56efeca13926c3
certificateFile: sha256:25802dfd49cadecb2e84d10c0eb6077dc14cd8220eda4b924db8d51dccbba560
export: sha256:456e96fbacbb84ec968918cae2b0914f9b851c96f3bdf1fda65be372c247ea48
axiomReport: sha256:30155dfd0399b8bb9222cee6aff0c26065a6766282a10f97ef2d27d45d89aa6a
certificate: sha256:de182e1a592999e7b630930514be307ac7e38c012a6214196397bd96def89ed9

Source

import Std.Logic.Eq
import Mathlib.Algebra.Group.Basic

def KerSetoid.{u,v} :
  forall (G : Sort succ u), forall (H : Sort succ v), forall (f : forall (x : G), H), @Setoid.{u} G :=
  fun G => fun H => fun f => @Setoid.mk.{u} G (@KerRel.{succ u,succ v} G H f) (fun (P : Prop) => fun (mk_equiv : forall (refl_arg : forall (x : G), @KerRel.{succ u,succ v} G H f x x), forall (symm_arg : forall (x : G), forall (y : G), forall (p : @KerRel.{succ u,succ v} G H f x y), @KerRel.{succ u,succ v} G H f y x), forall (trans_arg : forall (x : G), forall (y : G), forall (z : G), forall (p : @KerRel.{succ u,succ v} G H f x y), forall (q : @KerRel.{succ u,succ v} G H f y z), @KerRel.{succ u,succ v} G H f x z), P) => mk_equiv (@ker_rel_refl.{succ u,succ v} G H f) (@ker_rel_symm.{succ u,succ v} G H f) (@ker_rel_trans.{succ u,succ v} G H f))

def KerQuot.{u,v} :
  forall (G : Sort succ u), forall (H : Sort succ v), forall (f : forall (x : G), H), Sort succ u :=
  fun G => fun H => fun f => @Quotient.{u} G (@KerSetoid.{u,v} G H f)

def KerQuotMk.{u,v} :
  forall (G : Sort succ u), forall (H : Sort succ v), forall (f : forall (x : G), H), forall (a : G), @KerQuot.{u,v} G H f :=
  fun G => fun H => fun f => fun a => @Quotient.mk.{u} G (@KerSetoid.{u,v} G H f) a

def KerQuotToH.{u,v} :
  forall (G : Sort succ u), forall (H : Sort succ v), forall (f : forall (x : G), H), forall (q : @KerQuot.{u,v} G H f), H :=
  fun G => fun H => fun f => @Quotient.lift.{u,v} G H (@KerSetoid.{u,v} G H f) f (fun (a : G) => fun (b : G) => fun (h : @Setoid.r.{u} G (@KerSetoid.{u,v} G H f) a b) => h)

theorem ker_quot_sound.{u,v} :
  forall (G : Sort succ u), forall (H : Sort succ v), forall (f : forall (x : G), H), forall (a : G), forall (b : G), forall (h : @KerRel.{succ u,succ v} G H f a b), @Eq.{succ u} (@KerQuot.{u,v} G H f) (@KerQuotMk.{u,v} G H f a) (@KerQuotMk.{u,v} G H f b) :=
  fun G => fun H => fun f => fun a => fun b => fun h => @Quotient.sound.{u} G (@KerSetoid.{u,v} G H f) a b h

theorem ker_quot_to_h_mk.{u,v} :
  forall (G : Sort succ u), forall (H : Sort succ v), forall (f : forall (x : G), H), forall (a : G), @Eq.{succ v} H (@KerQuotToH.{u,v} G H f (@KerQuotMk.{u,v} G H f a)) (f a) :=
  fun G => fun H => fun f => fun a => @Eq.refl.{succ v} H (f a)

theorem ker_quot_to_h_mul_mk.{u,v} :
  forall (G : Sort succ u), forall (oneG : G), forall (mulG : forall (a : G), forall (b : G), G), forall (invG : forall (a : G), G), forall (H : Sort succ v), forall (oneH : H), forall (mulH : forall (a : H), forall (b : H), H), forall (invH : forall (a : H), H), forall (f : forall (x : G), H), forall (hom_args : @GroupHomLawArgs.{succ u,succ v} G oneG mulG invG H oneH mulH invH f), forall (a : G), forall (b : G), @Eq.{succ v} H (@KerQuotToH.{u,v} G H f (@KerQuotMk.{u,v} G H f (mulG a b))) (mulH (@KerQuotToH.{u,v} G H f (@KerQuotMk.{u,v} G H f a)) (@KerQuotToH.{u,v} G H f (@KerQuotMk.{u,v} G H f b))) :=
  fun G => fun oneG => fun mulG => fun invG => fun H => fun oneH => fun mulH => fun invH => fun f => fun hom_args => fun a => fun b => @hom_mul.{succ u,succ v} G oneG mulG invG H oneH mulH invH f hom_args a b