:: A Characterization of Concept Lattices; Dual Concept Lattices
:: by Christoph Schwarzweller
::
:: Received August 17, 1999
:: Copyright (c) 1999-2012 Association of Mizar Users


begin

definition
let C be FormalContext;
let CP be strict FormalConcept of C;
func @ CP ->  Element of (ConceptLattice C) equals :: CONLAT_2:def 1
CP;
coherence
 CP is Element of (ConceptLattice C)
proofend;
end;

:: deftheorem  defines @ CONLAT_2:def_1_:_
 for C being FormalContext
for CP being strict FormalConcept of C holds @ CP = CP;

registration
let C be FormalContext;
cluster ConceptLattice C ->  bounded ;
coherence
 ConceptLattice C is bounded
proofend;
end;

theorem Th1: :: CONLAT_2:1
for C being FormalContext holds
( Bottom (ConceptLattice C) = Concept-with-all-Attributes C & Top (ConceptLattice C) = Concept-with-all-Objects C )
proofend;

theorem Th2: :: CONLAT_2:2
for C being FormalContext
for D being non empty Subset-Family of the carrier of C holds (ObjectDerivation C) . (union D) = meet  {  ((ObjectDerivation C) . O) where O is Subset of the carrier of C : O in D  }
proofend;

theorem Th3: :: CONLAT_2:3
for C being FormalContext
for D being non empty Subset-Family of the carrier' of C holds (AttributeDerivation C) . (union D) = meet  {  ((AttributeDerivation C) . A) where A is Subset of the carrier' of C : A in D  }
proofend;

theorem Th4: :: CONLAT_2:4
for C being FormalContext
for D being Subset of (ConceptLattice C) holds
( "/\" (D,(ConceptLattice C)) is FormalConcept of C & "\/" (D,(ConceptLattice C)) is FormalConcept of C )
proofend;

definition
let C be FormalContext;
let D be Subset of (ConceptLattice C);
func "/\" (D,C) ->  FormalConcept of C equals :: CONLAT_2:def 2
 "/\" (D,(ConceptLattice C));
coherence
 "/\" (D,(ConceptLattice C)) is FormalConcept of C by Th4;
func "\/" (D,C) ->  FormalConcept of C equals :: CONLAT_2:def 3
 "\/" (D,(ConceptLattice C));
coherence
 "\/" (D,(ConceptLattice C)) is FormalConcept of C by Th4;
end;

:: deftheorem  defines "/\" CONLAT_2:def_2_:_
 for C being FormalContext
for D being Subset of (ConceptLattice C) holds "/\" (D,C) = "/\" (D,(ConceptLattice C));

:: deftheorem  defines "\/" CONLAT_2:def_3_:_
 for C being FormalContext
for D being Subset of (ConceptLattice C) holds "\/" (D,C) = "\/" (D,(ConceptLattice C));

theorem :: CONLAT_2:5
for C being FormalContext holds
( "\/" (({} (ConceptLattice C)),C) = Concept-with-all-Attributes C & "/\" (({} (ConceptLattice C)),C) = Concept-with-all-Objects C )
proofend;

theorem :: CONLAT_2:6
for C being FormalContext holds
( "\/" (([#] the carrier of (ConceptLattice C)),C) = Concept-with-all-Objects C & "/\" (([#] the carrier of (ConceptLattice C)),C) = Concept-with-all-Attributes C )
proofend;

theorem :: CONLAT_2:7
for C being FormalContext
for D being non empty Subset of (ConceptLattice C) holds
( the Extent of ("\/" (D,C)) = (AttributeDerivation C) . ((ObjectDerivation C) . (union  {  the Extent of ConceptStr(# E,I #) where E is Subset of the carrier of C, I is Subset of the carrier' of C : ConceptStr(# E,I #) in D  }  )) & the Intent of ("\/" (D,C)) = meet  {  the Intent of ConceptStr(# E,I #) where E is Subset of the carrier of C, I is Subset of the carrier' of C : ConceptStr(# E,I #) in D  }  )
proofend;

theorem :: CONLAT_2:8
for C being FormalContext
for D being non empty Subset of (ConceptLattice C) holds
( the Extent of ("/\" (D,C)) = meet  {  the Extent of ConceptStr(# E,I #) where E is Subset of the carrier of C, I is Subset of the carrier' of C : ConceptStr(# E,I #) in D  }  & the Intent of ("/\" (D,C)) = (ObjectDerivation C) . ((AttributeDerivation C) . (union  {  the Intent of ConceptStr(# E,I #) where E is Subset of the carrier of C, I is Subset of the carrier' of C : ConceptStr(# E,I #) in D  }  )) )
proofend;

theorem Th9: :: CONLAT_2:9
for C being FormalContext
for CP being strict FormalConcept of C holds "\/" ( {  ConceptStr(# O,A #) where O is Subset of the carrier of C, A is Subset of the carrier' of C : ex o being Object of C st
( o in the Extent of CP & O = (AttributeDerivation C) . ((ObjectDerivation C) . {o}) & A = (ObjectDerivation C) . {o} )  }  ,(ConceptLattice C)) = CP
proofend;

theorem Th10: :: CONLAT_2:10
for C being FormalContext
for CP being strict FormalConcept of C holds "/\" ( {  ConceptStr(# O,A #) where O is Subset of the carrier of C, A is Subset of the carrier' of C : ex a being Attribute of C st
( a in the Intent of CP & O = (AttributeDerivation C) . {a} & A = (ObjectDerivation C) . ((AttributeDerivation C) . {a}) )  }  ,(ConceptLattice C)) = CP
proofend;

definition
let C be FormalContext;
func gamma C ->  Function of the carrier of C, the carrier of (ConceptLattice C) means :Def4: :: CONLAT_2:def 4
 for o being Element of C ex O being Subset of the carrier of C ex A being Subset of the carrier' of C st
( it . o = ConceptStr(# O,A #) & O = (AttributeDerivation C) . ((ObjectDerivation C) . {o}) & A = (ObjectDerivation C) . {o} );
existence
 ex b1 being Function of the carrier of C, the carrier of (ConceptLattice C) st
for o being Element of C ex O being Subset of the carrier of C ex A being Subset of the carrier' of C st
( b1 . o = ConceptStr(# O,A #) & O = (AttributeDerivation C) . ((ObjectDerivation C) . {o}) & A = (ObjectDerivation C) . {o} )
proofend;
uniqueness
 for b1, b2 being Function of the carrier of C, the carrier of (ConceptLattice C) st ( for o being Element of C ex O being Subset of the carrier of C ex A being Subset of the carrier' of C st
( b1 . o = ConceptStr(# O,A #) & O = (AttributeDerivation C) . ((ObjectDerivation C) . {o}) & A = (ObjectDerivation C) . {o} ) ) & ( for o being Element of C ex O being Subset of the carrier of C ex A being Subset of the carrier' of C st
( b2 . o = ConceptStr(# O,A #) & O = (AttributeDerivation C) . ((ObjectDerivation C) . {o}) & A = (ObjectDerivation C) . {o} ) ) holds
b1 = b2
proofend;
end;

:: deftheorem Def4 defines gamma CONLAT_2:def_4_:_
 for C being FormalContext
for b2 being Function of the carrier of C, the carrier of (ConceptLattice C) holds
( b2 = gamma C iff for o being Element of C ex O being Subset of the carrier of C ex A being Subset of the carrier' of C st
( b2 . o = ConceptStr(# O,A #) & O = (AttributeDerivation C) . ((ObjectDerivation C) . {o}) & A = (ObjectDerivation C) . {o} ) );

definition
let C be FormalContext;
func delta C ->  Function of the carrier' of C, the carrier of (ConceptLattice C) means :Def5: :: CONLAT_2:def 5
 for a being Element of the carrier' of C ex O being Subset of the carrier of C ex A being Subset of the carrier' of C st
( it . a = ConceptStr(# O,A #) & O = (AttributeDerivation C) . {a} & A = (ObjectDerivation C) . ((AttributeDerivation C) . {a}) );
existence
 ex b1 being Function of the carrier' of C, the carrier of (ConceptLattice C) st
for a being Element of the carrier' of C ex O being Subset of the carrier of C ex A being Subset of the carrier' of C st
( b1 . a = ConceptStr(# O,A #) & O = (AttributeDerivation C) . {a} & A = (ObjectDerivation C) . ((AttributeDerivation C) . {a}) )
proofend;
uniqueness
 for b1, b2 being Function of the carrier' of C, the carrier of (ConceptLattice C) st ( for a being Element of the carrier' of C ex O being Subset of the carrier of C ex A being Subset of the carrier' of C st
( b1 . a = ConceptStr(# O,A #) & O = (AttributeDerivation C) . {a} & A = (ObjectDerivation C) . ((AttributeDerivation C) . {a}) ) ) & ( for a being Element of the carrier' of C ex O being Subset of the carrier of C ex A being Subset of the carrier' of C st
( b2 . a = ConceptStr(# O,A #) & O = (AttributeDerivation C) . {a} & A = (ObjectDerivation C) . ((AttributeDerivation C) . {a}) ) ) holds
b1 = b2
proofend;
end;

:: deftheorem Def5 defines delta CONLAT_2:def_5_:_
 for C being FormalContext
for b2 being Function of the carrier' of C, the carrier of (ConceptLattice C) holds
( b2 = delta C iff for a being Element of the carrier' of C ex O being Subset of the carrier of C ex A being Subset of the carrier' of C st
( b2 . a = ConceptStr(# O,A #) & O = (AttributeDerivation C) . {a} & A = (ObjectDerivation C) . ((AttributeDerivation C) . {a}) ) );

theorem :: CONLAT_2:11
for C being FormalContext
for o being Object of C
for a being Attribute of C holds
( (gamma C) . o is FormalConcept of C & (delta C) . a is FormalConcept of C )
proofend;

theorem Th12: :: CONLAT_2:12
for C being FormalContext holds
( rng (gamma C) is supremum-dense & rng (delta C) is infimum-dense )
proofend;

theorem Th13: :: CONLAT_2:13
for C being FormalContext
for o being Object of C
for a being Attribute of C holds
( o is-connected-with a iff (gamma C) . o [= (delta C) . a )
proofend;

begin

Lm1:  for L1, L2 being Lattice
for f being Function of the carrier of L1, the carrier of L2 st ( for a, b being Element of L1 st f . a [= f . b holds
a [= b ) holds
f is one-to-one
proofend;

Lm2:  for L1, L2 being complete Lattice
for f being Function of the carrier of L1, the carrier of L2 st f is one-to-one & rng f = the carrier of L2 & ( for a, b being Element of L1 holds
( a [= b iff f . a [= f . b ) ) holds
f is Homomorphism of L1,L2
proofend;

Lm3:  for C being FormalContext
for CS being ConceptStr over C st (ObjectDerivation C) . the Extent of CS = the Intent of CS holds
not CS is empty
proofend;

theorem Th14: :: CONLAT_2:14
for L being complete Lattice
for C being FormalContext holds
( ConceptLattice C,L are_isomorphic iff ex g being Function of the carrier of C, the carrier of L ex d being Function of the carrier' of C, the carrier of L st
( rng g is supremum-dense & rng d is infimum-dense & ( for o being Object of C
for a being Attribute of C holds
( o is-connected-with a iff g . o [= d . a ) ) ) )
proofend;

definition
let L be Lattice;
func Context L ->  non quasi-empty strict ContextStr  equals :: CONLAT_2:def 6
 ContextStr(# the carrier of L, the carrier of L,(LattRel L) #);
coherence
 ContextStr(# the carrier of L, the carrier of L,(LattRel L) #) is non quasi-empty strict ContextStr by CONLAT_1:def_1;
end;

:: deftheorem  defines Context CONLAT_2:def_6_:_
 for L being Lattice holds Context L = ContextStr(# the carrier of L, the carrier of L,(LattRel L) #);

theorem Th15: :: CONLAT_2:15
for L being complete Lattice holds ConceptLattice (Context L),L are_isomorphic
proofend;

theorem :: CONLAT_2:16
for L being Lattice holds
( L is complete iff ex C being FormalContext st ConceptLattice C,L are_isomorphic )
proofend;

begin

registration
let L be complete Lattice;
clusterL .:  ->  complete ;
coherence
 L .: is complete
proofend;
end;

definition
let C be FormalContext;
funcC .:  ->  non quasi-empty strict ContextStr  equals :: CONLAT_2:def 7
 ContextStr(# the carrier' of C, the carrier of C,( the Information of C ~) #);
coherence
 ContextStr(# the carrier' of C, the carrier of C,( the Information of C ~) #) is non quasi-empty strict ContextStr by CONLAT_1:def_1;
end;

:: deftheorem  defines .: CONLAT_2:def_7_:_
 for C being FormalContext holds C .: = ContextStr(# the carrier' of C, the carrier of C,( the Information of C ~) #);

theorem :: CONLAT_2:17
for C being strict FormalContext holds (C .:) .: = C ;

theorem Th18: :: CONLAT_2:18
for C being FormalContext
for O being Subset of the carrier of C holds (ObjectDerivation C) . O = (AttributeDerivation (C .:)) . O
proofend;

theorem Th19: :: CONLAT_2:19
for C being FormalContext
for A being Subset of the carrier' of C holds (AttributeDerivation C) . A = (ObjectDerivation (C .:)) . A
proofend;

definition
let C be FormalContext;
let CP be ConceptStr over C;
funcCP .:  ->  strict ConceptStr over C .:  means :Def8: :: CONLAT_2:def 8
( the Extent of it = the Intent of CP & the Intent of it = the Extent of CP );
existence
 ex b1 being strict ConceptStr over C .: st
( the Extent of b1 = the Intent of CP & the Intent of b1 = the Extent of CP )
proofend;
uniqueness
 for b1, b2 being strict ConceptStr over C .: st the Extent of b1 = the Intent of CP & the Intent of b1 = the Extent of CP & the Extent of b2 = the Intent of CP & the Intent of b2 = the Extent of CP holds
b1 = b2 ;
end;

:: deftheorem Def8 defines .: CONLAT_2:def_8_:_
 for C being FormalContext
for CP being ConceptStr over C
for b3 being strict ConceptStr over C .: holds
( b3 = CP .: iff ( the Extent of b3 = the Intent of CP & the Intent of b3 = the Extent of CP ) );

registration
let C be FormalContext;
let CP be FormalConcept of C;
clusterCP .:  ->  strict non empty concept-like ;
coherence
 ( not CP .: is empty & CP .: is concept-like )
proofend;
end;

theorem :: CONLAT_2:20
for C being strict FormalContext
for CP being strict FormalConcept of C holds (CP .:) .: = CP
proofend;

definition
let C be FormalContext;
func DualHomomorphism C ->  Homomorphism of (ConceptLattice C) .: , ConceptLattice (C .:) means :Def9: :: CONLAT_2:def 9
 for CP being strict FormalConcept of C holds it . CP = CP .: ;
existence
 ex b1 being Homomorphism of (ConceptLattice C) .: , ConceptLattice (C .:) st
for CP being strict FormalConcept of C holds b1 . CP = CP .:
proofend;
uniqueness
 for b1, b2 being Homomorphism of (ConceptLattice C) .: , ConceptLattice (C .:) st ( for CP being strict FormalConcept of C holds b1 . CP = CP .: ) & ( for CP being strict FormalConcept of C holds b2 . CP = CP .: ) holds
b1 = b2
proofend;
end;

:: deftheorem Def9 defines DualHomomorphism CONLAT_2:def_9_:_
 for C being FormalContext
for b2 being Homomorphism of (ConceptLattice C) .: , ConceptLattice (C .:) holds
( b2 = DualHomomorphism C iff for CP being strict FormalConcept of C holds b2 . CP = CP .: );

theorem Th21: :: CONLAT_2:21
for C being FormalContext holds DualHomomorphism C is bijective
proofend;

theorem :: CONLAT_2:22
for C being FormalContext holds ConceptLattice (C .:),(ConceptLattice C) .: are_isomorphic
proofend;